Redundancy in states dump

[Ivanov Dmitriy]

Hello, I am new to TLA+ and is trying to play with cat puzzle:

https://github.com/tlaplus/Examples/tree/master/specifications/Moving_Cat_Puzzle

I created a little different code with hard coded initial observed_box =
2 /\ direction = "right"

I tried with a small number of boxes: 3. I don't understand is why there
are so many states in the dump:

State 1:
/\ direction = "right"
/\ cat_box = 1
/\ observed_box = 2

State 2:
/\ direction = "right"
/\ cat_box = 2
/\ observed_box = 2 <- the cat is caught

State 3:
/\ direction = "right"
/\ cat_box = 3
/\ observed_box = 2

--------------------------
State 4:
/\ direction = "left"
/\ cat_box = 2
/\ observed_box = 2 <- the cat is caught

--------------------------
State 5:
/\ direction = "right"
/\ cat_box = 1
/\ observed_box = 2<- duplicate of State 1

State 6:
/\ direction = "left"
/\ cat_box = 3
/\ observed_box = 2 <- this should be impossible, cat is already caught

State 7:
/\ direction = "left"
/\ cat_box = 1
/\ observed_box = 2 <- this should be impossible, cat is already caught

State 8:
/\ direction = "right"
/\ cat_box = 2
/\ observed_box = 2 <- duplicate of State 2

State 9:
/\ direction = "right"
/\ cat_box = 3
/\ observed_box = 2 <- duplicate of State 3

State 10:
/\ direction = "left"
/\ cat_box = 2
/\ observed_box = 2 <- duplicate of State 4

State 11:
/\ direction = "left"
/\ cat_box = 3
/\ observed_box = 2 <- this should be impossible, cat is already caught

State 12:
/\ direction = "left"
/\ cat_box = 1
/\ observed_box = 2 <- this should be impossible, cat is already caught

In reality only states 1 - 4 that are possible. How were states 5 - 12
created?

Maybe, there are not enough properties in the code and it's moving back
and forth?

[Andrew Helwer]

Hi Ivanov, thanks for the question. I took a look at the spec, and the spec with your modifications.

So fundamentally nothing in the spec stops the process once the cat has been caught. The only property of interest in the spec is a temporal property, saying that from all possible initial states, eventually the cat is caught:

Victory == <>(observed_box = cat_box)

However, the spec will continue exploring the state space after this property has been satisfied. There is no precondition on Next or any of its sub-actions to prevent the cat or observer from continuing to move around. The full state space has size |Boxes| * |Observed_Boxes| * |{"left", "right"}| = 3 * 2 * 2 = 12, which is what you see.

Andrew

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/f4b54198-e4f8-4c0e-9e7e-9197345e4bc6%40danilovplaza.org.

[Andrew Helwer]

Correction: the state cardinality is |Boxes| * |Observed_Boxes| * |{"left", "right"}| = 3 * 1 * 2 = 6, which is why you see duplicate states.