NuSMV supports the analysis of specifications expressed in
computation tree logic (CTL) and
linear temporal logic (LTL). It can be run in
batch mode, or interactively with a textual user interface.
Running NuSMV Interactively The interaction shell of NuSMV is activated from the system prompt as follows: [system_prompt]$ NuSMV -int NuSMV> go NuSMV> NuSMV first tries to read and execute commands from an initialization file if such file exists and is readable unless -s was passed on the command line. File master.nusmvrc is looked for in the directories defined in environment variable NUSMV_LIBRARY_PATH or in the default library path if no such variable is defined. If no such file exists, user's home directory and the current directory will also be checked. Commands in the initialization file are executed consecutively. When the initialization phase is completed the NuSMV shell prompt is displayed and the system is now ready to execute user commands. A NuSMV command usually consists of a command name and arguments to the invoked command. It is possible to make NuSMV read and execute a sequence of commands from a file, through the command line option -source: [system_prompt]$ NuSMV -source cmd_file
Running NuSMV batch When the -int option is not specified, NuSMV runs as a batch program, which is with the form as follows: [system_prompt]$ NuSMV [command line options] input_file == Checking for LTL specification or CTL specification ==