[tlaplus] Redundancy in states dump

[Ivanov Dmitriy <dima@xxxxxxxxxxxxxxxx>]

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?

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/f4b54198-e4f8-4c0e-9e7e-9197345e4bc6%40danilovplaza.org.

You have N boxes numbered 1 to N, arranged on a line. A cat is hiding
in one of the boxes. Every night, she moves to an adjacent box, and
every morning, you have one chance to inspect a box to find her. How
do you find the cat?

Solution: You start at box 2 and move one by one to N - 1. Then you
observe N - 1 again and start moving back to box 2. Repeat and
eventually you will find the cat. E.g with 5 boxes you check 2, 3, 4,
4, 3, 2; with 4 boxes you check 2, 3, 3, 2.

There is a simpler solution if the number of boxes is odd. The
solution here works in both even and odd cases.

The puzzle is trivial / impossible for a single box, since the cat
cannot move.

---- MODULE Cat ----

EXTENDS Naturals

CONSTANTS
  Number_Of_Boxes

ASSUME Number_Of_Boxes >= 2

VARIABLES
  \* The box the cat is currently hiding in
  cat_box,

  \* The box that is observed
  observed_box,

  \* The direction in which our search is progressing
  direction

vars == <<cat_box, observed_box, direction>>

----------------------------------------------------------------------

Directions == {"left", "right"}

Boxes == 1 .. Number_Of_Boxes

Observed_Boxes == 2 .. Number_Of_Boxes - 1

----------------------------------------------------------------------

\* Initially the cat is in an arbitrary box. We start our search
\* anywhere in the pattern described by the solution.
Init ==
  /\ cat_box \in Boxes
  /\ observed_box = 2
  /\ direction = "right"

\* The action performed by the cat: she either moves left or
\* right. There is no wrap-around.
Move_Cat ==
  /\ \/ cat_box' = cat_box + 1
     \/ cat_box' = cat_box - 1
  /\ cat_box' \in Boxes

\* The action performed by us: we observe boxes one by one. If we hit
\* the end of our search we reverse direction. For N boxes, we
\* alternate between 2 and N - 1.
Observe_Box ==
  LET next_box == IF direction = "right"
                  THEN observed_box + 1
                  ELSE observed_box - 1
  IN \/ /\ next_box \in Observed_Boxes
        /\ observed_box' = next_box
        /\ UNCHANGED direction
     \/ /\ next_box \notin Observed_Boxes
        /\ direction' = CHOOSE d \in Directions: d /= direction
        /\ UNCHANGED observed_box

\* Each step both the cat moves, and we make a choice on where to
\* look. Note that while in the puzzle description these things happen
\* one after the other, in the spec here there is no need. We can do
\* both at the same time.
Next ==
  /\ Move_Cat
  /\ Observe_Box

Spec ==
  /\ Init
  /\ [][Next]_vars

  \* The cat must always make a move, it is not allowed to sit
  \* still. Note that we could also apply weak fairness directly to
  \* Next, but this seems more precise to me.
  (* Weak Fairness - слабая справедливость *)
  /\ WF_cat_box(Move_Cat)

----------------------------------------------------------------------

\* The game ends if the cat is in the observed box. With the above
\* algorithm, this will eventually happen.
Victory == <>(observed_box = cat_box)

----------------------------------------------------------------------

TypeOK ==
  /\ cat_box \in Boxes
  /\ observed_box \in Observed_Boxes
  /\ direction \in Directions

====

CONSTANTS
  Number_Of_Boxes = 3

SPECIFICATION Spec

(* Предикат, который должен быть истинен во всех возможных мирах *)
INVARIANT TypeOK

(* Указание предиката, который должен быть проверен на истиность *)
(* Если он истинен, модель считается корректной *)
PROPERTY Victory