NuSMV中的自动售货机
NuSMV中的自动售货机
提问于 2016-05-08 23:51:59
我是NuSMV的新手，我试图从克里普克结构创建Vending实现，我有三个布尔值(硬币、选择、酝酿)和三个states.However，当我编译收到的代码时，我收到的代码是“第25行: at token ":"：语法错误”--如果有人在我的代码中看到任何错误，我将非常感谢您的帮助。
克里普克结构
我编写代码的尝试如下：
MODULE main
VAR
location : {s1,s2,s3};
coin : boolean;
selection: boolean;
brweing: boolean;
ASSIGN
init(location) := s1;
init(coin) := FALSE;
init(selection) := FALSE;
init(brweing) := FALSE;
next(location) :=
case
location = s1 : s2;
TRUE: coin;
esac;
next(location) :=
case
location = (s2 : s3 & (TRUE: selection));
location = (s2 : s1 & (FALSE: selection) & (FALSE: coin));
esac;
next(location) :=
case
location = (s3 : s3 & (TRUE: brewing));
location = (s3 : s1 & (FALSE: selection) & (FALSE: coin) & (FALSE: brewing));
esac;
-- specification
• AG [s ⇒ b] whenever a selection is made coffee is brewed for sure.
• E [(¬s) U (b)] the coffee will not be brewed as no selection were made.
• EF[b] there is a state where coffee is brewed.回答 2
Stack Overflow用户
回答已采纳
发布于 2016-05-09 08:45:48
线(除其他外)
location = (s2 : s3 & (TRUE: selection));没有多大意义。您只需要一个next语句就可以从location的所有可能值分配下一个location。另外，不需要将coin、selection和brewing声明为变量。使用DEFINE基于location定义它们的值
MODULE main
VAR
location : {s1,s2,s3};
ASSIGN
init(location) := s1;
next(location) :=
case
location = s1 : s2;
location = s2 : {s1,s3};
location = s3 : {s1,s3};
esac;
DEFINE
coin := location = s2 | location = s3;
-- similarly for selection and brewingStack Overflow用户
发布于 2016-05-11 19:22:34
我从模型中了解到，coin、selection和brew不仅是标签，而且是触发转换的事件。如果是这样的话，我会这样写模型：
MODULE main
VAR
location: {s1, s2, s3};
coin: boolean;
selection: boolean;
brew: boolean;
abort: boolean;
INIT
!coin & !selection & !brew;
ASSIGN
init(location) := s1;
next(location) := case
location = s1 & next(coin) : s2;
location = s2 & next(selection) : s3;
location = s2 & next(abort) : s1;
location = s3 : {s1, s3};
TRUE : location;
esac;
next(brew) := (next(location) = s3);
next(coin) := case
next(state) = s1 : FALSE;
state = s1 : {TRUE, FALSE};
TRUE : coin;
esac;
next(selection) := case
state = s2 : {TRUE, FALSE};
next(state) = s1 : FALSE;
esac;页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/37106066
复制相关文章
相似问题
腾讯云开发者
