将 FSM 转换为 NuSMV 模型

Question

我喜欢这样的 FSM

我写了一段代码来检查 FSM 上的 LTL 属性这是我的 LTL 属性

G!(r1 & r2) -> (G(!g1 | !g2) & G(r1 -> F(g1)) & G(r2 -> F(g2)))

我的 NuSMV 代码是

MODULE main
VAR
    state : 0 .. 2;
    r1 : boolean;
    r2 : boolean;
    g1 : boolean;
    g2 : boolean;
ASSIGN
    init (state) := 0;
    init(r1) := FALSE;
    init(r2) := FALSE;
    init(g1) := FALSE;
    init(g2) := FALSE;
    next(state) :=
        case
            (state = 0) & (g1) & (r1) & (!r2) & (!g2)  : 1;
            (state = 1) & (g1) & (!r1) & (r2) & (g2)  : 0;
            (state = 0) & (!g1) & (!r1) & (!r2) & (!g2)  : 0;
            (state = 0) & (!g1) & (!r1) & (r2) & (g2)  : 0;
            (state = 0) & (g1) & (r1) & (r2) & (!g2)  : 0;
            (state = 1) & (g1) & (!r1) & (!r2) & (g2)  : 1;
            (state = 1) & (g1) & (r1) & (r2) & (!g2)  : 1;
            (state = 1) & (!g1) & (r1) & (!r2) & (!g2)  : 1;
            TRUE : state;
        esac;
    next(g1) :=
        case
            (state = 1) & (!r1) & (r2) & (g2)  : TRUE;
            (state = 0) & (!r1) & (!r2) & (!g2)  : FALSE;
            (state = 0) & (r1) & (!r2) & (!g2)  : TRUE;
            (state = 1) & (!r1) & (!r2) & (g2)  : TRUE;
            (state = 1) & (r1) & (!r2) & (!g2)  : FALSE;
            (state = 0) & (r1) & (r2) & (!g2)  : TRUE;
            (state = 1) & (r1) & (r2) & (!g2)  : TRUE;
            (state = 0) & (!r1) & (r2) & (g2)  : FALSE;
            TRUE : g1;
        esac;
    next(r1) :=
        case
            (state = 0) & (g1) & (!r2) & (!g2)  : TRUE;
            (state = 0) & (!g1) & (r2) & (g2)  : FALSE;
            (state = 1) & (!g1) & (!r2) & (!g2)  : TRUE;
            (state = 0) & (g1) & (r2) & (!g2)  : TRUE;
            (state = 1) & (g1) & (!r2) & (g2)  : FALSE;
            (state = 0) & (!g1) & (!r2) & (!g2)  : FALSE;
            (state = 1) & (g1) & (r2) & (!g2)  : TRUE;
            (state = 1) & (g1) & (r2) & (g2)  : FALSE;
            TRUE : r1;
        esac;
    next(r2) :=
        case
            (state = 0) & (g1) & (r1) & (!g2)  : {TRUE, FALSE};
            (state = 1) & (!g1) & (r1) & (!g2)  : FALSE;
            (state = 0) & (!g1) & (!r1) & (g2)  : TRUE;
            (state = 1) & (g1) & (!r1) & (g2)  : {TRUE, FALSE};
            (state = 1) & (g1) & (r1) & (!g2)  : TRUE;
            (state = 0) & (!g1) & (!r1) & (!g2)  : FALSE;
            TRUE : r2;
        esac;
    next(g2) :=
        case
            (state = 1) & (g1) & (r1) & (r2)  : FALSE;
            (state = 0) & (!g1) & (!r1) & (!r2)  : FALSE;
            (state = 1) & (g1) & (!r1) & (!r2)  : TRUE;
            (state = 0) & (g1) & (r1) & (!r2)  : FALSE;
            (state = 1) & (g1) & (!r1) & (r2)  : TRUE;
            (state = 1) & (!g1) & (r1) & (!r2)  : FALSE;
            (state = 0) & (!g1) & (!r1) & (r2)  : TRUE;
            (state = 0) & (g1) & (r1) & (r2)  : FALSE;
            TRUE : g2;
        esac;

使用以下命令进行模型检查后，我想知道我何时会看到 NuSMV return True

NuSMV -int
read_model -i test2.smv
flatten_hierarchy
encode_variables
build_model
pick_state -i

check_ltlspec -p "G!(r1 & r2) -> (G(!g1 | !g2) & G(r1 -> F(g1)) & G(r2 -> F(g2)))"

NuSMV 结果是：

-- specification ( G !(r1 & r2) -> (( G (!g1 | !g2) &  G (r1 ->  F g1)) &  G (r2 ->  F g2)))  is true

但我可以手动找到CE 阅读 NuSMV 2.6 用户手册后，我找不到 NuSMV 代码的哪一部分是错误的

Answer 1

我发现了问题我的模型出了点问题在这段代码输入中建模，但这不是必需的，因为我们只是建模系统而不是环境

next(r1) :=
        case
            (state = 0) & (g1) & (!r2) & (!g2)  : TRUE;
            (state = 0) & (!g1) & (r2) & (g2)  : FALSE;
            (state = 1) & (!g1) & (!r2) & (!g2)  : TRUE;
            (state = 0) & (g1) & (r2) & (!g2)  : TRUE;
            (state = 1) & (g1) & (!r2) & (g2)  : FALSE;
            (state = 0) & (!g1) & (!r2) & (!g2)  : FALSE;
            (state = 1) & (g1) & (r2) & (!g2)  : TRUE;
            (state = 1) & (g1) & (r2) & (g2)  : FALSE;
            TRUE : r1;
        esac;
    next(r2) :=
        case
            (state = 0) & (g1) & (r1) & (!g2)  : {TRUE, FALSE};
            (state = 1) & (!g1) & (r1) & (!g2)  : FALSE;
            (state = 0) & (!g1) & (!r1) & (g2)  : TRUE;
            (state = 1) & (g1) & (!r1) & (g2)  : {TRUE, FALSE};
            (state = 1) & (g1) & (r1) & (!g2)  : TRUE;
            (state = 0) & (!g1) & (!r1) & (!g2)  : FALSE;
            TRUE : r2;
        esac;

将 FSM 转换为 NuSMV 模型

Convert FSM to NuSMV model

model-checking

fsm

nusmv