blocks|key|2573629|text|我能够从你的图像中创建一个MVCE：|type|unstyled|depth|inlineStyleRanges|entityRanges|offset|length|data|2573630|MODULE+trans(cond)
VAR
++++fired+:+boolean;
ASSIGN
++++init(fired)+:=+FALSE;
++++next(fired)+:=+case
++++++++!next(cond)+:+TRUE;
++++++++TRUE++++++++:+FALSE;
++++esac;

MODULE+main
VAR
++++_b+:+boolean;
++++t++:+trans(_cond);
DEFINE
++++_cond+:=+(_b+!=+next(_b));|code-block|syntax|javascript|2573631|这里的设计问题正是模型检查器在错误消息中告诉您的：|2573632|NuSMV+>+reset;+read_model+-i+t.smv+;+go

file+t.smv:+line+6:+nested+NEXT+operators:+next(_b)
in+definition+of+next(_cond)
in+definition+of+next(t.fired)+at+line+6|2573633|next()运算符在其内部有一个双重嵌套，这是不受支持的，因为它需要将执行范围增加到current_state+%2B+chosen_transition对之外，并且知道从仍在构造中的未来状态进行哪个转换。|style|CODE|2573634|2573635|解决方法。|BOLD|2573636|让我们以下面的模型为例，它与您的模型有相同的问题：|2573637|MODULE+main()
VAR
++++frst+:+0+..+1;
++++scnd+:+boolean;

ASSIGN
++++init(frst)+:=+0;
++++init(scnd)+:=+FALSE;

++++next(scnd)+:=+case
++++++++next(middle)+:+TRUE;
++++++++TRUE+++++++++:+FALSE;
++++esac;

DEFINE
++++middle+:=+(frst+!=+next(frst));|2573638|我们希望scnd为true，当frst的值在next()和next(next())状态之间发生变化时。|2573639|要做到这一点，我们可以在执行跟踪的开始时延迟()，这样我们就可以对frst的未来值进行充分的预测。|2573640|让我们用一个例子来看一下：|2573641|MODULE+main()
VAR
++++hidden+:+0+..+1;
++++frst+++:+0+..+1;
++++scnd+++:+boolean;

ASSIGN
++++init(hidden)+:=+0;
++++init(frst)+++:=+0;
++++init(scnd)+++:=+FALSE;

++++next(frst)+:=+hidden;+--+frst+does+not+start+"changing"+arbitrarily
++++++++++++++++++++++++++--+in+the+second+state,+but+in+the+third+state

++++next(scnd)+:=+case
++++++++predicted+:+TRUE;+--+true+iff+frst+changes+value+2+states+from+now
++++++++TRUE++++++:+FALSE;
++++esac;

DEFINE
++++middle++++:=+(frst+!=+next(frst));+++++--+true+iff+frst+changes+value
+++++++++++++++++++++++++++++++++++++++++++--+from+the+current+state+to+the
+++++++++++++++++++++++++++++++++++++++++++--+next()+state
++++predicted+:=+(hidden+!=+next(hidden));+--+true+iff+frst+changes+value
+++++++++++++++++++++++++++++++++++++++++++--+from+the+next+state+to+the
+++++++++++++++++++++++++++++++++++++++++++--+next(next())+state|2573642|entityMap|0|LINK|mutability|MUTABLE|url|https://stackoverflow.com/help/mcve^0|D|4|0|0|0|0|0|0|6|0|0|0|5|0|0|0|4|4|9|4|F|4|M|6|T|C|0|X|4|0|0|0^^$0|@$1|2|3|4|5|6|7|1E|8|@]|9|@$A|1F|B|1G|1|1H]]|C|$]]|$1|D|3|E|5|F|7|1I|8|@]|9|@]|C|$G|H]]|$1|I|3|J|5|6|7|1J|8|@]|9|@]|C|$]]|$1|K|3|L|5|F|7|1K|8|@]|9|@]|C|$G|H]]|$1|M|3|N|5|6|7|1L|8|@$A|1M|B|1N|O|P]]|9|@]|C|$]]|$1|Q|3|-4|5|6|7|1O|8|@]|9|@]|C|$]]|$1|R|3|S|5|6|7|1P|8|@$A|1Q|B|1R|O|T]]|9|@]|C|$]]|$1|U|3|V|5|6|7|1S|8|@]|9|@]|C|$]]|$1|W|3|X|5|F|7|1T|8|@]|9|@]|C|$G|H]]|$1|Y|3|Z|5|6|7|1U|8|@$A|1V|B|1W|O|P]|$A|1X|B|1Y|O|P]|$A|1Z|B|20|O|P]|$A|21|B|22|O|P]|$A|23|B|24|O|P]]|9|@]|C|$]]|$1|10|3|11|5|6|7|25|8|@$A|26|B|27|O|P]]|9|@]|C|$]]|$1|12|3|13|5|6|7|28|8|@]|9|@]|C|$]]|$1|14|3|15|5|F|7|29|8|@]|9|@]|C|$G|H]]|$1|16|3|-4|5|6|7|2A|8|@]|9|@]|C|$]]]|17|$18|$5|19|1A|1B|C|$1C|1D]]]]

