NuSMV interactively
The main interaction mode of NuSMV is through an interactive
shell. In this mode NuSMV enters a read-eval-print loop. The
user can activate the various NuSMV computation steps as system
commands with different options. These steps can therefore be invoked
separately, possibly undone or repeated under different
modalities. These steps include the construction of the model under
different partitioning techniques, model checking of specifications, and
the configuration of the BDD package. The interactive shell of
NuSMV is activated from the system prompt as follows
(`NuSMV>' is the default NuSMV shell prompt):
system_prompt> NuSMV -int RET NuSMV release 1.1 (compiled 30-Jul-99 at 7:25 PM) NuSMV>
A NuSMV command is a sequence of words. The first word specifies
the command to be executed. The remaining words are arguments to the
invoked command. Commands separated by a `;' are executed
sequentially; the NuSMV shell waits for each command to terminate
in turn. The behavior of commands can depend on environment variables,
similar to "csh" environment variables.
In the following we present the possible commands followed by the
related environment variables, classified in different categories. Every
command answers to the option -h by printing out the command
usage. When output is paged for some commands (option -m), it is
piped through the program specified by the UNIX PAGER shell
variable, if defined, or through UNIX command "more". Environment
variables can be assigned a value with the set command.
Command sequences to NuSMV must obey the (partial) order
specified in the figure depicted in the previous page. For instance, it
is not possible to evaluate CTL expressions before the model is built.
The following commands allow for the parsing and the compilation of the model into BDD.
read_model [-h] [-i model-file]
Reads a NuSMV file. If the -i option is
not specified, it reads from the file specified in the environment
variable input_file.
Command options:
-i model-file
input_file to
model-file, and reads the model from the specified file.
set' command or by the command
line option `-i'. There is no default value.
flatten_hierarchy [-h]
This command is responsible of the instantiation of modules and processes. The instantiation is performed by substituting the actual parameters for the formal parameters, and then by prefixing the result via the instance name.
show_vars [-h] [-s] [-i] [-m | -o output-file]
Prints symbolic input and state variables of the model with their range of values (as defined in the input file).
Command Options:
-s
-i
-m
PAGER shell variable if defined, else through the
UNIX command "more".
-o output-file
output-file
encode_variables [-h] [-i order-file]
Generates the boolean BDD variables and the ADD needed to encode
propositionally the (symbolic) variables declared in the model.
The variables are created as default in the order in which they
appear in a depth first traversal of the hierarchy.
The input order file can be partial and can contain variables not declared in the model. Variables not declared in the model are simply discarded. Variables declared in the model which are not listed in the ordering input file will be created and appended at the end of the given ordering list, according to the default ordering.
Command options:
-i order-file
input_order_file to
order-file, and reads the variable ordering to be used from
file order-file. This can be combined with the
write_order command. The variable ordering is written to a
file, which can be inspected and reordered by the user, and then
read back in.
encode_variables' command. There
is no default value.
write_order [-h] [(-o | -f) order-file]
Writes the current order of BDD variables in the
file specified via the -o option. If no option is specified the environment
variable output_order_file will be considered. If the variable
output_order_file is unset (or set to an empty value) then standard
output will be used.
Command options:
-o order-file
output_order_file
to order-file and then dumps the ordering list into that file.
-f order-file
build_model [-h] [-f] [-m Method]
Compiles the flattened hierarchy into BDD (initial states, invariants,
and transition relation) using the method specified in the environment
variable partition_method for building the transition relation.
Command options:
-m Method
partition_method to
the value Method, and then builds the transition
relation. Available methods are Monolithic,
Threshold and Iwls95CP.
-f
conj_part_threshold. It is possible (default) to use affinity
clustering to improve model checking performance. See affinity
variable.
image_cluster_size,
image_W1, image_W2, image_W3, image_W4.
It is possible (default) to use affinity clustering to improve model
checking performance. See affinity variable. It is also possible
to avoid (default) preordering of clusters (see [RAP+95]) using
iwls95preorder variable.
image_cluster_size is used as threshold
value for the clusters. The default value is 1000 BDD nodes. The other
parameters attribute different weights to the different factors in the
algorithm. The default values are 6, 1, 1, 2 respectively. (For a detailed
description, please refer to [RAP+95].)
0 or 1. The default value is 0.
print_iwls95options [-h]
This command prints out the configuration
parameters of the IWLS95 clustering algorithm, i.e.
image_verbosity, image_cluster_size and
image_W{1,2,3,4}.
go [-h]
This command initializes the system for
verification. It is equivalent to the command sequence
read_model, flatten_hierarchy,
encode_variables, build_model,
build_flat_model, build_boolean_model.
If some commands have already been
executed, then only the remaining ones will be invoked.
Command options:
process_model [-h] [-i model-file] [-m Method]
Reads the model, compiles it into BDD and
performs the model checking of all the specification contained in
it. If the environment variable forward_search has been set
before, then the set of reachable states is computed. If the
environment variables enable_reorder and
reorder_method are set, then the reordering of variables is
performed accordingly. This command simulates the batch behavior of
NuSMV and then returns the control to the interactive shell.
Command options:
-i model-file
input_file to file
model-file, and reads the model from file
model-file.
-m Method
partition_method to
Method and uses it as partitioning method.
process_model command and when used in conjunction with the
ag_only_search environment variable enables the use of an ad hoc
algorithm to verify invariants.
check_trans [-h] [-m | -o output-file]
Checks if the transition relation is total. If the transition relation is not total then a potential deadlock state is shown out.
Command options:
-m
PAGER shell variable if
defined, else through the UNIX command "more".
-o output-file
output-file.
At the beginning reachable states are computed in order to guarantee that deadlock states are actually reachable.
process_model call. Possible values are 0 or
1. Default value is 0.
compute_reachable [-h]
Computes the set of reachable states. The result
is then used to simplify image and preimage computations. This can
result in improved performances for models with sparse state
spaces. Sometimes this option may slow down the performances because
the computation of reachable states may be very expensive. The
environment variable forward_search is set during the execution
of this command.
print_reachable_states [-h]
Prints the number of reachable states of the given model. The reachable states are computed if needed.
check_spec [-h] [-m | -o output-file] [-n number | -p "ctl-expr [IN context]"]
Performs fair CTL model checking.
A ctl-expr to be checked can be specified at command line
using option -p. Alternatively, option -n can be used
for checking a particular formula in the property database. If
neither -n nor -p are used, all the SPEC formulas in
the database are checked.
Command options:
-m
SPECs to the program specified by the
PAGER shell variable if defined, else
through the UNIX command "more".
-o output-file
SPECs to the file output-file.
-p "ctl-expr [IN context]"
context is the module
instance name which the variables in ctl-expr must
be evaluated in.
-n number
number in the property
database.
If the ag_only_search environment variable has been set, and
the set of reachable states has been already computed, then a
specialized algorithm to check AG formulas is used instead of the
standard model checking algorithms.
check_invar [-h] [-m | -o output-file] [-n number | -p "invar-expr [IN context]"]
Performs invariant checking on the given
model. An invariant is a set of states. Checking the invariant is
the process of determining that all states reachable from the
initial states lie in the invariant.
Invariants to be verified can be provided as simple formulas
(without any temporal operators) in the input file via the
INVARSPEC keyword or directly at command line, using the option
-p.
Option -n can be used for checking a particular invariant
of the model. If neither -n nor -p are
used, all the invariants are checked.
During checking of invariant all the fairness conditions associated with the model are ignored.
If an invariant does not hold, a proof of failure is demonstrated. This consists of a path starting from an initial state to a state lying outside the invariant. This path has the property that it is the shortest path leading to a state outside the invariant.
Command options:
-m
INVARSPECs to the program specified by the
PAGER shell variable if defined, else
through the UNIX command "more".
-o output-file
INVARSPECs to the file output-file.
-p "invar-expr [IN context]"
context is the module instance name which the variables
in invar-expr must be evaluated in.
check_ltlspec [-h] [-m | -o output-file] [-n number | -p "ltl-expr [IN context]"]
Performs model checking of LTL formulas. LTL model checking is reduced to CTL model checking as described in the paper by [CGH97].
A ltl-expr to be checked can be specified at command line
using option -p. Alternatively, option -n can be used
for checking a particular formula in the property database. If
neither -n nor -p are used, all the LTLSPEC formulas in
the database are checked.
Command options:
-m
LTLSPECs to the program specified by the
PAGER shell variable if defined, else
through the Unix command "more".
-o output-file
LTLSPECs to the file output-file.
-p "ltl-expr [IN context]"
context is the module
instance name which the variables in ltl_expr must be
evaluated in.
-n number
number in the property
database.
compute [-h] [-m | -o output-file] [-n number | -p "compute-expr [IN context]"]
This command deals with the computation of quantitative characteristics of real time systems. It is able to compute the length of the shortest (longest) path from two given set of states.
MAX [ alpha , beta ]
MIN [ alpha , beta ]
Properties of the above form can be specified in the input file via
the keyword COMPUTE or directly at command line,
using option -p.
Option -n can be used for computing a particular expression
in the model. If neither -n nor -p are
used, all the COMPUTE specifications are computed.
Command options:
-m
COMPUTEs to the program specified by the
PAGER shell variable if defined, else
through the UNIX command "more".
-o output-file
COMPUTEs to the file output-file.
-p "compute-expr [IN context]"
context is the module
instance name which the variables in compute-expr must
be evaluated in.
-n number
number
add_property [-h] [(-c | -l | -i | -q) -p "formula [IN context]"]
Adds a property in the list of properties. It is possible to insert LTL, CTL, INVAR and quantitative (COMPUTE) properties. Every newly inserted property is initialized to unchecked. A type option must be given to properly execute the command.
Command options:
-c
-l
-i
-q
-p "formula [IN context]"
formula specified on the command-line. context is the module instance name which the variables
in formula must be evaluated in.
To give the user the opportunity to get familiar with the behavior of the model
to be checked, a simulation feature has been provided in the NuSMV system.
A simulation's facility lets the user widely navigate structures and properties
of the model under test through the generation of its possible executions (traces
from now on). It also allows the user to acquire confidence with the
correctness of the model before actual verification of properties. Maximum
flexibility and degrees of freedom in a simulation session are achieved introducing
three different trace generation policies: deterministic, random and interactive.
Each of them corresponds to a different way a state is chosen from a set.
In deterministic simulation mode the first state of a set (whatever it is) is
chosen, while in the random one the choice is non deterministically performed.
In these two first modes traces are automatically generated by NuSMV:
the user obtains the whole of the trace in a time without control over the generation
itself (except for the simulation mode and the number of states entered via
command line).
Third simulation mode lets the user have a complete control over traces generation
by interactively building the trace. During an interactive simulation session,
the system stops at every step showing a list of possible future states: the
user is requested to choose one of the items. This feature is particularly
useful when one wants to inspect some particular reactions of the model to
be checked.
To avoid that the user easily gets confused when the number of possible choices
is too high, an internal limit on the number of states that are showed step by
step has been set. If, eventually, such a situation should take place, the system
will ask the user to "guide" the simulation via the insertion of some further
constraints (as simple expressions) over the variables.
The system will continue to ask for constraints insertion until the number of
future states will be under a predefined threshold: expressions entered during
this particular phase are accumulated (in a logical product) in a single big constraint
used only for the actual step of the simulation and discarded before the next one.
The system also makes a control over the expressions given by the user and will
request for a further insertion if an inconsistency arises.
Cases of inconsistency (i.e. empty set of states) may be located in:
It is also possible to specify some constraints as a command line parameter: these expressions will be considered in all of the simulation steps. If entered constraints were too strong an execution may not exist, simulation stops in the last found state and the trace generated until that point is stored in the system (see also command descriptions below).
Every trace generated during a NuSMV session (created either by the
counterexample generator or by the simulator itself) can be explored in a second
time via the show_traces command or the goto_state
command (see section Traces Inspection Commands).
Commands descriptions follow:
pick_state [-h] [-v] [-r | -i [-a]] [-c "constraints"]
Chooses an element from the set of initial states, and makes it the
current state (replacing the old one). The chosen state is
stored as the first state of a new trace ready to be lengthened by
steps states by the simulate command. The state can be
chosen according to different policies which can be specified via command
line options. By default the state is chosen in a deterministic way.
Command Options:
-v
t.1 of the state chosen, where
t is the number of the new trace, that is the number of
traces so far generated plus one).
-r
-i
-a
-i options has been specified.
-c "constraints"
constraints to restrict the set of initial states
in which the state has to be picked. constraints must be
enclosed between double quotes " ".
show_traces [ [-h] [-v] [-t] [-m | -o output-file] -a | trace_number ]
Shows the traces currently stored in system memory, if any. By default it shows the last generated trace, if any.
Command Options:
-v
-t
-a
-m
PAGER shell variable if defined, else through the
UNIX command "more".
-o output-file
output-file
trace_number
simulate [-h] [-p | -v] [-r | -i [-a]] [-c "constraints"] steps
Generates a sequence of at most steps states (representing a
possible execution of the model), starting from the current state.
The current state must be set via the pick_state or
goto_state commands.
It is possible to run the simulation in three ways (according to different command line policies): deterministic (the default mode), random and interactive.
The resulting sequence is stored in a trace indexed with an integer number taking into account the total number of traces stored in the system. There is a different behavior in the way traces are built, according to how current state is set: current state is always put at the beginning of a new trace (so it will contain at most steps + 1 states) except when it is the last state of an existent old trace. In this case the old trace is lengthened by at most steps states.
Command Options:
-p
-v
-r
-i
-a
-i option has been specified.
-c "constraints"
constraints. The desired sequence of states
could not exist if such constraints were too strong or it may happen
that at some point of the simulation a future state satisfying those
constraints doesn't exist: in that case a trace with a number of
states less than steps trace is obtained.
Note: constraints must be enclosed between double quotes
" ".
steps
steps states:
this is the case in which simulation stops in an intermediate
step because it may not exist any future state satisfying those
constraints.
A typical execution sequence of a simulation session could be as follows:
suppose
to use the model described below (2).
MODULE main
VAR
request : boolean;
state : {ready,busy};
ASSIGN
init(state) := ready;
next(state) := case
state = ready & request : busy;
1 : {ready,busy};
esac;
SPEC
AG(request -> AF state = busy)
This model has now to be read into the NuSMV system
(3) (see section Model Reading and Building).
A starting point (i.e. a state) is needed before the simulator could start
to build any trace. By default the simulator gets the actual current state
as a starting point of every new trace: so it will be included as the first state
of a new trace except if otherwise stated; the user has been provided with
the following two NuSMV commands to overcome this behavior:
goto_state: this command (see section Traces Inspection Commands)
provides the user to set any state of any already existent trace as the
current state;
pick_state: this command can be used whenever one wants to choose the
starting point of a new trace among the set of initial states, and it has to be
used when a current state doesn't exist yet (that is when the system has being
reset).
As at this point of the example current state doesn't exist, and there
is no trace currently stored in the system, an item from the set of initial states
has to be picked using the NuSMV pick_state command.
A simulation session can be started now, using the simulate command.
The system will generate a trace according to the options entered
via command line (4).
New builded traces are numbered: every trace is identified by an integer
number, while every state belonging to a trace is identified by a dot
notation: for example state 1.3 is the third state of the first generated
trace.
system_prompt> NuSMV -int short.smv
NuSMV release 1.1 (compiled 30-Jul-99 at 7:25 PM)
NuSMV > go
NuSMV > pick_state -r
NuSMV > print_current_state -v
Current state is 1.1
request = 0
state = ready
NuSMV > simulate -r 3
********* Starting Simulation From State 1.1 *********
NuSMV > show_traces -t
There is 1 trace currently available.
NuSMV > show_traces -v
#################### Trace number: 1 ####################
-> State 1.1 <-
request = 0
state = ready
-> State 1.2 <-
request = 1
state = busy
-> State 1.3 <-
request = 1
state = ready
-> State 1.4 <-
request = 1
state = busy
All that the user has to do to change the starting point of the next new
trace is to use the pick_state or the goto_state commands
(5).
Note that in the next example trace 1 has been lengthened as current state
was set to the last state of an existing trace.
NuSMV > goto_state 1.4
request = 1
state = busy
NuSMV > simulate -r 3
********* Starting Simulation From State 1.4 *********
NuSMV > show_traces 1
#################### Trace number: 1 ####################
-> State 1.1 <-
request = 0
state = ready
-> State 1.2 <-
request = 1
state = busy
-> State 1.3 <-
state = ready
-> State 1.4 <-
state = busy
-> State 1.5 <-
state = ready
-> State 1.6 <-
request = 0
state = busy
-> State 1.7 <-
request = 1
The user is also able to interactively choose the states of the trace he wants to build: an example of an interactive picking of an initial state is showed below:
NuSMV > pick_state -i -a
*************** AVAILABLE FUTURE STATES ***************
0) -------------------------
request = 0
state = ready
1) -------------------------
request = 1
state = ready
Choose a state from the above (0-1): 1 RET
Chosen state is: 1
request = 1
state = ready
Furthermore, the user is able to specify some constraints to restrict
sets of states from which the simulator will pick out. Constraints can
be set for both the pick_state command and the simulate
command. For the simulate command these constraints are "global"
for the actual trace to be generated, in the sense that they are always
included in every step of the simulation. They are therefore to be
intended in an opposite way with respect to those constraints eventually
entered together with the pick_state command, or during an
interactive simulation session (when the number of future states to be
displayed is too high), that are "local" only to a single step of the
simulation and are "forgotten" in the next one. For example lets pick an
initial state with some simple constraints:
NuSMV > pick_state -c "request = 1" -i
*************** AVAILABLE FUTURE STATES ***************
0) -------------------------
request = 1
state = ready
There's only one future state. Press Return to Proceed. RET
Chosen state is: 0
request = 1
state = ready
Note how the set of possible states to choose has being restricted (in this case there is only one future state, so the system will automatically pick it, waiting for the user to press the RET key).
A trace is a sequence of states corresponding to a possible execution of
the model. Traces are created by NuSMV when a formula is found to
be false; they are also generated by the simulation feature (section Simulation Commands).
Each trace has a number, and the states are numbered within the trace.
Trace n has states n.1, n.2, n.3, "...".
The trace inspection commands of NuSMV allow to navigate
along the traces produced by NuSMV. During the navigation, there
is a current state, and the current trace is the trace the
current state belongs to. The commands are the following:
goto_state [-h] state
Makes state the current
state. This command is used to navigate alongs traces
produced by NuSMV. During the navigation, there is a current
state, and the current trace is the trace the
current state belongs to.
print_current_state [-h] [-v]
Prints the name of the current state if defined.
Command options:
-v
NuSMV uses the state of the art BDD package CUDD
[Som98]. Control over the BDD package can very important to tune
the performance of the system. In particular, the order of variables is
critical to control the memory and the time required by operations over
BDDs. Reordering methods can be activated to determine better variable
orders, in order to reduce the size of the existing BDDs. Reordering
methods can be activated either
Reordering of the variables can be triggered in two ways: by the user,
or by the BDD package. In the first way, reordering is triggered by the
interactive shell command dynamic_var_ordering with the -f
option.
Reordering is triggered by the BDD package when the number of nodes
reaches a given threshold. The threshold is initialized and
automatically adjusted after each reordering by the package. This is
called dynamical reordering, and can be enabled or disabled by the user.
Dynamic reordering is enabled with the shell command
dynamic_var_ordering with the option -e, and disabled with
the -d option.
sift.
sift:
random:
random_pivot:
random, but the two variables are chosen so that the
first is above the variable with the largest number of nodes, and the
second is below that variable. In case there are several variables tied
for the maximum number of nodes, the one closest to the root is used.
sift_converge:
sift method is iterated until no further improvement is
obtained.
symmetry_sift:
symmetry_sift_converge:
symmetry_sift method is iterated until no further improvement
is obtained.
window{2,3,4}:
window{2,3,4}_converge:
group_sift:
symmetry_sift, but uses more general
criteria to create groups.
group_sift_converge:
group_sift method is iterated until no further improvement
is obtained.
annealing:
genetic:
exact:
linear:
linear_conv:
linear method is iterated until no further improvement is obtained.
dynamic_var_ordering [-d] [-e <method>] [-f <method>] [-h]
Controls the application and the modalities of (dynamic) variable
ordering. Dynamic ordering is a technique to reorder the BDD variables
to reduce the size of the existing BDDs. When no options are specified,
the current status of dynamic ordering is displayed. At most one of the
options -e, -f, and -d should be specified.
Dynamic ordering may be time consuming, but can often reduce the size of
the BDDs dramatically. A good point to invoke dynamic ordering
explicitly (using the -f option) is after the commands
build_model, once the transition relation has been built. It is
possible to save the ordering found using write_order in order to
reuse it (using build_model -i order-file) in the future.
Command options:
-d
-e <method>
<method> must be one of the following:
-f <method>
<method> are the same as in option -e.
print_bdd_stats [-h]
Prints the statistics for the BDD package. The amount of information depends on the BDD package configuration established at compilation time. The configurtion parameters are printed out too. More information about statistics and parameters can be found in the documentation of the CUDD Decision Diagram package.
set_bdd_parameters [-h] [-s]
Applies the variables table of the NuSMV environnement
to the BDD package, so the user can set specific BDD parameters to the
given value. This command works in conjunction with the
print_bdd_stats and set commands.
print_bdd_stats first prints a report of the parameters and
statistics of the current bdd_manager. By using the command set,
the user may modify the value of any of the parameters of the
underlying BDD package. The way to do it is by setting a value in
the variable BDD.parameter name where parameter
name is the name of the parameter exactly as printed by the
print_bdd_stats command.
Command options:
bin/sh -c shell_command. If the command does not exists or
you have not the right to execute it, then an error message is printed.
alias [-h] [<name> [<string>]]
The "alias" command, if given no arguments, will print the definition of all current aliases.
Given a single argument, it will print the definition of that alias (if any).
Given two arguments, the keyword <name> becomes an alias for
the command string <string>, replacing any other alias with
the same name.
Command options:
It is possible to create aliases that take arguments by using the history
substitution mechanism. To protect the history substitution
character `%' from immediate expansion, it must be preceded
by a `\' when entering the alias.
For example:
NuSMV> alias read "read_model -i \%:1.smv ; set input_order_file \%:1.ord"
NuSMV> read short
will create an alias `read', execute "read_model -i short.smv; set input_order_file short.ord".
And again:
NuSMV> alias echo2 "echo Hi ; echo \%* !"
NuSMV> echo2 happy birthday
will print:
Hi
happy birthday !
CAVEAT: Currently there is no check to see if there is a circular
dependency in the alias definition. e.g.
NuSMV> alias foo "echo print_bdd_stats; foo"
creates an alias which refers to itself. Executing the command foo
will result an infinite loop during which the command
print_bdd_stats will be executed.
echo [-h] <args>
Echoes its arguments to standard output.
help [-a] [-h] [<command>]
If invoked with no arguments "help" prints the list of all commands known to the command interpreter. If a command name is given, detailed information for that command will be provided.
Command options:
history [-h] [<num>]
Lists previous commands and their event numbers. This is a UNIX-like history mechanism inside the NuSMV shell.
Command options:
History Substitution:
The history substitution mechanism is a simpler version of the csh history substitution mechanism. It enables you to reuse words from previously typed commands.
The default history substitution character is the `%' (`!' is default for
shell escapes, and `#' marks the beginning of a comment). This can be changed
using the "set" command. In this description '%' is used as the history_char.
The `%' can appear anywhere in a line. A line containing a history
substitution is echoed to the screen after the substitution takes place.
`%' can be preceded by a `\' in order to escape the substitution,
for example, to enter a `%' into an alias or to set the prompt.
Each valid line typed at the prompt is saved. If the "history" variable is set (see help page for "set"), each line is also echoed to the history file. You can use the "history" command to list the previously typed commands.
Substitutions:
At any point in a line these history substitutions are available.
print_usage [-h]
Prints a formatted dump of processor-specific
usage statistics, and BDD usage statistics. For Berkeley Unix, this
includes all of the information in the getrusage() structure.
Command options:
quit [-h] [-s]
Stops the program. Does not save the current network before exiting.
Command options:
reset [-h]
Resets the whole system, in order to read in another model and to perform verification on it.
Command options:
set [-h] [<name>] [<value>]
A variable environment is maintained by the command interpreter. The "set" command sets a variable to a particular value, and the "unset" command removes the definition of a variable. If "set" is given no arguments, it prints the current value of all variables.
Command options:
Interpolation of variables is allowed when using the set command. The
variables are referred to with the prefix of '$'. So for example,
what follows can be done to check the value of a set variable:
NuSMV> set foo bar
The last line "bar" will be the output produced by NuSMV.
NuSMV> echo $foo
bar
Variables can be extended by using the character ':' to concatenate
values. For example:
NuSMV> set foo bar
The variable
NuSMV> set foo $foo:foobar
NuSMV> echo $foo
bar:foobar
foo is extended with the value foobar .
Whitespace characters may be present within quotes. However, variable
interpolation lays the restriction that the characters ':' and '/' may
not be used within quotes. This is to allow for recursive interpolation.
So for example, the following is allowed
NuSMV> set "foo bar" this
The last line will be the output produced by NuSMV.
NuSMV> echo $"foo bar"
this
But in the following, the value of the variable foo/bar
will not be interpreted correctly:
NuSMV> set "foo/bar" this
If a variable is not set by the "set" command, then the variable is returned
unchanged.
NuSMV> echo $"foo/bar"
foo/bar
Different commands use environment information for different purposes. The command interpreter makes use of the following parameters:
source [-h] [-p] [-s] [-x] <file> [<args>]
Reads and executes commands from a file.
Command options:
Arguments on the command line after the filename are remembered but not evaluated. Commands in the script file can then refer to these arguments using the history substitution mechanism.
EXAMPLE:
Contents of test.scr:
read_model -i %:2
flatten_hierarchy
build_variables
build_model
compute_fairness
Typing "source test.scr short.smv" on the command line will execute the
sequence
read_model -i short.smv
flatten_hierarchy
build_variables
build_model
compute_fairness
(In this case %:0 gets "source", %:1 gets
"test.scr", and %:2 gets "short.smv".)
If you type "alias st source test.scr" and then type "st short.smv bozo",
you will execute
read_model -i bozo
flatten_hierarchy
build_variables
build_model
compute_fairness
because "bozo" was the second argument on the last command line typed. In
other words, command substitution in a script file depends on how the script
file was invoked. Switches passed to a command are also counted as
positional parameters. Therefore, if you type "st -x short.smv bozo",
you will execute
read_model -i short.smv
flatten_hierarchy
build_variables
build_model
compute_fairness
To pass the "-x" switch (or any other switch) to "source" when the
script uses positional parameters, you may define an alias. For
instance, "alias srcx source -x".
time [-h]
Prints the processor time used since the last invocation of the "time" command, and the total processor time used since NuSMV was started.
unalias [-h] <alias-names>
Removes the definition of an alias specified via the alias command.
Command options:
unset [-h] <variables>
A variable environment is maintained by the command interpreter. The "set" command sets a variable to a particular value, and the "unset" command removes the definition of a variable.
Command options:
usage [-h]
Prints a formatted dump of processor-specific usage statistics. For Berkeley Unix, this includes all of the information in the getrusage() structure.
which [-h] <file_name>
Looks for a file in a set of directories
which includes the current directory as well as those in the NuSMV path.
If it finds the specified file, it reports the found file's path.
The searching path is specified through the "set open_path" command
in ".nusmvrc".
Command options:
The behavior of the system depends on the value of some environment
variables. For instance, an environment variable specifies the
partitioning method to be used in building the transition relation. The
value of environment variables can be inspected and modified with the
`set' command. Environment variables can be either logical
or utility.
TAB key (in a way similar to the file
completion inside the "bash" shell). If the system has not been compiled
with the "readline" library, a built-in method to perform file
completion a la "csh" can be used. This method is enabled with the
`set filec' command. The "csh" file completion method can be
also enabled if the "readline" library has been used. In this case the
features offered by readline will be disabled.
shell_char specifies a character to be used as shell escape.
The default value of this environment variable is `!'.
history_char specifies a character to be used in history
substitutions.
The default value of this environment variable is `%'.
open_path (in analogy to the shell-variable PATH) is a list
of colon-separated strings giving directories to be searched
whenever a file is opened for read. Typically the current
directory (`.') is first in this list. The standard system
library (NuSMV_LIBRARY_PATH)
is always implicitly appended to the current path. This provides a
convenient short-hand mechanism for reaching standard library files.
stderr) can be re-directed to a file
by setting the variable nusmv_stderr.
stdout) can be re-directed to a file
by setting the internal variable nusmv_stdout.
stdin) can be re-directed to a file
by setting the internal variable nusmv_stdin.
Go to the first, previous, next, last section, table of contents.