Торговый автомат в NuSMV

Question

Я новичок в NuSMV, я пытаюсь создать реализацию торгового автомата из структуры Kripke, у меня есть три булева (монета, выбор, пивоварение), а также три состояния. Однако, когда я скомпилирую код I получите "Строка 25: в токене": ": синтаксическая ошибка" Если кто-нибудь увидит какие-либо ошибки в моем коде, я был бы признателен за помощь.

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;