I was able to create a <a href="https://stackoverflow.com/help/mcve">MVCE</a> out of your image:

<pre><code>MODULE trans(cond)
VAR
 fired : boolean;
ASSIGN
 init(fired) := FALSE;
 next(fired) := case
 !next(cond) : TRUE;
 TRUE : FALSE;
 esac;

MODULE main
VAR
 _b : boolean;
 t : trans(_cond);
DEFINE
 _cond := (_b != next(_b));
</code></pre>

Here the design problem is exactly what the model checker tells you in the error message:

<pre><code>NuSMV &gt; reset; read_model -i t.smv ; go

file t.smv: line 6: nested NEXT operators: next(_b)
in definition of next(_cond)
in definition of next(t.fired) at line 6
</code></pre>

There is a double nesting of the <code>next()</code> operator within itself, and this isn't supported as it would require the execution horizon to be increased beyond the current_state + chosen_transition pair, and know which transition is taken from a future state that is still under construction.

<hr>

Workaround.

Let's take the following model, which has the same problem as yours:

<pre><code>MODULE main()
VAR
 frst : 0 .. 1;
 scnd : boolean;

ASSIGN
 init(frst) := 0;
 init(scnd) := FALSE;

 next(scnd) := case
 next(middle) : TRUE;
 TRUE : FALSE;
 esac;

DEFINE
 middle := (frst != next(frst));
</code></pre>

we want <code>scnd</code> to be <code>true</code> iff the value of <code>frst</code> is going to change amidst the <code>next()</code> and the <code>next(next())</code> state.

To do so, we can delay the beginning of the execution trace, so that we can predict the future value of <code>frst</code> with sufficient advantage.

Let's see it with an example:

<pre><code>MODULE main()
VAR
 hidden : 0 .. 1;
 frst : 0 .. 1;
 scnd : boolean;

ASSIGN
 init(hidden) := 0;
 init(frst) := 0;
 init(scnd) := FALSE;

 next(frst) := hidden; -- frst does not start "changing" arbitrarily
 -- in the second state, but in the third state

 next(scnd) := case
 predicted : TRUE; -- true iff frst changes value 2 states from now
 TRUE : FALSE;
 esac;

DEFINE
 middle := (frst != next(frst)); -- true iff frst changes value
 -- from the current state to the
 -- next() state
 predicted := (hidden != next(hidden)); -- true iff frst changes value
 -- from the next state to the
 -- next(next()) state
</code></pre>

I try to use NuSMV to check my model and here is the code.

<a href="https://i.stack.imgur.com/CPl3K.png" rel="nofollow noreferrer"><img src="https://i.stack.imgur.com/CPl3K.png" alt="enter image description here"></a>

However, when I input <code>NuSMV kernel.smv</code> in the shell, it occur an error

<pre><code>file kernel.smv: line 16: nested NEXT operators: next(_b)
in definition of next(_cond)
in definition of next(tx.fired) at line 16
</code></pre>

I'm a newbie in NuSMV model checker, so I could not fix this syntax error. Please help, thanks!

syntax error nested NEXT operator in NuSMV

V模型

我尝试使用NuSMV来检查我的模型，下面是代码。​​但是，当我在外壳程序中输入NuSMV kernel.smv时，它出现错误file kernel.smv: line 16: nested NEXT operators: next(_b)in definition of next(_cond)in definition...

问NuSMV中嵌套的NEXT运算符存在语法错误
EN

社区

活动

资源

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问NuSMV中嵌套的NEXT运算符存在语法错误EN

社区

活动

资源

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问NuSMV中嵌套的NEXT运算符存在语法错误
EN