通过here查看主要显示动作规范的简单示例,其中您使用'
引用下一个状态,如:
UponV1(self) ==
/\ pc[self] = "V1"
/\ pc' = [pc EXCEPT ![self] = "AC"]
/\ sent' = sent \cup { <<self, "ECHO">> }
/\ nCrashed' = nCrashed
/\ Corr' = Corr
例如,/\ nCrashed' = nCrashed
是一个逻辑语句,说“...... AND next(nCrashed)== this(nCrashed)`。所以基本上,上面的函数设置了一些变量”在下一个状态“。但所有这一切都在一步中发生基本上(逻辑上至少)。
我想知道的是如何定义在多个步骤中发生的事情。说10个步骤。
UpdateWithTenSteps(self) ==
/\ foo' = foo + 1
/\ bar'' = foo' + 1
/\ baz''' = bar'' + 1
/\ ...
....
因此,“在现在的第三个状态中,巴兹将在第二个州加上一个。”这样的事情。但这并没有多大意义。在命令式语言中,您只需执行以下操作:
function updateInTenSteps() {
incFoo()
incBar()
incBaz()
}
但这是有道理的,因为每个函数调用都发生在之前。但我不知道如何在TLA +中代表这一点。
想知道你应该如何完成在Temporal Logic of Actions +中采取不止一步的事情。另一个例子是while循环。
TLA的设计只考虑当前状态和后继状态(或整个行为)。您总是可以通过引入一个显式变量来分割相互依赖的多个步骤,该变量可以告诉您已经完成了哪些分配:
EXTENDS Naturals
Labels == { "foo", "bar", "baz", "fin" } (* just for documentation purposes *)
VARIABLE currstate, foo, baz, bar
Init == /\ currstate = "foo"
/\ foo = 0
/\ bar = 0
/\ baz = 0
Next == \/ (currstate = "foo" /\ currstate' = "bar" /\ foo' = foo +1 /\ UNCHANGED <<bar,baz>>)
\/ (currstate = "bar" /\ currstate' = "baz" /\ bar' = foo +1 /\ UNCHANGED <<foo,baz>>)
\/ (currstate = "baz" /\ currstate' = "fin" /\ baz' = bar +1 /\ UNCHANGED <<foo,bar>>)
\/ (currstate = "fin" /\ UNCHANGED <<foo,bar,baz,currstate>>
如果你为此创建一个模型,设置Init
和Next
定义的行为,然后检查不变的baz = 0
,你会得到一个跟踪信息,显示导致baz更改的状态(你的最后一个任务)。循环只是将后继标签指定为已经发生的标签(例如,而不是定义baz' = "foo"
)。
对TLA的Pluscal转换类似地工作:每个标记的行对应于id,并且从行l到行m的每次转换将在下一状态中将程序计数器从l改变为m。