- Started server broadcast module

Clocks-Test-4.xml

@@ -89,7 +89,7 @@ NONCE	server_nonce_unicast_response;
 int [0, server_clock_counter_max] 	server_t2 = 0,
 					server_t3 = 0;
 
-clock calculating;</declaration><location id="id15" x="-128" y="-128"><name x="-320" y="-144">CALCULATIONS_STAGE5</name><urgent/></location><location id="id16" x="0" y="96" color="#ff00ff"><name x="-96" y="112">CALCULATIONS_STAGE3</name><label kind="invariant" x="-96" y="128">calculating &lt;= server_computation_max</label></location><location id="id17" x="128" y="0"><name x="152" y="0">CALCULATIONS_STAGE2</name><urgent/></location><location id="id18" x="416" y="160" color="#ffa500"><name x="432" y="128">FINISH</name><committed/></location><location id="id19" x="-128" y="0"><name x="-320" y="-16">CALCULATIONS_STAGE4</name><urgent/></location><location id="id20" x="128" y="-128"><name x="152" y="-128">CALCULATIONS_STAGE1</name><urgent/></location><location id="id21" x="0" y="-224" color="#00ff00"><name x="-16" y="-208">IDLE</name></location><location id="id22" x="0" y="-448" color="#ffffff"><name x="-10" y="-478">START</name><committed/></location><init ref="id22"/><transition><source ref="id15"/><target ref="id21"/><label kind="synchronisation" x="-320" y="-320">server_send_unicast_response!</label><label kind="assignment" x="-320" y="-304">network_t2 := server_t2,
+clock calculating;</declaration><location id="id15" x="-128" y="-128"><name x="-320" y="-144">CALCULATIONS_STAGE5</name><urgent/></location><location id="id16" x="0" y="96" color="#ff00ff"><name x="-96" y="120">CALCULATIONS_STAGE3</name><label kind="invariant" x="-96" y="136">calculating &lt;= server_computation_max</label></location><location id="id17" x="128" y="0"><name x="152" y="0">CALCULATIONS_STAGE2</name><urgent/></location><location id="id18" x="416" y="160" color="#ffa500"><name x="432" y="128">FINISH</name><committed/></location><location id="id19" x="-128" y="0"><name x="-320" y="-16">CALCULATIONS_STAGE4</name><urgent/></location><location id="id20" x="128" y="-128"><name x="152" y="-128">CALCULATIONS_STAGE1</name><urgent/></location><location id="id21" x="0" y="-224" color="#00ff00"><name x="-16" y="-200">IDLE</name></location><location id="id22" x="0" y="-448" color="#ffffff"><name x="16" y="-480">START</name><committed/></location><init ref="id22"/><transition><source ref="id15"/><target ref="id21"/><label kind="synchronisation" x="-320" y="-320">server_send_unicast_response!</label><label kind="assignment" x="-320" y="-304">network_t2 := server_t2,
 server_t2 := 0,
 network_t3 := server_t3,
 server_t3 := 0,
@@ -142,7 +142,10 @@ client_t1 := t_client,
 t_client := 0</label></transition><transition><source ref="id36"/><target ref="id35"/><label kind="assignment" x="-232" y="-832">unicast_repetitions_counter := 0,
 broadcast_repetitions_counter := 0,
 client_nonce_unicast_request := 0,
