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

Question

假设我有一组简单的顺序操作（我将首先命令式定义）：

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

也就是说，我们有一个棋子 a 并从位置 1 开始。然后我们依次将它移动到 3，然后是 5，然后是 4，然后是 2。每一步一次。

您如何使用 TLA+ 定义它？试图围绕如何在 TLA+ 中指定复杂的 命令动作序列 。

Answer 1

问题中描述的行为可以用 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。进一步更改为a 是不可能的。一旦 a 等于 2，它就永远等于 2。这些是 a 的可能变化，由连词 [][Next]_a 指定，即 [](Next \/ UNCHANGED a)，即， [](Next \/ (a' = a))，符号[]表示“永远”。

连词 Init 和 [][Next]_a 指定安全属性。安全是关于可能发生的事情，而不是必须发生的事情。 Liveness（必须发生的事情）用连词 WF_a(Next) 指定，它描述了弱公平性。公式WF_a(Next)要求如果一个步骤满足公式Next和改变变量a的值是enabled不间断，那么最终必然会出现这样的步骤。

换句话说，如果可以通过满足Next（<<Next>>_a步）的步骤来改变变量a，那么a就不能永远保持不变，但最终必须以 Next 描述的方式改变。实际上，虽然 a 不是 2，而是 1、3、5 或 4，但操作 <<Next>>_a（表示 Next /\ (a' # a)，即 Next 和 a更改值）已启用，因此 a 将一直更改，直到达到值 2。当 a 为 2 时，<<Next>>_a 将被禁用。

Answer 2

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

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

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

请注意，只有当您的一系列移动未 return 达到相同状态时，以上内容才有效。如果是这样，您将不得不添加类似 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 VS Code 扩展中的命令
java pcal.trans Steps.tla 与 CLI

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

How to use TLA+ to define sequential actions?

specifications

function

tla+