Skip to content
Snippets Groups Projects
Commit 840651f6 authored by Kristof's avatar Kristof
Browse files

- Friday last minute changes

parent a49d9750
Branches
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Clocks-Test-3.q
+ 2
− 2
View file @ 840651f6
......@@ -28,12 +28,12 @@ E<> P_ClientClock.FINISH_CLOCKOUTOFBOUNDS
/*
*/
E<> P_ClientBehavior.FINISH_TIMEOUT
A[] P_ClientBehavior.FINISH_PROCEDURE imply (P_ClientClock.client_clock_counter - P_ServerClock.server_clock_counter < P_ClientBehavior.unicast_roundtrip / 2)
/*
*/
A[] P_ClientBehavior.FINISH_PROCEDURE imply (P_ClientClock.client_clock_counter - P_ServerClock.server_clock_counter < P_ClientBehavior.unicast_roundtrip / 2)
A[] P_ClientBehavior.UNICAST_FINISHED imply (P_ClientClock.client_clock_counter - P_ServerClock.server_clock_counter < P_ClientBehavior.unicast_roundtrip / 2)
/*
......
Clocks-Test-3.xml
+ 12
− 12
View file @ 840651f6
......@@ -37,7 +37,7 @@ const int max_measurable = server_clock_counter_max;
typedef int[-max_measurable, max_measurable] MEASURED_OFFSET;
typedef int[-1, max_measurable] MEASURED_DELAY;
// The typedef for measured roundtrip(s). Creates "out of bounds" problems for some reason
// The typedef for measured roundtrip(s). Creates "out of bounds" problems for some reason.
typedef int [0, (2 * network_delay_max + server_computation_max + malicious_delay_max + 1)*clock_incrementation_value] MEASURED_ROUNDTRIP;
MEASURED_OFFSET client_clock_correction = 0;
......@@ -120,13 +120,13 @@ MEASURED_ROUNDTRIP unicast_roundtrip;
int[0, 1] unicast_sufficient_precision = 0;
clock unicast_timeout;</declaration><location id="id23" x="-128" y="-320"><name x="-376" y="-344">UNICAST_OFFSET_CALCULATION</name><urgent/></location><location id="id24" x="0" y="-480" color="#ffa500"><name x="-56" y="-512">FINISH_TIMEOUT</name></location><location id="id25" x="0" y="-288"><name x="-8" y="-272">UNICAST_RESPONSE_TIMESTAMPED</name><urgent/></location><location id="id26" x="416" y="-864" color="#ffa500"><name x="264" y="-896">FINISH_PROCEDURE</name><committed/></location><location id="id27" x="-768" y="-672"><name x="-840" y="-712">BROADCAST_FINISHED</name><committed/></location><location id="id28" x="-608" y="-544"><name x="-592" y="-576">INITIALIZING_BROADCAST</name><committed/></location><location id="id29" x="-928" y="-544"><name x="-1128" y="-576">BROAD_TIMELINESS_DONE</name><committed/></location><location id="id30" x="160" y="-544"><name x="184" y="-560">UNICAST_REQUEST_READY_TO_SEND</name><urgent/></location><location id="id31" x="-928" y="-416"><name x="-1176" y="-440">BROAD_PACKET_RECEIVED</name><committed/></location><location id="id32" x="-768" y="-288" color="#ff00ff"><name x="-1016" y="-272">WAITING_FOR_BROADCAST_PACKET</name></location><location id="id33" x="-160" y="-544"><name x="-304" y="-576">UNICAST_FINISHED</name><urgent/></location><location id="id34" x="128" y="-320"><name x="144" y="-320">UNICAST_RESPONSE_RECEIVED</name><urgent/></location><location id="id35" x="160" y="-416" color="#ff00ff"><name x="184" y="-432">WAITING_FOR_UNICAST_RESPONSE</name></location><location id="id36" x="0" y="-672"><name x="32" y="-696">IDLE_UNICAST</name><urgent/></location><location id="id37" x="0" y="-864" color="#ffffff"><name x="16" y="-896">START</name><committed/></location><init ref="id37"/><transition><source ref="id23"/><target ref="id33"/><label kind="synchronisation" x="-136" y="-416">client_setclock!</label><label kind="assignment" x="-136" y="-400">client_clock_correction := unicast_offset,
unicast_offset := 0</label><nail x="-160" y="-416"/></transition><transition><source ref="id35"/><target ref="id24"/><label kind="synchronisation" x="64" y="-480">stop_clock?</label><nail x="64" y="-448"/></transition><transition><source ref="id34"/><target ref="id25"/><label kind="synchronisation" x="48" y="-296">timestamp_client!</label></transition><transition><source ref="id36"/><target ref="id26"/><label kind="guard" x="208" y="-856">unicast_repetitions_counter
&gt;= unicast_repetitions_max</label><label kind="synchronisation" x="208" y="-824">stop_clock!</label><nail x="192" y="-864"/></transition><transition><source ref="id29"/><target ref="id27"/><nail x="-896" y="-640"/></transition><transition><source ref="id27"/><target ref="id28"/><label kind="guard" x="-624" y="-648">broadcast_repetitions_counter
&lt; broadcast_repetitions_max</label><nail x="-640" y="-640"/></transition><transition><source ref="id27"/><target ref="id36"/><label kind="guard" x="-440" y="-712">broadcast_repetitions_counter
&gt;= broadcast_repetitions_max</label></transition><transition><source ref="id33"/><target ref="id28"/><label kind="guard" x="-480" y="-536">unicast_sufficient_precision == 1
and broadcast_repetitions_max &gt; 0</label><label kind="assignment" x="-480" y="-504">broadcast_repetitions_counter := 0</label></transition><transition><source ref="id31"/><target ref="id29"/></transition><transition><source ref="id36"/><target ref="id30"/><label kind="guard" x="160" y="-640">unicast_repetitions_counter
&lt; unicast_repetitions_max</label><label kind="synchronisation" x="160" y="-656">timestamp_client!</label><label kind="assignment" x="160" y="-608">unicast_repetitions_counter += 1</label><nail x="128" y="-640"/></transition><transition><source ref="id32"/><target ref="id31"/><label kind="synchronisation" x="-1136" y="-352">client_receive_broadcast_packet?</label><nail x="-896" y="-320"/></transition><transition><source ref="id28"/><target ref="id32"/><label kind="assignment" x="-656" y="-312">broadcast_repetitions_counter += 1</label><nail x="-608" y="-416"/><nail x="-640" y="-320"/></transition><transition><source ref="id33"/><target ref="id36"/><label kind="guard" x="-344" y="-640">broadcast_repetitions_max == 0</label><nail x="-128" y="-640"/></transition><transition><source ref="id25"/><target ref="id23"/><label kind="assignment" x="-152" y="-248">client_t4 := t_client,
clock unicast_timeout;</declaration><location id="id23" x="-128" y="-320"><name x="-376" y="-344">UNICAST_OFFSET_CALCULATION</name><urgent/></location><location id="id24" x="0" y="-288"><name x="-8" y="-272">UNICAST_RESPONSE_TIMESTAMPED</name><urgent/></location><location id="id25" x="416" y="-864" color="#ffa500"><name x="264" y="-896">FINISH_PROCEDURE</name><committed/></location><location id="id26" x="-768" y="-672"><name x="-840" y="-712">BROADCAST_FINISHED</name><committed/></location><location id="id27" x="-608" y="-544"><name x="-592" y="-576">INITIALIZING_BROADCAST</name><committed/></location><location id="id28" x="-928" y="-544"><name x="-1128" y="-576">BROAD_TIMELINESS_DONE</name><committed/></location><location id="id29" x="160" y="-544"><name x="184" y="-560">UNICAST_REQUEST_READY_TO_SEND</name><urgent/></location><location id="id30" x="-928" y="-416"><name x="-1176" y="-440">BROAD_PACKET_RECEIVED</name><committed/></location><location id="id31" x="-768" y="-288" color="#ff00ff"><name x="-1016" y="-272">WAITING_FOR_BROADCAST_PACKET</name></location><location id="id32" x="-160" y="-544"><name x="-304" y="-576">UNICAST_FINISHED</name><urgent/></location><location id="id33" x="128" y="-320"><name x="144" y="-320">UNICAST_RESPONSE_RECEIVED</name><urgent/></location><location id="id34" x="160" y="-416" color="#ff00ff"><name x="184" y="-432">WAITING_FOR_UNICAST_RESPONSE</name></location><location id="id35" x="0" y="-672"><name x="32" y="-696">IDLE_UNICAST</name><urgent/></location><location id="id36" x="0" y="-864" color="#ffffff"><name x="16" y="-896">START</name><committed/></location><init ref="id36"/><transition><source ref="id23"/><target ref="id32"/><label kind="synchronisation" x="-136" y="-416">client_setclock!</label><label kind="assignment" x="-136" y="-400">client_clock_correction := unicast_offset,
unicast_offset := 0</label><nail x="-160" y="-416"/></transition><transition><source ref="id33"/><target ref="id24"/><label kind="synchronisation" x="48" y="-296">timestamp_client!</label></transition><transition><source ref="id35"/><target ref="id25"/><label kind="guard" x="208" y="-856">unicast_repetitions_counter
&gt;= unicast_repetitions_max</label><label kind="synchronisation" x="208" y="-824">stop_clock!</label><nail x="192" y="-864"/></transition><transition><source ref="id28"/><target ref="id26"/><nail x="-896" y="-640"/></transition><transition><source ref="id26"/><target ref="id27"/><label kind="guard" x="-624" y="-648">broadcast_repetitions_counter
&lt; broadcast_repetitions_max</label><nail x="-640" y="-640"/></transition><transition><source ref="id26"/><target ref="id35"/><label kind="guard" x="-440" y="-712">broadcast_repetitions_counter
&gt;= broadcast_repetitions_max</label></transition><transition><source ref="id32"/><target ref="id27"/><label kind="guard" x="-480" y="-536">unicast_sufficient_precision == 1
and broadcast_repetitions_max &gt; 0</label><label kind="assignment" x="-480" y="-504">broadcast_repetitions_counter := 0</label></transition><transition><source ref="id30"/><target ref="id28"/></transition><transition><source ref="id35"/><target ref="id29"/><label kind="guard" x="160" y="-640">unicast_repetitions_counter
&lt; unicast_repetitions_max</label><label kind="synchronisation" x="160" y="-656">timestamp_client!</label><label kind="assignment" x="160" y="-608">unicast_repetitions_counter += 1</label><nail x="128" y="-640"/></transition><transition><source ref="id31"/><target ref="id30"/><label kind="synchronisation" x="-1136" y="-352">client_receive_broadcast_packet?</label><nail x="-896" y="-320"/></transition><transition><source ref="id27"/><target ref="id31"/><label kind="assignment" x="-656" y="-312">broadcast_repetitions_counter += 1</label><nail x="-608" y="-416"/><nail x="-640" y="-320"/></transition><transition><source ref="id32"/><target ref="id35"/><label kind="guard" x="-344" y="-640">broadcast_repetitions_max == 0</label><nail x="-128" y="-640"/></transition><transition><source ref="id24"/><target ref="id23"/><label kind="assignment" x="-152" y="-248">client_t4 := t_client,
t_client := 0,
unicast_offset := (client_t1 + client_t4) / 2 - (client_t2 + client_t3) / 2,
unicast_roundtrip := client_t4 - client_t1,
......@@ -134,15 +134,15 @@ broadcast_delay := client_t4 - client_t1 - (client_t3 - client_t2),
client_t1 := 0,
client_t2 := 0,
client_t3 := 0,
client_t4 := 0</label><nail x="-160" y="-256"/><nail x="-160" y="-128"/><nail x="-192" y="-128"/><nail x="-192" y="-256"/></transition><transition><source ref="id35"/><target ref="id34"/><label kind="synchronisation" x="160" y="-400">client_receive_unicast_response?</label><label kind="assignment" x="160" y="-384">client_t2 := network_t2,
client_t4 := 0</label><nail x="-160" y="-256"/><nail x="-160" y="-128"/><nail x="-192" y="-128"/><nail x="-192" y="-256"/></transition><transition><source ref="id34"/><target ref="id33"/><label kind="synchronisation" x="160" y="-400">client_receive_unicast_response?</label><label kind="assignment" x="160" y="-384">client_t2 := network_t2,
network_t2 := 0,
client_t3 := network_t3,
network_t3 := 0</label></transition><transition><source ref="id30"/><target ref="id35"/><label kind="synchronisation" x="168" y="-512">client_send_unicast_request!</label><label kind="assignment" x="168" y="-496">client_nonce_unicast_request := 1,
network_t3 := 0</label></transition><transition><source ref="id29"/><target ref="id34"/><label kind="synchronisation" x="168" y="-512">client_send_unicast_request!</label><label kind="assignment" x="168" y="-496">client_nonce_unicast_request := 1,
client_t1 := t_client,
t_client := 0</label></transition><transition><source ref="id37"/><target ref="id36"/><label kind="assignment" x="-232" y="-832">unicast_repetitions_counter := 0,
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="id38" 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="id39" x="0" y="-224"><name x="-176" y="-248">MESSAGE_DELIVERED</name><committed/></location><location id="id40" 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="id41" x="0" y="-544" color="#00ff00"><name x="-96" y="-576">LISTENING</name></location><location id="id42" x="0" y="-672" color="#ffffff"><name x="16" y="-704">START</name><committed/></location><init ref="id42"/><transition><source ref="id38"/><target ref="id39"/><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="id40"/><target ref="id38"/><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="id39"/><target ref="id41"/><label kind="assignment" x="-120" y="-432">propagation := 0</label></transition><transition><source ref="id41"/><target ref="id40"/><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="id42"/><target ref="id41"/></transition></template><template><name>Network_Unicast_Response</name><declaration>clock propagation;</declaration><location id="id43" 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="id44" x="-32" y="192"><name x="-208" y="168">MESSAGE_DELIVERED</name><committed/></location><location id="id45" 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="id46" x="-32" y="-128" color="#00ff00"><name x="-128" y="-160">LISTENING</name></location><location id="id47" x="-32" y="-256" color="#ffffff"><name x="-16" y="-288">START</name><committed/></location><init ref="id47"/><transition><source ref="id43"/><target ref="id44"/><label kind="synchronisation" x="48" y="136">client_receive_unicast_response!</label></transition><transition><source ref="id44"/><target ref="id46"/><label kind="assignment" x="-152" y="8">propagation := 0</label></transition><transition><source ref="id45"/><target ref="id43"/><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="id46"/><target ref="id45"/><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="id47"/><target ref="id46"/></transition></template><template><name>Network_Broadcast_Packet</name><declaration>clock propagation;</declaration><location id="id48" x="-64" y="224"><name x="-56" y="232">MESSAGE_DELIVERED</name><committed/></location><location id="id49" x="0" y="64"><name x="8" y="32">MESSAGE_ON_WIRE</name></location><location id="id50" x="-64" y="-96"><name x="-48" y="-128">LISTENING</name></location><location id="id51" x="-64" y="-224"><name x="-74" y="-254">START</name><committed/></location><init ref="id51"/><transition><source ref="id48"/><target ref="id50"/></transition><transition><source ref="id49"/><target ref="id48"/></transition><transition><source ref="id50"/><target ref="id49"/></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="224"><name x="-56" y="232">MESSAGE_DELIVERED</name><committed/></location><location id="id48" x="0" y="64"><name x="8" y="32">MESSAGE_ON_WIRE</name></location><location id="id49" x="-64" y="-96"><name x="-48" y="-128">LISTENING</name></location><location id="id50" x="-64" y="-224"><name x="-74" y="-254">START</name><committed/></location><init ref="id50"/><transition><source ref="id47"/><target ref="id49"/></transition><transition><source ref="id48"/><target ref="id47"/></transition><transition><source ref="id49"/><target ref="id48"/></transition><transition><source ref="id50"/><target ref="id49"/></transition></template><system>// Place template instantiations here.
P_Ticker = Ticker();
P_ClientClock = Client_Clock();
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment