Wie Formel in TLA + Code übersetzen

Question

ich eine TLA + spec der Türme von Hanoi Problem geschrieben haben:

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 
============================================================================= 

Der TLA Model Checker wird das Rätsel für mich lösen, wenn ich denspezifiziereFormel als Invariante.

Ich möchte es aber ein bisschen weniger ausführlich machen, idealerweise möchte ich nicht die unveränderte Variable an Move() übergeben, aber ich kann nicht herausfinden, wie. Was ich tun möchte, ist zu schreiben

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

Wie kann ich das in der Sprache TLA ausdrücken?

Answer 1

Anstelle der Variablen A, B, C sollten Sie eine einzige Sequenz haben, towers, wobei die Türme Indizes sind. Dies hätte auch den Vorteil, in der Anzahl der Türme generisch zu sein. Ihre Next Formel wäre kürzer, auch:

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) 

Alternativ, wenn Sie mit Buchstaben fortsetzen möchten, können Sie einen Datensatz anstelle einer Sequenz für towers verwenden, und alles, was Sie brauchen in mir vorgeschlagenen Spezifikation zu ändern:

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