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

/*
The most basic property is freedom from deadlocks

*/
A[] not deadlock

/*
Nodes should be synchronised halfway the duration of a slot, since at this time they will send and receive information. Prove for each pair (i, j) of first-order neighbours

*/
A[] forall(i: nodeid_t) forall(j: nodeid_t) (Node(i).t==1 imply Node(j).t==1)

/*
Eventually node 0 and 1 allocate different slots? Answer: yes
*/
A<> (slot_no[0]!=slot_no[1] and slot_no[0]>=0 and slot_no[1]>=0)

/*
Eventually node 0 and 2 allocate different slots? Answer: yes
*/
A<> (slot_no[0]!=slot_no[2] and slot_no[0]>=0 and slot_no[2]>=0)

/*
Eventually node 0 and 3 allocate different slots? Answer: NO (strange)
*/
A<> (slot_no[0]!=slot_no[3] and slot_no[0]>=0 and slot_no[3]>=0)

/*
Eventually node 1 and 2 allocate different slots? Answer: NO (strange)
*/
A<> (slot_no[1]!=slot_no[2] and slot_no[1]>=0 and slot_no[2]>=0)

/*
Eventually node 1 and 3 allocate different slots? Answer: NO (strange)
*/
A<> (slot_no[1]!=slot_no[3] and slot_no[1]>=0 and slot_no[3]>=0)

/*
Eventually node 2 and 3 allocate different slots? Answer: NO (maybe OK)
*/
A<> (slot_no[2]!=slot_no[3] and slot_no[2]>=0 and slot_no[3]>=0)

/*
Eventually all nodes allocate different slots? Answer: NO (strange)
*/
A<> forall(i: nodeid_t) forall(j: nodeid_t) (i==j || (slot_no[i]>=0 && slot_no[j]>=0 && slot_no[i]!=slot_no[j]))

/*

*/
sup: Node(0).detected, Node(1).detected, Node(2).detected, Node(3).detected

/*

*/
E<> exists(i:nodeid_t) Node(i).detected>=0

/*
SMC says that the model violates independent progress in this particular state (probably bug, but very hard to reproduce)
*/
E<> Node(0).listening && Node(1).ready && Node(2).rec_one && Node(3).listening &&\
aux_node==0 && aux_slot==-1 && \
first[0][0]==0 && first[0][1]==0 && first[0][2]==0 && first[0][3]==0 && first[0][4]==0 && \
first[1][0]==1 && first[1][1]==0 && first[1][2]==1 && first[1][3]==0 && first[1][4]==0 && \
first[2][0]==1 && first[2][1]==0 && first[2][2]==0 && first[2][3]==0 && first[2][4]==0 && \
first[3][0]==0 && first[3][1]==0 && first[3][2]==0 && first[3][3]==0 && first[3][4]==0 && \
second[0][0]==0 && second[0][1]==0 && second[0][2]==0 && second[0][3]==0 && second[0][4]==0 && \
second[1][0]==0 && second[1][1]==0 && second[1][2]==0 && second[1][3]==0 && second[1][4]==0 && \
second[2][0]==0 && second[2][1]==0 && second[2][2]==0 && second[2][3]==0 && second[2][4]==0 && \
second[3][0]==0 && second[3][1]==0 && second[3][2]==0 && second[3][3]==0 && second[3][4]==0 && \
slot_no[0]==0 && slot_no[1]==1 && slot_no[2]==3 && slot_no[3]==2 && \
Node(0).counter==0 && Node(0).curr==1 && Node(0).detected==-1 && Node(0).col==-1 && \
Node(0).aux_vec[0]==0 && Node(0).aux_vec[1]==0 && Node(0).aux_vec[2]==0 && Node(0).aux_vec[3]==0 && Node(0).aux_vec[4]==0 && \
Node(0).rec_vec[0]==0 && Node(0).rec_vec[1]==0 && Node(0).rec_vec[2]==0 && Node(0).rec_vec[3]==0 && Node(0).rec_vec[4]==0 && \
Node(0).got_info==0 && Node(0).sent_info==1 && \
Node(1).counter==4 && Node(1).curr==1 && Node(1).detected==-1 && Node(1).col==-1 && \
Node(1).aux_vec[0]==0 && Node(1).aux_vec[1]==0 && Node(1).aux_vec[2]==0 && Node(1).aux_vec[3]==0 && Node(1).aux_vec[4]==0 && \
Node(1).rec_vec[0]==0 && Node(1).rec_vec[1]==0 && Node(1).rec_vec[2]==0 && Node(1).rec_vec[3]==0 && Node(1).rec_vec[4]==0 && \
Node(1).got_info==0 && Node(1).sent_info==1 && Node(2).counter==4 && Node(2).curr==0 && Node(2).detected==-1 && Node(2).col==-1 && \
Node(2).aux_vec[0]==0 && Node(2).aux_vec[1]==0 && Node(2).aux_vec[2]==0 && Node(2).aux_vec[3]==0 && Node(2).aux_vec[4]==0 && \
Node(2).rec_vec[0]==0 && Node(2).rec_vec[1]==0 && Node(2).rec_vec[2]==0 && Node(2).rec_vec[3]==0 && Node(2).rec_vec[4]==0 && \
Node(2).got_info==0 && Node(2).sent_info==1 && Node(3).counter==4 && \
Node(3).curr==0 && Node(3).detected==-1 && Node(3).col==-1 && \
Node(3).aux_vec[0]==0 && Node(3).aux_vec[1]==0 && Node(3).aux_vec[2]==0 && Node(3).aux_vec[3]==0 && Node(3).aux_vec[4]==0 && \
Node(3).rec_vec[0]==0 && Node(3).rec_vec[1]==0 && Node(3).rec_vec[2]==0 && Node(3).rec_vec[3]==0 && Node(3).rec_vec[4]==0 && \
Node(3).got_info==0 && Node(3).sent_info==1 

/*

*/
Pr[<=100] (<> exists(i:nodeid_t) Node(i).detected>=0)
