Синтаксическая ошибка nuXmv при использовании переменной вместо целого числа

У меня есть модель в muXmv, где я инициализирую диапазон значений, например -

VAR 
  x : 0..100;
ASSIGN
  init(x) := 10..50;

это отлично работает.

Однако, когда я использую переменную вместо значений,

ASSIGN 
  init(x) := LB..UB;

DEFINE
  LB := 10;
  UB := 50;

выдает синтаксическую ошибку -

строка 14: в токене ..: синтаксическая ошибка

строка 14: ошибка парсера

Не уверен, где я иду не так?

Также есть ли лучший способ объявить константы в nuxmv?


syntax model-checking nuxmv
person Sneha Sahu    schedule 22.11.2019    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Определение не обязательно является константой, это просто имя выражения (значение которого может меняться после каждого перехода). например

MODILE main()
VAR
    x : 0..100;
    y : 0..100;
DEFINE
    sum := x + y;

...

Я не знаю, почему Грамматика для NuSMV/nuXmv специально запрещает запись интервала с использованием пары идентификаторов вместо пары констант.

Одна альтернатива:

MODULE main()
VAR
    x : 0..100;

ASSIGN
  init(x) := INTERVAL;

DEFINE
  INTERVAL := 10 .. 50;

Другой альтернативой является использование подхода в стиле ограничений:

MODULE main()
VAR
    x : 0..100;

DEFINE
    LB := 10;
    UB := 50;

INIT
    LB <= x & x <= UB;

Если вы действительно испытываете затруднения со многими постоянными значениями, один из вариантов — написать общую модель TEMPLATE, а затем использовать регулярные выражения + инструменты сценариев для автоматически создавать различные конкретные модели, которые вам нужны.

person Patrick Trentin    schedule 24.11.2019
comment
первое решение по-прежнему дает ту же ошибку, но второй вариант работает. - person Sneha Sahu; 28.11.2019
comment
сможете ли вы объяснить 3-й подход на примере? - person Sneha Sahu; 28.11.2019
comment
@SnehaSahu Я протестировал оба примера с NuSMv 2.6.0, и они оба работают. - person Patrick Trentin; 28.11.2019
comment
Я поигрался и нашел причину проблемы. Всякий раз, когда я использую флаг при инициализации, который является входом в процесс, переменные не работают. Я могу поделиться примером кода, но в комментарии я не могу отформатировать - person Sneha Sahu; 28.11.2019
comment
@SnehaSahu, не могли бы вы отправить его по электронной почте (см. профиль) - person Patrick Trentin; 28.11.2019