-
Notifications
You must be signed in to change notification settings - Fork 5
/
clock.ltl
11 lines (11 loc) · 661 Bytes
/
clock.ltl
1
2
3
4
5
6
7
8
9
10
11
G((!event(T) || action(z5)) && (!action(z5) || event(T)))
G((!event(H) || (action(z1) || action(z3))) && (!(action(z1) || action(z3)) || event(H)))
!F(action(z1) && action(z3))
G((!event(M) || (action(z2) || action(z4))) && (!(action(z2) || action(z4)) || event(M)))
!F(action(z2) && action(z4))
G(!(event(A) && action(z7)) || X(R(event(A), !action(z3) && !action(z4))))
G(!(action(z3) || action(z4)) || X(R(event(A), !action(z6) && !action(z7))))
G(!(action(z1) || action(z2)) || X(R(event(A), !action(z3) && !action(z4))))
G(!(action(z3) || action(z4)) || X(R(event(A), !action(z1) && !action(z2))))
!F(action(z6) && action(z7))
F(!(event(A) && !action(z7)))