- Last minute at work: cleaned up set of queries so that now all are relevant,...

- Last minute at work: cleaned up set of queries so that now all are relevant, and also so that affirmative results always represent the respective hypothesis / expected behavior

Clocks-Test-7.q

@@ -22,21 +22,6 @@ E<> P_ClientBehavior.FINISH_PROCEDURE
 
 /*
 
-*/
-E<> P_ClientBehavior.FINISH_PROCEDURE and (client_clock_counter() == server_clock_counter)
-
-/*
-
-*/
-A[] P_ClientBehavior.UNICAST_FINISHED imply (client_clock_counter() - server_clock_counter < P_ClientBehavior.unicast_roundtrip / 2)
-
-/*
-
-*/
-//NO_QUERY
-
-/*
-
 */
 A[] P_ClientBehavior.UNICAST_FINISHED imply abs(client_clock_counter_diff) == 0
 
@@ -68,16 +53,6 @@ imply \
 
 /*
 
-*/
-E<> abs(client_clock_counter_diff) >= bc_interval_length
-
-/*
-
-*/
-//NO_QUERY
-
-/*
-
 */
 E<>\
 (server_clock_counter >= (bc_interval_length / bc_offset_max_accepted - 1) * bc_interval_length + bc_interval_length + network_delay_min) \
@@ -96,23 +71,3 @@ imply \
 
 */
 //NO_QUERY
-
-/*
-
-*/
-//NO_QUERY
-
-/*
-
-*/
-E<> client_clock_counter_diff <= -bc_interval_length
-
-/*
-
-*/
-E<> P_ClientBehavior.BROADCAST_FINISHED and broadcast_repetitions_counter == broadcast_repetitions_max-1
-
-/*
-
-*/
-//NO_QUERY