diff --git a/mCRL2/TrafficLights/v4/v4_spec.lps b/mCRL2/TrafficLights/v4/v4_spec.lps
new file mode 100644
index 0000000..f9c31e4
Binary files /dev/null and b/mCRL2/TrafficLights/v4/v4_spec.lps differ
diff --git a/mCRL2/TrafficLights/v4/v4_spec.lts b/mCRL2/TrafficLights/v4/v4_spec.lts
new file mode 100644
index 0000000..d8a302d
Binary files /dev/null and b/mCRL2/TrafficLights/v4/v4_spec.lts differ
diff --git a/mCRL2/TrafficLights/v4/v4_spec.mcrl2 b/mCRL2/TrafficLights/v4/v4_spec.mcrl2
index ba4aab3..e6a6eab 100644
--- a/mCRL2/TrafficLights/v4/v4_spec.mcrl2
+++ b/mCRL2/TrafficLights/v4/v4_spec.mcrl2
@@ -49,8 +49,8 @@ proc
 	TL(direction : CardinalDirection, colour : Colour) =
 		show(direction, colour).
 		(colour == red) 
-			-> ChangeLight(direction, colour)
-			<> changeDirection(nextDirection(direction)) . ChangeLight(direction, colour)
+			-> (changeDirection(nextDirection(direction)) . changeDirection(direction) . ChangeLight(direction, colour))
+			<> ChangeLight(direction, colour)
 	;
 	
 	ChangeLight(direction : CardinalDirection, colour : Colour) =