如何使用TLA +定义顺序动作？

问题描述

说我有一组简单的顺序动作（我将首先对它进行强制性定义）：

start(a,1)
move(a,3)
move(a,5)
move(a,4)
move(a,2)

也就是说，我们有一个游戏作品a，并从位置1开始。然后我们依次将其依次移动到3、5、4、2。每步一次。

您如何使用TLA +定义它？试图让我思考如何在TLA +中指定复杂的命令式动作序列。

解决方法

问题中概述的行为可以在TLA +中描述如下：

---- MODULE Steps ----

VARIABLE a


Init == a = 1
Next == \/ /\ a = 1
           /\ a' = 3
        \/ /\ a = 3
           /\ a' = 5
        \/ /\ a = 5
           /\ a' = 4
        \/ /\ a = 4
           /\ a' = 2

Spec == Init /\ [][Next]_a /\ WF_a(Next)

=====================

变量a的行为由时间公式Spec指定（其他变量可以以任意方式表现）。

变量a开始等于1（通过合取Init），并且时间步长将a保持不变，或者将其从1更改为3。发生时，随后的时间步长将a保持不变，或将其从3更改为5。对a的值更改可能会持续到a等于2。 1}}是不可能的。一旦a等于2，它将永远等于2。这些是a的可能变化，如联合a所指定，这意味着[][Next]_a，即， [](Next \/ UNCHANGED a)，符号[](Next \/ (a' = a))表示“始终”。

联合[]和Init指定安全属性。安全是指可能发生的事情，而不是必须发生的事情。活泼（必须发生的事情）由连接[][Next]_a指定，它描述了较弱的公平性。公式WF_a(Next)要求，如果满足公式WF_a(Next) 和的步骤更改了变量Next的值，则必须不间断地启用，那么这样的步骤必须最终发生。

换句话说，如果可以通过执行满足a的步骤（a步骤）来更改变量Next，则<<Next>>_a不能永远保留不变，但最终必须以a描述的方式进行更改。实际上，虽然Next不是2，而是1，3、5或4，但动作a（即<<Next>>_a，即Next /\ (a' # a)和Next启用了更改值），因此a会不断更改，直到达到值2。a为2时，a被禁用。

有很多方法可以做到这一点，但是这里有两个简单的解决方案值得考虑：第一个使用宏：

---- MODULE Steps ----

VARIABLE a

move(start,end) ==
    /\ a = start
    /\ a' = end

Init ==
    /\ a = 1

Next == 
    \/ move(1,3)
    \/ move(3,5)
    \/ move(5,4)
    \/ move(4,2)

Spec ==
    /\ Init
    /\ [][Next]_a

=====================

请注意，上述操作仅在您的移动顺序未返回相同状态时才有效。如果确实如此，则必须添加类似pc“程序计数器”变量，序列和yada yada yada的内容……此时，最好使用PlusCal（一种TLA +变体），更适合编写顺序操作：

---- MODULE Steps ----

(* --algorithm Steps
variables a = 1;
begin
    a := 3;
    a := 5;
    a := 4;
    a := 2;
end algorithm; *)

=====================

必须先将其翻译为TLA +，然后才能由TLC运行。使用

CTRL+T在TLA +工具箱中
Parse module命令
java pcal.trans Steps.tla和CLI

function function function specifications tla+