-client_nonce_unicast_response := 0</label></transition></template><template><name>Network_Unicast_Request</name><declaration>clock propagation;</declaration><location id="id37" x="128" y="-320"><name x="144" y="-344">MESSAGE_ON_WIRE_MALICIOUS_DELAY</name><label kind="invariant" x="144" y="-328">propagation &lt;= malicious_delay_max</label></location><location id="id38" x="0" y="-224"><name x="-176" y="-248">MESSAGE_DELIVERED</name><committed/></location><location id="id39" x="128" y="-448"><name x="144" y="-464">MESSAGE_ON_WIRE_REGULAR</name><label kind="invariant" x="144" y="-448">propagation &lt;= network_delay_max</label></location><location id="id40" x="0" y="-544" color="#00ff00"><name x="-96" y="-576">LISTENING</name></location><location id="id41" x="0" y="-672" color="#ffffff"><name x="16" y="-704">START</name><committed/></location><init ref="id41"/><transition><source ref="id37"/><target ref="id38"/><label kind="synchronisation" x="72" y="-272">server_receive_unicast_request!</label><label kind="assignment" x="72" y="-256">propagation := 0</label></transition><transition><source ref="id39"/><target ref="id37"/><label kind="guard" x="136" y="-400">propagation &gt;= network_delay_min</label><label kind="assignment" x="136" y="-384">propagation := 0</label></transition><transition><source ref="id38"/><target ref="id40"/><label kind="assignment" x="-120" y="-432">propagation := 0</label></transition><transition><source ref="id40"/><target ref="id39"/><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="id41"/><target ref="id40"/></transition></template><template><name>Network_Unicast_Response</name><declaration>clock propagation;</declaration><location id="id42" 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="id43" x="-32" y="192"><name x="-208" y="168">MESSAGE_DELIVERED</name><committed/></location><location id="id44" 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="id45" x="-32" y="-128" color="#00ff00"><name x="-128" y="-160">LISTENING</name></location><location id="id46" x="-32" y="-256" color="#ffffff"><name x="-16" y="-288">START</name><committed/></location><init ref="id46"/><transition><source ref="id42"/><target ref="id43"/><label kind="synchronisation" x="48" y="136">client_receive_unicast_response!</label></transition><transition><source ref="id43"/><target ref="id45"/><label kind="assignment" x="-152" y="8">propagation := 0</label></transition><transition><source ref="id44"/><target ref="id42"/><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="id45"/><target ref="id44"/><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="id46"/><target ref="id45"/></transition></template><template><name>Network_Broadcast_Packet</name><declaration>clock propagation;</declaration><location id="id47" 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_max</label></location><location id="id48" x="-56" y="224"><name x="-232" y="200">MESSAGE_DELIVERED</name><committed/></location><location id="id49" 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="id50" x="-56" y="-96" color="#00ff00"><name x="-152" y="-128">LISTENING</name></location><location id="id51" x="-56" y="-224" color="#ffffff"><name x="-40" y="-256">START</name><committed/></location><init ref="id51"/><transition><source ref="id49"/><target ref="id47"/><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="id48"/><target ref="id50"/><label kind="assignment" x="-176" y="48">propagation := 0</label></transition><transition><source ref="id47"/><target ref="id48"/><label kind="synchronisation" x="32" y="168">client_receive_broadcast_packet!</label></transition><transition><source ref="id50"/><target ref="id49"/><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="id51"/><target ref="id50"/></transition></template><system>// Place template instantiations here.
+client_nonce_unicast_response := 0</label></transition></template><template><name>Network_Unicast_Request</name><declaration>clock propagation;</declaration><location id="id37" x="128" y="-320"><name x="144" y="-344">MESSAGE_ON_WIRE_MALICIOUS_DELAY</name><label kind="invariant" x="144" y="-328">propagation &lt;= malicious_delay_max</label></location><location id="id38" x="0" y="-224"><name x="-176" y="-248">MESSAGE_DELIVERED</name><committed/></location><location id="id39" x="128" y="-448"><name x="144" y="-464">MESSAGE_ON_WIRE_REGULAR</name><label kind="invariant" x="144" y="-448">propagation &lt;= network_delay_max</label></location><location id="id40" x="0" y="-544" color="#00ff00"><name x="-96" y="-576">LISTENING</name></location><location id="id41" x="0" y="-672" color="#ffffff"><name x="16" y="-704">START</name><committed/></location><init ref="id41"/><transition><source ref="id37"/><target ref="id38"/><label kind="synchronisation" x="72" y="-272">server_receive_unicast_request!</label><label kind="assignment" x="72" y="-256">propagation := 0</label></transition><transition><source ref="id39"/><target ref="id37"/><label kind="guard" x="136" y="-400">propagation &gt;= network_delay_min</label><label kind="assignment" x="136" y="-384">propagation := 0</label></transition><transition><source ref="id38"/><target ref="id40"/><label kind="assignment" x="-120" y="-432">propagation := 0</label></transition><transition><source ref="id40"/><target ref="id39"/><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="id41"/><target ref="id40"/></transition></template><template><name>Network_Unicast_Response</name><declaration>clock propagation;</declaration><location id="id42" 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="id43" x="-32" y="192"><name x="-208" y="168">MESSAGE_DELIVERED</name><committed/></location><location id="id44" 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="id45" x="-32" y="-128" color="#00ff00"><name x="-128" y="-160">LISTENING</name></location><location id="id46" x="-32" y="-256" color="#ffffff"><name x="-16" y="-288">START</name><committed/></location><init ref="id46"/><transition><source ref="id42"/><target ref="id43"/><label kind="synchronisation" x="48" y="136">client_receive_unicast_response!</label></transition><transition><source ref="id43"/><target ref="id45"/><label kind="assignment" x="-152" y="8">propagation := 0</label></transition><transition><source ref="id44"/><target ref="id42"/><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="id45"/><target ref="id44"/><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="id46"/><target ref="id45"/></transition></template><template><name>Network_Broadcast_Packet</name><declaration>clock propagation;</declaration><location id="id47" 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_max</label></location><location id="id48" x="-56" y="224"><name x="-232" y="200">MESSAGE_DELIVERED</name><committed/></location><location id="id49" 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="id50" x="-56" y="-96" color="#00ff00"><name x="-152" y="-128">LISTENING</name></location><location id="id51" x="-56" y="-224" color="#ffffff"><name x="-40" y="-256">START</name><committed/></location><init ref="id51"/><transition><source ref="id49"/><target ref="id47"/><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="id48"/><target ref="id50"/><label kind="assignment" x="-176" y="48">propagation := 0</label></transition><transition><source ref="id47"/><target ref="id48"/><label kind="synchronisation" x="32" y="168">client_receive_broadcast_packet!</label></transition><transition><source ref="id50"/><target ref="id49"/><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="id51"/><target ref="id50"/></transition></template><template><name>Server_Broadcast</name><declaration>int [0, server_clock_counter_max] 	server_tb = 0;
+
+clock calculating;</declaration><location id="id52" x="-88" y="272"></location><location id="id53" x="88" y="272"></location><location id="id54" x="0" y="160" color="#ff00ff"></location><location id="id55" x="0" y="0" color="#ffffff"><name x="-10" y="-30">START</name><committed/></location><init ref="id55"/><transition><source ref="id52"/><target ref="id54"/></transition><transition><source ref="id53"/><target ref="id52"/><label kind="assignment" x="-60" y="272">server_tb := t_server,
+t_server := 0</label></transition><transition><source ref="id54"/><target ref="id53"/><label kind="synchronisation" x="48" y="192">timestamp_server!</label></transition><transition><source ref="id55"/><target ref="id54"/><label kind="assignment" x="16" y="72">calculating := 0</label></transition></template><system>// Place template instantiations here.
 P_Ticker 			= Ticker();
 
 P_ClientClock 			= Client_Clock();