//This file was generated from (Commercial) UPPAAL 4.1.1 (rev. 4172), December 2008 /* ===== Validation Properties: */ //NO_QUERY /* Train 1 can reach crossing. */ E<> train(1).Cross /* 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) /* Train 0 can be crossing bridge while Train 1 is waiting to cross. */ E<> train(0).Cross and train(1).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 /* ===== Deadlock checking: */ //NO_QUERY /* The system is deadlock-free. */ A[] not deadlock