How TLA+ Evaluation Next Action
TLC是如何计算状态的
当TLC计算一个invariant,直接计算值,返回TRUE/FALSE
当TLC计算Init和Next,返回一个状态集合(这个集合被加入到sq中):
- Init: 所有可能的初始状态;
- Next:所有可能的后继状态;
TLC如何计算Next
- 状态:是对变量的赋值;
- TLC计算一个状态s的后继状态:
- 对所有unprimed变量进行赋值;
- 对所有的primed变量赋值为null;
- 开始计算next Action;
- TLC在计算Next Action和普通的表达式是不同的
第一个不同点
<p>拆分成3个子表达式:</p>
<ol>
<li>非A;</li>
<li>B;</li>
<li>C / (E i in S : D(i) / E);</li>
</ol>
<p>计算第3个表达式的过程是:</p>
<ol>
<li>计算C</li>
<li>如果C为TRUE,把后边的E i in S : D(i) / E 根据S中的元素i拆分成多个表达式D(i) / E;</li>
<li>计算D(i) / E时,应用同样的规则,先计算D(i)</li>
<li>
<p>如果D(i)为TRUE,计算E</p>
<p># 第二个不同点</p>
</li>
</ol>
如何计算primed变量
- 计算x’ = e时,首先把x’赋值为null,然后计算e的值给x’,返回TRUE;
- 计算x’ in S,等价于 E v in S : x’ = v;
- UNCHANGED«e1, … , en»,等价于 (UNCHANGED e1) / … / (UNCHANGED en)
当primed变量没有被赋值时会报错;
当一个‘与’返回FALSE,这个子表达式计算就停止了,没有找到任何状态;
当一个表达式计算完毕,就找到一些状态,这些状态就是primed变量的赋值;
一个具体的例子
/ / x' in 1..Len(y)
/ y' = Append(Tail(y), x')
/ / x' = x + 1
/ y' = Append(y, x')
- 假设Init初始化之后的状态是: x = 1, y = «2, 3»
- 由于最外层是两个‘或’,TLC把表达式拆分成两个子表达式;
- 计算第一个子表达式:x’ in 1..Len(y) / y’ = Append(Tail(y), x’) 这个表达式一个‘与’因此从左往右依次计算,由于Len(y)为2,因此,这个表达式被拆成两个:
- 第一个:
/ x' = 1
/ y' = Append(Tail(y), x')
得到x = 1, y = «3, 1»
- 第二个:
/ x' = 2
/ y' = Append(Tail(y), x')
得到x = 2, y = «3, 2»
- 计算第二个子表达式:这是一个‘与’表达式,从左往右依次计算两个
- 计算第一个x = 2
- 计算第二个y = «2, 3, 2»
- 整个Next的后继状态一共有3个。
- 假设Init初始化之后的状态是: x = 1, y = « »
- 由于最外层是两个‘或’,TLC把表达式拆分成两个子表达式;
-
计算第一个子表达式:x' in 1..Len(y) / y' = Append(Tail(y), x')
由于Len(y)为0,第一个‘与’的子表达式:
<div class="highlighter-rouge"><div class="highlight"><pre class="highlight"><code> / x' in 1..0
/ y' = Append(Tail(y), x')