NuSMV/code/nusmv/core/compile/compileInt.h File Reference

#include "nusmv/core/compile/compile.h"
#include "nusmv/core/compile/symb_table/symb_table_int.h"
#include "nusmv/core/compile/symb_table/SymbTable.h"
#include "nusmv/core/compile/symb_table/SymbLayer.h"
#include "nusmv/core/fsm/FsmBuilder.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/utils/NodeList.h"
#include "nusmv/core/utils/assoc.h"
#include "nusmv/core/opt/opt.h"
#include "nusmv/core/dd/dd.h"
#include "nusmv/core/node/node.h"
#include "nusmv/core/set/set.h"
#include "nusmv/core/hrc/HrcNode.h"

Go to the source code of this file.

Defines
#define	ST_BEVAL_EXPR2BEXPR_HASH   "cbeh"
#define	ST_CHECK_INPUTS_HASH   "ccih"
#define	ST_CHECK_NESTED_ATTIME_HASH   "ccnah"
	This hash associates to each formula --> 1 (false) or 2 (true) depending on expr contains attime nodes or not in it.
#define	ST_CHECK_NEXT_HASH   "ccnh"
	Internal declaration needed for the compilation.
#define	ST_CONE_COI0_HASH   "cc0h"
#define	ST_CONE_COI_HASH   "ccch"
#define	ST_CONE_CONSTS_HASH   "cccoh"
#define	ST_CONE_DEPENDENCIES_HASH   "ccdh"
Functions
cmp_struct_ptr	cmp_struct_init (void)
	Initializes the cmp structure.
void	cmp_struct_quit (cmp_struct_ptr)
	Free the cmp structure.
int	CommandCPPrintClusterInfo (NuSMVEnv_ptr env, int argc, char **argv)
int	CommandIwls95PrintOption (NuSMVEnv_ptr env, int argc, char **argv)
void	compile_add_assign_hrc (NodeMgr_ptr nodemgr, HrcNode_ptr hrc_result, node_ptr assign_list)
	Add assign declarations in hrc_result.
void	Compile_ConstructHierarchy (const NuSMVEnv_ptr env, SymbTable_ptr symb_table, SymbLayer_ptr, node_ptr, node_ptr, node_ptr, FlatHierarchy_ptr, HrcNode_ptr, hash_ptr, boolean)
	Traverses the module hierarchy and extracts the information needed to compile the automaton.
node_ptr	compile_flatten_rewrite_word_toint_cast (const NuSMVEnv_ptr env, node_ptr body, SymbType_ptr type)
	Rewrites the toint operator for word expressions conversion.
void	compile_make_params_hrc (const NuSMVEnv_ptr env, node_ptr basename, node_ptr actual_list, node_ptr formal_list, HrcNode_ptr hrc_result)
	Builds the parameters of a module from the list of formal and actual parameters of the module itself.
void	error_bit_selection_assignment_not_supported (NuSMVEnv_ptr env, node_ptr name)
	Error message for unsupported feature.
Variables
cmp_struct_ptr	cmps
int	nusmv_yylineno

---

Define Documentation

#define ST_BEVAL_EXPR2BEXPR_HASH   "cbeh"

Todo:

Missing synopsis

Todo:

Missing description

#define ST_CHECK_INPUTS_HASH   "ccih"

Todo:

Missing synopsis

Todo:

Missing description

#define ST_CHECK_NESTED_ATTIME_HASH   "ccnah"

This hash associates to each formula --> 1 (false) or 2 (true) depending on expr contains attime nodes or not in it.

Todo:

Missing synopsis

Todo:

Missing description

#define ST_CHECK_NEXT_HASH   "ccnh"

Internal declaration needed for the compilation.

Author:

Marco Roveri, Roberto Cavada This file provides the user routines to perform compilation of the model

Todo:

Missing synopsis

Todo:

Missing description

#define ST_CONE_COI0_HASH   "cc0h"

Todo:

Missing synopsis

Todo:

Missing description

#define ST_CONE_COI_HASH   "ccch"

Todo:

Missing synopsis

