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 ?