Skip to content
Snippets Groups Projects
Commit 35ead2cc authored by Kristof Teichel's avatar Kristof Teichel
Browse files

- Attempt to solve via multiple broadcast synchronization "channels". Creates... 

- Attempt to solve via multiple broadcast synchronization "channels". Creates out-of-bound error, untraceable under OS X
parent 933ff88d
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 23 additions and 19 deletions
Clocks-Test-7.xml
+ 23
− 19
View file @ 35ead2cc
...@@ -18,8 +18,10 @@ chan server_send_unicast_response, ...@@ -18,8 +18,10 @@ chan server_send_unicast_response,
client_receive_unicast_response; client_receive_unicast_response;
chan client_unicast_successful; chan client_unicast_successful;
broadcast chan server_send_broadcast_packet; const int number_bc_channels = 2;
broadcast chan client_receive_broadcast_packet;
broadcast chan server_send_broadcast_packet[number_bc_channels];
broadcast chan client_receive_broadcast_packet[number_bc_channels];
broadcast chan packet_loss; broadcast chan packet_loss;
...@@ -38,10 +40,10 @@ int abs(int x){ ...@@ -38,10 +40,10 @@ int abs(int x){
const int bc_repetitions_global_max = 10; const int bc_repetitions_global_max = 10;
const int unicast_repetitions_max = 1; const int unicast_repetitions_max = 2;
int [0, unicast_repetitions_max] unicast_repetitions_counter = 0; int [0, unicast_repetitions_max] unicast_repetitions_counter = 0;
const int broadcast_repetitions_max = 10; const int broadcast_repetitions_max = 0;
int[0, 2*broadcast_repetitions_max] broadcast_repetitions_counter = 0; int[0, 2*broadcast_repetitions_max] broadcast_repetitions_counter = 0;
const int const int
...@@ -69,6 +71,7 @@ const int ...@@ -69,6 +71,7 @@ const int
const int bc_disclosure_delay = 3; const int bc_disclosure_delay = 3;
// DERIVED DATA // DERIVED DATA
// int [0, malicious_delay_broad_max] malicious_delay_broad_smart = 1; // int [0, malicious_delay_broad_max] malicious_delay_broad_smart = 1;
...@@ -127,14 +130,13 @@ int client_clock_counter() {return server_clock_counter + client_clock_counter_d ...@@ -127,14 +130,13 @@ int client_clock_counter() {return server_clock_counter + client_clock_counter_d
NONCE network_nonce_unicast_request, NONCE network_nonce_unicast_request,
network_nonce_unicast_response; network_nonce_unicast_response;
TIMESTAMP network_t2 = 0; TIMESTAMP network_t2 = 0;
DIFF_TIMESTAMP network_t3 = 0; DIFF_TIMESTAMP network_t3 = 0;
// NETWORK VARIABLES (Broadcast) // // NETWORK VARIABLES (Broadcast) //
INTERVAL_TIMESTAMP msg_network_bc_tb = 0; 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="-376" color="#ffffff"><name x="16" y="-408">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="-104" y="-200">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="-64">ticker == 1</label><label kind="synchronisation" x="-192" y="-48">tick!</label><label kind="assignment" x="-192" y="-32">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="-72" y="-128"><committed/></location><location id="id4" x="544" y="152"><name x="568" y="120">BACK_TO_IDLE</name><committed/></location><location id="id5" x="0" y="272" color="#ffa500"><name x="-64" y="288">FINISH</name><committed/></location><location id="id6" x="0" y="-256" color="#ffffff"><name x="16" y="-288">START</name></location><location id="id7" x="544" y="-256" color="#ffa500"><name x="560" y="-288">FINISH_CLOCKOUTOFBOUNDS</name><committed/></location><location id="id8" x="544" y="-72"><name x="568" y="-104">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="-184" y="-80">server_interval_step!</label></transition><transition><source ref="id8"/><target ref="id4"/><label kind="guard" x="552" y="24">server_clock_counter &lt; server_clock_counter_max</label></transition><transition><source ref="id4"/><target ref="id9"/><label kind="guard" x="64" y="176">server_clock_counter &gt;= bc_interval_length * (server_interval_counter + 1)</label><label kind="synchronisation" x="64" y="208">server_interval_step!</label><label kind="assignment" x="64" y="192">server_interval_counter += 1</label><nail x="56" y="152"/></transition><transition><source ref="id9"/><target ref="id5"/><label kind="synchronisation" x="-80" y="120">stop_clock?</label></transition><transition><source ref="id6"/><target ref="id3"/><label kind="synchronisation" x="-136" y="-200">start_system?</label></transition><transition><source ref="id8"/><target ref="id7"/><label kind="guard" x="552" y="-144">server_clock_counter &gt;= server_clock_counter_max</label><label kind="synchronisation" x="552" y="-128">stop_clock!</label></transition><transition><source ref="id4"/><target ref="id9"/><label kind="guard" x="72" y="32">server_clock_counter &lt; bc_interval_length * (server_interval_counter + 1)</label></transition><transition><source ref="id9"/><target ref="id8"/><label kind="synchronisation" x="144" y="-128">tick?</label><label kind="assignment" x="144" y="-112">server_clock_counter += clock_incrementation_value</label><nail x="192" y="-72"/></transition></template><template><name>Server_Unicast</name><declaration>NONCE server_nonce_unicast_request;
INTERVAL_COUNTER msg_network_bc_interval = 0;</declaration><template><name x="5" y="5">Ticker</name><location id="id0" x="0" y="-376" color="#ffffff"><name x="16" y="-408">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="-104" y="-200">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="-64">ticker == 1</label><label kind="synchronisation" x="-192" y="-48">tick!</label><label kind="assignment" x="-192" y="-32">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="-72" y="-128"><committed/></location><location id="id4" x="544" y="152"><name x="568" y="120">BACK_TO_IDLE</name><committed/></location><location id="id5" x="0" y="272" color="#ffa500"><name x="-64" y="288">FINISH</name><committed/></location><location id="id6" x="0" y="-256" color="#ffffff"><name x="16" y="-288">START</name></location><location id="id7" x="544" y="-256" color="#ffa500"><name x="560" y="-288">FINISH_CLOCKOUTOFBOUNDS</name><committed/></location><location id="id8" x="544" y="-72"><name x="568" y="-104">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="-184" y="-80">server_interval_step!</label></transition><transition><source ref="id8"/><target ref="id4"/><label kind="guard" x="552" y="24">server_clock_counter &lt; server_clock_counter_max</label></transition><transition><source ref="id4"/><target ref="id9"/><label kind="guard" x="64" y="176">server_clock_counter &gt;= bc_interval_length * (server_interval_counter + 1)</label><label kind="synchronisation" x="64" y="208">server_interval_step!</label><label kind="assignment" x="64" y="192">server_interval_counter += 1</label><nail x="56" y="152"/></transition><transition><source ref="id9"/><target ref="id5"/><label kind="synchronisation" x="-80" y="120">stop_clock?</label></transition><transition><source ref="id6"/><target ref="id3"/><label kind="synchronisation" x="-136" y="-200">start_system?</label></transition><transition><source ref="id8"/><target ref="id7"/><label kind="guard" x="552" y="-144">server_clock_counter &gt;= server_clock_counter_max</label><label kind="synchronisation" x="552" y="-128">stop_clock!</label></transition><transition><source ref="id4"/><target ref="id9"/><label kind="guard" x="72" y="32">server_clock_counter &lt; bc_interval_length * (server_interval_counter + 1)</label></transition><transition><source ref="id9"/><target ref="id8"/><label kind="synchronisation" x="144" y="-128">tick?</label><label kind="assignment" x="144" y="-112">server_clock_counter += clock_incrementation_value</label><nail x="192" y="-72"/></transition></template><template><name>Server_Unicast</name><declaration>NONCE server_nonce_unicast_request;
NONCE server_nonce_unicast_response; NONCE server_nonce_unicast_response;
int [0, server_clock_counter_max] server_t2 = 0; int [0, server_clock_counter_max] server_t2 = 0;
...@@ -191,8 +193,8 @@ client_bc_interval := 0</label><nail x="-1248" y="-344"/></transition><transitio ...@@ -191,8 +193,8 @@ client_bc_interval := 0</label><nail x="-1248" y="-344"/></transition><transitio
&gt;= broadcast_repetitions_max</label><nail x="-592" y="-672"/></transition><transition><source ref="id23"/><target ref="id21"/><label kind="guard" x="-400" y="-544">broadcast_repetitions_max &gt; 0</label><label kind="assignment" x="-400" y="-528">broadcast_repetitions_counter := 1</label><nail x="-416" y="-544"/></transition><transition><source ref="id26"/><target ref="id25"/><label kind="guard" x="176" y="-584">unicast_repetitions_counter &gt;= broadcast_repetitions_max</label><nail x="-592" y="-672"/></transition><transition><source ref="id23"/><target ref="id21"/><label kind="guard" x="-400" y="-544">broadcast_repetitions_max &gt; 0</label><label kind="assignment" x="-400" y="-528">broadcast_repetitions_counter := 1</label><nail x="-416" y="-544"/></transition><transition><source ref="id26"/><target ref="id25"/><label kind="guard" x="176" y="-584">unicast_repetitions_counter
&lt; unicast_repetitions_max</label><label kind="synchronisation" x="176" y="-504">client_send_unicast_request!</label><label kind="assignment" x="176" y="-552">client_nonce_unicast_request := 1, &lt; unicast_repetitions_max</label><label kind="synchronisation" x="176" y="-504">client_send_unicast_request!</label><label kind="assignment" x="176" y="-552">client_nonce_unicast_request := 1,
unicast_repetitions_counter += 1, unicast_repetitions_counter += 1,
client_t1 := client_clock_counter()</label><nail x="128" y="-640"/><nail x="160" y="-544"/></transition><transition><source ref="id22"/><target ref="id17"/><label kind="synchronisation" x="-1328" y="-224">client_receive_broadcast_packet?</label><label kind="assignment" x="-1328" y="-208">client_bc_interval := msg_network_bc_interval, client_t1 := client_clock_counter()</label><nail x="128" y="-640"/><nail x="160" y="-544"/></transition><transition><source ref="id22"/><target ref="id17"/><label kind="select" x="-1440" y="-208">i: int[1, number_bc_channels]</label><label kind="synchronisation" x="-1440" y="-192">client_receive_broadcast_packet[i]?</label><label kind="assignment" x="-1440" y="-176">client_bc_interval := msg_network_bc_interval[i],
client_bc_tb := msg_network_bc_tb + (msg_network_bc_interval - 1)*bc_interval_length, client_bc_tb := msg_network_bc_tb[i] + (msg_network_bc_interval[i] - 1)*bc_interval_length,
broadcast_offset := client_clock_counter() - (client_bc_tb + broadcast_delay)</label></transition><transition><source ref="id21"/><target ref="id22"/><label kind="guard" x="-600" y="-504">broadcast_repetitions_counter broadcast_offset := client_clock_counter() - (client_bc_tb + broadcast_delay)</label></transition><transition><source ref="id21"/><target ref="id22"/><label kind="guard" x="-600" y="-504">broadcast_repetitions_counter
&lt; broadcast_repetitions_max</label><nail x="-608" y="-416"/><nail x="-640" y="-320"/></transition><transition><source ref="id23"/><target ref="id26"/><label kind="guard" x="-352" y="-632">broadcast_repetitions_max == 0</label><nail x="-128" y="-640"/></transition><transition><source ref="id25"/><target ref="id24"/><label kind="synchronisation" x="160" y="-400">client_receive_unicast_response?</label><label kind="assignment" x="160" y="-384">client_t2 := network_t2, &lt; broadcast_repetitions_max</label><nail x="-608" y="-416"/><nail x="-640" y="-320"/></transition><transition><source ref="id23"/><target ref="id26"/><label kind="guard" x="-352" y="-632">broadcast_repetitions_max == 0</label><nail x="-128" y="-640"/></transition><transition><source ref="id25"/><target ref="id24"/><label kind="synchronisation" x="160" y="-400">client_receive_unicast_response?</label><label kind="assignment" x="160" y="-384">client_t2 := network_t2,
client_t3 := network_t3 + client_t2, client_t3 := network_t3 + client_t2,
...@@ -203,17 +205,17 @@ client_nonce_unicast_response := 0</label></transition></template><template><nam ...@@ -203,17 +205,17 @@ 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="-560">ticker &lt; 1</label><label kind="synchronisation" x="72" y="-544">client_send_unicast_request?</label><label kind="assignment" x="72" y="-528">propagation := 0</label></transition><transition><source ref="id32"/><target ref="id31"/><label kind="synchronisation" x="16" y="-632">start_system?</label></transition></template><template><name>Network_Unicast_Response</name><declaration>clock propagation;</declaration><location id="id33" x="96" y="96" color="#ff00ff"><name x="120" y="80">MESSAGE_ON_WIRE_MALICIOUS_DELAY</name><label kind="invariant" x="120" y="96">propagation &lt;= malicious_delay_max</label></location><location id="id34" x="-32" y="192"><name x="-208" y="168">MESSAGE_DELIVERED</name><committed/></location><location id="id35" x="96" y="-32" color="#ff00ff"><name x="120" y="-48">MESSAGE_ON_WIRE_REGULAR</name><label kind="invariant" x="120" y="-32">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="48" y="136">ticker &lt; 1</label><label kind="synchronisation" x="48" y="152">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="-560">ticker &lt; 1</label><label kind="synchronisation" x="72" y="-544">client_send_unicast_request?</label><label kind="assignment" x="72" y="-528">propagation := 0</label></transition><transition><source ref="id32"/><target ref="id31"/><label kind="synchronisation" x="16" y="-632">start_system?</label></transition></template><template><name>Network_Unicast_Response</name><declaration>clock propagation;</declaration><location id="id33" x="96" y="96" color="#ff00ff"><name x="120" y="80">MESSAGE_ON_WIRE_MALICIOUS_DELAY</name><label kind="invariant" x="120" y="96">propagation &lt;= malicious_delay_max</label></location><location id="id34" x="-32" y="192"><name x="-208" y="168">MESSAGE_DELIVERED</name><committed/></location><location id="id35" x="96" y="-32" color="#ff00ff"><name x="120" y="-48">MESSAGE_ON_WIRE_REGULAR</name><label kind="invariant" x="120" y="-32">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="48" y="136">ticker &lt; 1</label><label kind="synchronisation" x="48" y="152">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="112" y="16">propagation &gt;= network_delay_min</label><label kind="assignment" x="112" y="32">propagation := 0</label></transition><transition><source ref="id36"/><target ref="id35"/><label kind="guard" x="40" y="-136">ticker &lt; 1</label><label kind="synchronisation" x="40" y="-120">server_send_unicast_response?</label><label kind="assignment" x="40" y="-104">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><declaration>clock propagation;</declaration><location id="id38" x="64" y="136" color="#ff00ff"><name x="88" y="112">MESSAGE_ON_WIRE_MALICIOUS_DELAY</name><label kind="invariant" x="88" y="128">propagation &lt;= malicious_delay_broad_max</label></location><location id="id39" x="-56" y="224"><name x="-232" y="200">MESSAGE_DELIVERED</name><committed/></location><location id="id40" x="64" y="8" color="#ff00ff"><name x="88" y="-24">MESSAGE_ON_WIRE_REGULAR</name><label kind="invariant" x="88" y="-8">propagation &lt;= network_delay_max</label></location><location id="id41" x="-56" y="-96" color="#00ff00"><name x="-152" y="-128">LISTENING</name></location><location id="id42" x="-56" y="-224" color="#ffffff"><name x="-40" y="-256">START</name></location><init ref="id42"/><transition><source ref="id38"/><target ref="id39"/><label kind="synchronisation" x="-40" y="112">packet_loss?</label><nail x="-16" y="136"/></transition><transition><source ref="id40"/><target ref="id38"/><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="id39"/><target ref="id41"/><label kind="assignment" x="-272" y="56">propagation := 0, network_nonce_unicast_response</label></transition><transition><source ref="id35"/><target ref="id33"/><label kind="guard" x="112" y="16">propagation &gt;= network_delay_min</label><label kind="assignment" x="112" y="32">propagation := 0</label></transition><transition><source ref="id36"/><target ref="id35"/><label kind="guard" x="40" y="-136">ticker &lt; 1</label><label kind="synchronisation" x="40" y="-120">server_send_unicast_response?</label><label kind="assignment" x="40" y="-104">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="64" y="136" color="#ff00ff"><name x="88" y="112">MESSAGE_ON_WIRE_MALICIOUS_DELAY</name><label kind="invariant" x="88" y="128">propagation &lt;= malicious_delay_broad_max</label></location><location id="id39" x="-56" y="224"><name x="-232" y="200">MESSAGE_DELIVERED</name><committed/></location><location id="id40" x="64" y="8" color="#ff00ff"><name x="88" y="-24">MESSAGE_ON_WIRE_REGULAR</name><label kind="invariant" x="88" y="-8">propagation &lt;= network_delay_max</label></location><location id="id41" x="-56" y="-96" color="#00ff00"><name x="-152" y="-128">LISTENING</name></location><location id="id42" x="-56" y="-224" color="#ffffff"><name x="-40" y="-256">START</name></location><init ref="id42"/><transition><source ref="id38"/><target ref="id39"/><label kind="synchronisation" x="-40" y="112">packet_loss?</label><nail x="-16" y="136"/></transition><transition><source ref="id40"/><target ref="id38"/><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="id39"/><target ref="id41"/><label kind="assignment" x="-288" y="56">propagation := 0,
msg_network_bc_tb := 0, msg_network_bc_tb[i] := 0,
msg_network_bc_interval := 0</label></transition><transition><source ref="id38"/><target ref="id39"/><label kind="synchronisation" x="8" y="208">client_receive_broadcast_packet!</label></transition><transition><source ref="id41"/><target ref="id40"/><label kind="synchronisation" x="24" y="-96">server_send_broadcast_packet?</label><label kind="assignment" x="24" y="-80">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="synchronisation" x="8" y="208">client_receive_broadcast_packet[i]!</label></transition><transition><source ref="id41"/><target ref="id40"/><label kind="synchronisation" x="24" y="-96">server_send_broadcast_packet[i]?</label><label kind="assignment" x="24" y="-80">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;</declaration><location id="id43" x="-328" y="448" color="#ffa500"><name x="-392" y="416">FINISH</name><committed/></location><location id="id44" x="0" y="448" color="#00ff00"><name x="-72" y="464">BROADCAST_TRIGGERED</name><urgent/></location><location id="id45" x="0" y="160" color="#00ff00"><name x="16" y="128">IDLE</name></location><location id="id46" x="0" y="-48" color="#ffffff"><name x="16" y="-80">START</name></location><init ref="id46"/><transition><source ref="id45"/><target ref="id43"/><label kind="guard" x="-312" y="96">bc_repetitions_global_counter int[0, 2*bc_repetitions_global_max] bc_repetitions_global_counter = 0;</declaration><location id="id43" x="-328" y="448" color="#ffa500"><name x="-392" y="416">FINISH</name><committed/></location><location id="id44" x="0" y="448" color="#00ff00"><name x="-72" y="464">BROADCAST_TRIGGERED</name><urgent/></location><location id="id45" x="0" y="160" color="#00ff00"><name x="16" y="128">IDLE</name></location><location id="id46" x="0" y="-48" color="#ffffff"><name x="16" y="-80">START</name></location><init ref="id46"/><transition><source ref="id45"/><target ref="id43"/><label kind="guard" x="-312" y="96">bc_repetitions_global_counter
&gt;= bc_repetitions_global_max</label><label kind="synchronisation" x="-312" y="128">stop_clock!</label><nail x="-328" y="160"/></transition><transition><source ref="id44"/><target ref="id45"/><label kind="synchronisation" x="400" y="209">server_send_broadcast_packet!</label><label kind="assignment" x="400" y="224">server_tb := server_clock_counter - (server_interval_counter - 1)*bc_interval_length, &gt;= bc_repetitions_global_max</label><label kind="synchronisation" x="-312" y="128">stop_clock!</label><nail x="-328" y="160"/></transition><transition><source ref="id44"/><target ref="id45"/><label kind="select" x="400" y="192">i: int[1, number_bc_channels]</label><label kind="synchronisation" x="400" y="209">server_send_broadcast_packet[i]!</label><label kind="assignment" x="400" y="224">server_tb := server_clock_counter - (server_interval_counter - 1)*bc_interval_length,
msg_network_bc_tb := 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 := server_bc_interval, msg_network_bc_interval[i] := server_bc_interval,
server_bc_interval := 0</label><nail x="392" y="448"/><nail x="392" 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="-232" 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="392" y="448"/><nail x="392" 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="-232" y="264">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="296">server_interval_step?</label><label kind="assignment" x="16" y="280">bc_repetitions_global_counter += 1</label></transition><transition><source ref="id46"/><target ref="id45"/><label kind="synchronisation" x="-104" y="8">start_system?</label></transition></template><template><name>Client_Clock_Diff</name><location id="id47" x="304" y="184" color="#ffa500"><name x="320" y="152">FINISH_CLOCKOUTOFBOUNDS</name><committed/></location><location id="id48" x="-80" y="-8"><name x="-64" y="-40">CLOCK_SET</name><committed/></location><location id="id49" x="-256" y="184" color="#ffa500"><name x="-240" y="152">FINISH</name><committed/></location><location id="id50" x="-256" y="-8" color="#00ff00"></location><location id="id51" x="-256" y="-224" color="#ffffff"><name x="-240" y="-256">START</name></location><init ref="id51"/><transition><source ref="id48"/><target ref="id47"/><label kind="guard" x="320" y="0">abs(client_clock_counter_diff) &lt; bc_repetitions_global_max</label><label kind="synchronisation" x="16" y="296">server_interval_step?</label><label kind="assignment" x="16" y="280">bc_repetitions_global_counter += 1</label></transition><transition><source ref="id46"/><target ref="id45"/><label kind="synchronisation" x="-104" y="8">start_system?</label></transition></template><template><name>Client_Clock_Diff</name><location id="id47" x="304" y="184" color="#ffa500"><name x="320" y="152">FINISH_CLOCKOUTOFBOUNDS</name><committed/></location><location id="id48" x="-80" y="-8"><name x="-64" y="-40">CLOCK_SET</name><committed/></location><location id="id49" x="-256" y="184" color="#ffa500"><name x="-240" y="152">FINISH</name><committed/></location><location id="id50" x="-256" y="-8" color="#00ff00"></location><location id="id51" x="-256" y="-224" color="#ffffff"><name x="-240" y="-256">START</name></location><init ref="id51"/><transition><source ref="id48"/><target ref="id47"/><label kind="guard" x="320" y="0">abs(client_clock_counter_diff)
&gt; 3*bc_interval_length</label><nail x="304" y="-8"/></transition><transition><source ref="id48"/><target ref="id50"/><label kind="guard" x="-184" y="-136">abs(client_clock_counter_diff) &gt; 3*bc_interval_length</label><nail x="304" y="-8"/></transition><transition><source ref="id48"/><target ref="id50"/><label kind="guard" x="-184" y="-136">abs(client_clock_counter_diff)
...@@ -230,14 +232,16 @@ P_ServerUnicast = Server_Unicast(); ...@@ -230,14 +232,16 @@ P_ServerUnicast = Server_Unicast();
P_NetworkUnicastRequest = Network_Unicast_Request(); P_NetworkUnicastRequest = Network_Unicast_Request();
P_NetworkUnicastResponse = Network_Unicast_Response(); P_NetworkUnicastResponse = Network_Unicast_Response();
P_NetworkBroadcastPacket = Network_Broadcast_Packet(); P_NetworkBroadcastPacket1 = Network_Broadcast_Packet(1);
P_NetworkBroadcastPacket2 = Network_Broadcast_Packet(2);
P_ServerBroadcast = Server_Broadcast(); P_ServerBroadcast = Server_Broadcast();
// List one or more processes to be composed into a system. // List one or more processes to be composed into a system.
system P_ClientBehavior, system P_ClientBehavior,
P_NetworkBroadcastPacket, P_NetworkBroadcastPacket1,
//P_NetworkBroadcastPacket2,
P_ServerBroadcast, P_ServerBroadcast,
P_NetworkUnicastRequest, P_NetworkUnicastRequest,
P_ServerUnicast, P_ServerUnicast,
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment