NuSMV/code/nusmv/shell/dd/ddCmd.c File Reference

#include "nusmv/shell/cmd/cmd.h"
#include "nusmv/shell/dd/ddCmd.h"
#include "nusmv/core/opt/opt.h"
#include "nusmv/core/utils/StreamMgr.h"
#include "nusmv/core/utils/error.h"

Functions
int	CommandDynamicVarOrdering (NuSMVEnv_ptr env, int argc, char **argv)
	The shell interface of the DD package.
int	CommandPrintBddStats (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandSetBddParameters (NuSMVEnv_ptr env, int argc, char **argv)
void	dd_AddCmd (NuSMVEnv_ptr env)
	Module header for shell commands.

---

Function Documentation

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

The shell interface of the DD package.

Author:

Marco Roveri Shell interface of the DD package. here are provided the shell commands to modyfy all the modifiable DD options.

Command:

dynamic_var_ordering: Deals with the dynamic variable ordering.

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

Disable dynamic ordering from triggering automatically.

-e <method>

Enable dynamic ordering to trigger automatically whenever a certain threshold on the overall BDD size is reached. <method> must be one of the following:

• sift: Moves each variable throughout the order to find an optimal position for that variable (assuming all other variables are fixed). This generally achieves greater size reductions than the window method, but is slower.
• random: Pairs of variables are randomly chosen, and swapped in the order. The swap is performed by a series of swaps of adjacent variables. The best order among those obtained by the series of swaps is retained. The number of pairs chosen for swapping equals the number of variables in the diagram.
• random_pivot: Same as 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: The sift method is iterated until no further improvement is obtained.
• symmetry_sift: This method is an implementation of symmetric sifting. It is similar to sifting, with one addition: Variables that become adjacent during sifting are tested for symmetry. If they are symmetric, they are linked in a group. Sifting then continues with a group being moved, instead of a single variable.
• symmetry_sift_converge: The symmetry_sift method is iterated until no further improvement is obtained.

• window{2,3,4}: Permutes the variables within windows of "n" adjacent variables, where "n" can be either 2, 3 or 4, so as to minimize the overall BDD size.

• window{2,3,4}_converge: The window{2,3,4} method is iterated until no further improvement is obtained.
• group_sift: This method is similar to symmetry_sift, but uses more general criteria to create groups.
• group_sift_converge: The group_sift method is iterated until no further improvement is obtained.
• annealing: This method is an implementation of simulated annealing for variable ordering. This method is potentially very slow.
• genetic: This method is an implementation of a genetic algorithm for variable ordering. This method is potentially very slow.
• exact: This method implements a dynamic programming approach to exact reordering. It only stores a BDD at a time. Therefore, it is relatively efficient in terms of memory. Compared to other reordering strategies, it is very slow, and is not recommended for more than 16 boolean variables.
• linear: This method is a combination of sifting and linear transformations.
• linear_converge: The linear method is iterated until no further improvement is obtained.

-f <method>

Force dynamic ordering to be invoked immediately. The values for <method> are the same as in option -e.

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

Command:

print_bdd_stats: Prints out the BDD statistics and parameters

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

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

Command:

set_bdd_parameters: Creates a table with the value of all currently active NuSMV flags and change accordingly the configurable parameters of the BDD package.

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

-s

Prints the BDD parameter and statistics after the modification.

void dd_AddCmd

(

NuSMVEnv_ptr

env

)

Module header for shell commands.

Author:

Michele Dorigatti

Todo:

: Missing description

AutomaticStart

Todo:

Missing synopsis

Todo:

Missing description