A2b4: halb fertig

mCRL2/TrafiicLights/v1/v1_spec.mcrl2

@@ -2,10 +2,12 @@
 sort
 	CardinalDirection = struct north | east | south | west;
 
-
+%-----------------------------------------------------------------------------
 sort
 	Colour = struct red | green | yellow;
 
+%Definition Farbliche Reihenfolge
+
 map
 	nextColour: Colour -> Colour;
 
@@ -14,6 +16,7 @@ eqn
 	nextColour(green) = yellow;
 	nextColour(yellow) = red;
 
+%------------------------------------------------------------------------------
 act
 	show : CardinalDirection # Colour;
 
@@ -21,12 +24,12 @@ proc
 	TrafficLight(direction : CardinalDirection) = TF(direction, red);
 
 	TF(direction : CardinalDirection, colour : Colour) =
-		show(direction, colour).
+		show(direction, colour) . %zeige aktuellen Zustand
-		TF(direction, nextColour(colour))
+			TF(direction, nextColour(colour)) %zum nächsten Zustand wechseln
 	;
 
-		
+%-----------------------------------------------------------------------------
-
+%Initialisation der seperaten Ampeln
 init
 	TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west)
 ;

mCRL2/TrafiicLights/v2/v2_spec.mcrl2

@@ -3,14 +3,6 @@
 sort
 	CardinalDirection = struct north | east | south | west;
 
-map
-	otherDirection : CardinalDirection -> CardinalDirection;
-
-eqn
-	otherDirection(north) = south;
-	otherDirection(south) = north;
-	otherDirection(east) = west;
-	otherDirection(west) = east;
 
 %-----------------------------------------------------------------------
 
@@ -19,18 +11,14 @@ sort
 
 map
 	nextColour: Colour -> Colour;
-	safeColour: Colour -> Colour;
 
 eqn
 	nextColour(red) = green;
 	nextColour(green) = yellow;
 	nextColour(yellow) = red;
 
-	safeColour(green) = red;
-	safeColour(red) = green;
-	safeColour(yellow) = red;
-
 %------------------------------------------------------------------------
+%die aktuellen Werte für die verschiedenen Ampeln werden in einer KeyValue Map gespeichert.
 
 sort
 	Map = K -> V;
@@ -72,15 +60,15 @@ proc
 	;
 
 	Monitor(status : Map) = 
-		((status(north) in {green, yellow} || status(south) in {green, yellow}) && (status(east) in {green, yellow} || status(west) in {green, yellow})) 
+		((status(north) in {green, yellow} || status(south) in {green, yellow}) && (status(east) in {green, yellow} || status(west) in {green, yellow})) %ist aktueller Zustand unsicher ?
-			-> crossingUnsafe(status(north), status(east), status(south), status(west)) . delta
+			-> crossingUnsafe(status(north), status(east), status(south), status(west)) . delta %unsicherer Zustand, deadlock
 			
