Compatibility with CMU SMV

NuSMV is mostly source compatible with the original version of SMV distributed at Carnegie Mellon University from which we started. The main problem you will run into is variable names in old programs that conflicts with new reserved words. In section New reserved words you will find the list of all the new reserved words of NuSMV with respect to CMU SMV.

The IMPLEMENTS, INPUT, OUTPUT statements are all parsed from the input file, but they are internally ignored.

NuSMV differs from CMU SMV also in the kind of formulas accepted as input. The main differences are listed below.

• It is no longer possible to write formulas containing nested `next'.

  TRANS
    next(alpha & next(beta | next(gamma))) -> delta
  

• It is no longer possible to write formulas containing `next' in the right hand side of "normal" and "init" assignments (they are allowed in the right hand side of "next" assignments), and with the statements `INVAR' and `INIT'.

  INVAR
    next(alpha) & beta
  INIT
    next(beta) -> alpha
  ASSIGN
    delta := alpha & next(gamma);       -- normal assignments
    init(gamma) := alpha & next(delta); -- init assignments
  

• It is no longer possible to write `SPEC', `FAIRNESS' statements containing `next'.

  FAIRNESS
   next(running)
  SPEC
   next(x) & y
  

• The check for circular dependencies among variables has been restricted. We say that variable x depends on variable y if x := f(y). We say that there is a circular dependency in the definition of x if:
  • x depends on itself ( e.g. x := f(x,y) );
  • x depends on y and y depends on x (e.g. x := f(y) and y := f(x) or x := f(z), z := f(y) and y := f(x) ).
  In the case of circular dependencies among variables there is no fixed order in which we can compute the involved variables. Avoiding circular dependencies among variables guarantee that there exists an order in which the variables can be computed. In NuSMV circular dependencies are not allowed. In CMU SMV the test for circular dependencies is able to detect circular dependencies only in "normal" assignments, and not in "next" assignments. The circular dependencies check of NuSMV has been extended to detect circularities also in "next" assignments. For instance the following fragment of code is accepted by CMU SMV but discarded by NuSMV.

  MODULE main
  VAR
    y : boolean;
    x : boolean;
  ASSIGN
    next(x) := x & next(y);
    next(y) := y & next(x);
  

In order to have full control on the ordering of variables the variable used to encode processes has been made explicit (in CMU SMV it is not possible to control the position in the ordering of such a variable. It is hardcoded at the top of the ordering.). Its name is _process_selector_.

Another difference between NuSMV and CMU SMV is in the variable order file. The variable ordering file accepted by NuSMV can be partial and can contain variables not declared in the model. Variables listed in the ordering file but not declared in the model are simply discarded. The variables declared in the model but not listed in the variable file provided in input are created at the end of the given ordering following the default ordering. All the ordering files generated by CMU SMV are accepted in input from NuSMV but the ordering files generated by NuSMV are not accepted in input to CMU SMV for free (it is necessary to remove the _process_selector_ variable. Notice that there is no guarantee that such ordering is a good ordering for CMU SMV.).

All the NuSMV programs that do not contain keywords regarding new features (such us LTL model checking, invariant checking, etc.) are accepted by CMU SMV.

With respect to the CMU SMV version from which we started (SMV 2.4.4), we treat the invariant defined via the `INVAR' statement.

Go to the first, previous, next, last section, table of contents.