1

我目前正在做一些 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

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

4

1 回答 1

3

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

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
于 2014-10-16T15:33:14.613 回答