如何公式转换为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 |-> <<>>]