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>
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 verbosity of NuSMV is controlled by the following environment variable.
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.
The following commands allow for the BDD-based model checking of a
NuSMV model.
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] [-v]
Prints the number of reachable states of the given model. In verbose mode, prints also the list of all reachable states. The reachable states are computed if needed.
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.
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.
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_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.
In this section we describe in detail the commands for doing and controlling
Bounded Model Checking in NuSMV.
Bounded Model Checking is based on the reduction of the bounded
model checking problem to a propositional satisfiability problem. After
the problem is generated, NuSMV internally calls a
propositional SAT solver in order to find an assignment which satisfies
the problem.
Currently NuSMV supplies two SAT solvers: SIM and Zchaff.
Notice that Zchaff is for non-commercial purposes only, and is therefore
not included in the source code distribution, as well as in some of the
binary distributions of NuSMV.
It is also possible to generate the satisfiability
problem without calling the SAT
solver. Each generated problem is dumped in DIMACS format into a
file. DIMACS is the standard format used as input by most external SAT
solver, so it is possible to use NuSMV with
an external SAT solver separately.
bmc_setup [-h]
You must call this command before use any other bmc-related command. Only one call per session is required.
go_bmc [-h]
This command initializes the system for
verification. It is equivalent to the command sequence
read_model, flatten_hierarchy,
encode_variables, build_boolean_model, bmc_setup.
If some commands have already been
executed, then only the remaining ones will be invoked.
Command options:
check_ltlspec_bmc [-h | -n idx | -p "formula" [IN context]] [-k max_length] [-l loopback] [-o filename]
This command generates one or more problems, and calls
SAT solver for each one. Each problem is related to a specific problem
bound, which increases from zero (0) to the given maximum problem
length. Here "length" is the bound of the problem that system
is going to generate and/or solve.
In this context the maximum problem bound is represented by the
-k command parameter, or by its default value stored in the
environment variable bmc_length.
The single generated problem also depends on the "loopback"
parameter you can explicitly specify by the -l option, or by its
default value stored in the environment variable bmc_loopback.
The property to be checked may be specified using the -n idx or
the -p "formula" options.
If you need to generate a dimacs dump file of all generated problems, you
must use the option -o "filename".
Command options:
-n index
-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.
-k max_length
-l loopback
-o filename
check_ltlspec_bmc_onepb [-h | -n idx | -p "formula" [IN context]] [-k length] [-l loopback] [-o filename]
As command check_ltlspec_bmc but it produces only one
single problem with fixed bound and loopback values, with no iteration
of the problem bound from zero to max_length.
Command options:
-n index
-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.
-k length
-l loopback
-o filename
gen_ltlspec_bmc [-h | -n idx | -p "formula" [IN context]] [-k max_length] [-l loopback] [-o filename]
This command generates one or more problems, and
dumps each problem into a dimacs file. Each problem is related to a specific
problem bound, which increases from zero (0) to the given maximum problem
bound. In this short description "length" is the bound of the
problem that system is going to dump out.
In this context the maximum problem bound is represented by the
max_length parameter, or by its default value stored in the
environment variable bmc_length.
Each dumped problem also depends on the loopback you can explicitly
specify by the -l option, or by its default value stored in the
environment variable bmc_loopback.
The property to be checked may be specified using the -n idx or
the -p "formula" options.
You may specify dimacs file name by using the option -o "filename",
otherwise the default value stored in the environment variable
bmc_dimacs_filename will be considered.
Command options:
-n index
-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.
-k max_length
-l loopback
-o filename
gen_ltlspec_bmc_onepb [-h | -n idx | -p "formula" [IN context]] [-k length] [-l loopback] [-o filename]
As the gen_ltlspec_bmc command, but it generates
and dumps only one problem given its bound and loopback.
Command options:
-n index
-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.
-k length
-l loopback
-o filename
10.
The default value is *.
The default value is "@f_k@k_l@l_n@n.dimacs".
check_invar_bmc [-h | -n idx | -p "formula" [IN context]] [-o filename]
Command options:
-n index
-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.
-o filename
gen_invar_bmc [-h | -n idx | -p "formula" [IN context]] [-o filename]
Command options:
-n index
-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.
-o filename
The default value is "@f_invar_n@n.dimacs".
NuSMV configuration, also the Zchaff SAT solver
can be available or not.
Notice that Zchaff is for non-commercial purposes only.
bmc_simulate [-h | -k ]
bmc_simulate does not require a specification
to build the problem, because only the model is used to build it.
The problem length is represented by the -k command parameter,
or by its default value stored in the environment variable
bmc_length.
Command options:
-k length
In this section we describe the commands that allow to simulate a
NuSMV specification.
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] [-m | -o output-file] -t | -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 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:
This section describes the administrative commands offered by the
interactive shell of NuSMV.
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.