2

我有一个关于 nuXmv 解决方案的问题。我有一个简单的图表，其中初始状态是 s1，并且从 s1 有两条弧线，一条通往 s2，另一条通往 s3。从 s2 和 s3 有一条弧线通向 s1。这是 nuXmv 中描述情况的程序。

MODULE main
VAR
    s : {s1, s2, s3};  
    p : boolean;
    q : boolean;
    w : boolean;
ASSIGN 
    init(s) := {s1};
    next(s) := case 
        s = s1 : {s2, s3}; 
        s = s2 : s1;
        s = s3 : s1;
    esac;
    p := case 
        s = s2 : TRUE;
        TRUE : FALSE; 
    esac;
    q := case
        s = s1 : TRUE;  
        TRUE : FALSE; 
    esac;
    w := case
       s = s3 : TRUE;
        TRUE : FALSE;
    esac;
CTLSPEC (AF p) & (AF w);
CTLSPEC AG (AF p) & AG (AF w);

我不明白已经处于初始状态 s1 的 nuXmv 如何知道公式是错误的。它没有给出基于循环的反例，只是在 s1 中立即说基于 s1 的公式是错误的。我的解释是，如果没有正义假设，nuXmv 会立即假设其中一条路径永远不会被执行。但它不应该以循环为例吗？如果我只留下“CTLSPEC AF p;” nuXmv 返回一个循环作为反例。那么为什么对于“AF p & AF w”它只显示状态 s1 作为反例呢？

-- specification (AF p & AF w)  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
  -> State: 1.1 <-
    s = s1
    p = FALSE
    q = TRUE
    w = FALSE
4

0 回答 0