问题描述
我正在尝试使用 mcrl2 解决交通灯问题。我不知道我的代码是否 100% 正确,但它可以编译。
基本上我有 3 种颜色和 3 个交通灯,使用此代码我可以切换它们的颜色,但是我想做出限制,例如,如果一个交通灯是绿色,则其他交通灯不能更改为任何颜色,它们只能更改它们的颜色当绿灯变成黄灯时。
sort
Color = struct green | red | yellow;
map
next: Color -> Color;
eqn
next(green) = yellow;
next(yellow) = red;
next(red) = green;
act
toRed,toGreen,toRedYellow,toYellow;
proc
Lighter1 (c : Color) = (c == green) -> toYellow.Lighter1(next(c))
+(c == yellow) -> toRed.Lighter1(next(c))
+(c == red) -> toGreen.Lighter1(next(c));
Lighter2 (c : Color) = (c == green) -> toYellow.Lighter2(next(c))
+(c == yellow) -> toRed.Lighter2(next(c))
+(c == red) -> toGreen.Lighter2(next(c));
Lighter3 (c : Color) = (c == green) -> toYellow.Lighter3(next(c))
+(c == yellow) -> toRed.Lighter3(next(c))
+(c == red) -> toGreen.Lighter3(next(c));
init
Lighter1(green) || Lighter2(red) || Lighter3(green);
解决方法
暂无找到可以解决该程序问题的有效方法,小编努力寻找整理中!
如果你已经找到好的解决方法,欢迎将解决方案带上本链接一起发送给小编。
小编邮箱:dio#foxmail.com (将#修改为@)