Compatibility with CMU SMV

The NuSMV language is mostly source compatible with the original version of SMV distributed at Carnegie Mellon University from which we started. In this appendix we describe the most common problems that can be encountered when trying to use old CMU SMV programs with NuSMV.

The main problem is variable names in old programs that conflicts with new reserved words. The list of the new reserved words of NuSMV w.r.t. CMU SMV is the following:

F, G, X, U, V, W, H, O, Y, Z, S, T, B

These names are reserved for the LTL temporal operators.

LTLSPEC

It is used to introduce LTL specifications.

INVARSPEC

It is used to introduce invariant specifications.

IVAR

It is used to introduce input variables.

JUSTICE

It is used to introduce "justice" fairness constraints.

COMPASSION

It is used to introduce "compassion" fairness constraints.

The IMPLEMENTS, INPUT, OUTPUT statements are not supported by NuSMV. They are parsed from the input file, but are internally ignored.

NuSMV differs from CMU SMV also in the controls that are performed on the input formulas. Several formulas that are valid for CMU SMV, but that have no clear semantics, are not accepted by NuSMV. In particular:

• 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 done more restrictive. 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);
  

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 may be not accepted by CMU SMV. Notice that there is no guarantee that a good ordering for CMU SMV is also a good ordering for NuSMV. In the ordering files for NuSMV, identifier _process_selector_ can be used to control the position of the variable that encodes process selection. In CMU SMV it is not possible to control the position of this variable in the ordering; it is hard-coded at the top of the ordering.

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