//This file was generated from (Academic) UPPAAL 4.1.4 (rev. 4771), April 2011

/*

*/
Pr[<=(TO + TDELAY + (N-1) * MAXDELAY)](<> forall (i : id_t) Node(i).leader==0)

/*

*/
Pr[<=(TO + TDELAY + (N-8) * MAXDELAY)](<> forall (i : id_t) Node(i).leader==0)

/*

*/
A[] (time >= (TO + TDELAY + (N -1)* MAXDELAY) imply ( forall (i : id_t) Node(i).leader==0) )

/*

*/
A[] (time > (TO + TDELAY + (N-1) * MAXDELAY) imply ( forall (i : id_t) Node(i).leader==0) )

/*

*/
Pr[<=(TO + TDELAY + N * MAXDELAY)/2](<> forall (i : id_t) Node(i).leader==0)

/*

*/
A[] not deadlock