-		<>
+		<>%wenn aktueller Zustand sicher:
 		sum direction : CardinalDirection.(
 			sum c : Colour .
-				 seeColour(direction, c) . 
+				 seeColour(direction, c) . %jede mögliche Kombination anbieten
-					Monitor(status= status[direction -> c])
+					Monitor(status= status[direction -> c])%und entsprechend speichern
-	);
+		);
 
 	System =
 		allow({

mCRL2/TrafiicLights/v3/v3_spec.mcrl2

@@ -3,15 +3,6 @@
 sort
 	CardinalDirection = struct north | east | south | west;
 
-map
-	otherDirections : CardinalDirection -> Set(CardinalDirection);
-
-eqn
-	otherDirections(north) = {east, west};
-	otherDirections(south) = {east, west};
-	otherDirections(east) = {north, south};
-	otherDirections(west) = {north, south};
-
 %-----------------------------------------------------------------------
 
 sort
@@ -19,7 +10,6 @@ sort
 
 map
 	nextColour: Colour -> Colour;
-	safeColour: Colour -> Colour;
 
 eqn
 	nextColour(red) = green;
@@ -71,17 +61,18 @@ proc
 			sum c : Colour .
 				(c == green) ->
 					(direction == north || direction == south) ->
-						((status(east) == red && status(west) == red) -> 
+						((status(east) == red && status(west) == red) ->  % sind die anderen Ampeln rot ?
-							seeColour(direction, c) . Monitor(status= status[direction -> c]))
+							seeColour(direction, c) . Monitor(status= status[direction -> c])) % dann darf fortgefahren werden
 					<>
 						((status(north) == red && status(south) == red) ->
 							seeColour(direction, c) . Monitor(status= status[direction -> c]))
-				<>
+				<> %soll nicht grün gezeigt werden kann einfach fortgefahren werden, es wurde ja bereits überprüft
-				seeColour(direction, c) . 
+				seeColour(direction, c) .
 						Monitor(status= status[direction -> c])
 				 	
 	);
 
+
 	System =
 		allow({
 			colourSeen

mCRL2/TrafiicLights/v4/v4.mcrl2proj

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

mCRL2/TrafiicLights/v4/v4_spec.mcrl2

@@ -0,0 +1,78 @@
+%-----------------------------------------------------------------------
+
+sort
+	CardinalDirection = struct north | east | south | west;
+
+map
+	oppositeDirection: CardinalDirection -> CardinalDirection;
+	nextDirection: CardinalDirection -> CardinalDirection;
+
+eqn
+	oppositeDirection(north) = south;
+	oppositeDirection(south) = north;
+	oppositeDirection(east) = west;
+	oppositeDirection(west) = east;
+
+	nextDirection(north) = east;
+	nextDirection(east) = south;
+	nextDirection(south) = west;
+	nextDirection(west) = north;
+
+%-----------------------------------------------------------------------
+
+sort
+	Colour = struct red | green | yellow;
+
+map
+	nextColour: Colour -> Colour;
+
+eqn
+	nextColour(red) = green;
+	nextColour(green) = yellow;
+	nextColour(yellow) = red;
+
+%------------------------------------------------------------------------
+
+act
+	show : CardinalDirection # Colour;
+	changeLight: Colour;
+	changedLight: Colour;
+	changeDirection: CardinalDirection;
+	changedDirection: CardinalDirection;
+	emptyAct;
+	
+%------------------------------------------------------------------------
+
+proc
+	TrafficLight(direction : CardinalDirection) = TL(direction, red);
+
+	TL(direction : CardinalDirection, colour : Colour) =
+		(colour == red) 
+		-> changeDirection(nextDirection(direction)) . TL(direction, nextColour(colour))
+		<> changeLight(nextColour(colour)) . show(direction, nextColour(colour)) . TL(direction, nextColour(colour))
+		
+	;
+
+	
+
+	System =
+		allow({
+			show, 
+			%changeLight,
+			changedLight,
+			%changeDirection, 
+			changedDirection,
+			emptyAct
+		},
+		comm({
+			changeDirection | changeDirection -> changedDirection,
+			changeLight | changeLight -> changedLight
+			
+		},
+
+		TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west)
+	));
+
+init
+	  System
+;

mCRL2/VendingMachine/VendingMachine_spec.mcrl2

@@ -67,21 +67,26 @@ act
 proc
 
 	VM(credit : Int) =
-		(credit < 200) -> sum c : Coin.accept(c).VM(credit + value(c)) %Coins akzeptieren, solange credit < 2€
+		(credit < 200) ->
+			 sum c : Coin
+				.accept(c).VM(credit + value(c)) %Coins akzeptieren, solange credit < 2€
 
-		+ (credit > 0) -> returnChange(credit).ReturnChange(credit)%Geld zurückgeben wenn credit > 0
+		+ (credit > 0) ->
+			 returnChange(credit).ReturnChange(credit)%Geld zurückgeben wenn credit > 0
 
 		+ sum p : Product.(
-			(credit >= price(p)) -> offer(p).serve(p).VM(credit - price(p))%Produkt anbieten, wenn genug credit
+			(credit >= price(p)) ->
-		);
+				offer(p).serve(p).VM(credit - price(p))%Produkt anbieten, wenn genug credit
+	);
 	
 
 	ReturnChange(credit : Int) =
-		sum c : Coin.((credit >= value(c) && credit < next(c)) ->  %größt möglichen Coin ermitteln
+		sum c : Coin.(
-			return(c).(	%diesen zurückgeben
+			(credit >= value(c) && credit < next(c)) ->  %größt möglichen Coin ermitteln
-			((credit - value(c)) > 0) 	%wenn noch Geld übrig
+				return(c).(	%diesen zurückgeben
-				-> ReturnChange(credit - value(c)) %dieses zurückgeben
+					((credit - value(c)) > 0) 	%wenn noch Geld übrig
-				<> VM(credit - value(c)) % oder nur abziehen 
+					-> ReturnChange(credit - value(c)) %dieses zurückgeben
+					<> VM(credit - value(c)) % oder nur abziehen 
 	));