NuSMV/code/nusmv/shell/compile/compileCmd.c File Reference

#include "nusmv/shell/cmd/cmd.h"
#include "nusmv/shell/compile/compileCmd.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/utils/ErrorMgr.h"
#include "nusmv/core/utils/defs.h"
#include "nusmv/core/utils/assoc.h"
#include "nusmv/core/node/NodeMgr.h"
#include "nusmv/core/node/printers/MasterPrinter.h"
#include "nusmv/core/node/normalizers/MasterNormalizer.h"
#include "nusmv/core/compile/symb_table/SymbTable.h"
#include "nusmv/core/compile/symb_table/symb_table.h"
#include "nusmv/core/compile/PredicateNormaliser.h"
#include "nusmv/core/parser/symbols.h"
#include "nusmv/core/parser/parser.h"
#include "nusmv/core/fsm/FsmBuilder.h"
#include "nusmv/core/fsm/sexp/SexpFsm.h"
#include "nusmv/core/fsm/sexp/BoolSexpFsm.h"
#include "nusmv/core/fsm/bdd/BddFsm.h"
#include "nusmv/core/prop/propPkg.h"
#include "nusmv/core/mc/mc.h"
#include "nusmv/core/enc/enc.h"
#include "nusmv/core/trace/pkg_trace.h"
#include "nusmv/core/trace/exec/PartialTraceExecutor.h"
#include "nusmv/core/trace/exec/BDDPartialTraceExecutor.h"
#include "nusmv/core/trace/exec/CompleteTraceExecutor.h"
#include "nusmv/core/trace/exec/BDDCompleteTraceExecutor.h"
#include "nusmv/core/utils/ucmd.h"
#include "nusmv/core/utils/utils_io.h"
#include "nusmv/core/utils/error.h"
#include "nusmv/core/utils/Olist.h"
#include <stdlib.h>
#include "nusmv/core/utils/portability.h"
#include "nusmv/core/cinit/NuSMVEnv.h"
#include "nusmv/core/cinit/cinit.h"
#include "nusmv/core/node/anonymizers/NodeAnonymizerBase.h"
#include "nusmv/core/node/anonymizers/NodeAnonymizerST.h"

Defines
#define	RC_EXPERIMENTAL_CODE_PREDICATES   1
	Shell interface for the compile package.
