Hello everyone,
I`m making first steps with TLA and wrote a simple program, supposed to find some numbers with the given logic (i.e. x1 > x2, x = 5). I did setup it in such way: each step it expects 'random' value in variables the way numbers are choosen supposed to be improved later. The problem is: when (in next) I do set p3' \in 0..100 model checker answers that invariant is violated even before the init step. but when i do set something like p3' = 0 - it works. Program works with two variables without problems. Can you please help me? Seems question is trivial, but still not clear to me :(. here is my code:
EXTENDS Naturals
VARIABLES p1, p2, p3
TypeOK == /\ p1 \in 0..100
/\ p2 \in 0..100
/\ p3 \in 0..100
Init == /\ p1 = 0
/\ p2 = 0
/\ p3 = 0
x1 == /\ p1' \in 0..100
/\ p2' \in 0..100
/\ p3' \in 0..100
Next == x1
Spec == Init /\ [][Next]_<<p1, p2, p3>>
NotSolved == ~( /\ p1 > p2 + 10
/\ p2 = 10)