Go to the first, previous, next, last section, table of contents.

4.7 Administration Commands

Command: ! shell_command

Executes a shell command. The shell_command is executed by calling 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.

Command: alias [-h] [name [string]]

Defines command alias. If given no arguments, will print the definition of all current aliases. Given a single argument (name), it will print the definition of that alias (if any). Given two arguments, the keyword name becomes an alias for the command string, replacing any other alias with the same name.

name [string]

Defines name to be an alias of the command specified by string if given, else prints out the definition of alias name if any. 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 image_set set image_\%:1 \%:2
NuSMV> image_set W1 100

will create an alias `image_set', execute `set image_W1 100'.
Caveat: Currently there is no check to see if there is a circular dependency in the alias definition. e.g.

NuSMV> alias foo "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. At execution time this problem is solved by a loop detection check.

Command: echo [-h] [string]

Echoes the arguments to standard output.

Command: help [-a] [-h] [command_name]

Given no arguments, will print a list of all commands known to the command interpreter. If a command_name is given, detailed informations for that command will be provided if they are available.

-a

Provides a list of all internal commands, which by convention begin with an underscore (`_').

Command: history [-h] [#num]

Lists previous commands and their event numbers. This is a UNIX-like history mechanism inside the NuSMV shell.

#num

Lists the last #num events. Lists the last 30 events if #num is not specified.

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). @cindex shell escape This can be changed using the set command. The shell escape can be changed by assigning a character to the environment variable `shell_char'. 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 the documentation of the set command), 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.

%:0

Initial word of last command.

%:n

n-th argument of last command.

%$

Last argument of last command.

%*

All but initial word of last command.

%%

Last command.

%stuf

Last command beginning with "stuf".

%n

Repeat the n-th command.

%-n

Repeat the n-th previous command.

^old^new

Replace `old' with `new' in previous command. Trailing spaces are significant during substitution. Initial spaces are not significant.

Command: 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: quit [-h] [-s]

Exits NuSMV by stopping the program.

-s

Free all the memory before quitting. This is slower, and is used for finding memory leaks.

Command: reset [-h]

Resets the whole system, in order to read in another model and to perform verification on it.

Command: 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.

name [value]

name is a variable name, and value is the value to be assigned to the variable.

Command: source [-h] [-p] [-s] [-x] script-file [args]

Reads and executes commands from a file.

-p

Prints a prompt before reading each command.

-s

Silently ignores an attempt to execute commands from a nonexistent file.

-x

Echoes each command before it is executed.

script-file

A file name containing NuSMV commands.

The args 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.

Command: time [-h]

Prints the processor time used since the last `time' command, and the total processor time used since NuSMV was started.

Command: unalias [-h] alias-names

Removes the definition of an alias.

alias-names

Aliases to be removed

Command: 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.

variables

Variables to be unset.

Command: usage [-h]

Prints a formatted dump of processor-specific usage statistics. For Berkeley UNIX, this includes all of the information in the getrusage() structure.

Command: which [-h] file-name

Looks for a file in a set of directories which includes the current directory as well as those in the open_path environment variable. If it finds it, it reports the path. The directories are specified through the `set open_path' command in the `{~/}.nusmvrc' or by the shell variable NuSMV_LIBRARY_PATH.

file-name

File to be searched.