Functions
int	CommandBuildBooleanModel (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandBuildFlatModel (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandBuildModel (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandCPPrintClusterInfo (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandEncodeVariables (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandFlattenHierarchy (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandGetInternalStatus (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandGo (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandGoBmc (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandIwls95PrintOption (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandPrintFsmStats (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandProcessModel (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandShowDependencies (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandShowVars (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandWriteCoiModel (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandWriteModelFlat (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandWriteModelFlatBool (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandWriteModelFlatUdg (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandWriteOrder (NuSMVEnv_ptr env, int argc, char **argv)
void	Compile_init_cmd (NuSMVEnv_ptr env)
	Module header file for shell commands.
Variables
cmp_struct_ptr	cmps

---

Define Documentation

#define RC_EXPERIMENTAL_CODE_PREDICATES   1

Shell interface for the compile package.

Author:

Marco Roveri This file contains the interface of the compile package with the interactive shell.

Todo:

Missing synopsis

Todo:

Missing description

---

Function Documentation

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

Command:

build_boolean_model: Compiles the flattened hierarchy into boolean SEXP

Command arguments: [-h] [-f]

Compiles the flattened hierarchy into boolean SEXP (initial states, invariants, and transition relation).

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

Command:

build_flat_model: Compiles the flattened hierarchy into SEXP

Command arguments: [-h]

Compiles the flattened hierarchy into SEXP (initial states, invariants, and transition relation).

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

Command:

build_model: Compiles the flattened hierarchy into BDD

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

Sets the environment variable partition_method to the value Method, and then builds the transition relation. Available methods are Monolithic, Threshold and Iwls95CP.

-f

Forces model construction. By default, only one partition method is allowed. This option allows to overcome this default, and to build the transition relation with different partitioning methods.

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

Command:

print_clusterinfo: Prints out information about the clustering. This command is *deprecated* in 2.4

Command arguments: [-h] | [-m] | [-o output-file]

Deprecated in 2.4: use print_fsm_stats instead.

This command prints out information regarding each cluster. In particular for each cluster it prints out the cluster number, the size of the cluster (in BDD nodes), the variables occurring in it, the size of the cube that has to be quantified out relative to the cluster and the variables to be quantified out.

Command options:

-m

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

-o output-file

Redirects the generated output to the file output-file.

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

Command:

encode_variables: Builds the BDD variables necessary to compile the model into BDD.

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

Sets the environment variable 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.

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

Command:

flatten_hierarchy: Flattens the hierarchy of modules

Command arguments: [-h] [-d]

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.

Command options:

-d

Delays the construction of vars constraints until needed

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

Command:

get_internal_status: Returns the internal status of the system.

Command arguments: [-h]

Prints out the internal status of the system. i.e.

• -1 : read_model has not yet been executed or an error occurred during its execution.
• 0 : flatten_hierarchy has not yet been executed or an error occurred during its execution.
• 1 : encode_variables has not yet been executed or an error occurred during its execution.
• 2 : build_model has not yet been executed or an error occurred during its execution.

Command options:

-h

Prints the command usage.

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

Command:

go: Initializes the system for the verification.

Command arguments: [-h][-f]

This command initializes the system for verification. It is equivalent to the command sequence read_model, flatten_hierarchy, build_flat_model, encode_variables, build_model.

If some commands have already been executed, then only the remaining ones will be invoked.

Command options:

-f

Forces the model contruction.

-h

Prints the command usage.

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

Command:

go_bmc: Initializes the system for the BMC verification.

Command arguments: [-h] | [-f]

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:

-f

Forces the model construction.

-h

Prints the command usage.

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

Command:

print_iwls95options: Prints the Iwls95 Options.

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

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

Command:

print_fsm_stats: Prints out information about the fsm and clustering.

Command arguments: [-h] | [-m] | [-p] | [-o output-file]

This command prints out information regarding the fsm and each cluster. In particular for each cluster it prints out the cluster number, the size of the cluster (in BDD nodes), the variables occurring in it, the size of the cube that has to be quantified out relative to the cluster and the variables to be quantified out.

Also the command can print all the normalized predicates the FMS consists of. A normalized predicate is a boolean expression which does not have other boolean sub-expressions. For example, expression (b<0 ? a/b : 0) = c is normalized into (b<0 ? a/b=c : 0=c) which has 3 normalized predicates inside: b<0, a/b=c, 0=c.

Command options:

-m

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

-p

Prints out the normalized predicates the FSM consists of.

-o output-file

Redirects the generated output to the file output-file.

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

Command:

process_model: Performs the batch steps and then returns control to the interactive shell.

Command arguments: [-h] [-f] [-r] [-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 option -r is specified, 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:

-f

Forces model construction even when COI is enabled.

-r

Performs a variable ordering at the end of the computation, and dumps the variable ordering as the command line option -reorder does.

-i model-file

Sets the environment variable input_file to file model-file, and reads the model from file model-file.

-m Method

Sets the environment variable partition_method to Method and uses it as partitioning method.

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

Command:

show_dependencies: Shows the expression dependencies

Command arguments: [-h] [-k bound] -e expr

Shows the dependencies of the given expression

Command options:

-k bound

Stop dependencies computation at step "bound"

-e expr

The expression on which the dependencies are computed on

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

Command:

show_vars: Shows model's symbolic variables and their values

Command arguments: [-h] [-s] [-f] [-i] [-v] [-t|-V] [-m | -o output-file]

Prints symbolic input, frozen and state variables of the model with their range of values (as defined in the input file).

Command Options:

-s

Prints state variables.

-f

Prints frozen variables.

-i

Prints input variables.

-t

Prints only the number of variables (among selected kinds), grouped by type. Incompatible with -V.

-V

Prints only the list of variables with their types (among selected kinds), and no other summary information. Incompatible with -t.

-D

Prints only the list of defines. Incompatible with -V.

-v

Prints verbosely. With this option, all scalar variable values are printed

-m

Pipes the output 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 output-file

By default, if no type specifiers (-s, -f, -i) are used, all variables type will be printed. When using one or more type specifiers (e.g. -s), only variables belonging to selected types will be printed.

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

Command:

write_coi_model: Writes a flat model of SMV file, restricted to the COI of the model properties

Command arguments: [-h] [-o filename] [-n <prop> | -p <expr> | -P <name>] | [-c] | [-l] | [-i] | [-s] | [-q] | [-p expr] | [-C] | [-g]

Writes the currently loaded SMV model in the specified file, after having flattened it. If a property is specified, the dumped model is the result of applying the COI over that property. otherwise, a restricted SMV model is dumped for each property in the property database.

Processes are eliminated and a corresponding equivalent model is printed out.

If no file is specified, stderr is used for output

Command options:

-o filename

Attempts to write the flat and boolean SMV model in filename.

-c

Dumps COI model for all CTL properties

-l

Dumps COI model for all LTL properties

-i

Dumps COI model for all INVAR properties

-s

Dumps COI model for all PSL properties

-q

Dumps COI model for all COMPUTE properties

-p expr

Applies COI for the given expression "expr"

-n idx

Applies COI for property stored at index "idx"

-P name

Applies COI for property named "name" idx

-C

Only prints the list of variables that are in the COI of properties

-g

Dumps the COI model that represents the union of all COI properties

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

Command:

write_flat_model: Writes a flat model of a given SMV file

Command arguments: [-h] [-o filename] [-A] [-m]

Processes are eliminated and a corresponding equivalent model is printed out. If no file is specified, the file specified with the environment variable output_flatten_model_file is used if any, otherwise standard output is used as output.

Command options:

-o filename

Attempts to write the flat SMV model in filename.

-A

Write the model using variables and defines rewriting to make it anonimized.

-m

Disable printing of key map when writing anonimized model

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

Command:

write_boolean_model: Writes a flattened and booleanized model of a given SMV file

Command arguments: [-h] [-o filename]

Writes the currently loaded SMV model in the specified file, after having flattened and booleanized it. Processes are eliminated and a corresponding equivalent model is printed out.

If no file is specified, the file specified via the environment variable output_boolean_model_file is used if any, otherwise standard output is used.

Command options:

-o filename

Attempts to write the flat and boolean SMV model in filename.

New in 2.4.0 and later ** Scalar variables are dumped as DEFINEs whose body is their boolean encoding.

This allows the user to still express and see parts of the generated boolean model in terms of the original model's scalar variables names and values, and still keeping the generated model purely boolean.

Also, symbolic constants are dumped within a CONSTANTS statement to declare the values of the original scalar variables' for future reading of the generated file.

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

Command:

write_flat_model_udg: Writes a flat model of a given SMV file in uDraw format

Command arguments: [-h] [-o filename]

Processes are eliminated and a corresponding equivalent model is printed out. If no file is specified, the file specified with the environment variable output_flatten_model_file is used if any, otherwise standard output is used as output.

Command options:

-o filename

Attempts to write the flat SMV model in filename.

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

Command:

write_order: Writes variable order to file.

Command arguments: [-h] [-b] [(-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. The option -b forces the dumped variable ordering to contain only boolean variables. All the scalar variables will be substituted by those variables bits that encode them. The variables bits will occur within the dumped variable ordering depending on the position they have within the system when the command is executed.

Command options:

-b

Dumps bits of scalar variables instead of the single scalar variables. When specified, this option temporary overloads the current value of the system variable write_order_dumps_bits.

-o order-file

Sets the environment variable output_order_file to order-file and then dumps the ordering list into that file.

-f order-file

Alias for -o option. Supplied for backward compatibility.

void Compile_init_cmd

(

NuSMVEnv_ptr

env

)

Module header file for shell commands.

Author:

Michele Dorigatti

Todo:

: Missing description

AutomaticStart

Initializes the commands provided by this package

---

Variable Documentation

cmp_struct_ptr cmps