Anfang A2b_v2

mCRL2/TrafiicLights/v2/v2.mcrl2proj

@@ -0,0 +1,4 @@
+<root>
+ <spec>v2_spec.mcrl2</spec>
+ <properties/>
+</root>

mCRL2/TrafiicLights/v2/v2_spec.mcrl2

@@ -0,0 +1,55 @@
+%-----------------------------------------------------------------------
+
+sort
+	CardinalDirection = struct north | east | south | west;
+
+map
+	otherDirection : CardinalDirection -> CardinalDirection;
+
+eqn
+	otherDirection(north) = south;
+	otherDirection(south) = north;
+	otherDirection(east) = west;
+	otherDirection(west) = east;
+
+%-----------------------------------------------------------------------
+
+sort
+	Colour = struct red | green | yellow;
+
+map
+	nextColour: Colour -> Colour;
+
+eqn
+	nextColour(red) = green;
+	nextColour(green) = yellow;
+	nextColour(yellow) = red;
+
+
+%------------------------------------------------------------------------
+
+act
+	show : CardinalDirection # Colour;
+	crossingUnsafe : Colour # Colour # Colour # Colour;
+	safe : Bool;
+	emptyAct;
+
+%------------------------------------------------------------------------
+
+proc
+	TrafficLight(direction : CardinalDirection) = TF(direction, red);
+
+	TF(direction : CardinalDirection, colour : Colour) =
+		show(direction, colour) . TF(direction, nextColour(colour))
+	;
+
+	Monitor =
+		emptyAct
+	;
+
+	
+		
+
+init
+	  TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) || Monitor
+;

mCRL2/VendingMachine/VendingMachine_spec.mcrl2

@@ -65,14 +65,15 @@ act
 % Definition of the processes
 %
 proc
-	VendingMachine = VM(0);	
 
 	VM(credit : Int) =
 		(credit < 200) -> sum c : Coin.accept(c).VM(credit + value(c))
-		+ (credit > 0) -> returnChange(credit).ReturnChange(credit);
+
+		+ (credit > 0) -> returnChange(credit).ReturnChange(credit)
+
 		+ sum p : Product.(
 			(credit >= price(p)) -> offer(p).serve(p).VM(credit - price(p))
-		)
+		);
 	
 
 	ReturnChange(credit : Int) =
@@ -80,8 +81,10 @@ proc
 			((credit - value(c)) > 0) -> ReturnChange(credit - value(c)) <> VM(credit - value(c))
 	));
 
+
+
 % -----------------------------------------------------------------------------------------------------------------------
 
 init
-    	VendingMachine
+    	VM(0)
 ;