Синтаксическая ошибка вложенного оператора NEXT в NuSMV - PullRequest
Новая
       95

Синтаксическая ошибка вложенного оператора NEXT в NuSMV

0 голосов
/ 07 октября 2018

Я пытаюсь использовать NuSMV для проверки моей модели, и вот код.

enter image description here

Однако, когда я вводю NuSMV kernel.smv в оболочке, это происходит ошибка 

file kernel.smv: line 16: nested NEXT operators: next(_b)
in definition of next(_cond)
in definition of next(tx.fired) at line 16

Я новичок в проверке модели NuSMV, поэтому я не мог исправить эту синтаксическую ошибку.Пожалуйста, помогите, спасибо!

1 Ответ

0 голосов
/ 07 октября 2018

Я смог создать MVCE из вашего изображения: 

MODULE trans(cond)
VAR
    fired : boolean;
ASSIGN
    init(fired) := FALSE;
    next(fired) := case
        !next(cond) : TRUE;
        TRUE        : FALSE;
    esac;

MODULE main
VAR
    _b : boolean;
    t  : trans(_cond);
DEFINE
    _cond := (_b != next(_b));

Здесь проблема дизайна - это именно то, о чем вам говорит средство проверки моделей всообщение об ошибке: 

NuSMV > reset; read_model -i t.smv ; go

file t.smv: line 6: nested NEXT operators: next(_b)
in definition of next(_cond)
in definition of next(t.fired) at line 6

* * * * * * * * * * * * * * * * * next() * * * * * * * * * * * * *1015* *1015* должен быть увеличен за пределы пары current_state + selected_transition и знать, какой переход взят из будущего состояния, которое все еще находится в стадии разработки.

Обходной путь.

Давайте возьмем следующую модель, которая имеет ту же проблему, что и ваша: 

MODULE main()
VAR
    frst : 0 .. 1;
    scnd : boolean;

ASSIGN
    init(frst) := 0;
    init(scnd) := FALSE;

    next(scnd) := case
        next(middle) : TRUE;
        TRUE         : FALSE;
    esac;

DEFINE
    middle := (frst != next(frst));

мы хотим, чтобы scnd было true, если значение frst изменитсясреди состояний next() и next(next()).

Для этого мы можем задержка начало трассы выполнения, так что мы можем предсказывать будущее значение frst с достаточным преимуществом.

Давайте посмотрим на это спример: 

MODULE main()
VAR
    hidden : 0 .. 1;
    frst   : 0 .. 1;
    scnd   : boolean;

ASSIGN
    init(hidden) := 0;
    init(frst)   := 0;
    init(scnd)   := FALSE;

    next(frst) := hidden; -- frst does not start "changing" arbitrarily
                          -- in the second state, but in the third state

    next(scnd) := case
        predicted : TRUE; -- true iff frst changes value 2 states from now
        TRUE      : FALSE;
    esac;

DEFINE
    middle    := (frst != next(frst));     -- true iff frst changes value
                                           -- from the current state to the
                                           -- next() state
    predicted := (hidden != next(hidden)); -- true iff frst changes value
                                           -- from the next state to the
                                           -- next(next()) state
...