How to create a simple Kripke model in NuSMV?

问题:

I am currently doing some theoretical research in LTL (Linear-time Temporal Logic) and CTL (Computation Tree Logic). I am new to NuSMV and I have difficulty to create a simple Kripke structure.

My structure is M = (S, R, L) where S = {s0, s1, s2} is the set of possible states, R is a transition relation such that: s0 -> s1, s0 -> s2, s1 -> s0, s1 -> s2, and s2 -> s2, and L is the labeling function for each state defined by: L(s0) = {p, q}, L(s1) = {q, r}, and L(s2) = {r}. I am using notations describe in Logic in Computer Science textbook by Huth and Ryan. I have tried two following codes:

The first code:

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

The second code:

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

Something was wrong and I got this message: "case conditions are not exhaustive". What does it mean? How do I fix my problem?

回答1:

Because you must enter for each case also its "default". The first code:

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

and the second code:

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