- Lots of cleanup

- Resolved some unintended behavior (mostly inconsistencies in interval numbering)

- Modified query set towards the goal

Still TODO: introducing the disclosure delay (of 2, usualy)

Clocks-Test-7.q

@@ -23,12 +23,12 @@ E<> P_ClientBehavior.FINISH_PROCEDURE
 /*
 
 */
-E<> P_ClientBehavior.BROADCAST_TIMELY
+E<> P_ClientBehavior.FINISH_PROCEDURE and (client_clock_counter() == server_clock_counter)
 
 /*
 
 */
-E<> P_ClientBehavior.BROADCAST_TIMELY and broadcast_repetitions_counter > 5 and P_ClientBehavior.broadcast_offset > 0
+A[] P_ClientBehavior.UNICAST_FINISHED imply (client_clock_counter() - server_clock_counter < P_ClientBehavior.unicast_roundtrip / 2)
 
 /*
 
@@ -38,22 +38,28 @@ E<> P_ClientBehavior.BROADCAST_TIMELY and broadcast_repetitions_counter > 5 and
 /*
 
 */
-E<> P_ClientBehavior.FINISH_PROCEDURE and (client_clock_counter == server_clock_counter)
+A[] P_ClientBehavior.UNICAST_FINISHED imply abs(client_clock_counter_diff) == 0
 
 /*
 
 */
-A[] P_ClientBehavior.FINISH_PROCEDURE imply (client_clock_counter() - server_clock_counter < P_ClientBehavior.unicast_roundtrip / 2)
+//NO_QUERY
 
 /*
 
 */
-A[] P_ClientBehavior.UNICAST_FINISHED imply (client_clock_counter() - server_clock_counter < P_ClientBehavior.unicast_roundtrip / 2)
+E<> \
+(broadcast_repetitions_counter + 1 == bc_interval_length / bc_offset_max_accepted)\
+and\
+(abs(client_clock_counter_diff) >= bc_interval_length)
 
 /*
 
 */
-A[] P_ClientBehavior.BROADCAST_FINISHED imply (client_clock_counter() - server_clock_counter < P_ClientBehavior.unicast_roundtrip)
+A[] \
+(broadcast_repetitions_counter + 1 < bc_interval_length / bc_offset_max_accepted) \
+imply \
+(abs(client_clock_counter_diff) < bc_interval_length)
 
 /*
 
@@ -63,7 +69,7 @@ A[] P_ClientBehavior.BROADCAST_FINISHED imply (client_clock_counter() - server_c
 /*
 
 */
-A[] P_ClientBehavior.UNICAST_FINISHED imply abs(client_clock_counter_diff) == 0
+E<> abs(client_clock_counter_diff) >= bc_interval_length
 
 /*
 
@@ -73,12 +79,18 @@ A[] P_ClientBehavior.UNICAST_FINISHED imply abs(client_clock_counter_diff) == 0
 /*
 
 */
-E<> P_ClientClockDiff.FINISH_CLOCKOUTOFBOUNDS
+E<>\
+(server_clock_counter >= (bc_interval_length / bc_offset_max_accepted - 1) * bc_interval_length + bc_interval_length + network_delay_min) \
+and\
+(abs(client_clock_counter_diff) >= bc_interval_length)
 
 /*
 
 */
-E<> P_ClientBehavior.broadcast_offset > 0
+A[] \
+(server_clock_counter <  (bc_interval_length / bc_offset_max_accepted - 1) * bc_interval_length + bc_interval_length + network_delay_min)\
+imply \
+(abs(client_clock_counter_diff) < bc_interval_length)
 
 /*
 
@@ -87,33 +99,13 @@ E<> P_ClientBehavior.broadcast_offset > 0
 
 /*
 
-*/
-E<> abs(client_clock_counter_diff) >= bc_interval_length and broadcast_repetitions_counter == 10
-
-/*
-
-*/
-E<> abs(client_clock_counter_diff) >= bc_interval_length and broadcast_repetitions_counter == bc_interval_length / bc_offset_max_accepted
-
-/*
-
-*/
-E<> abs(client_clock_counter_diff) >= bc_interval_length and broadcast_repetitions_counter < bc_interval_length / bc_offset_max_accepted
-
-/*
-
 */
 //NO_QUERY
 
 /*
 
 */
-E<> abs(client_clock_counter_diff) >= bc_interval_length
-
-/*
-
-*/
-E<> abs(client_clock_counter_diff) >= bc_interval_length - 4
+E<> client_clock_counter_diff <= -bc_interval_length
 
 /*
 
@@ -122,10 +114,5 @@ E<> P_ClientBehavior.BROADCAST_FINISHED and broadcast_repetitions_counter == bro
 
 /*
 
-*/
-E<> P_ClientBehavior.BROADCAST_FINISHED and broadcast_repetitions_counter == 2
-
-/*
-
 */
 //NO_QUERY