FAQ

Currently, there is not a tutorial for developers. We are working on it. However, if you have any question please send an e-mail to we will try to answer your question as soon as possible.

It is likely that such an error is thrown by NuSMV because of a lack of memory on your system (i.e. Memory out). You should check if while running NuSMV there is enough memory left. If this is the case then you may have found a bug. Please report it to with the following information: the commands you ran, the SMV model you used, all options passed to NuSMV and the specification of your system.

You may also try to re-execute NuSMV enabling BDD dynamic variable ordering, i.e. providing -dynamic flag at the command line, or dynamic_var_ordering -e sift at NuSMV shell prompt.

One reason could be a low stack size limit: NuSMV still uses some recursive functions. Under Linux/Unix generally it does not create problems to remove this limitation entirely;

• with (ba)sh issue ulimit -s unlimited;
• with (t)csh limit stacksize unlimited.

Under Windows the stack size is hard-coded in the executable. It is possible to use the Visual Studio utility editbin.exe to increase the stack size. However, since this memory will be reserved, it is better to set it to a reasonable amount (e.g. 10 MB).

The command is editbin /stack:10485760 NuSMV.exe.
To check that it worked, run dumpbin /headers NuSMV.exe and look for string size of stack reserve.

Always remember that the CPP pre-processor is designed for the C/C++ languages. It might be that the part of the SMV file where macros are used is not recognized as "expandable" by the CPP pre-processor.

For example, calling "NuSMV -pre cpp" with the following model:

1

#define A_MACRO 5

1
2

MODULE main
VAR myarr: array 1..A_MACRO of boolean;

will cause the following error:

1

Unexpected value at token 'A_MACRO' file cpp.smv: line 3: A number was expected but not found.

since the two dots (..) followed by A_MACRO is not expanded by the CPP pre-processor. A solution is to add a white-space after the two dots:

1

#define A_MACRO 5

1
2

MODULE main
VAR myarr: array 1.. A_MACRO of boolean;

NuSMV provides the "fixed point" semantics. This is the standard set of fixed point characterization of the temporal operators (which differ in case of fairness and no fairness), and it assumes the transition relation to be total and deadlock free.

Moreover, in NuSMV there is an implicit universal quantifier over all the initial fair states. A consequence of this is that if there are no initial fair states then all formulas pass.

The (possibly arguable) choice of quantifying over all initial fair states turns out to be different from the "classical" definition of model checking problem that does not restrict to the fair initial states. However, this choice has also been adopted by CadenceSMV.

NuSMV is not suitable to check the satisfiability of CTL, whereas for LTL using an unconstrained model does the work.

In fact, a model with a TRUE transition relation exhibits all LTL behaviors (i.e. sequences of states) but it exhibits only particular CTL behaviors (i.e. trees of states) where every state has exactly 2^n successors (n being the number of propositional variables in the model, since the model is a clique). For instance, such model satisfies EX p but not AX p, although both are satisfiable.

Finally, from a theoretical point of view, we remark that CTL satisfiability is EXPTIME-complete and thus likely not reducible to CTL model checking which is PSPACE-complete.

Of course the checks are correct. The point is that the option -coi (Cone of Influence) forces the construction of a partial model which includes only those variables affected by the property being checked. This way, NuSMV may find a loop that does not exist in the original model. If the model does not contain deadlocks, the it is possible to reconstruct a concrete counterexample by refining the computed counterexample. However, this is not performed by NuSMV.

Here a small example showing this behavior.

1
2
3
4
5
6
7
8
9

MODULE main
VAR x : word[3];
VAR y : word[4];
ASSIGN
init(x) := 0ud3_0;
next(x) := x + 0ud3_1;
init(y) := 0ud4_0;
next(y) := y + 0ud4_1;
LTLSPEC ! G F (x = 0ud3_7);

