如何在 NuSMV 中创建一个简单的 Kripke 模型？答案

【问题标题】：How to create a simple Kripke model in NuSMV?如何在 NuSMV 中创建一个简单的 Kripke 模型？
【发布时间】：2014-04-05 17:18:27
【问题描述】：

我目前正在做一些LTL（线性时间逻辑）和CTL（计算树逻辑）的理论研究。我是 NuSMV 的新手，我很难创建一个简单的 Kripke 结构。

我的结构是 M = (S, R, L) 其中 S = {s0, s1, s2} 是可能状态的集合，R 是一个转换关系，使得：s0 -> s1, s0 -> s2, s1 -> s0, s1 -> s2, and s2 -> s2, L是每个状态的标记函数，定义为：L(s0) = {p, q}, L(s1) = {q, r},和 L(s2) = {r}。我正在使用 Huth 和 Ryan 在计算机科学教科书中的逻辑中描述的符号。我尝试了以下两个代码：

第一个代码：

MODULE main
VAR
    p : boolean;
    q : boolean;
    r : boolean;
    state : {s0, s1, s2};

ASSIGN
    init(state) := s0;
    next(state) := 
        case
            state = s0          : {s1, s2};
            state = s1          : {s2};
            state = s2          : {s2};
        esac;

    init(p) := TRUE; 
    init(q) := TRUE;
    init(r) := FALSE;

    next(p) :=
        case
            state = s1 | state = s2     : FALSE;
        esac;
    next(q) :=
        case
            state = s1                  : TRUE;
            state = s2                  : FALSE;
        esac;
    next(r) :=
        case
            state = s1                  : FALSE;
            state = s2                  : TRUE;
        esac;

SPEC
    p & q

第二个代码：

MODULE main
VAR
    p : boolean;
    q : boolean;
    r : boolean;
    state : {s0, s1, s2};

ASSIGN
    init(state) := s0;
    next(state) := 
        case
            state = s0          : {s1, s2};
            state = s1          : {s2};
            state = s2          : {s2};
        esac;

    init(p) := TRUE; 
    init(q) := TRUE;
    init(r) := FALSE;

    next(p) := !p;
    next(q) :=
        case
            state = s0 & next(state) = s1   : q;
            state = s0 & next(state) = s2   : !q;
            state = s1 & next(state) = s0   : q;
            state = s1 & next(state) = s2   : !q;
        esac;
    next(r) :=
        case
            state = s0 & next(state) = s1   : r;
            state = s0 & next(state) = s2   : r;
            state = s1 & next(state) = s0   : !r;
            state = s1 & next(state) = s2   : r;
        esac;

LTLSPEC
    p & q

出了点问题，我收到了这条消息：“案例条件并不详尽”。这是什么意思？如何解决我的问题？

【问题讨论】：

标签： logic ctl nusmv

【解决方案1】：

因为您必须为每种情况输入其“默认值”。第一段代码：

MODULE main
VAR
    p : boolean;
    q : boolean;
    r : boolean;
    state : {s0, s1, s2};

ASSIGN
    init(state) := s0;
    next(state) := 
    case
        state = s0          : {s1, s2};
        state = s1          : {s2};
        state = s2          : {s2};
        TRUE                : state;
    esac;

   init(p) := TRUE; 
   init(q) := TRUE;
   init(r) := FALSE;

   next(p) :=
    case
        state = s1 | state = s2     : FALSE;
    esac;
   next(q) :=
    case
        state = s1                  : TRUE;
        state = s2                  : FALSE;
        TRUE                        : q;
    esac;
   next(r) :=
    case
        state = s1                  : FALSE;
        state = s2                  : TRUE;
        TRUE                        : r;
    esac;

SPEC
    p & q

和第二个代码：

MODULE main
VAR
p : boolean;
q : boolean;
r : boolean;
state : {s0, s1, s2};

ASSIGN
init(state) := s0;
next(state) := 
    case
        state = s0          : {s1, s2};
        state = s1          : {s2};
        state = s2          : {s2};
        TRUE                : state;
    esac;

init(p) := TRUE; 
init(q) := TRUE;
init(r) := FALSE;

next(p) := !p;
next(q) :=
    case
        state = s0 & next(state) = s1   : q;
        state = s0 & next(state) = s2   : !q;
        state = s1 & next(state) = s0   : q;
        state = s1 & next(state) = s2   : !q;
        TRUE                            : q;
    esac;
next(r) :=
    case
        state = s0 & next(state) = s1   : r;
        state = s0 & next(state) = s2   : r;
        state = s1 & next(state) = s0   : !r;
        state = s1 & next(state) = s2   : r;
        TRUE                            : r;
    esac;

LTLSPEC
    p & q

【讨论】：

谢谢，我看到您通过添加以下脚本修复了我的代码：TRUE : state、TRUE : p、TRUE : q 和 TRUE : r。你能解释一下这些脚本是什么意思吗？我知道对于一个原子命题 x（或一组原子命题），脚本 x : TRUE 意味着将真值 TRUE 分配给 x（或 x 中的每个元素）。这是我第一次看到倒数（例如 TRUE : x）。
如果你用任何语言编程，switch case 有一个“default” case。如果任何其他情况不成立，则默认情况为真，并且 NuSMV 的这种情况是必要的。在 next(r) 中，如果前四个案例为假，最后一个案例 (TRUE) 为 TRUE，则 next(r) := r;你明白吗？请检查我的最后一个问题..我需要它。 stackoverflow.com/questions/26428769/…