16 lines
214 B
Text
16 lines
214 B
Text
---- MODULE topics2_constraint ----
|
|
EXTENDS Naturals
|
|
|
|
VARIABLES x, y
|
|
|
|
Init == /\ x = 0
|
|
/\ y = 0
|
|
|
|
Inv == x = y /\ x < 10
|
|
|
|
Next == /\ x' = x + 1
|
|
/\ y' = y + 1
|
|
|
|
Spec == Init /\ [][Next]_<<x, y>>
|
|
|
|
====
|