nuXmv模型检查中的语法错误

Question

现在有两种选择，客户，电话和短信到诊所预约医生。电话或短信需要送到电话接待员或接待处，然后再做下一个.正如我们所知，电话和短信可以成功传递或失败传递，失败传递的解决方案将继续尝试同样的方式，用户选择或另一个。

基于上述背景，我编写了一些代码来进行模型检查行为的实现。我是这门课的新手，任何人都可以帮我找出我的密码有什么问题。

MODULE call
VAR
option:{call,sms};
call:{successful,fail,again};
sms:{successful,fail,again};
phone_attender:{available,unavailable};

ASSIGN
init(option):=call|sms;
next(call):=case
call=successful:successful;
call=successful&phone_attender=available:{successful,available};
call=fail&phone_attender=fail:{fail,unavailable};
call=fail&phone_attender=fail:{again,unavailable};
call=again&phone_attender=successful:{again,available};
1:{successful,fail,again};
esac;

next(sms):=case
sms=successful&phone_attender:successful{successful};
sms=fail&phone_attender=fail:{fail,unavailable};
sms=fail&phone_attender=fail:{again,unavailable};
sms=again&phone_attender=successful:{again,available};
1:{successful,fail,again};

next(phone_attender):=case
phone_attender=available(call=successful|call=again)&(sms=successful|sms=again);
phone_attender=unavailable(call=fail|call=again)&(sms=fail|sms=again);
1:phone_attender;
esac;

它总是余数我的语法错误，并运行在终端与nuXmv。

Answer 1

20号线：

file test.smv: line 20: at token "{": syntax error

这个问题是由以下条件提出的：

sms=successful&phone_attender:successful{successful};

successful{successful}值没有任何意义，可以在successful或{succesful}之间进行选择。两者的解释是相同的。

26号线：

file test.smv: line 26: at token ":=": syntax error

您没有关闭上一次赋值的case构造。在最后一个条件之后添加esac;。

第28/29行：

file test.smv: line 28: at token ";": syntax error
file test.smv: line 29: at token ";": syntax error

您没有为前两种情况提供next值用于phone_attender。

注意:我没有检查您的模型的语义，因为它甚至在语法上都不正确。