16 lines
211 B
Text
16 lines
211 B
Text
---- MODULE topics2_alias ----
|
|
EXTENDS Integers
|
|
|
|
VARIABLE x
|
|
Init == x = 0
|
|
|
|
Next == x' = x + 1
|
|
Inv == x < 10
|
|
Spec == Init /\ [][Next]_x
|
|
|
|
Alias == [
|
|
x |-> x,
|
|
xnext |-> x',
|
|
twice |-> x' = 2 * x
|
|
]
|
|
=====
|