Как бороться с ошибкой, что Nusmv не может проверить свойства ctl с входными переменными (ИВАР)?

МОДУЛЬ основной

IVAR v1: логическое значение;

VAR v2 : логическое значение;

ИМЯ СПЕЦИФИКАЦИИ p1 := AG (v1&v2);

файл ltlerror.smv: строка 8: свойство содержит входные переменные:


ctl nusmv
person Alvin    schedule 10.04.2018    source источник
comment
Пожалуйста, добавьте немного контекста и расскажите нам, чего вы пытаетесь достичь   -  person rak007    schedule 10.04.2018

Ответы (1)


arrow_upward
1
arrow_downward

На страницах 24-25 руководства пользователя NuSMV 2.6 написано:

[...] входные переменные не могут встречаться в:

[...]

  • Некоторые виды спецификаций: CTLSPEC, SPEC, INVARSPEC, COMPUTE, PSLSPEC. Например:

    IVAR i : boolean;
VAR s : boolean;
SPEC AF (i -> s) – this is NOT allowed 
LTLSPEC F (X i -> s) – this is allowed

Обходные пути:

  1. используйте LTL:

    MODULE main
IVAR
  v1 : boolean;
VAR
  v2 : boolean;

LTLSPEC NAME p1 := G (v1 & v2);

  2. Объявите v1 как обычную переменную, но используйте ее как входную переменную. Для этого не накладывайте никаких ограничений на начальное и будущее значения v1, т.е. не пишите init(v1) := или next(v1) := или эквивалентные ограничения.

person Patrick Trentin    schedule 10.04.2018