NuSMV中的自动售货机答案

【问题标题】：Vending Machine in NuSMVNuSMV中的自动售货机
【发布时间】：2016-05-08 23:51:59
【问题描述】：

我是 NuSMV 的新手，我正在尝试从 Kripke 结构创建自动售货机实现，我有三个布尔值（硬币、选择、酿造）以及三个状态。但是，当我编译代码时，我收到“第 25 行: at token ":": syntax error" 如果有人在我的代码中看到任何错误，我将不胜感激。

Kripke structure

我尝试编写代码如下：

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.

【问题讨论】：

标签： model-checking nusmv

【解决方案1】：

生产线（以及其他）

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 brewing

【讨论】：

【解决方案2】：

我从模型中了解到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;

【讨论】：