//This file was generated from (Academic) UPPAAL 4.1.4 (rev. 4854), July 2011

/*

*/
E[ <= 100; 20000](max: sum(i:id_t) Train(i).Stop)

/*

*/
Pr[ <= 100](<> Train(0).Cross)

/*

*/
Pr[ <= 100](<> Train(1).Cross)

/*

*/
Pr[ <= 100](<> Train(2).Cross)

/*

*/
Pr[ <= 100](<> Train(3).Cross)

/*

*/
Pr[ <= 100](<> Train(4).Cross)

/*

*/
Pr[ <= 100](<> Train(5).Cross)

/*

*/
Pr[ <= 100](<> Train(0).Cross and (forall (i : id_t) i != 0 imply Train(i).Stop))

/*

*/
Pr[ <= 100](<> Train(1).Cross and (forall (i : id_t) i != 1 imply Train(i).Stop))

/*

*/
Pr[ <= 100](<> Train(2).Cross and (forall (i : id_t) i != 2 imply Train(i).Stop))

/*

*/
Pr[ <= 100](<> Train(3).Cross and (forall (i : id_t) i != 3 imply Train(i).Stop))

/*

*/
Pr[ <= 100](<> Train(4).Cross and (forall (i : id_t) i != 4 imply Train(i).Stop))

/*

*/
Pr[ <= 100](<> Train(5).Cross and (forall (i : id_t) i != 5 imply Train(i).Stop))

/*

*/
Pr[ <= 600](<> Train(1).Cross and (forall (i : id_t) i != 1 imply Train(i).Stop)) >=\
Pr[ <= 600](<> Train(5).Cross and (forall (i : id_t) i != 5 imply Train(i).Stop))

/*

*/
Pr[# <= 20]([] forall (i : id_t) forall (j : id_t) Train(i).Cross && Train(j).Cross imply i == j) >= 0.98

/*
===== Validation Properties:
*/
//NO_QUERY

/*
Gate can receive (and store in queue) msg's from approaching trains.
*/
E<> Gate.Occ

/*
Train 0 can reach crossing.
*/
E<> Train(0).Cross

/*
Train 1 can reach crossing.
*/
E<> Train(1).Cross

/*
Train 0 can be crossing bridge while Train 1 is waiting to cross.
*/
E<> Train(0).Cross and Train(1).Stop

/*
Train 0 can cross bridge while the other trains are waiting to cross.
*/
E<> Train(0).Cross and (forall (i : id_t) i != 0 imply Train(i).Stop)

/*
===== Safety Properties:
*/
//NO_QUERY

/*
There is never more than one train crossing the bridge (at
any time instance).
*/
A[] forall (i : id_t) forall (j : id_t) Train(i).Cross && Train(j).Cross imply i == j

/*
There can never be N elements in the queue (thus the array will not overflow).
*/
A[] Gate.list[N] == 0

/*
===== Liveness Properties:
*/
//NO_QUERY

/*
Whenever a train approaches the bridge, it will eventually cross.
*/
Train(0).Appr --> Train(0).Cross

/*

*/
Train(1).Appr --> Train(1).Cross

/*

*/
Train(2).Appr --> Train(2).Cross

/*

*/
Train(3).Appr --> Train(3).Cross

/*

*/
Train(4).Appr --> Train(4).Cross

/*

*/
Train(5).Appr --> Train(5).Cross
