NuSMV 的自动售货机

Question

我是 NuSMV 的新手，我正在尝试从 Kripke 结构创建自动售货机实现，我有三个布尔值（硬币、选择、酿造）以及三个 states.However，当我编译代码时我收到 "Line 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.

Answer 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

Answer 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;

NuSMV 的自动售货机

Vending Machine in NuSMV

model-checking

nusmv