1

私は NuSMV を初めて使用します。Kripke 構造から自動販売機の実装を作成しようとしています。3 つのブール値 (コイン、選択、醸造) と 3 つの状態があります。しかし、コードをコンパイルすると、"Line 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.
4

2 に答える 2

2

ライン（とりわけ）

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

あまり意味がありません。のすべての可能な値からnext次のステートメントを割り当てるには、1 つのステートメントのみが必要です。また、 、、およびを変数として宣言する必要はありません。以下に基づいて値を定義するために使用します。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 に答える