25 lines
678 B
Plaintext
25 lines
678 B
Plaintext
MODULE main
|
|
-- Model of the switch
|
|
IVAR
|
|
press : boolean;
|
|
VAR
|
|
mode : {on, off};
|
|
x : 0..15;
|
|
ASSIGN
|
|
init(mode) := off;
|
|
next(mode) := case
|
|
mode = off & press : on;
|
|
mode = on & (press | x >= 10) : off;
|
|
TRUE : mode;
|
|
esac;
|
|
init(x) := 0;
|
|
next(x) := case
|
|
mode = on & next(mode) = off : 0;
|
|
mode = on & x < 10 : x + 1;
|
|
TRUE : x;
|
|
esac;
|
|
|
|
INVARSPEC x <= 10;
|
|
INVARSPEC mode = off -> x = 0;
|
|
INVARSPEC x < 10;
|
|
INVARSPEC mode = off; |