如何公式轉換爲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 
============================================================================= 

當我指定0123時，TLA模型檢查器將爲我解決難題公式作爲不變量。

雖然我想盡量減少冗餘，理想情況下我不想將未更改的變量傳遞給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 |-> <<>>]