发布于 

How TLA+ Evaluation Next Action

TLC是如何计算状态的

当TLC计算一个invariant，直接计算值，返回TRUE/FALSE 当TLC计算Init和Next，返回一个状态集合（这个集合被加入到sq中）:

  1. Init: 所有可能的初始状态；
  2. Next：所有可能的后继状态；

TLC如何计算Next

  • 状态：是对变量的赋值；
  • TLC计算一个状态s的后继状态：
    1. 对所有unprimed变量进行赋值；
    2. 对所有的primed变量赋值为null；
    3. 开始计算next Action；
  • TLC在计算Next Action和普通的表达式是不同的

第一个不同点

  • TLC对‘或’表达式并不是从左到右计算：
    • 当计算 A1 / … / An，首先拆分成n个子表达式；
    • 当计算E x in S : p，对于S中的每个元素，拆分成若干个子表达式；
    • P => Q，等价于(非P) / Q

  • 举个例子

    <div class="highlighter-rouge"><div class="highlight"><pre class="highlight"><code>  (A =&gt; B) / ( C / (E i in S : D(i) / E)) 


<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变量
  • 当primed变量没有被赋值时会报错；
  • 当一个‘与’返回FALSE，这个子表达式计算就停止了，没有找到任何状态；
  • 当一个表达式计算完毕，就找到一些状态，这些状态就是primed变量的赋值；

    • 一个具体的例子

    / / x' in 1..Len(y)
    / y' = Append(Tail(y), x')
/ / x' = x + 1
    / y' = Append(y, x')

    ​

    ​

    许可协议

    Candylab 糖果的实验室 https://lua.ren