9 lines
115 B
Plaintext
9 lines
115 B
Plaintext
|
MODULE e
|
||
|
|
VAR
|
||
|
|
e : { e };
|
||
|
|
ASSIGN
|
||
|
|
init(e) := e;
|
||
|
|
next(e) := e;
|
||
|
|
esac;
|
||
|
|
SPEC AG ( TRUE -> AF e = e)
|