私はハノイの問題のタワーの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 Modelチェッカーが私のパズルを解決します不変式としての式。

私はそれを少し冗長にしたいと思っていますが、理想的には変更されていない変数を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 |-> <<>>]