## Languages.VMT History

Hide minor edits - Show changes to output - Cancel

Changed line 43 from:

a simple example of interaction with the shell of nuXmv to generate the VMT file from a nuXmv model.

to:

a simple example of interaction with the shell of nuXmv to generate the VMT file from a nuXmv model saved in @@file.smv@@.

Changed lines 45-46 from:

to:

@@shell > nuXmv -int file.smv@@\\

@@nuXmv > go_msat; write_vmt_model -o file.vmt; quit@@

@@nuXmv > go_msat; write_vmt_model -o file.vmt; quit@@

Changed lines 45-46 from:

@@nuXmv > go_msat; write_vmt_model -o file.vmt; quit@@\\

to:

@@shell > nuXmv -int file.smv@@\\

@@nuXmv > go_msat; write_vmt_model -o file.vmt; quit@@\\

@@nuXmv > go_msat; write_vmt_model -o file.vmt; quit@@\\

Changed lines 42-47 from:

nuXmv allows to dump a transition system specified in the nuXmv language in the VMT format using the @@write_vmt_model@@ command.\\

to:

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.

@@shell > nuXmv -int file.smv@@\\

@@nuXmv > go_msat; write_vmt_model -o file.vmt; quit@@\\

a simple example of interaction with the shell of nuXmv to generate the VMT file from a nuXmv model.

@@shell > nuXmv -int file.smv@@\\

@@nuXmv > go_msat; write_vmt_model -o file.vmt; quit@@\\

Changed line 40 from:

In the distribution of the nuXmv (within directory contrib), we also provide conversion scripts from other formats (e.g.~~ the~~ from the [[http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf|BTOR]] language of [[http://fmv.jku.at/boolector|Boolector]]) to the language of the nuXmv and vice-versa.

to:

In the distribution of the nuXmv (within directory contrib), we also provide conversion scripts from other formats (e.g. from the [[http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf|BTOR]] language of [[http://fmv.jku.at/boolector|Boolector]]) to the language of the nuXmv and vice-versa.

Deleted lines 4-12:

* '''@@: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'^n^'@@, representing respectively the current and next version of @@x@@. The two variables are linked by annotating @@x'^c^'@@ with the attribute @@:next x'^n^'@@. 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.)

Added lines 26-35:

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'^n^'@@, representing respectively the current and next version of @@x@@. The two variables are linked by annotating @@x'^c^'@@ with the attribute @@:next x'^n^'@@. 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.)

Changed line 41 from:

nuXmv allows to dump a transition system specified in the nuXmv language in the VMT format using the @@write_vmt_model@@ command.\\~~ ~~

to:

nuXmv allows to dump a transition system specified in the nuXmv language in the VMT format using the @@write_vmt_model@@ command.\\

Changed line 18 from:

(:head bgcolor=#~~cccc99~~ :) VMT

to:

(:head bgcolor=#D8D8D8 :) VMT

Changed line 17 from:

(:head bgcolor=#~~cccc99~~ :) nuXmv

to:

(:head bgcolor=#D8D8D8 :) nuXmv

Changed lines 17-18 from:

(:head~~:) nuXmv~~

~~(~~:~~head:)~~ VMT

to:

(:head bgcolor=#cccc99 :) nuXmv

(:head bgcolor=#cccc99 :) VMT

(:head bgcolor=#cccc99 :) VMT

Changed line 41 from:

nuXmv allows to dump a transition system specified in the nuXmv language in the VMT format using the @@write_vmt_model@@ command.

to:

Changed lines 41-42 from:

nuXmv allows to dump a transition system specified in the nuXmv language in the VMT format using the @@write_vmt_model@@ command ~~(see~~ the ~~nuXmv ~~user~~ ~~manual ~~for further details)~~.

to:

nuXmv allows to dump a transition system specified in the nuXmv language in the VMT format using the @@write_vmt_model@@ command.

See the [[https://es.fbk.eu/tools/nuxmv/downloads/nuxmv-user-manual.pdf|nuXmv User Manual]] ([[https://es.fbk.eu/tools/nuxmv/downloads/nuxmv-user-manual.pdf|pdf]]) for further details.

See the [[https://es.fbk.eu/tools/nuxmv/downloads/nuxmv-user-manual.pdf|nuXmv User Manual]] ([[https://es.fbk.eu/tools/nuxmv/downloads/nuxmv-user-manual.pdf|pdf]]) for further details.

Changed lines 39-41 from:

In the distribution of the nuXmv (within directory contrib), we also provide conversion scripts from other formats (e.g. the from the [[http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf|BTOR]] language of [[http://fmv.jku.at/boolector|Boolector]]) to the language of the nuXmv and vice-versa.

to:

In the distribution of the nuXmv (within directory contrib), we also provide conversion scripts from other formats (e.g. the from the [[http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf|BTOR]] language of [[http://fmv.jku.at/boolector|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 (see the nuXmv user manual for further details).

nuXmv allows to dump a transition system specified in the nuXmv language in the VMT format using the @@write_vmt_model@@ command (see the nuXmv user manual for further details).

Changed lines 6-7 from:

* ''':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'^n^'@@, representing respectively the current and next version of @@x@@. The two variables are linked by annotating @@x'^c^'@@ with the attribute @@:next x'^n^'@@. 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.)

*''':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.)

to:

* '''@@: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'^n^'@@, representing respectively the current and next version of @@x@@. The two variables are linked by annotating @@x'^c^'@@ with the attribute @@:next x'^n^'@@. 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.)

*''':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.)

Changed line 39 from:

In the distribution of the nuXmv (within directory contrib), we also provide conversion scripts from other formats (e.g. the from the [[http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf|BTOR]] language of [[http://fmv.jku.at/boolector|Boolector]] to the language of the nuXmv and vice-versa.

to:

In the distribution of the nuXmv (within directory contrib), we also provide conversion scripts from other formats (e.g. the from the [[http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf|BTOR]] language of [[http://fmv.jku.at/boolector|Boolector]]) to the language of the nuXmv and vice-versa.

Changed line 6 from:

* ''':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'~~^n^'~~''~~, representing respectively the current and next version of ~~''~~x~~''~~. The two variables are linked by annotating '~~'x'~~^c^'~~''~~ with the attribute ''~~:next x'^n^'''. ~~All the variables that are not in relation with another by means of a ~~''~~:next~~''~~ attribute are considered inputs.

to:

* ''':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'^n^'@@, representing respectively the current and next version of @@x@@. The two variables are linked by annotating @@x'^c^'@@ with the attribute @@:next x'^n^'@@. All the variables that are not in relation with another by means of a @@:next@@ attribute are considered inputs.

Changed lines 9-13 from:

*''':invar-property ~~''~~idx'''~~''~~ is used to specify invariant properties, i.e. formulas of the form ''~~Gp~~'', 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 ''~~FGp~~'', 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.)

*''':live-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:

to:

*''':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.)

*''':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.)

Changed line 37 from:

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'~~^n^'~~''~~.

to:

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'^n^'@@.

Changed lines 24-25 from:

INVARSPEC x > 0;~~\\~~@@

to:

INVARSPEC x > 0;@@

Changed line 32 from:

(define-fun .p0 () Bool (! (> x 0) :invar-property 0))~~\\~~@@

to:

(define-fun .p0 () Bool (! (> x 0) :invar-property 0))@@

Changed lines 16-24 from:

||!

||

||MODULE main ||

||VAR x : integer

||INIT x = 1; ||

||TRANS next

||INVARSPEC x > 0; ||

||

to:

(:table border=1 cellpadding=5 cellspacing=0:)

(:head:) nuXmv

(:head:) VMT

(:cellnr:) @@-- this is a comment\\

MODULE main\\

VAR x : integer;\\

INIT x = 1;\\

TRANS next(x) = x + 1;\\

INVARSPEC x > 0;\\@@

(:cell:) @@; 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))\\@@

(:tableend:)

(:head:) nuXmv

(:head:) VMT

(:cellnr:) @@-- this is a comment\\

MODULE main\\

VAR x : integer;\\

INIT x = 1;\\

TRANS next(x) = x + 1;\\

INVARSPEC x > 0;\\@@

(:cell:) @@; 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))\\@@

