Skip to content
Snippets Groups Projects
Commit 88cec48c authored by Kristof's avatar Kristof
Browse files

- Efficiency changes and queries regarding considerations about "stop_clock"... 

- Efficiency changes and queries regarding considerations about "stop_clock" transitions for all automata being unnecessary
parent c33f25ab
Branches
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Clocks-Test-6.xml
+ 4
− 4
View file @ 88cec48c
......@@ -26,7 +26,7 @@ chan server_interval_step;
// PREFERENCES (Fixed constants, chosen by user via this source code) //
const int unicast_repetitions_max = 3;
const int unicast_repetitions_max = 2;
int [0, unicast_repetitions_max] unicast_repetitions_counter = 0;
const int broadcast_repetitions_max = 7;
......@@ -56,7 +56,7 @@ const int
bc_trigger_delay_min = 0,
bc_trigger_delay_max = 0,
bc_offset_max_accepted = 2,
bc_offset_max_accepted = 3,
bc_disclosure_delay = 1;
......@@ -110,7 +110,7 @@ int [0, client_clock_counter_max] t_client;
int [server_clock_starting_value, server_clock_counter_max] server_clock_counter = server_clock_starting_value;
int [0, client_clock_counter_max] client_clock_counter_old = 0;
int [ -(bc_disclosure_delay+1)*bc_interval_length,
(bc_disclosure_delay+1)*bc_interval_length] client_clock_counter_diff = 0;
(bc_disclosure_delay)*bc_interval_length] client_clock_counter_diff = 0;
// CLIENT CLOCK READ FUNCTION
// int client_clock_counter() {return client_clock_counter_old;}
......@@ -172,7 +172,7 @@ MEASURED_ROUNDTRIP unicast_roundtrip;
int[0, 1] unicast_sufficient_precision = 0;
clock unicast_timeout;</declaration><location id="id23" x="-1248" y="-808"><name x="-1432" y="-792">BROADCAST_EVALUATED</name><committed/></location><location id="id24" x="-768" y="-24" color="#ffa500"><name x="-784" y="0">FINISH_TIMEOUT</name><committed/></location><location id="id25" x="-1056" y="-240"><name x="-1224" y="-224">BROAD_TIMELINESS_CHECK</name><committed/></location><location id="id26" x="-776" y="-672"><name x="-760" y="-704">BROADCAST_AGAIN</name><committed/></location><location id="id27" x="0" y="-288"><name x="-8" y="-272">UNICAST_RESPONSE_TIMESTAMPED</name><urgent/></location><location id="id28" x="392" y="-864" color="#ffa500"><name x="240" y="-896">FINISH_PROCEDURE</name><committed/></location><location id="id29" x="-888" y="-808"><name x="-856" y="-848">BROADCAST_FINISHED</name><committed/></location><location id="id30" x="-608" y="-544"><name x="-592" y="-576">INITIALIZING_BROADCAST</name><committed/></location><location id="id31" x="-1248" y="-576"><name x="-1456" y="-576">BROAD_TIMELINESS_DONE</name><committed/></location><location id="id32" x="160" y="-544"><name x="184" y="-560">UNICAST_REQUEST_READY_TO_SEND</name><urgent/></location><location id="id33" x="-1248" y="-448"><name x="-1456" y="-448">BROAD_PACKET_RECEIVED</name><committed/></location><location id="id34" x="-768" y="-240" color="#ff00ff"><name x="-704" y="-168">WAITING_FOR_BROADCAST_PACKET</name></location><location id="id35" x="-160" y="-544"><name x="-312" y="-576">UNICAST_FINISHED</name><urgent/></location><location id="id36" x="128" y="-320"><name x="144" y="-320">UNICAST_RESPONSE_RECEIVED</name><urgent/></location><location id="id37" x="160" y="-416" color="#ff00ff"><name x="184" y="-432">WAITING_FOR_UNICAST_RESPONSE</name></location><location id="id38" x="0" y="-672"><name x="32" y="-696">IDLE_UNICAST</name><urgent/></location><location id="id39" x="0" y="-864" color="#ffffff"><name x="16" y="-896">START</name><committed/></location><init ref="id39"/><transition><source ref="id38"/><target ref="id24"/><label kind="synchronisation" x="424" y="-48">stop_clock?</label><nail x="520" y="-672"/><nail x="520" y="-16"/></transition><transition><source ref="id23"/><target ref="id29"/><label kind="guard" x="-1160" y="-944">broadcast_offset &gt; bc_offset_max_accepted</label><label kind="assignment" x="-1160" y="-928">broadcast_offset := 0</label><nail x="-1064" y="-904"/></transition><transition><source ref="id23"/><target ref="id29"/><label kind="guard" x="-1184" y="-792">broadcast_offset &lt;= bc_offset_max_accepted</label><label kind="synchronisation" x="-1184" y="-776">client_setclock!</label><label kind="assignment" x="-1184" y="-760">client_clock_correction := broadcast_offset,
clock unicast_timeout;</declaration><location id="id23" x="-1248" y="-808"><name x="-1432" y="-792">BROADCAST_EVALUATED</name><committed/></location><location id="id24" x="-768" y="-24" color="#ffa500"><name x="-784" y="0">FINISH_TIMEOUT</name><committed/></location><location id="id25" x="-1056" y="-240"><name x="-1224" y="-224">BROAD_TIMELINESS_CHECK</name><committed/></location><location id="id26" x="-776" y="-672"><name x="-760" y="-704">BROADCAST_AGAIN</name><committed/></location><location id="id27" x="0" y="-288"><name x="-8" y="-272">UNICAST_RESPONSE_TIMESTAMPED</name><urgent/></location><location id="id28" x="392" y="-864" color="#ffa500"><name x="240" y="-896">FINISH_PROCEDURE</name><committed/></location><location id="id29" x="-888" y="-808"><name x="-856" y="-848">BROADCAST_FINISHED</name><committed/></location><location id="id30" x="-608" y="-544"><name x="-592" y="-576">INITIALIZING_BROADCAST</name><committed/></location><location id="id31" x="-1248" y="-576"><name x="-1456" y="-576">BROAD_TIMELINESS_DONE</name><committed/></location><location id="id32" x="160" y="-544"><name x="184" y="-560">UNICAST_REQUEST_READY_TO_SEND</name><urgent/></location><location id="id33" x="-1248" y="-448"><name x="-1456" y="-448">BROAD_PACKET_RECEIVED</name><committed/></location><location id="id34" x="-768" y="-240" color="#ff00ff"><name x="-704" y="-168">WAITING_FOR_BROADCAST_PACKET</name></location><location id="id35" x="-160" y="-544"><name x="-312" y="-576">UNICAST_FINISHED</name><urgent/></location><location id="id36" x="128" y="-320"><name x="144" y="-320">UNICAST_RESPONSE_RECEIVED</name><urgent/></location><location id="id37" x="160" y="-416" color="#ff00ff"><name x="184" y="-440">WAITING_FOR_UNICAST_RESPONSE</name></location><location id="id38" x="0" y="-672"><name x="32" y="-696">IDLE_UNICAST</name><urgent/></location><location id="id39" x="0" y="-864" color="#ffffff"><name x="16" y="-896">START</name><committed/></location><init ref="id39"/><transition><source ref="id37"/><target ref="id24"/><label kind="synchronisation" x="-364" y="-235">stop_clock?</label><nail x="472" y="-416"/><nail x="472" y="-72"/><nail x="-712" y="-80"/></transition><transition><source ref="id38"/><target ref="id24"/><label kind="synchronisation" x="424" y="-48">stop_clock?</label><nail x="520" y="-672"/><nail x="520" y="-16"/></transition><transition><source ref="id23"/><target ref="id29"/><label kind="guard" x="-1160" y="-944">broadcast_offset &gt; bc_offset_max_accepted</label><label kind="assignment" x="-1160" y="-928">broadcast_offset := 0</label><nail x="-1064" y="-904"/></transition><transition><source ref="id23"/><target ref="id29"/><label kind="guard" x="-1184" y="-792">broadcast_offset &lt;= bc_offset_max_accepted</label><label kind="synchronisation" x="-1184" y="-776">client_setclock!</label><label kind="assignment" x="-1184" y="-760">client_clock_correction := broadcast_offset,
broadcast_offset := 0</label></transition><transition><source ref="id34"/><target ref="id24"/><label kind="synchronisation" x="-848" y="-96">stop_clock?</label></transition><transition><source ref="id25"/><target ref="id33"/><label kind="guard" x="-1488" y="-320">client_clock_counter()
&lt; (msg_network_bc_interval + 1)*bc_interval_length</label></transition><transition><source ref="id25"/><target ref="id26"/><label kind="guard" x="-1160" y="-616">client_clock_counter() &gt;=
(msg_network_bc_interval + 1)*bc_interval_length</label><label kind="assignment" x="-1160" y="-584">client_bc_tb := 0,
......
license.txt
+ 1
− 1
View file @ 88cec48c
bFUmUgUIGFQaAFIADAwcbwFQBQ8VBUJGJA0RDRMLF08ARA0RAxtaFhseVRsJFRtSWxNFHAwDDSoHeEwFChEaHwAOFh0TGxcRUyoPAFQ4SDRARUpSTi4HCwBWVV1fVlRBSRJBUlNAAFxVEl5VbwgqFAFFQgQVF1FXGEkBUUhRQBpEDU4KChpyD0kZVVRQF18TVV9cD0wARUlBR0RVTBoTVxpcUV9UeE8XRFYMEVhZURoQUVlHVE4TE1QVW1YQeEAETFtaAUhWEV5VClMTUkgSEX0ECBdFGRZFQAMJCy4BG04LVBIVABZFeQkGExYRDgMPGAAIfzUDWCwJG0hSVxNELxkHVldCQhZXWVJOEkFfElpFTlR9RUIqAAAXEQIWRV0JChEAGlMQC0kdCUkiBABIVU5MJjdpJSlFYxoMERZOBA1PH0UOWBBeVVVJf0VCEGYFHRcJC1MWSwIRER1WFBoRDTNBNVExEBRCREJcAC4QAklEVUNFAEZbW0YWTVcUTk5VVn9FeEwJCAcRQhNBHwwHLQMGTxhTIAEZDGFcXFgrGwpSVxBVU0xYRV9ARRpFXEFfEEVVEGQ=
\ No newline at end of file
bFUmUgUIGFQaAFIADAwcbwFQBQ8VBUJGJA0RDRMLF08ARA0RAxtaFhseVRsJFRtSWxNFHAwDDSoHeEwFChEaHwAOFh0TGxcRUyoPAFQhTy9ARUpUTi4HCQBWVV1fVlVLSRNFUlJNAFxVEl5VbwgqFAFFQgQVF1FXGEkBUUhRQBpEDU4KChpyD0kZVVRQF18TVV9cD0wARUlBR0RVTBoTVxpcUV9UeE8XRFYMEVhZURoQUVlHVE4TE1QVW1YQeEAETFtaAUhWEV5VClMTUkgSEX0ECBdFGRZFQAMJCy4BG04LVBIVABZFeQkGExYRDgMPGAAIfzUDWDUOAEhSVxVELxkFVldCQhZXWFhOE0VfE1dFTlR9RUIqAAAXEQIWRV0JChEAGlMQC0kdCUkiBABIVU5MJjdpJSlFYxoMERZOBA1PH0UOWBBeVVVJf0VCEGYFHRcJC1MWSwIRER1WFBoRDTNBNVEoFw9CRENUAC4QAElEVUNFAEdRW0cSTVYZTk5VVn9FeEwJCAcRQhNBHwwHLQMGTxhTOQYCDGFdVFgrGwhSVxBVU0xZT19BQRpEUUFfEEVVEGQ=
\ No newline at end of file
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment