unittest.smv 321 Bytes
Newer Older
FAGES Francois's avatar
FAGES Francois committed
1 2 3 4 5 6 7 8 9 10
MODULE main

VAR a: boolean;
INIT a in TRUE;
VAR b: boolean;
INIT b in {FALSE, TRUE};
VAR c: boolean;
INIT c in TRUE;

TRANS (a <-> next(a)) & (b <-> next(b)) & (c <-> next(c)) & (!a | FALSE) & (!a | !b | FALSE) | a & TRUE & next(b) & next(a) & TRUE & (c <-> next(c)) | a & b & TRUE & next(a) & next(b) & !next(c) & TRUE