//This file was generated from (Academic) UPPAAL 4.0.13 (rev. 4577), September 2010

/*

*/
A[] not deadlock

/*
For P2 in HW6
*/
A[] !rbv1.Bad

/*
P1 in HW6
*/
A[] !lbv1.Bad

/*
P4 - this property never works (regardless of the value of now)
*/
A[] now >=127 imply (lb.end && j1.idle && j2.idle)

/*
Property for P3, another version
*/
A[] ((lb.end && j1.idle && j2.idle) imply now >= 100)

/*
P3 - find the minimal amount of time for the jobs to be finished (sat'd when now >=100)
*/
E<> (lb.end && j1.idle && j2.idle)