nuXmv - The VMT Format

The VMT Format

The VMT format is an extension of the SMT-LIBv2 (SMT2 for short) format to represent symbolic transition systems.

The following example shows a simple nuXmv model (first one) and its corresponding VMT translation (second one).

nuXmv:

-- this is a comment
MODULE main
VAR x : integer;
INIT x = 1;
TRANS next(x) = x + 1;
INVARSPEC x > 0;

VMT:

; this is a comment
(declare-fun x () Int)
(declare-fun xn () Int)
(define-fun .sv0 () Int (! x :next xn))
(define-fun .init () Bool (! (= x 1) :init true))
(define-fun .trans () Bool (! (= xn (+ x 1)) :trans true))
(define-fun .p0 () Bool (! (> x 0) :invar-property 0))

VMT exploits the capability offered by the SMT2 language of attaching annotations to terms and formulas in order to specify the components of the transition system and the properties to verify. More specifically, the following annotations are used:

:next name is used to represent state variables. For each variable x in the model, the VMT file contains a pair of variables, x^c and xⁿ, representing respectively the current and next version of x. The two variables are linked by annotating x^c with the attribute :next xⁿ. All the variables that are not in relation with another by means of a :next attribute are considered inputs.
:init true is used to specify the formula for the initial states of the model. This formula should contain neither next-state variables nor input variables. (The “dummy” value true in the annotation is needed because the current SMT2 standard requires annotations to always have an associated value.)
:trans true is used to specify the formula for the transition relation.
:invar-property idx is used to specify invariant properties, i.e. formulas of the form G p, where p is the formula annotated with :invar-property. The non-negative integer idx is a unique identifier for the property.
:live-property idx is used to specify an LTL property of the form F G p, where p is the formula annotated with :live-property. The non-negative integer idx is a unique identifier for the property.

In a VMT file, only annotated terms and their sub-terms are meaningful. Any other term is ignored. Moreover, only the following commands are allowed to occur in VMT files: set-logic, set-option, declare-sort, define-sort, declare-fun, define-fun. (For convenience, an additional (assert true) command is allowed to appear at the end of the file.)

Since the SMT2 format (and thus also the VMT one that inherits from SMT2) does not allow to annotate the declaration of variables, it is a good practice to insert immediately after the declaration of the variables a set of defines to specify the relations among variables. See for instance the define .sv0 in the example above that introduces the relation between x and xⁿ.

In the distribution of the nuXmv (within directory contrib), we also provide conversion scripts from other formats (e.g. from the BTOR language of Boolector) to the language of the nuXmv and vice-versa.

nuXmv allows to dump a transition system specified in the nuXmv language in the VMT format using the write_vmt_model command. Below is a simple example of interaction with the shell of nuXmv to generate the VMT file from a nuXmv model saved in file.smv.

 shell > nuXmv -int file.smv
 nuXmv > go_msat; write_vmt_model -o file.vmt; quit

See the nuXmv User Manual (pdf) for further details.