Search code examples
nusmvctl

How to deal with the error that Nusmv cannot check ctl properties with input variables (IVAR)?

MODULE main

IVAR v1 ：boolean;

VAR v2 : boolean;

SPEC NAME p1 := AG (v1&v2);

file ltlerror.smv: line 8: Property contains input variables:

Solution

  • At pages 24-25 of NuSMV 2.6 user manual, it's written:

    [...] input variables cannot occur in:

    [...]

    • Some specification kinds: CTLSPEC, SPEC, INVARSPEC, COMPUTE, PSLSPEC. For example:

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

    Workarounds:

    1. use LTL:

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

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

    2. Declare v1 as a normal variable, but use it as an input variable. To do this, do not impose any constraint on the initial and future values of v1, i.e. do not write init(v1) := or next(v1) := or equivalent constraints.