We present now the complete syntax of the input language of
NuSMV. In the following, an atom may be any sequence of
characters starting with a character in the set {A-Za-z_} and
followed by a possibly empty sequence of characters belonging to the set
{A-Za-z0-9_\$#-}.
A number is any sequence of digits. A digit belongs to the set
{0-9}.
All characters and case in a name are significant. Whitespace
characters are space (SPACE), tab (TAB) and
newline (RET). @cindex comments in NuSMV language
Any string starting with two dashes (`--') and
ending with a newline is a comment. Any other tokens recognized by the
parser are enclosed in quotes in the syntax expressions below.
Grammar productions enclosed in square brackets (`[]') are
optional.
Expressions are constructed from variables, constants, and a collection of operators, including boolean connectives, integer arithmetic operators, case expressions and set expressions.
Simple expressions are expressions built only from current state variables. Simple expressions can be used to specify sets of states, e.g. the initial set of states. The syntax of simple expressions is as follows:
simple_expr ::
atom ;; a symbolic constant
| number ;; a numeric constant
| "TRUE" ;; The boolean constant 1
| "FALSE" ;; The boolean constant 0
| var_id ;; a variable identifier
| "(" simple_expr ")"
| "!" simple_expr ;; logical not
| simple_expr "&" simple_expr ;; logical and
| simple_expr "|" simple_expr ;; logical or
| simple_expr "xor" simple_expr ;; logical exclusive or
| simple_expr "->" simple_expr ;; logical implication
| simple_expr "<->" simple_expr ;; logical equivalence
| simple_expr "=" simple_expr ;; equality
| simple_expr "!=" simple_expr ;; inequality
| simple_expr "<" simple_expr ;; less than
| simple_expr ">" simple_expr ;; greater than
| simple_expr "<=" simple_expr ;; less than or equal
| simple_expr ">=" simple_expr ;; greater than or equal
| simple_expr "+" simple_expr ;; integer addition
| simple_expr "-" simple_expr ;; integer subtraction
| simple_expr "*" simple_expr ;; integer multiplication
| simple_expr "/" simple_expr ;; integer division
| simple_expr "mod" simple_expr ;; integer remainder
| set_simple_expr ;; a set simple_expression
| case_simple_expr ;; a case expression
A var_id, (see section Identifiers) or identifier, is a symbol or
expression which identifies an object, such as a variable or a defined
symbol. Since a var_id can be an atom, there is a possible
ambiguity if a variable or defined symbol has the same name as a
symbolic constant. Such an ambiguity is flagged by the interpreter as an
error.
The order of parsing precedence for operators from high to low is:
*,/ +,- mod =,!=,<,>,<=,>= ! & |,xor <-> ->
Operators of equal precedence associate to the left, except -> that
associates to the right.
Parentheses may be used to group expressions.
A case expression has the following syntax:
case_simple_expr ::
"case"
simple_expr ":" simple_expr ";"
simple_expr ":" simple_expr ";"
...
simple_expr ":" simple_expr ";"
"esac"
A case_simple_expr returns the value of the first expression on
the right hand side of `:', such that the corresponding
condition on the left hand side evaluates to 1. Thus, if
simple_expr on the left side is true, then the result is the
corresponding simple_expr on the right side. If none of the
expressions on the left hand side evaluates to 1, the result of
the case_expression is the numeric value 1. It is an error
for any expression on the left hand side to return a value other than
the truth values 0 or 1.
A set expression has the following syntax:
set_expr ::
"{" set_elem "," ... "," set_elem "}" ;; set definition
| simple_expr "in" simple_expr ;; set inclusion test
| simple_expr "union" simple_expr ;; set union
set_elem :: simple_expr
A set can be defined by enumerating its elements inside
curly braces `{...}'. The inclusion operator `in'
tests a value for membership in a set. The union operator
`union' takes the union of two sets. If either argument is a
number or a symbolic value instead of a set, it is coerced to a
singleton set.
While simple expressions can represent sets of states, next expressions relate current and next state variables to express transitions in the FSM. The structure of next expressions is similar to the structure of simple expressions (See section Simple Expressions). The difference is that next expression allow to refer to next state variables. The grammar is depicted below.
next_expr ::
atom ;; a symbolic constant
| number ;; a numeric constant
| "TRUE" ;; The boolean constant 1
| "FALSE" ;; The boolean constant 0
| var_id ;; a variable identifier
| "(" next_expr ")"
| "next" "(" simple_expr ")" ;; next value of an "expression"
| "!" next_expr ;; logical not
| next_expr "&" next_expr ;; logical and
| next_expr "|" next_expr ;; logical or
| next_expr "xor" next_expr ;; logical exclusive or
| next_expr "->" next_expr ;; logical implication
| next_expr "<->" next_expr ;; logical equivalence
| next_expr "=" next_expr ;; equality
| next_expr "!=" next_expr ;; inequality
| next_expr "<" next_expr ;; less than
| next_expr ">" next_expr ;; greater than
| next_expr "<=" next_expr ;; less than or equal
| next_expr ">=" next_expr ;; greater than or equal
| next_expr "+" next_expr ;; integer addition
| next_expr "-" next_expr ;; integer subtraction
| next_expr "*" next_expr ;; integer multiplication
| next_expr "/" next_expr ;; integer division
| next_expr "mod" next_expr ;; integer remainder
| set_next_expr ;; a set next_expression
| case_next_expr ;; a case expression
set_next_expr and case_next_expr are the same
as set_simple_expr (see section Set Expressions) and
case_simple_expr (see section Case Expressions) respectively, with the
replacement of "simple" with "next".
The only additional production is "next" "(" simple_expr ")",
which allows to "shift" all the variables in simple_expr to the
next state. The next operator distributes on every
operator. For instance, the formula next((A & B) | C) is a
shorthand for the formula (next(A) & next(B)) | next(C). It is
an error if in the scope of the next operator occurs another
next operator.
A state of the model is an assignment of values to a set of state variables. These variables (and also instances of modules) are declared by the notation:
var_declaration :: "VAR"
atom ":" type ";"
atom ":" type ";"
...
The type associated with a variable declaration can be either a boolean, a scalar, a user defined module, or an array of any of these (including arrays of arrays).
A type specifier has the syntax:
type ::boolean| "{" val "," val "," ... val "}" | number ".." number | "array" number ".." number "of" type | atom [ "(" simple_expr "," simple_expr "," ... ")" ] | "process" atom [ "(" simple_expr "," ... "," simple_expr ")" ] val :: atom | number
A variable of type boolean can take on the numerical values
0 and 1 (representing false and true, respectively). In
the case of a list of values enclosed in quotes (where atoms are taken
to be symbolic constants), the variable is a scalar which take any of
these values. In the case of an array declaration, the first
simple_expr is the lower bound on the subscript and the second
simple_expr is the upper bound. Both of these expressions must
evaluate to integer constants. Finally, an atom optionally followed by
a list of expressions in parentheses indicates an instance of module
atom (See section MODULE declarations). The keyword causes the module to
be instantiated as an asynchronous process (See section Processes).
A state of the model is an assignment of values to a set of state variables. These variables (and also instances of modules) are declared by the notation:
ivar_declaration :: "IVAR"
atom ":" type ";"
atom ":" type ";"
...
The type associated with a variable declaration can be either a boolean, a scalar, a user defined module, or an array of any of these (including arrays of arrays) (See section State Variables).
ASSIGN declarationsAn assignment has the form:
assign_declaration :: "ASSIGN"
assign_body ";"
assign_body ";"
...
assign_body ::
atom ":=" simple_expr ;; normal assignment
| "init" "(" atom ")" ":=" simple_expr ;; init assignment
| "next" "(" atom ")" ":=" next_expr ;; next assignment
On the left hand side of the assignment, atom denotes the current value of a variable, `init(atom)' denotes its initial value, and `next(atom)' denotes its value in the next state. If the expression on the right hand side evaluates to an integer or symbolic constant, the assignment simply means that the left hand side is equal to the right hand side. On the other hand, if the expression evaluates to a set, then the assignment means that the left hand side is contained in that set. It is an error if the value of the expression is not contained in the range of the variable on the left hand side.
In order for a program to be implementable, there must be some order in which the assignments can be executed such that no variable is assigned after its value is referenced. This is not the case if there is a circular dependency among the assignments in any given process. Hence, such a condition is an error. It is also an error for a variable to be assigned more than once at any given time. More precisely, it is an error if:
TRANS declarations
The transition relation R of the model is a set of current state/next
state pairs. Whether or not a given pair is in this set is determined by
a boolean valued expression T, introduced by the `TRANS' keyword. The
syntax of a TRANS declaration is:
trans_declaration :: "TRANS" trans_expr [";"]
trans_expr :: next_expr
It is an error for the expression to yield any value other than 0
or 1. If there is more than one TRANS declaration, the
transition relation is the conjunction of all of TRANS
declarations.
INIT declarations
The set of initial states of the model is determined by a boolean expression
under the `INIT' keyword. The syntax of a INIT declaration is:
init_declaration :: "INIT" init_expr [";"]
init_expr :: simple_expr
It is an error for the expression to contain the next() operator,
or to yield any value other than 0 or 1. If there is more
than one INIT declaration, the initial set is the conjunction of
all of the INIT declarations.
INVAR declarations
The set of invariant states (i.e. the analogous of normal assignments,
as described in section ASSIGN declarations) can be specified using a
boolean expression under the `INVAR' keyword. The syntax of a
INVAR declaration is:
invar_declaration :: "INVAR" invar_expr [";"]
invar_expr :: simple_expr
It is an error for the expression to contain the next() operator,
or to yield any value other than 0 or 1. If there is more
than one INVAR declaration, the invariant set is the conjunction of
all of the INVAR declarations.
DEFINE declarationsIn order to make descriptions more concise, a symbol can be associated with a commonly expression. The syntax for this kind of declaration is:
define_declaration :: "DEFINE"
atom ":=" simple_expr ";"
atom ":=" simple_expr ";"
...
atom ":=" simple_expr ";"
Whenever an identifier referring to the symbol on the left hand side of
the `:=' in a DEFINE occurs in an expression, it is
replaced by the expression on the right hand side. The expression on the
right hand side is always evaluated in its context, however
(see section MODULE declarations for an explanation of contexts). Forward
references to defined symbols are allowed, but circular definitions are not
allowed, and result in an error.
It is not possible to assign values to defined symbols non-deterministically. Another difference between defined symbols and variables is that while variables are statically typed, definitions are not.
ISA declarations
There are cases in which some parts of a module could be shared among
different modules, or could be used as a module themselves. In
NuSMV it is possible to declare the common parts as separate
modules, and then use the ISA declaration to import the common
parts inside a module declaration.
The syntax of an ISA declaration is as follows:
isa_declaration :: "ISA" atom
where atom must be the name of a declared module.
The ISA declaration can be thought as a simple macro expansion
command, because the body of the module referenced by an ISA
command is replaced to the ISA declaration.
MODULE declarationsA module is an encapsulated collection of declarations. Once defined, a module can be reused as many times as necessary. Modules can also be so that each instance of a module can refer to different data values. A module can contain instances of other modules, allowing a structural hierarchy to be built.
The syntax of a module declaration is as follows.
module ::
"MODULE" atom [ "(" atom "," atom "," ... atom ")" ]
[ var_declaration ]
[ ivar_declaration ]
[ assign_declaration ]
[ trans_declaration ]
[ init_declaration ]
[ invar_declaration ]
[ spec_declaration ]
[ checkinvar_declaration ]
[ ltlspec_declaration ]
[ compute_declaration ]
[ fairness_declaration ]
[ define_declaration ]
[ isa_declaration ]
The atom immediately following the keyword "MODULE" is
the name associated with the module. Module names are drawn from a
separate name space from other names in the program, and hence may
clash with names of variables and definitions. The optional list of
atoms in parentheses are the formal parameters of the module. Whenever
these parameters occur in expressions within the module, they are
replaced by the actual parameters which are supplied when the module
is instantiated (see below).
An instance of a module is created using the VAR
declaration (see section State Variables). This declaration supplies a name
for the instance, and also a list of actual parameters, which are
assigned to the formal parameters in the module definition. An actual
parameter can be any legal expression. It is an error if the number of
actual parameters is different from the number of formal
parameters. The semantic of module instantiation is similar to
call-by-reference. For example, in the following program fragment:
MODULE main ... VAR a : boolean; b : foo(a); ... MODULE foo(x) ASSIGN x := 1;
the variable a is assigned the value 1. This
distinguishes the call-by-reference mechanism from a call-by-value
scheme.
Now consider the following program:
MODULE main ... DEFINE a := 0; VAR b : bar(a); ... MODULE bar(x) DEFINE a := 1; y := x;
In this program, the value of y is 0. On the
other hand, using a call-by-name mechanism, the value of y would
be 1, since a would be substituted as an expression for
x.
Forward references to module names are allowed, but circular references are not, and result in an error.
An id, or identifier, is an expression which references an
object. Objects are instances of modules, variables, and defined
symbols. The syntax of an identifier is as follows.
id ::
atom
| "self"
| id "." atom
| id "[" simple_expr "]"
An atom identifies the object of that name as defined in a
VAR or DEFINE declaration. If a identifies an
instance of a module, then the expression `a.b' identifies
the component object named `b' of instance `a'. This
is precisely analogous to accessing a component of a structured data
type. Note that an actual parameter of module `a' can
identify another module instance `b', allowing `a'
to access components of `b', as in the following example:
... VAR a : foo(b); b : bar(a); ... MODULE foo(x) DEFINE c := x.p | x.q; MODULE bar(x) VAR p : boolean; q : boolean;
Here, the value of `c' is the logical or of `p' and `q'.
If `a' identifies an array, the expression `a[b]' identifies element `b' of array `a'. It is an error for the expression `b' to evaluate to a number outside the subscript bounds of array `a', or to a symbolic value.
It is possible to refer the name the current module has been
instantiated to by using the self builtin identifier.
MODULE element(above, below, token) VAR Token : boolean; ASSIGN init(Token) := token; next(Token) := token-in; DEFINE above.token-in := Token; grant-out := below.grant-out; MODULE cell VAR e2 : element(self, e1, 0); e1 : element(e1 , self, 1); DEFINE e1.token-in := token-in; grant-out := grant-in & !e1.grant-out; MODULE main VAR c1 : cell;
In this example the name the cell module has been instantiated to
is passed to the submodule element. In the main module,
declaring c1 to be an instance of module cell and defining
above.token-in in module e2, really amounts to defining
the symbol c1.token-in. When you, in the cell module,
declare e1 to be an instance of module element, and you
define grant-out in module e1 to be
below.grant-out, you are really defining it to be the symbol
c1.grant-out.
main module
The syntax of a NuSMV program is:
program ::
module_1
module_2
...
module_n
There must be one module with the name main and no formal parameters.
The module main is the one evaluated by the interpreter.
Processes are used to model interleaving concurrency. A process
is a module which is instantiated using the keyword `process'
(see section State Variables). The program executes a step by
non-deterministically choosing a process, then executing all of the
assignment statements in that process in parallel. It is implicit that
if a given variable is not assigned by the process, then its value
remains unchanged. Each instance of a process has a special boolean
variable associated with it called running.
The value of this variable is 1 if and only if the process
instance is currently selected for execution.
A process may run only when its parent is running. In addition no two
processes with the same parents may be running at the same time.
FAIRNESS declarationsA fairness constraint restricts the attention only to fair execution paths. When evaluating specifications, the model checker considers path quantifiers to apply only to fair paths.
NuSMV supports two types of fairness constraints, namely justice
constraints and compassion constraints.
A justice constraint consists of a formula f which is
assumed to be true infinitely often in all the fair paths. In
NuSMV justice constraints are identified by keywords
JUSTICE and, for backward compatibility, FAIRNESS.
A compassion constraint consists of a pair of formulas
(p,q); if property p is true infinitely often in a fair
path, then also formula q has to be true infinitely often in the
fair path. In NuSMV compassion constraints are identified by
keyword COMPASSION.(3)
Fairness constraints are declared using the following syntax:
fairness_declaration ::
"FAIRNESS" simple_expr [";"]
| "JUSTICE" simple_expr [";"]
| "COMPASSION" "(" simple_expr "," simple_expr ")" [";"]
A path is considered fair if and only if it satisfies all the constraints declared in this manner.
The specifications to be checked on the FSM can be expressed in two different temporal logics: the Computation Tree Logic CTL, and the Linear Temporal Logic LTL extended with Past Operators. It is also possible to analyze quantitative characteristics of the FSM by specifying real-time CTL specifications. Specifications can be positioned within modules, in which case they are preprocessed to rename the variables according to the containing context.
CTL and LTL specifications are evaluated by NuSMV in order to
determine their truth or falsity in the FSM. When a
specification is discovered to be false, NuSMV constructs and
prints a counterexample, i.e. a trace of the FSM that
falsifies the property.
A CTL specification is given as a formula in the temporal logic CTL, introduced by the keyword `SPEC'. The syntax of this declaration is:
spec_declaration :: "SPEC" spec_expr [";"]
spec_expr :: ctl_expr
The syntax of CTL formulas recognized by the NuSMV parser is
as follows:
ctl_expr ::
simple_expr ;; a simple boolean expression
| "(" ctl_expr ")"
| "!" ctl_expr ;; logical not
| ctl_expr "&" ctl_expr ;; logical and
| ctl_expr "|" ctl_expr ;; logical or
| ctl_expr "xor" ctl_expr ;; logical exclusive or
| ctl_expr "->" ctl_expr ;; logical implies
| ctl_expr "<->" ctl_expr ;; logical equivalence
| "EG" ctl_expr ;; exists globally
| "EX" ctl_expr ;; exists next state
| "EF" ctl_expr ;; exists finally
| "AG" ctl_expr ;; forall globally
| "AX" ctl_expr ;; forall next state
| "AF" ctl_expr ;; forall finally
| "E" "[" ctl_expr "U" ctl_expr "]" ;; exists until
| "A" "[" ctl_expr "U" ctl_expr "]" ;; forall until
It is an error for an expressions in a CTL formula to contain a
`next()' operator, or to have non-boolean components, i.e.
subformulas which evaluate to a value other than 0 or 1.
It is also possible to specify invariants, i.e. propositional formulas which must hold invariantly in the model. The corresponding command is `INVARSPEC', with syntax:
checkinvar_declaration :: "INVARSPEC" simple_expr ";"
This statement corresponds to
SPEC AG simple_expr ";"
but can be checked by a specialized algorithm during reachability analysis.
LTL specifications are introduced by the keyword `LTLSPEC'. The syntax of this declaration is:
ltlspec_declaration :: "LTLSPEC" ltl_expr [";"]
where
ltl_expr ::
simple_expr ;; a simple boolean expression
| "(" ltl_expr ")"
| "!" ltl_expr ;; logical not
| ltl_expr "&" ltl_expr ;; logical and
| ltl_expr "|" ltl_expr ;; logical or
| ltl_expr "xor" ltl_expr ;; logical exclusive or
| ltl_expr "->" ltl_expr ;; logical implies
| ltl_expr "<->" ltl_expr ;; logical equivalence
;; FUTURE
| "X" ltl_expr ;; next state
| "G" ltl_expr ;; globally
| "F" ltl_expr ;; finally
| ltl_expr "U" ltl_expr ;; until
| ltl_expr "V" ltl_expr ;; releases
;; PAST
| "Y" ltl_expr ;; previous state
| "Z" ltl_expr ;; not previous state not
| "H" ltl_expr ;; historically
| "O" ltl_expr ;; once
| ltl_expr "S" ltl_expr ;; since
| ltl_expr "T" ltl_expr ;; triggered
In NuSMV, LTL specifications can be analyzed both by means of
BDD-based reasoning, or by means of SAT-based bounded model checking. In
the first case, NuSMV proceeds along the lines described in
[CGH97]. For each LTL specification, a tableau able to recognize
the behaviors falsifying the property is constructed, and then
synchronously composed with the model. With respect to [CGH97],
the approach is fully integrated within NuSMV, and allows for
full treatment of past temporal operators. In the
case of BDD-based reasoning, the counterexample generated to show the
falsity of a LTL specification may contain state variables which have
been introduced by the tableau construction procedure.
In the second case, a similar tableau construction is carried out to
encode the existence of a path of limited length violating the
property. NuSMV generates a propositional satisfiability problem,
that is then tackled by means of an efficient SAT solver [BCCZ99].
In both cases, the tableau constructions are completely transparent to the user.
NuSMV allows for Real Time CTL specifications
[EMSS90]. NuSMV assumes that each transition takes unit
time for execution. RTCTL extends the syntax of CTL path expressions
with the following bounded modalities:
rtctl_expr ::
ctl_expr
| "EBF" range rtctl_expr
| "ABF" range rtctl_expr
| "EBG" range rtctl_expr
| "ABG" range rtctl_expr
| "A" "[" rtctl_expr "BU" range rtctl_expr "]"
| "E" "[" rtctl_expr "BU" range rtctl_expr "]"
range :: number ".." number"
Intuitively, in the formula E [ a BU m..n b ]
m (n, resp.) represents the minimum (maximum) number of
permitted transition along a path of a structure before the eventuality
holds.
Real time CTL specifications can be defined with the following syntax, which extends the syntax for CTL specifications.
spec_declaration :: "SPEC" rtctl_expr [";"]
With the `COMPUTE' statement, it is also possible to compute quantitative information on the FSM. In particular, it is possible to compute the exact bound on the delay between two specified events, expressed as CTL formulas. The syntax is the following:
compute_declaration :: "COMPUTE" compute_expr [";"]
where
compute_expr ::
"MIN" "[" rtctl_expr "," rtctl_expr "]"
| "MAX" "[" rtctl_expr "," rtctl_expr "]"
MIN [start , final] computes the set of
states reachable from start. If at any point, we encounter a state
satisfying final, we return the number of steps taken to reach the
state. If a fixed point is reached and no states intersect final
then infinity is returned.
MAX [start , final] returns the length of
the longest path from a state in start to a state in final. If
there exists an infinite path beginning in a state in start that
never reaches a state in final, then infinity is returned.
Go to the first, previous, next, last section, table of contents.