SPIN：无限频繁地访问语句答案

【问题标题】：SPIN: Visit statements infinitely oftenSPIN：无限频繁地访问语句
【发布时间】：2013-10-03 10:56:15
【问题描述】：

我想知道是否可以在具有公平约束的程序中验证 LTL 属性，该公平约束规定必须无限频繁地执行多个语句。

例如：

bool no_flip;
bool flag;

active[1] proctype node()
{
  do
  :: skip -> progress00: no_flip = 1
  :: skip -> progress01: flag = 1
  :: !no_flip -> flag = 0
  od;
}

// eventually we have flag==1 forever
ltl p0  { <> ([] (flag == 1)) }

如果no_flip 标志最终变为真并且 flag 变为真，则此程序是正确的。

但是，同时运行 'pan -a' 和 'pan -a -f'（弱公平性）会产生一个循环通过 no_flip=1 语句和接受状态（来自 LTL 公式）。

我认为进度标签会强制执行无限频繁地通过它们，但情况似乎并非如此。那么，是否可以添加这种公平约束？

谢谢，努诺

【问题讨论】：

标签： spin promela

【解决方案1】：

仅包含进度标签本身并不能保证执行将仅限于非进度案例。您需要在 ltl 或 never 声明中的某处添加“非进度”。

作为never 声明，您使用<>[](np_) 强制执行进度（使用spin -p '<>[](np_)' 生成从不声明本身）。用于验证的可能ltl 表单是：

ltl { []<>!(np_) && <>[](flag==1) }

还要注意，取得“进步”并不意味着无限频繁地访问每个进度标签；这意味着无限频繁地访问 any 进度标签。因此，在执行进度时，通过代码的可行路径是第一个 do 选项 - 这不是您所期望的。

【讨论】：

感谢您的回答。不幸的是，我没有完全理解你的意思。我认为我不能将 LTL 公式直接写入从不声明中。你能展示你如何用公平约束来扩展上面的例子吗？谢谢！
我更新了我的答案。运行您的示例仍然会导致违规 - 我已在“注释”中解释过
我明白了，谢谢！那么，有什么常规技巧可以解决这个 np_ 问题吗？我认为可能有人可以重写程序以使其“工作”（即，以某种方式将自旋限制为公平调度）。

【解决方案2】：

回答我自己的问题，对于这个简单的示例，我可以将每个循环分支拆分为单独的进程。然后通过在弱公平模式下运行 pan，我保证每个进程最终都会被调度。但是，这个“解决方案”对我的案例来说并不是很有趣，因为我有一个模型，每个流程都有几十个分支。还有其他想法吗？

bool no_flip;
bool flag;

active[1] proctype n1()
{
  do
  :: skip -> no_flip = 1
  od;
}

active[1] proctype n2()
{
  do
  :: skip -> flag = 1
  od;
}

active[1] proctype n3()
{
  do
  :: !no_flip -> flag = 0
  od;
}

// eventually we have flag==1 forever
ltl p0  { <>[] (flag == 1) }

【讨论】：