Skip to content
Snippets Groups Projects
Commit 3be47d98 authored by unknown's avatar unknown
Browse files

- Further work towards broadcast:

  * Server broadcast module now triggered by server's clock (at interval jumps)
  * Diagnostic work. Problem arose because atomic operations (triggering and reading a timestamp) were not strictly encoded as such

(This version does NOT include any more syntax errors)
parent 8fa07b10
No related branches found
No related tags found
No related merge requests found
...@@ -18,22 +18,32 @@ E<> P_ClientBehavior.UNICAST_OFFSET_CALCULATION ...@@ -18,22 +18,32 @@ E<> P_ClientBehavior.UNICAST_OFFSET_CALCULATION
/* /*
*/ */
E<> P_ClientBehavior.FINISH_PROCEDURE and (P_ClientClock.client_clock_counter == P_ServerClock.server_clock_counter) E<> P_ClientBehavior.FINISH_PROCEDURE and (P_ClientClock.client_clock_counter == server_clock_counter)
/* /*
*/ */
E<> P_ClientClock.FINISH_CLOCKOUTOFBOUNDS A[] not 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.FINISH_PROCEDURE imply (P_ClientClock.client_clock_counter - 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) A[] P_ClientBehavior.UNICAST_FINISHED imply (P_ClientClock.client_clock_counter - server_clock_counter < P_ClientBehavior.unicast_roundtrip / 2)
/*
*/
//NO_QUERY
/*
*/
E<> server_interval_counter == 5
/* /*
...@@ -48,7 +58,7 @@ A<> P_ClientBehavior.UNICAST_RESPONSE_RECEIVED and unicast_repetitions_counter = ...@@ -48,7 +58,7 @@ A<> P_ClientBehavior.UNICAST_RESPONSE_RECEIVED and unicast_repetitions_counter =
/* /*
*/ */
A<> P_ClientBehavior.UNICAST_RESPONSE_TIMESTAMPED and unicast_repetitions_counter == 2 A<> P_ClientBehavior.UNICAST_RESPONSE_TIMESTAMPED & unicast_repetitions_counter == 2
/* /*
......
This diff is collapsed.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment