Automat in NuSMV

Question

Ich bin neu in NuSMV, ich versuche, Vending Machine Implementierung von Kripke Struktur zu schaffen, ich habe drei boolean (Münze, Auswahl, brauen) sowie drei states.However, Wenn ich den Code, den ich kompilieren empfange "Zeile 25: bei Token": ": Syntaxfehler" Wenn jemand Fehler in meinem Code sieht, würde ich mich über die Hilfe freuen.

Kripke structure

mein Versuch, den Code zu schreiben, ist wie folgt:

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

Die Leitung (unter anderem)

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

macht nicht viel Sinn machen. Sie benötigen nur eine next Anweisung, um den nächsten location aus allen möglichen Werten von location zuzuweisen. Außerdem müssen Sie coin, selection und brewing nicht als Variablen deklarieren. Verwenden Sie DEFINE, um ihre Werte zu definieren, basierend auf 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

Was ich aus dem Modell zu verstehen ist, dass coin, selection und brew sind nicht nur Etiketten, sondern Ereignisse, die den Übergang auslösen. Wenn ja, würde ich das Modell wie folgt schreiben:

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;