A2b2: fertig

mCRL2/TrafiicLights/v2/v2_spec.mcrl2

@@ -19,37 +19,86 @@ 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;
+
+%------------------------------------------------------------------------
+
+sort
+	Map = K -> V;
+
+map
+	_Map: V -> Map;
+
+var
+	k: K;
+	v: V;
+
+eqn
+	_Map(v)(k) = v;
+
+sort
+	K = CardinalDirection;
+	V = Colour;
+
+map
+	combinations: Map;
+
+
 
 %------------------------------------------------------------------------
 
 act
 	show : CardinalDirection # Colour;
+	seeColour : CardinalDirection # Colour;
+	colourSeen : CardinalDirection # Colour;
 	crossingUnsafe : Colour # Colour # Colour # Colour;
-	safe : Bool;
-	emptyAct;
 
 %------------------------------------------------------------------------
 
 proc
-	TrafficLight(direction : CardinalDirection) = TF(direction, red);
+	TrafficLight(direction : CardinalDirection) = TL(direction, red);
 
-	TF(direction : CardinalDirection, colour : Colour) =
+	TL(direction : CardinalDirection, colour : Colour) =
-		show(direction, colour) . TF(direction, nextColour(colour))
+		show(direction, colour) . TL(direction, nextColour(colour))
 	;
 
-	Monitor =
+	Monitor(status : Map) = 
-		emptyAct
+		((status(north) in {green, yellow} || status(south) in {green, yellow}) && (status(east) in {green, yellow} || status(west) in {green, yellow})) 
-	;
+			-> crossingUnsafe(status(north), status(east), status(south), status(west)) . delta
+			
+		<>
+		sum direction : CardinalDirection.(
+			sum c : Colour .
+				 seeColour(direction, c) . 
+					Monitor(status= status[direction -> c])
+	);
+
+	System =
+		allow({
+			colourSeen,
+			crossingUnsafe
+		},
+		comm({
+			show | seeColour -> colourSeen
+			
+		},
+
+		TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) || Monitor(_Map(red))
+	));
+		
 
 	
 		
 
 init
-	  TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) || Monitor
+	  System
 ;

mCRL2/VendingMachine/VendingMachine_spec.mcrl2

@@ -18,7 +18,7 @@ sort
 
 map
 	value: Coin  -> Int;	% the value of a coin as an integer
-	next:  Coin -> Int;
+	next:  Coin -> Int;		%nächst größerer Betrag
 
 eqn
 	value(_5c) = 5;
@@ -27,7 +27,7 @@ eqn
 	value(_50c) = 50;
 	value(Euro) = 100;
 
-	next(Euro) = 10000;
+	next(Euro) = 500;
 	next(_50c) = 100;
 	next(_20c) = 50;
 	next(_10c) = 20;
@@ -67,18 +67,21 @@ act
 proc
 
 	VM(credit : Int) =
-		(credit < 200) -> sum c : Coin.accept(c).VM(credit + value(c))
+		(credit < 200) -> sum c : Coin.accept(c).VM(credit + value(c)) %Coins akzeptieren, solange credit < 2€
 
-		+ (credit > 0) -> returnChange(credit).ReturnChange(credit)
+		+ (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))
+			(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)) -> return(c).(
+		sum c : Coin.((credit >= value(c) && credit < next(c)) ->  %größt möglichen Coin ermitteln
-			((credit - value(c)) > 0) -> ReturnChange(credit - value(c)) <> VM(credit - value(c))
+			return(c).(	%diesen zurückgeben
+			((credit - value(c)) > 0) 	%wenn noch Geld übrig
+				-> ReturnChange(credit - value(c)) %dieses zurückgeben
+				<> VM(credit - value(c)) % oder nur abziehen 
 	));