Fixing IsSensical() in hanoi example [Models->Constants]

[vlebedev]

The implementation of IsSensical() assumption given in "Models->Constants" section won't catch the problem with TSPACES <- 3, TSIZE <- 3, SOLUTION <- <<<<1,2>>, <<>>, <<3,4>>>> which is the example you are discussing in this section.

So, instead of:

IsSensical(state) == /\ Len(state) = TSPACES \* Correct spaces
                     /\ \A n \in 1..TSIZE : \* All numbers appear
                        \E tower \in DOMAIN state:
                            \E disc \in DOMAIN state[tower]:
                                n = state[tower][disc] 

it's better to use the following:

  IsSensical(state) ==  /\ Len(state) = TSPACES \* Correct spaces
                        /\ \A tower \in DOMAIN state: \* Numbers do not exceed TSIZE
                            \A disc \in DOMAIN state[tower]:
                                state[tower][disc] \in 1..TSIZE
                        /\ \A n \in 1..TSIZE : \* All numbers appear
                            \E tower \in DOMAIN state:
                                \E disc \in DOMAIN state[tower]:
                                    n = state[tower][disc] 

[hwayne]

Haven't tried but ACKing the issue

[hwayne]

Yup, you're correct, fixing the issue now

[hwayne]

Fixed in 31b6232.