Todo:

Missing description

#define ST_CONE_CONSTS_HASH   "cccoh"

Todo:

Missing synopsis

Todo:

Missing description

#define ST_CONE_DEPENDENCIES_HASH   "ccdh"

Todo:

Missing synopsis

Todo:

Missing description

---

Function Documentation

cmp_struct_ptr cmp_struct_init

(

void

)

Initializes the cmp structure.

void cmp_struct_quit

(

cmp_struct_ptr

)

Free the cmp structure.

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 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}.

void compile_add_assign_hrc	(	NodeMgr_ptr	nodemgr,
		HrcNode_ptr	hrc_result,
		node_ptr	assign_list
	)

Add assign declarations in hrc_result.

Add assign declarations found in the assign list in hrc_result. The type of assign is inferred by the node type found.

Contents of hrc_result is changed adding an assign constraint.

void Compile_ConstructHierarchy	(	const NuSMVEnv_ptr	env,
		SymbTable_ptr	symb_table,
		SymbLayer_ptr	,
		node_ptr	,
		node_ptr	,
		node_ptr	,
		FlatHierarchy_ptr	,
		HrcNode_ptr	,
		hash_ptr	,
		boolean
	)

Traverses the module hierarchy and extracts the information needed to compile the automaton.

This function is a subfunction of Compile_FlattenHierarchy.

This function traverses the module hierarchy and extracts the information needed to compile the automaton. The hierarchy of modules is flattened, the variables are added to the symbol table, all the necessary parts of the model are collected (i.e. the formulae to be verified, the initial expressions, etc).

The returned value is a structure constraining all the collected parts which are: the list of TRANS, INIT, INVAR, ASSIGN, SPEC, COMPUTE, LTLSPEC, PSLSPEC, INVARSPEC, JUSTICE, COMPASSION, a full list of variables declared in the hierarchy, a hash table associating variables to their assignments and constrains. See FlatHierarchy class for more info.

node_ptr compile_flatten_rewrite_word_toint_cast	(	const NuSMVEnv_ptr	env,
		node_ptr	body,
		SymbType_ptr	type
	)

Rewrites the toint operator for word expressions conversion.

This functions takes a word expression and rewrites it as a circuit in order to convert the word expression into an integer expression.

For unsigned word[N], we rewrite the operator as follows:

(w[0:0] = 0ud1_1 ? 1 : 0) + (w[1:1] = 0ud1_1 ? 2 : 0) + ..... + (w[N-1:N-1] = 0ud1_1 ? 2^(N-1) : 0)

For signed word[N], we do the following: case w[N-1:N-1] = 0ud1_0 : (w[0:0] = 0ud1_1 ? 1 : 0) + (w[1:1] = 0ud1_1 ? 2 : 0) + ..... + (w[N-2:N-2] = 0ud1_1 ? 2^(N-2) : 0); TRUE: -((w[0:0] = 0ud1_1 ? 0 : 1) + (w[1:1] = 0ud1_1 ? 0 : 2) + ..... + (w[N-2:N-2] = 0ud1_1 ? 0 : 2^(N-2)) + 1); esac

void compile_make_params_hrc	(	const NuSMVEnv_ptr	env,
		node_ptr	basename,
		node_ptr	actual_list,
		node_ptr	formal_list,
		HrcNode_ptr	hrc_result
	)

Builds the parameters of a module from the list of formal and actual parameters of the module itself.

Builds the parameters of a module from the list of formal parameters of the module itself.
There must be a one to one correspondence between the elements of actual_list and formal_list parameters. If the number of elements of the lists are different then, an error occurs. The list actual_list must be a list of non-flattened actual parameters. For hrc structure it is not necessary to store the flattening information that is implicit in the hierarchy.

In hrc_result the lists of formal and actual parameter used to instatiate a module is changed.

void error_bit_selection_assignment_not_supported	(	NuSMVEnv_ptr	env,
		node_ptr	name
	)

Error message for unsupported feature.

---

Variable Documentation

cmp_struct_ptr cmps

int nusmv_yylineno