Skip to content
Snippets Groups Projects
Commit 814934e0 authored by Kristof's avatar Kristof
Browse files

- More embellishments for presentation

parent c9acb8f8
No related branches found
No related tags found
No related merge requests found
...@@ -156,7 +156,7 @@ DIFF_TIMESTAMP network_t3 = 0; ...@@ -156,7 +156,7 @@ DIFF_TIMESTAMP network_t3 = 0;
// NETWORK VARIABLES (Broadcast) // // NETWORK VARIABLES (Broadcast) //
INTERVAL_TIMESTAMP msg_network_bc_tb[number_bc_channels]; INTERVAL_TIMESTAMP msg_network_bc_tb[number_bc_channels];
INTERVAL_COUNTER msg_network_bc_interval[number_bc_channels];</declaration><template><name x="5" y="5">Ticker</name><location id="id0" x="0" y="-160" color="#ffffff"><name x="16" y="-192">START</name><committed/></location><location id="id1" x="0" y="96" color="#ffa500"><name x="16" y="64">FINISH</name><committed/></location><location id="id2" x="0" y="-32" color="#00ff00"><name x="32" y="-64">TICKING</name><label kind="invariant" x="32" y="-48">ticker &lt;=1</label></location><init ref="id0"/><transition><source ref="id0"/><target ref="id2"/><label kind="synchronisation" x="8" y="-112">start_system!</label></transition><transition><source ref="id2"/><target ref="id1"/><label kind="synchronisation" x="8" y="16">stop_clock?</label></transition><transition><source ref="id2"/><target ref="id2"/><label kind="guard" x="-192" y="-80">ticker == 1</label><label kind="synchronisation" x="-192" y="-64">tick!</label><label kind="assignment" x="-192" y="-48">ticker := 0</label><nail x="-64" y="32"/><nail x="-128" y="-32"/><nail x="-64" y="-96"/></transition></template><template><name>Server_Clock</name><location id="id3" x="-128" y="-128"><committed/></location><location id="id4" x="384" y="0"><name x="352" y="-40">BACK_TO_IDLE</name><committed/></location><location id="id5" x="-128" y="384" color="#ffa500"><name x="-192" y="392">FINISH</name><committed/></location><location id="id6" x="-128" y="-256" color="#ffffff"><name x="-112" y="-288">START</name></location><location id="id7" x="192" y="384" color="#ffa500"><name x="208" y="392">FINISH_CLOCKOUTOFBOUNDS</name><committed/></location><location id="id8" x="192" y="256"><name x="216" y="264">INCREMENTING_CLOCK</name><committed/></location><location id="id9" x="0" y="0" color="#00ff00"></location><init ref="id6"/><transition><source ref="id3"/><target ref="id9"/><label kind="synchronisation" x="-80" y="-112">server_interval_step!</label></transition><transition><source ref="id8"/><target ref="id4"/><label kind="guard" x="280" y="160">server_clock_counter INTERVAL_COUNTER msg_network_bc_interval[number_bc_channels];</declaration><template><name x="5" y="5">Ticker</name><location id="id0" x="0" y="-160" color="#ffffff"><name x="16" y="-192">START</name><committed/></location><location id="id1" x="0" y="96" color="#ffa500"><name x="16" y="64">FINISH</name><committed/></location><location id="id2" x="0" y="-32" color="#00ff00"><name x="32" y="-64">TICKING</name><label kind="invariant" x="32" y="-48">ticker &lt;=1</label></location><init ref="id0"/><transition><source ref="id0"/><target ref="id2"/><label kind="synchronisation" x="8" y="-112">start_system!</label></transition><transition><source ref="id2"/><target ref="id1"/><label kind="synchronisation" x="8" y="16">stop_clock?</label></transition><transition><source ref="id2"/><target ref="id2"/><label kind="guard" x="-192" y="-80">ticker == 1</label><label kind="synchronisation" x="-192" y="-64">tick!</label><label kind="assignment" x="-192" y="-48">ticker := 0</label><nail x="-64" y="32"/><nail x="-128" y="-32"/><nail x="-64" y="-96"/></transition></template><template><name>Server_Clock</name><location id="id3" x="-128" y="-128"><committed/></location><location id="id4" x="384" y="0"><name x="320" y="-48">BACK_TO_IDLE</name><committed/></location><location id="id5" x="-128" y="384" color="#ffa500"><name x="-112" y="400">FINISH</name><committed/></location><location id="id6" x="-128" y="-256" color="#ffffff"><name x="-112" y="-288">START</name></location><location id="id7" x="192" y="384" color="#ffa500"><name x="208" y="392">FINISH_CLOCKOUTOFBOUNDS</name><committed/></location><location id="id8" x="192" y="256"><name x="208" y="264">INCREMENTING_CLOCK</name><committed/></location><location id="id9" x="0" y="0" color="#00ff00"></location><init ref="id6"/><transition><source ref="id3"/><target ref="id9"/><label kind="synchronisation" x="-80" y="-112">server_interval_step!</label></transition><transition><source ref="id8"/><target ref="id4"/><label kind="guard" x="248" y="184">server_clock_counter
&lt; server_clock_counter_max</label></transition><transition><source ref="id4"/><target ref="id9"/><label kind="guard" x="112" y="-152">server_clock_counter &lt; server_clock_counter_max</label></transition><transition><source ref="id4"/><target ref="id9"/><label kind="guard" x="112" y="-152">server_clock_counter
&gt;= bc_interval_length &gt;= bc_interval_length
* (server_interval_counter)</label><label kind="synchronisation" x="112" y="-88">server_interval_step!</label><label kind="assignment" x="112" y="-104">server_interval_counter += 1</label><nail x="192" y="-64"/></transition><transition><source ref="id9"/><target ref="id5"/><label kind="synchronisation" x="-128" y="32">stop_clock?</label><nail x="-128" y="128"/></transition><transition><source ref="id6"/><target ref="id3"/><label kind="synchronisation" x="-120" y="-208">start_system?</label></transition><transition><source ref="id8"/><target ref="id7"/><label kind="guard" x="-8" y="296">server_clock_counter * (server_interval_counter)</label><label kind="synchronisation" x="112" y="-88">server_interval_step!</label><label kind="assignment" x="112" y="-104">server_interval_counter += 1</label><nail x="192" y="-64"/></transition><transition><source ref="id9"/><target ref="id5"/><label kind="synchronisation" x="-128" y="32">stop_clock?</label><nail x="-128" y="128"/></transition><transition><source ref="id6"/><target ref="id3"/><label kind="synchronisation" x="-120" y="-208">start_system?</label></transition><transition><source ref="id8"/><target ref="id7"/><label kind="guard" x="-8" y="296">server_clock_counter
...@@ -168,15 +168,16 @@ NONCE server_nonce_unicast_response; ...@@ -168,15 +168,16 @@ NONCE server_nonce_unicast_response;
int [0, server_clock_counter_max] server_t2 = 0; int [0, server_clock_counter_max] server_t2 = 0;
clock calculating;</declaration><location id="id10" x="384" y="-224" color="#ff00ff"><name x="408" y="-256">CALCULATIONS</name><label kind="invariant" x="408" y="-240">calculating &lt;= server_computation_max</label></location><location id="id11" x="0" y="-96" color="#ffa500"><name x="16" y="-120">FINISH</name><committed/></location><location id="id12" x="0" y="-224" color="#00ff00"><name x="-48" y="-248">IDLE</name></location><location id="id13" x="0" y="-352" color="#ffffff"><name x="16" y="-384">START</name></location><init ref="id13"/><transition><source ref="id10"/><target ref="id12"/><label kind="guard" x="128" y="-416">calculating &gt;= server_computation_min</label><label kind="synchronisation" x="128" y="-400">server_send_unicast_response!</label><label kind="assignment" x="128" y="-384">network_t2 := server_t2, clock calculating;</declaration><location id="id10" x="384" y="-224" color="#ff00ff"><name x="376" y="-200">CALCULATIONS</name><label kind="invariant" x="376" y="-184">calculating
&lt;= server_computation_max</label></location><location id="id11" x="0" y="-96" color="#ffa500"><name x="-64" y="-80">FINISH</name><committed/></location><location id="id12" x="0" y="-224" color="#00ff00"><name x="-48" y="-248">IDLE</name></location><location id="id13" x="0" y="-352" color="#ffffff"><name x="-64" y="-384">START</name></location><init ref="id13"/><transition><source ref="id10"/><target ref="id12"/><label kind="guard" x="96" y="-456">calculating &gt;= server_computation_min</label><label kind="synchronisation" x="96" y="-440">server_send_unicast_response!</label><label kind="assignment" x="96" y="-424">network_t2 := server_t2,
server_t2 := 0, server_t2 := 0,
network_t3 := (server_clock_counter - network_t2), network_t3 := (server_clock_counter - network_t2),
network_nonce_unicast_response network_nonce_unicast_response
:= server_nonce_unicast_response, := server_nonce_unicast_response,
server_nonce_unicast_response := 0</label><nail x="192" y="-288"/></transition><transition><source ref="id12"/><target ref="id11"/><label kind="synchronisation" x="-96" y="-176">stop_clock?</label></transition><transition><source ref="id12"/><target ref="id10"/><label kind="synchronisation" x="128" y="-160">server_receive_unicast_request?</label><label kind="assignment" x="128" y="-144">server_nonce_unicast_response server_nonce_unicast_response := 0</label><nail x="192" y="-320"/></transition><transition><source ref="id12"/><target ref="id11"/><label kind="synchronisation" x="-96" y="-176">stop_clock?</label></transition><transition><source ref="id12"/><target ref="id10"/><label kind="synchronisation" x="96" y="-120">server_receive_unicast_request?</label><label kind="assignment" x="96" y="-104">server_nonce_unicast_response
:= network_nonce_unicast_request, := network_nonce_unicast_request,
calculating := 0, calculating := 0,
server_t2 := server_clock_counter</label><nail x="192" y="-160"/></transition><transition><source ref="id13"/><target ref="id12"/><label kind="synchronisation" x="-96" y="-304">start_system?</label></transition></template><template><name>Client_Behavior</name><declaration>NONCE client_nonce_unicast_request; server_t2 := server_clock_counter</label><nail x="192" y="-128"/></transition><transition><source ref="id13"/><target ref="id12"/><label kind="synchronisation" x="-96" y="-304">start_system?</label></transition></template><template><name>Client_Behavior</name><declaration>NONCE client_nonce_unicast_request;
NONCE client_nonce_unicast_response; NONCE client_nonce_unicast_response;
// Unicast's t2 is modeled as a full-on timestamp, while t3 SHOULD BE modeled as the difference from t1 (to keep state space small) // Unicast's t2 is modeled as a full-on timestamp, while t3 SHOULD BE modeled as the difference from t1 (to keep state space small)
...@@ -200,7 +201,7 @@ MEASURED_DELAY broadcast_delay = network_delay_min * clock_incrementation_va ...@@ -200,7 +201,7 @@ MEASURED_DELAY broadcast_delay = network_delay_min * clock_incrementation_va
MEASURED_ROUNDTRIP unicast_roundtrip = 0; MEASURED_ROUNDTRIP unicast_roundtrip = 0;
clock propagation;</declaration><location id="id14" x="-192" y="-288"><name x="-344" y="-272">UNICAST_FINISHED</name><committed/></location><location id="id15" x="-1120" y="-1056"><name x="-1280" y="-1088">BROADCAST_TIMELY</name><committed/></location><location id="id16" x="-672" y="-224" color="#ffa500"><name x="-784" y="-192">FINISH_TIMEOUT</name><committed/></location><location id="id17" x="-1184" y="-416"><name x="-1400" y="-440">BROAD_TIMELINESS_CHECK</name><committed/></location><location id="id18" x="-672" y="-928"><name x="-656" y="-960">BROADCAST_AGAIN</name><committed/></location><location id="id19" x="512" y="-800" color="#ffa500"><name x="368" y="-832">FINISH_PROCEDURE</name><committed/></location><location id="id20" x="-736" y="-1056"><name x="-720" y="-1088">BROADCAST_FINISHED</name><committed/></location><location id="id21" x="-192" y="-672"><name x="-184" y="-664">INITIALIZING_BROADCAST</name><committed/></location><location id="id22" x="-672" y="-416" color="#ff00ff"><name x="-648" y="-408">WAITING_FOR_BROADCAST_PACKET</name><label kind="invariant" x="-648" y="-392">client_clock_counter() clock propagation;</declaration><location id="id14" x="-192" y="-288"><name x="-344" y="-272">UNICAST_FINISHED</name><committed/></location><location id="id15" x="-1088" y="-992"><name x="-1240" y="-1024">BROADCAST_TIMELY</name><committed/></location><location id="id16" x="-672" y="-224" color="#ffa500"><name x="-784" y="-192">FINISH_TIMEOUT</name><committed/></location><location id="id17" x="-1120" y="-416"><name x="-1280" y="-440">BROAD_TIMELINESS</name><committed/></location><location id="id18" x="-672" y="-864"><name x="-656" y="-896">BROADCAST_AGAIN</name><committed/></location><location id="id19" x="512" y="-800" color="#ffa500"><name x="368" y="-832">FINISH_PROCEDURE</name><committed/></location><location id="id20" x="-704" y="-992"><name x="-688" y="-1024">BROADCAST_FINISHED</name><committed/></location><location id="id21" x="-192" y="-672"><name x="-184" y="-664">INITIALIZING_BROADCAST</name><committed/></location><location id="id22" x="-672" y="-416" color="#ff00ff"><name x="-648" y="-408">WAITING_FOR_BROADCAST_PACKET</name><label kind="invariant" x="-648" y="-392">client_clock_counter()
&lt;= ((unicast_repetitions_counter - 1) &lt;= ((unicast_repetitions_counter - 1)
* broadcast_repetitions_max * broadcast_repetitions_max
+ broadcast_repetitions_counter + 1) + broadcast_repetitions_counter + 1)
...@@ -212,22 +213,22 @@ clock propagation;</declaration><location id="id14" x="-192" y="-288"><name ...@@ -212,22 +213,22 @@ clock propagation;</declaration><location id="id14" x="-192" y="-288"><name
and and
broadcast_repetitions_counter broadcast_repetitions_counter
&lt; broadcast_repetitions_max</label><label kind="assignment" x="-312" y="-864">broadcast_repetitions_counter += 1, &lt; broadcast_repetitions_max</label><label kind="assignment" x="-312" y="-864">broadcast_repetitions_counter += 1,
push_on_stack(bc_tesla_stack, 0)</label><nail x="-160" y="-768"/><nail x="-64" y="-800"/><nail x="-64" y="-992"/><nail x="-320" y="-992"/><nail x="-320" y="-800"/><nail x="-224" y="-768"/></transition><transition><source ref="id14"/><target ref="id23"/><label kind="assignment" x="-352" y="-360">unicast_roundtrip = 0</label></transition><transition><source ref="id25"/><target ref="id16"/><label kind="synchronisation" x="-400" y="-216">stop_clock?</label><nail x="448" y="-480"/><nail x="448" y="-224"/></transition><transition><source ref="id26"/><target ref="id16"/><label kind="synchronisation" x="-400" y="-152">stop_clock?</label><nail x="512" y="-672"/><nail x="512" y="-160"/><nail x="-640" y="-160"/></transition><transition><source ref="id15"/><target ref="id20"/><label kind="guard" x="-1048" y="-992">abs(broadcast_offset) &gt; bc_offset_max_accepted</label><label kind="synchronisation" x="-1048" y="-928">client_setclock!</label><label kind="assignment" x="-1048" y="-976">client_clock_correction := bc_tesla_stack[1], push_on_stack(bc_tesla_stack, 0)</label><nail x="-160" y="-768"/><nail x="-64" y="-800"/><nail x="-64" y="-992"/><nail x="-320" y="-992"/><nail x="-320" y="-800"/><nail x="-224" y="-768"/></transition><transition><source ref="id14"/><target ref="id23"/><label kind="assignment" x="-352" y="-360">unicast_roundtrip = 0</label></transition><transition><source ref="id25"/><target ref="id16"/><label kind="synchronisation" x="-560" y="-248">stop_clock?</label><nail x="448" y="-480"/><nail x="448" y="-224"/></transition><transition><source ref="id26"/><target ref="id16"/><label kind="synchronisation" x="-560" y="-184">stop_clock?</label><nail x="512" y="-672"/><nail x="512" y="-160"/><nail x="-640" y="-160"/></transition><transition><source ref="id15"/><target ref="id20"/><label kind="guard" x="-1064" y="-920">abs(broadcast_offset) &gt; bc_offset_max_accepted</label><label kind="synchronisation" x="-1064" y="-856">client_setclock!</label><label kind="assignment" x="-1064" y="-904">client_clock_correction := bc_tesla_stack[1],
push_on_stack(bc_tesla_stack, 0), push_on_stack(bc_tesla_stack, 0),
broadcast_offset := 0</label><nail x="-928" y="-992"/></transition><transition><source ref="id15"/><target ref="id20"/><label kind="guard" x="-1056" y="-1240">abs(broadcast_offset) &lt;= bc_offset_max_accepted</label><label kind="synchronisation" x="-1056" y="-1176">client_setclock!</label><label kind="assignment" x="-1056" y="-1224">client_clock_correction := bc_tesla_stack[1], broadcast_offset := 0</label><nail x="-928" y="-928"/></transition><transition><source ref="id15"/><target ref="id20"/><label kind="guard" x="-1032" y="-1088">abs(broadcast_offset) &lt;= bc_offset_max_accepted</label><label kind="synchronisation" x="-1032" y="-1024">client_setclock!</label><label kind="assignment" x="-1032" y="-1072">client_clock_correction := bc_tesla_stack[1],
push_on_stack(bc_tesla_stack, broadcast_offset), push_on_stack(bc_tesla_stack, broadcast_offset),
broadcast_offset := 0</label><nail x="-928" y="-1120"/></transition><transition><source ref="id22"/><target ref="id16"/><label kind="synchronisation" x="-656" y="-280">stop_clock?</label></transition><transition><source ref="id17"/><target ref="id18"/><label kind="guard" x="-1080" y="-832">client_clock_counter() broadcast_offset := 0</label></transition><transition><source ref="id22"/><target ref="id16"/><label kind="synchronisation" x="-656" y="-280">stop_clock?</label></transition><transition><source ref="id17"/><target ref="id18"/><label kind="guard" x="-1024" y="-776">client_clock_counter()
&gt;= (client_bc_interval)*bc_interval_length &gt;= (client_bc_interval)*bc_interval_length
or client_clock_counter() or client_clock_counter()
&lt; (client_bc_interval - 1)*bc_interval_length</label><label kind="assignment" x="-1080" y="-768">client_clock_correction := bc_tesla_stack[1], &lt; (client_bc_interval - 1)*bc_interval_length</label><label kind="assignment" x="-1024" y="-712">client_clock_correction := bc_tesla_stack[1],
push_on_stack(bc_tesla_stack, 0), push_on_stack(bc_tesla_stack, 0),
client_bc_tb := 0, client_bc_tb := 0,
client_bc_interval := 0, client_bc_interval := 0,
broadcast_offset := 0</label><label kind="comments">This is triggered if the packet does not arrive in a "timely" fashion.</label><nail x="-1088" y="-832"/></transition><transition><source ref="id20"/><target ref="id18"/><nail x="-672" y="-1056"/></transition><transition><source ref="id22"/><target ref="id18"/><label kind="guard" x="-920" y="-624">client_clock_counter() broadcast_offset := 0</label><label kind="comments">This is triggered if the packet does not arrive in a "timely" fashion.</label><nail x="-1088" y="-768"/></transition><transition><source ref="id20"/><target ref="id18"/><nail x="-672" y="-992"/></transition><transition><source ref="id22"/><target ref="id18"/><label kind="guard" x="-920" y="-592">client_clock_counter()
&gt;= ((unicast_repetitions_counter - 1) &gt;= ((unicast_repetitions_counter - 1)
* broadcast_repetitions_max * broadcast_repetitions_max
+ broadcast_repetitions_counter + 1) + broadcast_repetitions_counter + 1)
* bc_interval_length</label><label kind="synchronisation" x="-920" y="-528">packet_loss!</label><label kind="assignment" x="-920" y="-544">push_on_stack(bc_tesla_stack, 0)</label></transition><transition><source ref="id24"/><target ref="id14"/><label kind="synchronisation" x="-152" y="-464">client_setclock!</label><label kind="assignment" x="-152" y="-448">unicast_offset * bc_interval_length</label><label kind="synchronisation" x="-920" y="-496">packet_loss!</label><label kind="assignment" x="-920" y="-512">push_on_stack(bc_tesla_stack, 0)</label></transition><transition><source ref="id24"/><target ref="id14"/><label kind="synchronisation" x="-152" y="-464">client_setclock!</label><label kind="assignment" x="-152" y="-448">unicast_offset
:= (client_t1 + client_t4) / 2 := (client_t1 + client_t4) / 2
- (client_t2 + client_t3) / 2, - (client_t2 + client_t3) / 2,
unicast_roundtrip := client_t4 - client_t1, unicast_roundtrip := client_t4 - client_t1,
...@@ -237,16 +238,18 @@ client_t3 := 0, ...@@ -237,16 +238,18 @@ client_t3 := 0,
client_t4 := 0, client_t4 := 0,
client_clock_correction := unicast_offset, client_clock_correction := unicast_offset,
unicast_offset := 0</label></transition><transition><source ref="id26"/><target ref="id19"/><label kind="guard" x="256" y="-792">unicast_repetitions_counter unicast_offset := 0</label></transition><transition><source ref="id26"/><target ref="id19"/><label kind="guard" x="256" y="-792">unicast_repetitions_counter
&gt;= unicast_repetitions_max</label><label kind="synchronisation" x="256" y="-760">stop_clock!</label><nail x="256" y="-800"/></transition><transition><source ref="id17"/><target ref="id15"/><label kind="guard" x="-1480" y="-808">client_clock_counter() &gt;= unicast_repetitions_max</label><label kind="synchronisation" x="256" y="-760">stop_clock!</label><nail x="256" y="-800"/></transition><transition><source ref="id17"/><target ref="id15"/><label kind="guard" x="-1296" y="-792">client_clock_counter()
&lt; (client_bc_interval)*bc_interval_length &lt; (client_bc_interval)
*bc_interval_length
and client_clock_counter() and client_clock_counter()
&gt;= (client_bc_interval - 1)*bc_interval_length</label><label kind="assignment" x="-1480" y="-744">client_bc_tb := 0, &gt;= (client_bc_interval - 1)
client_bc_interval := 0</label><nail x="-1184" y="-1056"/></transition><transition><source ref="id18"/><target ref="id21"/><label kind="assignment" x="-560" y="-744">broadcast_repetitions_counter += 1</label></transition><transition><source ref="id21"/><target ref="id26"/><label kind="guard" x="-112" y="-728">broadcast_repetitions_counter *bc_interval_length</label><label kind="assignment" x="-1296" y="-704">client_bc_tb := 0,
client_bc_interval := 0</label><nail x="-1120" y="-992"/></transition><transition><source ref="id18"/><target ref="id21"/><label kind="assignment" x="-560" y="-744">broadcast_repetitions_counter += 1</label></transition><transition><source ref="id21"/><target ref="id26"/><label kind="guard" x="-112" y="-728">broadcast_repetitions_counter
&gt;= broadcast_repetitions_max</label><label kind="assignment" x="-112" y="-696">zero(bc_tesla_stack)</label></transition><transition><source ref="id23"/><target ref="id21"/><label kind="guard" x="-208" y="-600">broadcast_repetitions_max &gt; 0</label><label kind="assignment" x="-208" y="-584">broadcast_repetitions_counter := 0, &gt;= broadcast_repetitions_max</label><label kind="assignment" x="-112" y="-696">zero(bc_tesla_stack)</label></transition><transition><source ref="id23"/><target ref="id21"/><label kind="guard" x="-208" y="-600">broadcast_repetitions_max &gt; 0</label><label kind="assignment" x="-208" y="-584">broadcast_repetitions_counter := 0,
zero(bc_tesla_stack)</label></transition><transition><source ref="id26"/><target ref="id25"/><label kind="guard" x="200" y="-640">unicast_repetitions_counter zero(bc_tesla_stack)</label></transition><transition><source ref="id26"/><target ref="id25"/><label kind="guard" x="200" y="-640">unicast_repetitions_counter
&lt; unicast_repetitions_max</label><label kind="synchronisation" x="200" y="-560">client_send_unicast_request!</label><label kind="assignment" x="200" y="-608">client_nonce_unicast_request := 1, &lt; unicast_repetitions_max</label><label kind="synchronisation" x="200" y="-560">client_send_unicast_request!</label><label kind="assignment" x="200" y="-608">client_nonce_unicast_request := 1,
unicast_repetitions_counter += 1, unicast_repetitions_counter += 1,
client_t1 := client_clock_counter()</label></transition><transition><source ref="id22"/><target ref="id17"/><label kind="select" x="-1112" y="-408">i: int[0, number_bc_channels-1]</label><label kind="synchronisation" x="-1112" y="-392">client_receive_broadcast_packet[i]?</label><label kind="assignment" x="-1112" y="-376">client_bc_interval := msg_network_bc_interval[i], client_t1 := client_clock_counter()</label></transition><transition><source ref="id22"/><target ref="id17"/><label kind="select" x="-1080" y="-408">i: int[0, number_bc_channels-1]</label><label kind="synchronisation" x="-1080" y="-392">client_receive_broadcast_packet[i]?</label><label kind="assignment" x="-1080" y="-376">client_bc_interval := msg_network_bc_interval[i],
client_bc_tb := msg_network_bc_tb[i] client_bc_tb := msg_network_bc_tb[i]
+ (msg_network_bc_interval[i] - 1)*bc_interval_length, + (msg_network_bc_interval[i] - 1)*bc_interval_length,
broadcast_offset broadcast_offset
...@@ -266,28 +269,28 @@ client_nonce_unicast_response := 0</label></transition></template><template><nam ...@@ -266,28 +269,28 @@ client_nonce_unicast_response := 0</label></transition></template><template><nam
network_nonce_unicast_request := 0</label></transition><transition><source ref="id31"/><target ref="id30"/><label kind="guard" x="72" y="-536">ticker &lt; 1</label><label kind="synchronisation" x="72" y="-520">client_send_unicast_request?</label><label kind="assignment" x="72" y="-504">propagation := 0</label></transition><transition><source ref="id32"/><target ref="id31"/><label kind="synchronisation" x="8" y="-624">start_system?</label></transition></template><template><name>Network_Unicast_Response</name><declaration>clock propagation;</declaration><location id="id33" x="96" y="128" color="#ff00ff"><name x="120" y="112">MESSAGE_ON_WIRE_MALICIOUS_DELAY</name><label kind="invariant" x="120" y="128">propagation &lt;= malicious_delay_max</label></location><location id="id34" x="-32" y="256"><name x="-208" y="232">MESSAGE_DELIVERED</name><committed/></location><location id="id35" x="96" y="0" color="#ff00ff"><name x="120" y="-32">MESSAGE_ON_WIRE_REGULAR</name><label kind="invariant" x="120" y="-16">propagation &lt;= network_delay_max</label></location><location id="id36" x="-32" y="-128" color="#00ff00"><name x="-128" y="-160">LISTENING</name></location><location id="id37" x="-32" y="-256" color="#ffffff"><name x="-16" y="-288">START</name></location><init ref="id37"/><transition><source ref="id33"/><target ref="id34"/><label kind="guard" x="40" y="200">ticker &lt; 1</label><label kind="synchronisation" x="40" y="216">client_receive_unicast_response!</label></transition><transition><source ref="id34"/><target ref="id36"/><label kind="assignment" x="-256" y="-16">propagation := 0, network_nonce_unicast_request := 0</label></transition><transition><source ref="id31"/><target ref="id30"/><label kind="guard" x="72" y="-536">ticker &lt; 1</label><label kind="synchronisation" x="72" y="-520">client_send_unicast_request?</label><label kind="assignment" x="72" y="-504">propagation := 0</label></transition><transition><source ref="id32"/><target ref="id31"/><label kind="synchronisation" x="8" y="-624">start_system?</label></transition></template><template><name>Network_Unicast_Response</name><declaration>clock propagation;</declaration><location id="id33" x="96" y="128" color="#ff00ff"><name x="120" y="112">MESSAGE_ON_WIRE_MALICIOUS_DELAY</name><label kind="invariant" x="120" y="128">propagation &lt;= malicious_delay_max</label></location><location id="id34" x="-32" y="256"><name x="-208" y="232">MESSAGE_DELIVERED</name><committed/></location><location id="id35" x="96" y="0" color="#ff00ff"><name x="120" y="-32">MESSAGE_ON_WIRE_REGULAR</name><label kind="invariant" x="120" y="-16">propagation &lt;= network_delay_max</label></location><location id="id36" x="-32" y="-128" color="#00ff00"><name x="-128" y="-160">LISTENING</name></location><location id="id37" x="-32" y="-256" color="#ffffff"><name x="-16" y="-288">START</name></location><init ref="id37"/><transition><source ref="id33"/><target ref="id34"/><label kind="guard" x="40" y="200">ticker &lt; 1</label><label kind="synchronisation" x="40" y="216">client_receive_unicast_response!</label></transition><transition><source ref="id34"/><target ref="id36"/><label kind="assignment" x="-256" y="-16">propagation := 0,
network_t2 := 0, network_t2 := 0,
network_t3 := 0, network_t3 := 0,
network_nonce_unicast_response</label></transition><transition><source ref="id35"/><target ref="id33"/><label kind="guard" x="104" y="48">propagation &gt;= network_delay_min</label><label kind="assignment" x="104" y="64">propagation := 0</label></transition><transition><source ref="id36"/><target ref="id35"/><label kind="guard" x="40" y="-120">ticker &lt; 1</label><label kind="synchronisation" x="40" y="-104">server_send_unicast_response?</label><label kind="assignment" x="40" y="-88">propagation := 0</label></transition><transition><source ref="id37"/><target ref="id36"/><label kind="synchronisation" x="-24" y="-208">start_system?</label></transition></template><template><name>Network_Broadcast_Packet</name><parameter>const int[0, number_bc_channels] i</parameter><declaration>clock propagation;</declaration><location id="id38" x="192" y="160" color="#ff00ff"><name x="216" y="136">MESSAGE_ON_WIRE_MALICIOUS_DELAY</name><label kind="invariant" x="216" y="152">propagation &lt;= malicious_delay_broad_max</label></location><location id="id39" x="-64" y="416"><name x="-240" y="392">MESSAGE_DELIVERED</name><committed/></location><location id="id40" x="64" y="32" color="#ff00ff"><name x="88" y="0">MESSAGE_ON_WIRE_REGULAR</name><label kind="invariant" x="88" y="16">propagation &lt;= network_delay_max</label></location><location id="id41" x="-64" y="-96" color="#00ff00"><name x="-160" y="-128">LISTENING</name></location><location id="id42" x="-64" y="-224" color="#ffffff"><name x="-48" y="-256">START</name></location><init ref="id42"/><transition><source ref="id38"/><target ref="id39"/><label kind="guard" x="416" y="328">propagation network_nonce_unicast_response</label></transition><transition><source ref="id35"/><target ref="id33"/><label kind="guard" x="104" y="48">propagation &gt;= network_delay_min</label><label kind="assignment" x="104" y="64">propagation := 0</label></transition><transition><source ref="id36"/><target ref="id35"/><label kind="guard" x="40" y="-120">ticker &lt; 1</label><label kind="synchronisation" x="40" y="-104">server_send_unicast_response?</label><label kind="assignment" x="40" y="-88">propagation := 0</label></transition><transition><source ref="id37"/><target ref="id36"/><label kind="synchronisation" x="-24" y="-208">start_system?</label></transition></template><template><name>Network_Broadcast_Packet</name><parameter>const int[0, number_bc_channels] i</parameter><declaration>clock propagation;</declaration><location id="id38" x="192" y="160" color="#ff00ff"><name x="208" y="120">MESSAGE_ON_WIRE_MALICIOUS_DELAY</name><label kind="invariant" x="208" y="136">propagation &lt;= malicious_delay_broad_max</label></location><location id="id39" x="-64" y="416"><name x="-48" y="432">MESSAGE_DELIVERED</name><committed/></location><location id="id40" x="64" y="32" color="#ff00ff"><name x="80" y="-8">MESSAGE_ON_WIRE_REGULAR</name><label kind="invariant" x="80" y="8">propagation &lt;= network_delay_max</label></location><location id="id41" x="-64" y="-96" color="#00ff00"><name x="-48" y="-128">LISTENING</name></location><location id="id42" x="-64" y="-224" color="#ffffff"><name x="-48" y="-256">START</name></location><init ref="id42"/><transition><source ref="id38"/><target ref="id39"/><label kind="guard" x="288" y="208">propagation
&gt;= malicious_delay_broad_max</label><nail x="448" y="416"/></transition><transition><source ref="id38"/><target ref="id39"/><label kind="synchronisation" x="8" y="232">packet_loss?</label></transition><transition><source ref="id40"/><target ref="id38"/><label kind="guard" x="144" y="72">propagation &gt;= network_delay_min</label><label kind="assignment" x="144" y="88">propagation := 0</label></transition><transition><source ref="id39"/><target ref="id41"/><label kind="assignment" x="-288" y="56">propagation := 0, &gt;= malicious_delay_broad_max</label><nail x="448" y="416"/></transition><transition><source ref="id38"/><target ref="id39"/><label kind="synchronisation" x="8" y="240">packet_loss?</label></transition><transition><source ref="id40"/><target ref="id38"/><label kind="guard" x="136" y="56">propagation &gt;= network_delay_min</label><label kind="assignment" x="136" y="72">propagation := 0</label></transition><transition><source ref="id39"/><target ref="id41"/><label kind="assignment" x="-56" y="120">propagation := 0,
msg_network_bc_tb[i] := 0, msg_network_bc_tb[i] := 0,
msg_network_bc_interval[i] := 0</label></transition><transition><source ref="id38"/><target ref="id39"/><label kind="guard" x="104" y="336">ticker &lt; 1</label><label kind="synchronisation" x="104" y="352">client_receive_broadcast_packet[i]!</label><nail x="128" y="320"/></transition><transition><source ref="id41"/><target ref="id40"/><label kind="guard" x="8" y="-88">ticker &lt; 1</label><label kind="synchronisation" x="8" y="-72">server_send_broadcast_packet[i]?</label><label kind="assignment" x="8" y="-56">propagation := 0</label></transition><transition><source ref="id42"/><target ref="id41"/><label kind="synchronisation" x="-48" y="-184">start_system?</label></transition></template><template><name>Server_Broadcast</name><declaration>INTERVAL_TIMESTAMP server_tb = 0; msg_network_bc_interval[i] := 0</label></transition><transition><source ref="id38"/><target ref="id39"/><label kind="guard" x="104" y="336">ticker &lt; 1</label><label kind="synchronisation" x="104" y="352">client_receive_broadcast_packet[i]!</label><nail x="128" y="320"/></transition><transition><source ref="id41"/><target ref="id40"/><label kind="guard" x="8" y="-88">ticker &lt; 1</label><label kind="synchronisation" x="8" y="-72">server_send_broadcast_packet[i]?</label><label kind="assignment" x="8" y="-56">propagation := 0</label></transition><transition><source ref="id42"/><target ref="id41"/><label kind="synchronisation" x="-48" y="-184">start_system?</label></transition></template><template><name>Server_Broadcast</name><declaration>INTERVAL_TIMESTAMP server_tb = 0;
INTERVAL_COUNTER server_bc_interval = 0; INTERVAL_COUNTER server_bc_interval = 0;
int[0, 2*bc_repetitions_global_max] bc_repetitions_global_counter = 0; int[0, 2*bc_repetitions_global_max] bc_repetitions_global_counter = 0;
clock propagation;</declaration><location id="id43" x="-256" y="416" color="#ffa500"><name x="-320" y="384">FINISH</name><committed/></location><location id="id44" x="0" y="416" color="#00ff00"><name x="-72" y="432">BROADCAST_TRIGGERED</name><label kind="invariant" x="-72" y="448">propagation &lt; bc_interval_length</label></location><location id="id45" x="0" y="160" color="#00ff00"><name x="16" y="128">IDLE</name></location><location id="id46" x="0" y="32" color="#ffffff"><name x="16" y="0">START</name></location><init ref="id46"/><transition><source ref="id45"/><target ref="id43"/><label kind="guard" x="-248" y="104">bc_repetitions_global_counter clock propagation;</declaration><location id="id43" x="-256" y="416" color="#ffa500"><name x="-248" y="432">FINISH</name><committed/></location><location id="id44" x="0" y="416" color="#00ff00"><name x="16" y="432">BROADCAST_TRIGGERED</name><label kind="invariant" x="16" y="448">propagation &lt; bc_interval_length</label></location><location id="id45" x="0" y="160" color="#00ff00"><name x="16" y="128">IDLE</name></location><location id="id46" x="0" y="32" color="#ffffff"><name x="16" y="0">START</name></location><init ref="id46"/><transition><source ref="id45"/><target ref="id43"/><label kind="guard" x="-248" y="104">bc_repetitions_global_counter
&gt;= bc_repetitions_global_max</label><label kind="synchronisation" x="-248" y="136">stop_clock!</label><nail x="-256" y="160"/></transition><transition><source ref="id44"/><target ref="id45"/><label kind="select" x="160" y="8">i: int[0, number_bc_channels-1]</label><label kind="guard" x="160" y="-8">propagation &gt; 0</label><label kind="synchronisation" x="160" y="25">server_send_broadcast_packet[i]!</label><label kind="assignment" x="160" y="40">server_tb := server_clock_counter &gt;= bc_repetitions_global_max</label><label kind="synchronisation" x="-248" y="136">stop_clock!</label><nail x="-256" y="160"/></transition><transition><source ref="id44"/><target ref="id45"/><label kind="select" x="120" y="8">i: int[0, number_bc_channels-1]</label><label kind="guard" x="120" y="-8">propagation &gt; 0</label><label kind="synchronisation" x="120" y="25">server_send_broadcast_packet[i]!</label><label kind="assignment" x="120" y="40">server_tb := server_clock_counter
- (server_interval_counter - 1)*bc_interval_length, - (server_interval_counter - 1)*bc_interval_length,
msg_network_bc_tb[i] := server_tb, msg_network_bc_tb[i] := server_tb,
server_tb := 0, server_tb := 0,
server_bc_interval := server_interval_counter, server_bc_interval := server_interval_counter,
msg_network_bc_interval[i] := server_bc_interval, msg_network_bc_interval[i] := server_bc_interval,
server_bc_interval := 0</label><nail x="272" y="416"/><nail x="272" y="160"/></transition><transition><source ref="id44"/><target ref="id43"/><label kind="synchronisation" x="-192" y="416">stop_clock?</label></transition><transition><source ref="id45"/><target ref="id43"/><label kind="synchronisation" x="-208" y="264">stop_clock?</label></transition><transition><source ref="id45"/><target ref="id44"/><label kind="guard" x="16" y="248">bc_repetitions_global_counter server_bc_interval := 0</label><nail x="416" y="416"/><nail x="416" y="160"/></transition><transition><source ref="id44"/><target ref="id43"/><label kind="synchronisation" x="-128" y="424">stop_clock?</label></transition><transition><source ref="id45"/><target ref="id43"/><label kind="synchronisation" x="-200" y="256">stop_clock?</label></transition><transition><source ref="id45"/><target ref="id44"/><label kind="guard" x="16" y="248">bc_repetitions_global_counter
&lt; bc_repetitions_global_max</label><label kind="synchronisation" x="16" y="312">server_interval_step?</label><label kind="assignment" x="16" y="280">bc_repetitions_global_counter += 1, &lt; bc_repetitions_global_max</label><label kind="synchronisation" x="16" y="312">server_interval_step?</label><label kind="assignment" x="16" y="280">bc_repetitions_global_counter += 1,
propagation := 0</label></transition><transition><source ref="id46"/><target ref="id45"/><label kind="synchronisation" x="8" y="80">start_system?</label></transition></template><template><name>Client_Clock_Diff</name><location id="id47" x="128" y="128" color="#ffa500"><name x="144" y="96">FINISH_CLOCKOUTOFBOUNDS</name><committed/></location><location id="id48" x="0" y="0"><name x="16" y="-32">CLOCK_SET</name><committed/></location><location id="id49" x="-256" y="128" color="#ffa500"><name x="-320" y="144">FINISH</name><committed/></location><location id="id50" x="-256" y="0" color="#00ff00"></location><location id="id51" x="-256" y="-128" color="#ffffff"><name x="-240" y="-160">START</name></location><init ref="id51"/><transition><source ref="id48"/><target ref="id47"/><label kind="guard" x="136" y="0">abs(client_clock_counter_diff) propagation := 0</label></transition><transition><source ref="id46"/><target ref="id45"/><label kind="synchronisation" x="-96" y="48">start_system?</label></transition></template><template><name>Client_Clock_Diff</name><location id="id47" x="128" y="128" color="#ffa500"><name x="144" y="96">FINISH_CLOCKOUTOFBOUNDS</name><committed/></location><location id="id48" x="0" y="0"><name x="16" y="-32">CLOCK_SET</name><committed/></location><location id="id49" x="-256" y="128" color="#ffa500"><name x="-248" y="144">FINISH</name><committed/></location><location id="id50" x="-256" y="0" color="#00ff00"></location><location id="id51" x="-256" y="-128" color="#ffffff"><name x="-240" y="-160">START</name></location><init ref="id51"/><transition><source ref="id48"/><target ref="id47"/><label kind="guard" x="136" y="0">abs(client_clock_counter_diff)
&gt; 3*bc_interval_length</label><nail x="128" y="0"/></transition><transition><source ref="id48"/><target ref="id50"/><label kind="guard" x="-160" y="-104">abs(client_clock_counter_diff) &gt; 3*bc_interval_length</label><nail x="128" y="0"/></transition><transition><source ref="id48"/><target ref="id50"/><label kind="guard" x="-96" y="-88">abs(client_clock_counter_diff)
&lt;= 3*bc_interval_length</label><nail x="-128" y="-64"/></transition><transition><source ref="id50"/><target ref="id48"/><label kind="synchronisation" x="-160" y="64">client_setclock?</label><label kind="assignment" x="-160" y="80">client_clock_counter_diff &lt;= 3*bc_interval_length</label><nail x="-128" y="-64"/></transition><transition><source ref="id50"/><target ref="id48"/><label kind="synchronisation" x="-96" y="56">client_setclock?</label><label kind="assignment" x="-96" y="72">client_clock_counter_diff
-= client_clock_correction, -= client_clock_correction,
client_clock_correction := 0</label><nail x="-128" y="64"/></transition><transition><source ref="id50"/><target ref="id49"/><label kind="synchronisation" x="-344" y="80">stop_clock?</label></transition><transition><source ref="id51"/><target ref="id50"/><label kind="synchronisation" x="-352" y="-80">start_system?</label></transition></template><system>// Place template instantiations here. client_clock_correction := 0</label><nail x="-128" y="64"/></transition><transition><source ref="id50"/><target ref="id49"/><label kind="synchronisation" x="-248" y="80">stop_clock?</label></transition><transition><source ref="id51"/><target ref="id50"/><label kind="synchronisation" x="-248" y="-104">start_system?</label></transition></template><system>// Place template instantiations here.
P_Ticker = Ticker(); P_Ticker = Ticker();
P_ClientClockDiff = Client_Clock_Diff(); P_ClientClockDiff = Client_Clock_Diff();
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment