NuSMV/code/nusmv/shell/fsm/bdd/bddCmd.c File Reference

#include "nusmv/shell/cmd/cmd.h"
#include "nusmv/shell/fsm/bdd/bddCmd.h"
#include "nusmv/core/fsm/bdd/bdd.h"
#include "nusmv/core/compile/compile.h"
#include "nusmv/core/utils/OStream.h"
#include "nusmv/core/utils/StreamMgr.h"
#include "nusmv/core/utils/Logger.h"
#include "nusmv/core/parser/symbols.h"
#include "nusmv/core/utils/error.h"
#include "nusmv/core/utils/utils_io.h"
#include "nusmv/core/enc/enc.h"
#include "nusmv/core/prop/propPkg.h"
#include "nusmv/core/parser/parser.h"
#include "nusmv/core/utils/ErrorMgr.h"
#include <math.h>

Functions
void	Bdd_End (NuSMVEnv_ptr env)
	Quit the BddFsm package.
void	Bdd_Init (NuSMVEnv_ptr env)
	Module header file for bdd shell commands.
int	CommandCheckFsm (NuSMVEnv_ptr env, int argc, char **argv)
	Bdd FSM commands.
int	CommandComputeReachable (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandDumpFsm (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandPrintFairStateInputPairs (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandPrintFairStates (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandPrintFairTransitions (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandPrintReachableStates (NuSMVEnv_ptr env, int argc, char **argv)
Variables
cmp_struct_ptr	cmps

---

Function Documentation

void Bdd_End

(

NuSMVEnv_ptr

env

)

Quit the BddFsm package.

Quit the BddFsm package

void Bdd_Init

(

NuSMVEnv_ptr

env

)

Module header file for bdd shell commands.

AutomaticEnd

int CommandCheckFsm	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Bdd FSM commands.

Author:

Marco Roveri This file contains all the shell commands to dela with computation and printing of reachable states, fair states and fair transitions.

Command:

check_fsm: Checks the transition relation for totality.

Command arguments: [-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

Pipes the output generated by the command to the program specified by the PAGER shell variable if defined, else through the UNIX command "more".

-o output-file

Writes the output generated by the command to the file output-file.

At the beginning reachable states are computed in order to guarantee that deadlock states are actually reachable.

int CommandComputeReachable	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Command:

compute_reachable: Computes the set of reachable states

Command arguments: [-h] [-k number]

The set of reachable states is used to simplify image and preimage computations. This can result in improved performances for models with sparse state spaces.

Command Options:

-k number

Provides an explicit bound to perform at most "number" steps.

-t number

Provides a fail cut-off maximum CPU time to halt the computation. This option can be used to limit execution time.

int CommandDumpFsm	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Command:

dump_fsm: Dumps (in DOT format) selected parts of the bdd fsm, with optional expression

Command arguments: [-h] -o filename [-i] [-I] [-t] [-f] [-r] [-e expression]

Dumps selected parts of the bdd fsm, with optional expression, in DOT format. At least one among options [iIte] must be specified.

Command Options:

-o filename Dumps to the specified file name.

-i Dumps the initial states of the FSM, among with other selected outputs.

-I Dumps the invariant states of the FSM, among with other selected outputs.

-t Dumps the (monolithic) transition relation of the FSM, among with other selected outputs.

-F Dumps the (monolithic) fair states of the FSM, among with other selected outputs.

-r Dumps the (monolithic) reachable states of the FSM, among with other selected outputs.

-e Dumps the specified expression, among with other selected outputs (see also command dump_expr).

int CommandPrintFairStateInputPairs	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Command:

_print_fair_state_input_pairs: Prints the number of fair state/input pairs

Command arguments: [-h] [-v]

Prints the number of fair state/input pairs. In verbose mode, prints also the list of fair pairs.

Command Options:

-v

Verbosely prints the list of fair state/input pairs.

int CommandPrintFairStates	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Command:

print_fair_states: Prints out information about fair states

Command arguments: [-h] [-v]

This command provides information about the fair states of the current model.number of fair states. In verbose mode, prints also the list of fair states.

Command Options:

-v

Verbosely prints the list of fair states.

int CommandPrintFairTransitions	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Command:

print_fair_transitions: Prints the number of fair transitions, and list transitions in verbose mode.

Command arguments: [-h] [-v [-f format] [-o fname]]

Prints the number of fair transitions. In verbose mode, prints also the list of fair transitions.

Command Options:

-v

Verbosely prints the list of fair transitions.

-f

Use given format when printing the list of fair transitions.

-o fname

Writes to given filename (default: stderr).

int CommandPrintReachableStates	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Command:

print_reachable_states: Prints out information about reachable states

Command arguments: [-h] [-v] [-f] [-d] [-o filename]

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.

Command Options:

-v

Verbosely prints the list of reachable states.

-f

Print the list of reachable states as a formula.

-d

Prints the list of reachable states with defines (Requires -v).

-o filename

Prints the result on the specified filename instead of on standard output

---

Variable Documentation

cmp_struct_ptr cmps