NuSMV -coi file.smv generates a counterexample only with variable x that goes from x = 0 to x = 7 and then loops back to x = 0. If we ask to re-execute the partial trace generated with execute_partial_traces than NuSMV complains that the trace cannot be completed with assignments to variable y. This because, from x = 7 & y = 7 we cannot go to x = 0 & y = 0. The counterexample for the whole system requires a path that goes from x = 0 & y = 0 to x = 7 & y = 15 that can loop back to x = 0 & y = 0 (which is the counterexample generated by when NuSMV called with cone of influence reduction disabled.

We remark that, the cone of influence reduction, as well as CTL/LTL model checking algorithms implemented in NuSMV assume the concrete model to be deadlock free.

The main reasons for deprecating processes in NuSMV are:

1. Correctness
   At the moment processes work correctly if the model does not contain any TRANS/INIT/INVAR.
   

   If any of such constructs occurs, than it is not easy to define the frame conditions of the processes which are not running. For this reason, the current implementation does not support correctly processes when relational constructs are used to model the behaviour.

2. Semantics of process hierarchies
   Having a process within another process has the non-intuitive behavior that only one of them can be active, while one may expect the inner one to be running if the father is running as well.
   

   Furthermore, definition of behaviours in SMV is not local, as it is possible to define the logics of a process from outside that process. The non-locality makes the definition of a clear semantics of processes even more complex.

3. Synchronism
   The core of NuSMV is made with synchronism in mind. Adapting it to support asynchronous processes adds complexity which has bad effects on the core structure.

For these reasons, we decided to aim for a direction where the core supports only synchronous systems, and the support for asynchronism is built on top of it, possibly out of NuSMV.

The idea is to have a semantically clear level (possibly providing an expressive user language) supporting asynchronous processes, with a well-defined mapping between this level and the SMV language supported by the core.

We are aware that this decision may make some users complain. However, we think that inertia in this case does not help, and we are firmly convinced that at the end of the transition NuSMV will be much more robust and effectively usable than now.

If you are using PSL operators such as "always", "never", "next", "next!", etc ..., parenthesizing may fix your problem, changing how the expression is parsed. Here there are some examples on how NuSMV parses PSL expressions:

1
2
3
4

MODULE main
VAR
x : boolean;
y : boolean;

1
2
3
4

PSLSPEC
always x -> next(y);
-- Parsed as:
-- always ((x -> next (y)))

1
2
3
4

PSLSPEC
always (!x -> next(y <-> x));
-- Parsed as:
-- always ((!x -> next ((y <-> x))))

1
2
3
4

PSLSPEC
always (!x -> (next(y) <-> x));
-- Parsed as:
-- always ((!x -> (next (y) <-> x)))

1
2
3
4

PSLSPEC
always (!x -> (next y <-> x));
-- Parsed as:
-- always ((!x -> (next (y) <-> x)))

1
2
3
4

PSLSPEC
always (!x -> ((next(y)) <-> x));
-- Parsed as:
-- always ((!x -> (next (y) <-> x)))

NuSMV provides a wide variety of optimization techniques. Here we list the most effective (see the commands documentation for details):

GENERAL TECHNIQUES

1. Use cone of influence. Depending on the properties to check, this can be very effective.
   (option: -coi)
2. Disable some features:
   • computation of reachable states (option: -df);
   • generation of counterexample traces (option: -dcx);

TECHNIQUES FOR SAT-BASED MODEL CHECKING

In general, SAT-based bounded model checking (bmc) is usually faster than BDD's one, especially for big models and for finding bugs. However, being able to conclude the property holds might be more complex for SAT-based bmc because of the need to use very large bounds.

• Use incremental algorithms (check_ltlspec_bmc_inc, check_ltlspec_sbmc_inc);

TECHNIQUES FOR BDD-BASED MODEL CHECKING

• Enable the dynamic variable reordering
  (option: -dynamic
  command: dynamic_var_ordering -e sift);

• Use an existing variable ordering file
  (option: -i <fname>);

• Disable BDD caching
  (command: set enable_sexp2bdd_caching 0);

• Tune the cache of the BDD package
  (command: set BDD."Hard limit for cache size" <new_value>);
  (command: set BDD."Cache hit threshold for resizing" <new_value>);
  (command: set BDD."Limit for fast unique table growth" <new_value>);
  (see cudd-2.4.1.1/doc/cudd.ps)

• Generate a variable ordering file. Follow this steps:
  
  1. enable dynamic reordering (option -dynamic);
     launch the long process for some time (few minutes, one hour, one day, depending on the problem size);
  2. interrupt computation with ctrl+c (it may not work under windows);
  3. dump the ordering file (command write_order);
  4. exit and restart the computation using the generated ordering file
     (option -i <fname>).

Notice that a-c steps can be iterated multiple times to try improving the quality of the ordering file, i.e. i-th iteration uses the ordering file generated by (i-1)-th as initial ordering.

There are two solutions:

1. USE A COMMAND FILE
   Write in a file, e.g. script.cmd, the commands you would use in interactive mode. Then you can do simply:

   1	NuSMV -source script.cmd model.smv

   Here is a brief example of a command file:

   1 2	set on_failure_script_quits go_bmc check_invarspec_bmc_inc -a falsification quit

   You can even combine batch commands and interactive commands:

   1	NuSMV [-batch_command1 -batch_command2 ...] -source script.cmd model.smv

2. USE PIPES
   On UNIX-like systems you can simply do:

   1 2	echo "set on_failure_script_quits; go_bmc; check_invarspec_bmc_inc -a \ falsification; quit" | NuSMV -int

   or

   1	$ cat script.cmd | NuSMV -int

   The command "set on_failure_script_quits" is very useful because, without it, if a non-fatal error occurs during the interactive mode, the interpreter simply stops the currently executed command, prints the reason of the problem, and prompts for a new command, blocking your script.

For further information, see NuSMV 2.5 User Manual, introduction of the Chapter 3 "Running NuSMV interactively".

You compiled NuSMV from source code, but when configured it could not find a suitable SAT solver, like Minisat.

The configuration phase actually warned you with a message like:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16

------------------------------------------------------------------
The MINISAT sat solver will NOT be linked to NuSMV.
If you want to link it, please use configure options
--enable-minisat, --with-minisat-libdir, --with-minisat-incdir.
For further help, try "./configure --help".
------------------------------------------------------------------

------------------------------------------------------------------
WARNING: No SAT solver will be linked to NuSMV.
WARNING: All NuSMV commands and options that depend on a SAT 
WARNING: solver will not be available.
WARNING: If you want to use SAT solver NuSMV features, please 
WARNING: compile and link the zchaff SAT solver or the MiniSat
WARNING: SAT solver.
WARNING: For further help, try "./configure --help".
------------------------------------------------------------------

Solution: you have to recompile nusmv and at least one SAT solver like Minisat or ZChaff. For further information refer to nusmv/README in the source distribution.