我是NuSMV的新手，我尝试从Kripke结构创建自动售货机实现，我有三个布尔（硬币，选择，酿造）以及三个状态。但是，当我编译代码I收到“第25行：at token”：“：语法错误”如果任何人在我的代码中看到任何错误，我将不胜感激。 Kripke structure 我尝试写的代码如下： MODULE main
VAR
location : {s1,s2,s3};
coi
我是NuSMV的新手，并尝试对这个简单的回合制游戏进行建模。一堆中有10块砖，每个玩家每回合可以拿1-3块砖，谁拿走最后一块砖就赢得比赛。假设玩家A先去，这是我的尝试。我想表达的是，“最终有一个胜利者”，但是我的代码不起作用，因为它不阻止玩家在砖块= 0之后采取砖块，所以最终玩家a，b都会成为赢家。 这里是我的代码： MODULE main
VAR
bricks : 0..10;
i :
我的教授决定给我们数学学生一个代码，以改变成NuSMV，我似乎无法找到其他任何地方的帮助，我阅读的教科书只有6页，只描述某些属性。 Module main是NuSMV代码的一个例子，他说用这个格式的例子来编写伪代码。 我不知道如何编写while循环，并设置什么是真实的？并将旗1成为一个国家，并成为另一个国家？ while(true) do
flag1 := true
while