1

现在客户有两种选择，电话和短信到诊所预约医生。电话或短信需要发送给话务员或接待处，然后进行下一步....众所周知，电话和短信可以发送成功或发送失败，发送失败的解决方案将继续重试相同的用户选择方式或另一种方式。

基于以上背景，我写了一些做模型检查行为的代码来实现它。我是班上的新手，任何人都可以帮助找出我的代码有什么问题。

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 在终端中运行。

4

1 回答 1

0

第 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

您没有为前两种情况提供下一个值。phone_attender

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

于 2019-06-12T22:21:00.260 回答