0

我想知道是否可以在具有公平约束的程序中验证 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 公式）之间产生一个循环。

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

谢谢，努诺

4

2 回答 2

2

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

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

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

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

于 2013-10-14T22:40:31.180 回答
0

回答我自己的问题，对于这个简单的示例，我可以将每个循环分支拆分为单独的进程。然后通过在弱公平模式下运行 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) }
于 2013-10-16T13:59:02.580 回答