Как перевести формулу в код TLA+

Question

Я написал спецификацию TLA+ Ханойской башни:

TEX

ASCII

------------------------------- MODULE Hanoi -------------------------------

EXTENDS Sequences, Integers
VARIABLE A, B, C


CanMove(x,y) == /\ Len(x) > 0 
                /\ IF Len(y) > 0 THEN Head(y) > Head(x) ELSE TRUE

Move(x,y,z) == /\ CanMove(x,y)
               /\ x' = Tail(x)
               /\ y' = <<Head(x)>> \o y
               /\ z' = z

Invariant == C /= <<1,2,3>>   \* When we win!                           

Init == /\ A = <<1,2,3>>
        /\ B = <<>>
        /\ C = <<>>

Next == \/ Move(A,B,C) \* Move A to B
        \/ Move(A,C,B) \* Move A to C
        \/ Move(B,A,C) \* Move B to A
        \/ Move(B,C,A) \* Move B to C
        \/ Move(C,A,B) \* Move C to A
        \/ Move(C,B,A) \* Move C to B
=============================================================================

Проверка модели TLA решит для меня загадку, когда я укажу Invariant формула как инвариант.

Я хочу сделать это немного менее многословным, хотя, в идеале, я не хочу передавать неизмененную переменную в Move(), но я не могу понять, как. Что я хочу сделать, это написать

Move(x,y) == /\ CanMove(x,y)
             /\ x' = Tail(x)
             /\ y' = <<Head(x)>> \o y
             /\ UNCHANGED (Difference of and {A,B,C} and {y,x})

Как я могу выразить это на языке TLA?

Answer 1

Вместо переменных A, B, C вы должны иметь одну последовательность, towersгде башни являются указателями. Это также имело бы преимущество в том, чтобы быть общим по количеству башен. Ваш Next формула тоже будет короче:

CanMove(i,j) == /\ Len(towers[i]) > 0 
                /\ Len(towers[j]) = 0 \/ Head(towers[j]) > Head(towers[i])

Move(i, j) == /\ CanMove(i, j)
              /\ towers' = [towers EXCEPT ![i] = Tail(@),
                                          ![j] = <<Head(towers[i])>> \o @]

Init == towers = << <<1,2,3>>, <<>>, <<>> >> \* Or something more generic

Next == \E i, j \in DOMAIN towers: i /= j /\ Move(i, j)

В качестве альтернативы, если вы хотите продолжать использовать буквы, вы можете использовать запись вместо последовательности для towersи все, что вам нужно изменить в моей предлагаемой спецификации:

Init == towers = [a |-> <<1, 2, 3>>, b |-> <<>>, c |-> <<>>]