Блог

Я новичок в NuSMV. Я пытаюсь определить модуль, в котором каждое состояние имеет переменную длительности, которая может варьироваться от 0 до указанной границы.

 MODULE state(inc, bound)
 VAR 
   duration : 0..bound;
 
 ASSIGN 
  init(duration) := 0;
  next(duration) := inc ? (duration   1) mod (bound 1) : duration ;

 DEFINE limit := duration = bound; 
 

Однако это приводит к синтаксической ошибке : A variable is expected in left-hand-side of assignment: init(duration) := 0 . Я могу исправить это, объявив duration duration : 0..1 bound .

В моем основном модуле я хочу вычислить total_duration (или фактически вычислить все возможные комбинации длительности состояния и убедиться, что ни одна комбинация не превышает e.i. 3, как в СПЕЦИФИКАЦИИ) для запуска моей модели и убедиться, что переменная не достигает определенного предела.

Вот мой основной модуль:

 MODULE main
 VAR 
  s0 : state(TRUE, 0);
  s1 : state(s0.limit, 0);
  s2 : state(s1.limit, 3);
  state : {s0, s1, s2};

 DEFINE
  max_duration := s0.bound   s1.bound   s2.bound;

 VAR
  total_duration : 0..max_duration;

 ASSIGN
  init(state) := s0;

  next(state) := 
    case
      state = s0 : s1;
      state = s1 : s2;
      state = s2 : s2;
    esac;

  total_duration := s0.duration   s1.duration   s2.duration;

SPEC
  AG (state = s2 -> AF total_duration <= 3);
 

Моя проблема в том, что когда я запускаю модель, NuSMV продолжает добавлять к total_duration переменной и, таким образом, завершается ошибкой с сообщением « line 39: cannot assign value 5 to variable total_duration «. Это связано с объявлением duration : 0..1 bound , потому что в конкретном примере
s0.duration = 0, s1.duration = 0 и s2.duration = 3 он попытается добавить 1 1 4 to total_duration , поскольку это привязка состояния 1.

Однако, если я проверю трассировку, нет точки, где total_duration превышает 3. Я проверил следующие спецификации:

 -- specification AG total_duration < 4  is true

-- specification  F total_duration = 4  is false
-- specification EF total_duration >= 4  is false
 

Как я могу это исправить? Либо путем объявления продолжительности другим способом, либо путем изменения чего-либо еще?

Программное обеспечение делает что-то очень простое. Он принимает домен каждого дополнения и проверяет, сможет ли результирующая переменная содержать результат каждой возможной комбинации значений. В этом случае:

• область s0.duration 0..1
• область s1.duration 0..1
• область s2.duration 0..4

таким образом, в принципе, максимум total_duration может быть 6 , и его домен, таким образом, должен быть 0..6 . Поэтому:

 DEFINE
  max_duration := s0.bound   s1.bound   s2.bound   3
 

Возможно, вы захотите выполнить NuSMV следующий параметр:

 -keep_single_value_vars
  Does not convert variables that have only one
  single possible value into constant DEFINEs
 

Таким образом, вы сможете запускать модель без необходимости добавления 1 в домен bound .