(:tableend:)

Changed lines 6-10 from:

to:

* ''':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'^n^''', representing respectively the current and next version of ''x''. The two variables are linked by annotating ''x'^c^''' with the attribute '':next x'^n^'''. 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 ''Gp'', 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 ''FGp'', where ''p'' is the formula annotated with '':live-property''. The non-negative integer ''idx'' is a unique identifier for the property.

*''':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 ''Gp'', 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 ''FGp'', where ''p'' is the formula annotated with '':live-property''. The non-negative integer ''idx'' is a unique identifier for the property.

Changed line 16 from:

||border=1 rules=cols~~ frame=vsides~~

to:

||border=1 rules=cols

Changed line 6 from:

->''':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'^n^''', representing respectively the current and next version of ''x''. The two variables are linked by annotating ~~xc with the attribute ~~''~~:next ~~x'^~~n~~^''' . All the variables that are not in relation with another by means of a '':next'' attribute are considered inputs.

to:

->''':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'^n^''', representing respectively the current and next version of ''x''. The two variables are linked by annotating ''x'^c^''' with the attribute '':next x'^n^'''. All the variables that are not in relation with another by means of a '':next'' attribute are considered inputs.

Changed line 26 from:

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 ~~xn~~.

to:

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'^n^'''.

Changed line 16 from:

||border=1 rules=cols frame=vsides ~~||~~

to:

||border=1 rules=cols frame=vsides

Changed line 16 from:

||border=1 rules=cols frame=~~vsides~~

to:

||border=1 rules=cols frame=vsides ||

Added lines 16-30:

||border=1 rules=cols frame=vsides

||!nuXmv || !VMT ||

||-- this is a comment ||; this is a comment ||

||MODULE main ||(declare-fun x () Int) ||

||VAR x : integer; ||(declare-fun xn () Int) ||

||INIT x = 1; ||(define-fun .sv0 () Int (! x :next xn)) ||

||TRANS next(x) = x + 1; ||(define-fun .init () Bool (! (= x 1) :init true)) ||

||INVARSPEC x > 0; ||(define-fun .trans () Bool (! (= xn (+ x 1)) :trans true)) ||

|| ||(define-fun .p0 () Bool (! (> x 0) :invar-property 0)) ||

||!nuXmv || !VMT ||

||-- this is a comment ||; this is a comment ||

||MODULE main ||(declare-fun x () Int) ||

||VAR x : integer; ||(declare-fun xn () Int) ||

||INIT x = 1; ||(define-fun .sv0 () Int (! x :next xn)) ||

||TRANS next(x) = x + 1; ||(define-fun .init () Bool (! (= x 1) :init true)) ||

||INVARSPEC x > 0; ||(define-fun .trans () Bool (! (= xn (+ x 1)) :trans true)) ||

|| ||(define-fun .p0 () Bool (! (> x 0) :invar-property 0)) ||

Changed line 35 from:

