- V4 (getting ready for broadcast)

Clocks-Test-4.q

+//This file was generated from (Commercial) UPPAAL 4.0.12 (rev. 4561), July 2010
+
+/*
+"Does any deadlock exist?"
+*/
+E<> deadlock
+
+/*
+
+*/
+E<> P_ClientBehavior.FINISH_PROCEDURE
+
+/*
+
+*/
+E<> P_ClientBehavior.UNICAST_OFFSET_CALCULATION
+
+/*
+
+*/
+E<> P_ClientBehavior.FINISH_PROCEDURE and (P_ClientClock.client_clock_counter == P_ServerClock.server_clock_counter)
+
+/*
+
+*/
+E<> P_ClientClock.FINISH_CLOCKOUTOFBOUNDS
+
+/*
+
+*/
+A[] P_ClientBehavior.FINISH_PROCEDURE imply (P_ClientClock.client_clock_counter - P_ServerClock.server_clock_counter < P_ClientBehavior.unicast_roundtrip / 2)
+
+/*
+
+*/
+A[] P_ClientBehavior.UNICAST_FINISHED imply (P_ClientClock.client_clock_counter - P_ServerClock.server_clock_counter < P_ClientBehavior.unicast_roundtrip / 2)
+
+/*
+
+*/
+//NO_QUERY
+
+/*
+
+*/
+A<> P_ClientBehavior.UNICAST_RESPONSE_RECEIVED and unicast_repetitions_counter == 2
+
+/*
+
+*/
+A<> P_ClientBehavior.UNICAST_RESPONSE_TIMESTAMPED and unicast_repetitions_counter == 2
+
+/*
+
+*/
+A<> P_ClientBehavior.UNICAST_OFFSET_CALCULATION and unicast_repetitions_counter == 2
+
+/*
+
+*/
+A<> P_ClientBehavior.FINISH_PROCEDURE
+
+/*
+
+*/
+//NO_QUERY