1

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

克里普克结构

我编写代码的尝试如下：

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.
4

2 回答 2

2

线路（除其他外）

location = (s2 : s3 & (TRUE: selection));

没有多大意义。您只需要一个语句就可以从 的所有可能值中next分配下一个语句。此外，您不需要将 、 和 声明为变量。用于根据 定义它们的值：locationlocationcoinselectionbrewingDEFINElocation

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
于 2016-05-09T08:45:48.660 回答
1

我从模型中了解到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;
于 2016-05-11T19:22:34.217 回答