[SOLVED] invariant is violated while the variable is it not used in it

invariant is violated while the variable is it not used in it

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 problem is: when (in next) I do set p3' \in 0..100 program answers that invariant is violated. but when i do set something like p3' = 0 - it works. Program works with two variables without problems. Seems question is trivial, but still not clear to me :(. here is my test:

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)

Solution

Here are two things that both fix the spec:

writing p3' \in 0..97 instead of 0..100
adding the flag -maxSetSize 1030301. -maxSetSize 1030300 does not work.

Given this behavior, my best hypothesis is that TLC doesn't like it when a state generates more next states than can fit into maxSetSize. By default the maxSetSize is 1 million. Without p3, p1' and p2' combinatorically generate 10201 states; floor(1e6 / 10201) = 98 = Cardinality(0..97).