# Train example
Declaration : D1
[ X = ( (train1:ON v train2:ON) => gate:CLOSE) ^ [App] X ^ [Exit] X ^
[GoDown] X ^ [GoUp] X ^ [a] X ^ [@] X
];
F1 := (X,D1);
# F1 is the specification defined by the formula X w.r.t. the declaration D1
Declaration : D2
[ X = [Exit] z in Y ^ [App] X ^ [Exit] X ^ [GoDown] X ^
[GoUp] X ^ [a] X ^ [@] X ;
Y = (gate:OPEN ^ X) v ( z<70 ^ [App] X ^ [a] Y ^ [Exit] z in Y ^
[GoUp] Y ^ [GoDown] Y ^ [@] Y)
];
F2 := (X,D2);
# F2 is the specification defined by the formula X w.r.t. the declaration D2
Declaration : D3
[ X = ( tt => tt) ^ [App] X ^ [Exit] X ^ [GoDown] X ^
[GoUp] X ^ [a] X ^ [@] X ];
F3 := (X,D3);
# F3 is the specification defined by the formula X w.r.t. the declaration D3
Declaration : Dlive2
[ X = [Exit] z in Y ^ [App] X ^ [Exit] X ^ [GoDown] X ^
[GoUp] X ^ [a] X ^ [@] X ;
Y = gate:OPEN v ( z<65 ^ [a] Y ^ [Exit] Y ^ [GoUp] Y ^ [GoDown] Y ^ [@] Y)
];
Declaration : Dlive3
[ X = [Exit] z in Y ^ [App] X ^ [Exit] X ^ [GoDown] X ^
[GoUp] X ^ [a] X ^ [@] X ;
Y = gate:OPEN v ( z<69 ^ [a] Y ^ [Exit] Y ^ [GoUp] Y ^ [GoDown] Y ^ [@] Y)
];
Declaration : Dl
[ X = <@> Y ^ [App] X ^ [Exit] X ^ [GoDown] X ^
[GoUp] X ^ [a] X ^ [@] X ;
Y = * tt v tt v tt v tt v tt
];
# Verification of P1, P2 and P3
# Verify(F1,S,T);
# Verify(F2,S,T);
# Verify(F3,S,T);
# See the user-guide to get informations about the meaning of the
# results provided by the program.
*