2

I'm using nuXmv 1.1.1 to model check the following finite state machine.

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;

With the following CTL specification

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

nuXmv yields that the specification is true.

With the following LTL specfication

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

nuXmv produces the following warning

******** WARNING ******** The initial states set of the finite state machine is empty. This might make results of model checking not trustable. ******** END WARNING ********

I understand the warning, but I do not understand why does it appear. In my opinion, it should appear with both specifications or do not appear at all.

Does anyone have an explanation ?

Davidbrcz
  • 2,335
  • 18
  • 27
  • 1
    Interestingly, the same warning is printed with `LTLSPEC (FALSE -> TRUE)`. I would advice you to contact NuSMV/nuXmv mailing list to get direct support from the devs. Then you can report back and self-answer your question. – Patrick Trentin Jul 30 '18 at 12:51

0 Answers0