22 lines
843 B
Plaintext
22 lines
843 B
Plaintext
ltl phi3 {
|
|
!(eventually (((always (state[0] == 2)) ||
|
|
(always (state[0] == 3)) ||
|
|
(always (state[0] == 4)) ||
|
|
(always (state[0] == 5)) ||
|
|
(always (state[0] == 6)) ||
|
|
(always (state[0] == 7)) ||
|
|
(always (state[0] == 8)) ||
|
|
(always (state[0] == 9)) ||
|
|
(always (state[0] == 10)))
|
|
&&
|
|
((always (state[1] == 2)) ||
|
|
(always (state[1] == 3)) ||
|
|
(always (state[1] == 4)) ||
|
|
(always (state[1] == 5)) ||
|
|
(always (state[1] == 6)) ||
|
|
(always (state[1] == 7)) ||
|
|
(always (state[1] == 8)) ||
|
|
(always (state[1] == 9)) ||
|
|
(always (state[1] == 10)))))
|
|
}
|