2

我正在使用 nuXmv 1.1.1 对以下有限状态机进行模型检查。

MODULE main
VAR
    node :  {_0_0,_1_0,_1_1,_1_2,_1_3,_2_0};
DEFINE
setParentThis_r_ := case 
     TRUE : FALSE; 
 esac; 

setParent_r_ := case 
    node=_1_3 :TRUE;
     TRUE : FALSE; 
 esac; 

ASSIGN
     init(node) := _2_0 ;
     next(node) :=  case 
    node =_0_0:{_0_0}; 
    node =_1_0:{_1_1}; 
    node =_1_1:{_1_2}; 
    node =_1_2:{_1_3}; 
    node =_1_3:{_0_0}; 
    node =_2_0:{_1_0}; 

 esac;

使用以下 CTL 规范

SPEC
A[(!(setParent_r_)) U (setParentThis_r_ -> AX(AG(!(setParent_r_))))]

nuXmv 产生规范是真实的。

具有以下 LTL 规格

LTLSPEC
(!(setParent_r_)) U (setParentThis_r_ -> X(G(!(setParent_r_))))

nuXmv 产生以下警告

******** 警告 ******** 有限状态机的初始状态集是空的。这可能会使模型检查的结果不可信。********结束警告********

我理解警告，但我不明白为什么会出现。在我看来，它应该与两种规格一起出现，或者根本不出现。

有人有解释吗？

4

0 回答 0