promela - 在这个 promela 模型中，从不声称验证了什么

Question

bool p = true;

active proctype q() {
  do
    :: p=false; p=true; p=false
  od
}

never {
do
  :: !p -> goto acceptRun
  :: else -> skip; skip
od;
acceptRun : skip

}

在这个 promela 模型中，never 声明验证最初并且然后在每个第二时间步 p 成立。为什么？谢谢！

Answer 1

从未声明在模型的每一步中都采取了一步。因此，如果!p下一步将是接受状态（永远不会索赔失败）。但是，如果p这样，never 声明将需要两个添加步骤才能返回p再次检查。

虽然声明不是“寻找p”，但您可以“潜入”一些其他价值p。