In the distribution of the nuXmv (within directory contrib), we also provide conversion scripts from other formats (e.g. the from the [[http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf|BTOR]] language of [[http://fmv.jku.at/boolector|Boolector]] to the language of the nuXmv and vice-versa.

to:

In the distribution of the nuXmv (within directory contrib), we also provide conversion scripts from other formats (e.g. the from the [[http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf|BTOR]] language of [[http://fmv.jku.at/boolector|Boolector]] to the language of the nuXmv and vice-versa.

Changed lines 6-7 from:

->''':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 ~~xn~~, representing respectively the current and next version of x. The two variables are

~~linked~~ by annotating xc with the attribute :next ~~xn~~ . All the variables that are not in relation with another by means of a :next attribute are considered inputs.

to:

->''':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'^n^''', representing respectively the current and next version of ''x''. The two variables are linked by annotating xc with the attribute '':next x'^n^''' . All the variables that are not in relation with another by means of a '':next'' attribute are considered inputs.

Changed lines 9-12 from:

->''':invar-property ''idx''''' is used to specify invariant properties, i.e. formulas of the form Gp, 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 Gp, ~~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.)

->''':live-property ''idx''''' is used to specify an LTL property of the form

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.

to:

->''':invar-property ''idx''''' is used to specify invariant properties, i.e. formulas of the form ''Gp'', 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 ''FGp'', 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.)

->''':live-property ''idx''''' is used to specify an LTL property of the form ''FGp'', 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.)

Changed line 6 from:

->''':next name''' is used to represent state variables. For each variable ''x'' in the model, the VMT file contains a pair of variables, ~~xc~~ and xn, representing respectively the current and next version of x. The two variables are

to:

->''':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 xn, representing respectively the current and next version of x. The two variables are

Changed line 6 from:

->''':next name''' is used to represent state variables. For each variable x in the model, the VMT file contains a pair of variables, xc and xn, representing respectively the current and next version of x. The two variables are

to:

->''':next name''' is used to represent state variables. For each variable ''x'' in the model, the VMT file contains a pair of variables, xc and xn, representing respectively the current and next version of x. The two variables are

Changed line 6 from:

->''':next name''' is used to represent state variables. For each variable x in the model, the VMT file contains a pair of variables, xc and xn~~ ~~, representing respectively the current and next version of x. The two variables are

to:

->''':next name''' is used to represent state variables. For each variable x in the model, the VMT file contains a pair of variables, xc and xn, representing respectively the current and next version of x. The two variables are

Changed line 6 from:

->:next name is used to represent state variables. For each variable x in the model, the VMT file contains a pair of variables, xc and xn , representing respectively the current and next version of x. The two variables are

to:

->''':next name''' is used to represent state variables. For each variable x in the model, the VMT file contains a pair of variables, xc and xn , representing respectively the current and next version of x. The two variables are

Changed lines 8-12 from:

->: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 Gp, 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 Gp, where p is the formula annotated with :live-property. The non-negative integer idx is a unique identifier for the property.

->: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 Gp, 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 Gp, where p is the formula annotated with :live-property. The non-negative integer idx is a unique identifier for the property.

to:

->''':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 Gp, 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 Gp, where p is the formula annotated with :live-property. The non-negative integer idx is a unique identifier for the property.

->''':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 Gp, 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 Gp, where p is the formula annotated with :live-property. The non-negative integer idx is a unique identifier for the property.

Changed lines 15-16 from:

The following example shows a simple ~~NU X MV~~ model (left) and its corresponding VMT translation (right).

to:

The following example shows a simple nuXmv model (left) and its corresponding VMT translation (right).

Changed line 21 from:

In the distribution of the ~~NU X MV (within directory ~~contrib), we also provide conversion scripts from other formats (e.g. the from the ~~BTOR language of Boolector ~~[~~Boo~~] ~~to the language of~~ the ~~NU X MV~~ and vice-versa.

to:

Changed line 3 from:

The VMT format is an extension of the ~~SMT-LIBv2 ~~[~~BST12~~] (SMT2 for short) format to represent ~~symbolictransition~~ systems.

to:

The '''VMT''' format is an extension of the [[http://smtlib.cs.uiowa.edu|SMT-LIBv2]] (SMT2 for short) format to represent symbolic transition systems.

Changed lines 3-21 from:

to:

The VMT format is an extension of the SMT-LIBv2 [BST12] (SMT2 for short) format to represent symbolictransition systems.

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, xc and xn , representing respectively the current and next version of x. The two variables are

linked by annotating xc with the attribute :next xn . 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 Gp, 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 Gp, 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.)

The following example shows a simple NU X MV model (left) and its corresponding VMT translation (right).

table here

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 xn.

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

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, xc and xn , representing respectively the current and next version of x. The two variables are

linked by annotating xc with the attribute :next xn . 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 Gp, 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 Gp, 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.)

The following example shows a simple NU X MV model (left) and its corresponding VMT translation (right).

table here

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 xn.

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