- More sophisticated broadcast

- Included version 6

Clocks-Test-6.q

+//This file was generated from (Commercial) UPPAAL 4.0.12 (rev. 4561), July 2010
+
+/*
+"Does any deadlock exist?"
+*/
+E<> deadlock
+
+/*
+
+*/
+A[] deadlock imply (P_ClientBehavior.FINISH_PROCEDURE or P_ClientBehavior.FINISH_TIMEOUT)
+
+/*
+
+*/
+A<> P_ClientBehavior.FINISH_PROCEDURE or P_ClientBehavior.FINISH_TIMEOUT
+
+/*
+
+*/
+E<> P_ClientBehavior.FINISH_PROCEDURE
+
+/*
+
+*/
+//NO_QUERY
+
+/*
+
+*/
+E<> P_ClientBehavior.FINISH_PROCEDURE and (client_clock_counter == server_clock_counter)
+
+/*
+
+*/
+A[] P_ClientBehavior.FINISH_PROCEDURE imply (client_clock_counter - server_clock_counter < P_ClientBehavior.unicast_roundtrip / 2)
+
+/*
+
+*/
+A[] P_ClientBehavior.UNICAST_FINISHED imply (client_clock_counter - server_clock_counter < P_ClientBehavior.unicast_roundtrip / 2)
+
+/*
+
+*/
+A[] P_ClientBehavior.BROADCAST_FINISHED imply (client_clock_counter - server_clock_counter < P_ClientBehavior.unicast_roundtrip)
+
+/*
+
+*/
+//NO_QUERY
+
+/*
+
+*/
+E<> P_ClientBehavior.BROADCAST_FINISHED and (client_clock_counter - server_clock_counter <= -10) and (broadcast_repetitions_counter == 2)
+
+/*
+
+*/
+E<> P_ClientBehavior.BROADCAST_FINISHED and (client_clock_counter - server_clock_counter <= -bc_interval_length) and (broadcast_repetitions_counter == 2)
+
+/*
+
+*/
+E<> P_ClientBehavior.BROADCAST_FINISHED and (client_clock_counter - server_clock_counter <= -bc_interval_length)
+
+/*
+
+*/
+E<> P_ClientBehavior.BROADCAST_FINISHED and (client_clock_counter - server_clock_counter <= -6)
+
+/*
+
+*/
+E<> P_ClientBehavior.BROADCAST_FINISHED and broadcast_repetitions_counter == broadcast_repetitions_max
+
+/*
+
+*/
+E<> P_ClientBehavior.BROADCAST_FINISHED and broadcast_repetitions_counter == 2
+
+/*
+
+*/
+E<> P_ClientBehavior.BROADCAST_FINISHED and (client_clock_counter - server_clock_counter < 6)
+
+/*
+
+*/
+//NO_QUERY