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

【问题标题】：what does the never claim verify in this promela model在这个 promela 模型中，从不声称验证了什么
【发布时间】：2013-12-28 12:51:03
【问题描述】：

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 模型中，从不声明首先验证了 p 成立，然后在每第二个时间步 p 成立。为什么？谢谢！

【问题讨论】：

标签： promela

【解决方案1】：

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

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

【讨论】：