Skip to content
Snippets Groups Projects
Commit 13a0f263 authored by Kristof's avatar Kristof
Browse files

- New version 7: lots of simplification, but attack cannot be shown anymore...

- New version 7: lots of simplification, but attack cannot be shown anymore (drift never passes threshold of interval length, except if all at once)
parent 5891de98
No related branches found
No related tags found
No related merge requests found
color 0a color 0a
TimeMem-1.0 verifyta -d ../Clocks-Test-6.xml Out-of-bounds.q >> Out-of-bounds.txt TimeMem-1.0 verifyta -d ../Clocks-Test-7.xml Out-of-bounds.q >> Out-of-bounds.txt
\ No newline at end of file \ No newline at end of file
...@@ -3,4 +3,4 @@ ...@@ -3,4 +3,4 @@
/* /*
*/ */
A[] deadlock imply (P_ClientBehavior.FINISH_PROCEDURE or P_ClientBehavior.FINISH_TIMEOUT) A<> P_ClientBehavior.FINISH_PROCEDURE or P_ServerClock.FINISH or P_ServerClock.FINISH_CLOCKOUTOFBOUNDS
\ No newline at end of file \ No newline at end of file
This diff is collapsed.
//This file was generated from (Commercial) UPPAAL 4.0.12 (rev. 4561), July 2010
/*
"Does any deadlock exist?"
*/
E<> deadlock
/*
*/
A[] deadlock imply (P_ClientBehavior.FINISH_PROCEDURE or P_ClientBehavior.FINISH_TIMEOUT)
/*
*/
A<> P_ClientBehavior.FINISH_PROCEDURE or P_ServerClock.FINISH or P_ServerClock.FINISH_CLOCKOUTOFBOUNDS
/*
*/
A<> P_ClientBehavior.FINISH_PROCEDURE or P_ClientBehavior.FINISH_TIMEOUT
/*
*/
E<> P_ClientBehavior.FINISH_PROCEDURE
/*
*/
//NO_QUERY
/*
*/
E<> P_ClientBehavior.FINISH_PROCEDURE and (client_clock_counter == server_clock_counter)
/*
*/
A[] P_ClientBehavior.FINISH_PROCEDURE imply (client_clock_counter() - server_clock_counter < P_ClientBehavior.unicast_roundtrip / 2)
/*
*/
A[] P_ClientBehavior.UNICAST_FINISHED imply (client_clock_counter() - server_clock_counter < P_ClientBehavior.unicast_roundtrip / 2)
/*
*/
A[] P_ClientBehavior.BROADCAST_FINISHED imply (client_clock_counter() - server_clock_counter < P_ClientBehavior.unicast_roundtrip)
/*
*/
//NO_QUERY
/*
*/
E<> P_ClientBehavior.UNICAST_FINISHED and abs(client_clock_counter_diff) > 0
/*
*/
E<> P_ClientClockDiff.FINISH_CLOCKOUTOFBOUNDS
/*
*/
E<> abs(client_clock_counter_diff) >= bc_interval_length - 2 and P_ClientBehavior.broadcast_offset > 0
/*
*/
E<> abs(client_clock_counter_diff) >= bc_interval_length
/*
*/
E<> abs(client_clock_counter_diff) >= bc_interval_length - 2
/*
*/
E<> bc_used_counter >= broadcast_repetitions_max
/*
*/
E<> P_ClientBehavior.BROADCAST_FINISHED and broadcast_repetitions_counter == broadcast_repetitions_max-1
/*
*/
E<> P_ClientBehavior.BROADCAST_FINISHED and broadcast_repetitions_counter == 2
/*
*/
//NO_QUERY
This diff is collapsed.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment