A2b3: working version

mCRL2/TrafiicLights/v3/v3.mcrl2proj

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

mCRL2/TrafiicLights/v3/v3_spec.mcrl2

@@ -0,0 +1,103 @@
+%-----------------------------------------------------------------------
+
+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
+	Colour = struct red | green | yellow;
+
+map
+	nextColour: Colour -> Colour;
+	safeColour: Colour -> Colour;
+
+eqn
+	nextColour(red) = green;
+	nextColour(green) = yellow;
+	nextColour(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;
+
+%------------------------------------------------------------------------
+
+proc
+	TrafficLight(direction : CardinalDirection) = TL(direction, red);
+
+	TL(direction : CardinalDirection, colour : Colour) =
+		show(direction, colour) . TL(direction, nextColour(colour))
+	;
+
+	Monitor(status : Map) = 
+		sum direction : CardinalDirection.(
+			sum c : Colour .
+				(c == green) ->
+					(direction == north || direction == south) ->
+						((status(east) == red && status(west) == red) -> 
+							seeColour(direction, c) . Monitor(status= status[direction -> c]))
+					<>
+						((status(north) == red && status(south) == red) ->
+							seeColour(direction, c) . Monitor(status= status[direction -> c]))
+				<>
+				seeColour(direction, c) . 
+						Monitor(status= status[direction -> c])
+				 	
+	);
+
+	System =
+		allow({
+			colourSeen
+		},
+		comm({
+			show | seeColour -> colourSeen
+			
+		},
+
+		TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) || Monitor(_Map(red))
+	));
+		
+
+	
+		
+
+init
+	  System
+;