自動販売機NuSMV

Question

私はNuSMVを新しくしました。私はKripke構造から自動販売機実装を作成しようとしています.3つのブール値（コイン、選択、醸造）と3つの州があります。しかし、 "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)); 

はあまり意味がありません。すべての可能な値locationから次のlocationを割り当てるには、next文が1つだけ必要です。また、coin,selection、およびbrewingを変数として宣言する必要はありません。 locationに基づいてそれらの値を定義するためにDEFINEを使用します。

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;