This file provides the user routines to perform compilation of the model 

int 
CommandBuildBooleanModel(
  int  argc, 
  char ** argv 
)
Compiles the flattened hierarchy into boolean SEXP

Defined in compileCmd.c 

int 
CommandBuildFlatModel(
  int  argc, 
  char ** argv 
)
Compiles the flattened hierarchy into SEXP

Defined in compileCmd.c 

int 
CommandBuildModel(
  int  argc, 
  char ** argv 
)
Compiles the flattened hierarchy into BDD

Defined in compileCmd.c 

int 
CommandCPPrintClusterInfo(
  int  argc, 
  char ** argv 
)
Prints out information about the clustering. ** DEPRECATED in 2.4 **

Defined in compileCmd.c 

int 
CommandEncodeVariables(
  int  argc, 
  char ** argv 
)
Builds the BDD variables necessary to compile the model into BDD.

Defined in compileCmd.c 

int 
CommandFlattenHierarchy(
  int  argc, 
  char ** argv 
)
Flattens the hierarchy of modules

Defined in compileCmd.c 

int 
CommandGetInternalStatus(
  int  argc, 
  char ** argv 
)
Implements the get_internal_status command

Defined in compileCmd.c 

int 
CommandGoBmc(
  int  argc, 
  char ** argv 
)
Implements the go_bmc command

Defined in compileCmd.c 

int 
CommandGo(
  int  argc, 
  char ** argv 
)
Implements the go command

Defined in compileCmd.c 

int 
CommandIwls95PrintOption(
  int  argc, 
  char ** argv 
)
Prints the Iwls95 Options.

Defined in compileCmd.c 

int 
CommandPrintFsmStats(
  int  argc, 
  char ** argv 
)
Prints out information about the fsm and clustering.

Defined in compileCmd.c 

int 
CommandProcessModel(
  int  argc, 
  char ** argv 
)
Performs the batch steps and then returns control to the interactive shell.

Defined in compileCmd.c 

int 
CommandShowDependencies(
  int  argc, 
  char ** argv 
)
Show expression dependencies

Defined in compileCmd.c 

int 
CommandShowVars(
  int  argc, 
  char ** argv 
)
Shows model's symbolic variables and their values

Defined in compileCmd.c 

int 
CommandWriteCoiModel(
  int  argc, 
  char ** argv 
)
Writes a flat model of a given SMV file, restricted to the COI of the model properties

Defined in compileCmd.c 

int 
CommandWriteModelFlatBool(
  int  argc, 
  char ** argv 
)
Writes a flat and boolean model of a given SMV file

Defined in compileCmd.c 

int 
CommandWriteModelFlatUdg(
  int  argc, 
  char ** argv 
)
Writes the currently loaded SMV model in the specified uDraw file, after having flattened it

Defined in compileCmd.c 

int 
CommandWriteModelFlat(
  int  argc, 
  char ** argv 
)
Writes the currently loaded SMV model in the specified file, after having flattened it

Defined in compileCmd.c 

int 
CommandWriteOrder(
  int  argc, 
  char ** argv 
)
Writes variable order to file.

Defined in compileCmd.c 

node_ptr 
CompileFlatten_expand_range(
  int  a, 
  int  b 
)
Returns a range going from a to b. An empty range (Nil) is returned whether given 'a' is greater than 'b'

Defined in compileFlatten.c 

void 
CompileFlatten_hash_module(
  node_ptr  parsed_module 
)
Add the tableau module (coming from parser) to the list of known modules. After this function has been invoked, the module will be recognized by the flattener

Defined in compileFlatten.c 

void 
CompileFlatten_init_flattener(
    
)
Inits all the internal structures, in order to correctly bootstrap the flattener

Side Effects This module will be initialized, all previously iniitalized data will be lost

Defined in compileFlatten.c 

node_ptr 
CompileFlatten_normalise_value_list(
  node_ptr  old_values 
)
Takes a list of values and returns the same list being normalised

Defined in compileFlatten.c 

void 
CompileFlatten_quit_flattener(
    
)
Resets all internal structures, in order to correctly shut down the flattener. Calls clear_* local functions, and resets all private variables.

Side Effects This module will be deinitialized, all previously iniitalized data will be lost

Defined in compileFlatten.c 

node_ptr 
CompileFlatten_resolve_define_chains(
  const SymbTable_ptr  symb_table, 
  node_ptr  expr, 
  node_ptr  context 
)
Sometimes a define may be equal to another define. This function will remove such chain of defines/parameters and return the actual expression or a fully resolved variable or constant identifier. This operation may be considered more like an optimization to avoid define chains, eg, during FSM output. NEXT is processed not as an expression but as a part of an identifier, i.e. its operand will be resolved as well. Note that array defines are not resolved to its definition.

Defined in compileFlatten.c 

node_ptr 
CompileFlatten_resolve_number(
  SymbTable_ptr  symb_table, 
  node_ptr  n, 
  node_ptr  context 
)
If given symbol is a number, the node is simply returned. If it is a define, the body is returned if it is a number. If it is an actuial parameter, it is evaluated. Otherwise NULL is returned. Notice that returned nodes can be NUMBER, NUMBER_SIGNED_WORD or NUMBER_UNSIGNED_WORD.

Defined in compileFlatten.c 

void 
Compile_CheckAssigns(
  const SymbTable_ptr  symb_table, 
  node_ptr  procs 
)
The function checks that there are no multiple assignments and circular definitions.
Then the functions tries to detect multiple assignments between different modules.

Defined in compileCheck.c 

void 
Compile_ConstructHierarchy(
  SymbTable_ptr  st, 
  SymbLayer_ptr  layer, 
  node_ptr  module_name, the ATOM representing the name of the module being instantiated
  node_ptr  instance_name, the name of the module instance to be instantiated
  node_ptr  actual, the actual module arguments
  FlatHierarchy_ptr  result, 
  HrcNode_ptr  hrc_result, 
  hash_ptr  instances 
)
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.

Defined in compileFlatten.c 

boolean 
Compile_DeclareVariable(
  SymbTable_ptr  st, 
  SymbLayer_ptr  layer, 
  node_ptr  name, 
  SymbType_ptr  type, 
  node_ptr  context, 
  Instantiation_Variables_Mode_Type  mode 
)
It takes as input a variable name, its type and a context, and depending on the type of the variable some operation are performed in order to instantiate it in the given context: Depending on the kind of variable instantiation mode the variables are appended to input_variables, frozen_variables or state_variables, respectively. Note that if type is ARRAY then the "name" is declared with SymbLayer_declare_variable_array and then subvariables are created. Returns true iff a variable (input,state or frozen) or array was created. PRECONDITION: type has to be not memory-shared, and its ownership is passed to this function.

See Also compile_instantiate_var
Defined in compileFlatten.c 

FlatHierarchy_ptr 
Compile_FlattenHierarchy(
  const SymbTable_ptr  symb_table, 
  SymbLayer_ptr  layer, 
  node_ptr  module_name, 
  node_ptr  inst_name, 
  node_ptr  actual, 
  boolean  create_process_variables, enables creation of process variables
  boolean  calc_vars_constr, triggers calc of vars constr, or delays it
  HrcNode_ptr  hrc_result hrc node to be populated
)
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). Most of the collected expressions are flattened. The returned value is a structure containing all the collected parts. See FlatHierarchy_create function for more info about, and constrains on content of the class FlatHierarchy. It is the invoker's responsibility to destroy the returned value. Parameter `create_process_variables` enables the creation of process variable (i.e. declaration of 'running's ). So, this parameter can be set up only for users 'main' modules. For auxiliary modules created during execution (for example, during LTL tablaue generation) this parameter should be set to false (as is done in ltl.c). Parameter calc_vars_constr controls the time association between constraints and variables is calculated. If true, the association is calculated before existing the function, otherwise it is possibly calculated later when needed, i.e. when FlatHierarchy_lookup_constrains is called. Postponing this calculation can be effective when vars constraints are not used in later phases. Any value of calc_vars_constr is safe, but having this parameter set to false possibly postpones calculations from the model construction phase to the model checking phase, when LTL MC is carried out, or when COI is involved. Parameter hrc_result contains the hrc node to be constructed from the model. If hrc_result is NULL then the structure is not populated.

Side Effects None

Defined in compileFlatten.c 

node_ptr 
Compile_FlattenSexpExpandDefine(
  const SymbTable_ptr  symb_table, 
  node_ptr  sexp, 
  node_ptr  context 
)
Flattens an expression and expands defined symbols.

See Also Flatten_GetDefinition Compile_FlattenSexp
Defined in compileFlatten.c 

node_ptr 
Compile_FlattenSexp(
  const SymbTable_ptr  symb_table, 
  node_ptr  sexp, 
  node_ptr  context 
)
Builds the flattened version of an expression. It does not expand defined symbols with the corresponding body.

See Also Flatten_GetDefinition Compile_FlattenSexpExpandDefine
Defined in compileFlatten.c 

SymbType_ptr 
Compile_InstantiateType(
  SymbTable_ptr  st, 
  SymbLayer_ptr  layer, 
  node_ptr  name, 
  node_ptr  type, 
  node_ptr  context 
)
All normal simple and complex types can be processed. Note that PROCESS and MOD_TYPE are not types and cannot be processed here. Parameter: st -- is symbol table where constants met in type can be evaluated. layer -- is layer where constants will be declared (for enum types). type -- is the type to be converted. name -- is the name of variable a given type is processed for. It is used only in error messaged and also additional checks are done wrt special var _process_selector_. If type is constructed incorrectly then error is raise. I.e. NULL is never returned. NOTE: An invoker has to free the returned type.

Defined in compileFlatten.c 

void 
Compile_ProcessHierarchy(
  SymbTable_ptr  symb_table, 
  SymbLayer_ptr  layer, 
  FlatHierarchy_ptr  hierarchy, 
  node_ptr  name, 
  boolean  create_process_variables, 
  boolean  calc_vars_constr 
)
This processing means: 1. process_selector variable and running defines are declared (only if create_process_variables is on) 2. All the required lists of expressions are reversed. All the constrains (not specifications) are flattened. 3. An association between vars and constrains are created (for ASSIGN, INIT, INVAR, TRANS). 4. Type checking of the variable and define declarations and of all the expressions. 5. Also a correct use of input variables and lack of circular dependences are checked. The parameters: layer is a layer with module variables. hierachy is a hierarchy to be process. name is a name of the module instance, i.e. a context of all expressions. create_process_variables enables creation of process variables.

Defined in compileFlatten.c 

void 
Compile_WriteBoolFsm_udg(
  FILE* out, 
  const SymbTable_ptr  st, 
  NodeList_ptr  layers, 
  const char* fsm_name, 
  BoolSexpFsm_ptr  bool_sexp_fsm 
)
Prints into the specified file the boolean FSM of an SMV model. bool_sexp_fsm should be a boolean Sexp FSM. layer_names is an array of layers whose variables will be printed, usually this parameter is a list of all layers committed to enc. The array should be ended by a NULL element.

Defined in compileWriteUdg.c 

void 
Compile_WriteBoolFsm(
  FILE* out, 
  const SymbTable_ptr  st, 
  NodeList_ptr  layers, 
  const char* fsm_name, 
  BoolSexpFsm_ptr  bool_sexp_fsm, 
  boolean  force_flattening 
)
Prints into the specified file the boolean FSM of an SMV model. bool_sexp_fsm should be a boolean Sexp FSM. layer_names is an array of layers whose variables will be printed, usually this parameter is a list of all layers committed to enc. The array should be ended by a NULL element.

Defined in compileWrite.c 

void 
Compile_WriteBoolModel_udg(
  FILE* out, 
  BddEnc_ptr  enc, 
  NodeList_ptr  layers, 
  const char* fsm_name, 
  BoolSexpFsm_ptr  bool_sexp_fsm 
)
Prints the given boolean model

Defined in compileWriteUdg.c 

void 
Compile_WriteBoolModel(
  FILE* out, 
  BddEnc_ptr  enc, 
  NodeList_ptr  layers, 
  const char* fsm_name, 
  BoolSexpFsm_ptr  bool_sexp_fsm, 
  boolean  force_flattening 
)
Prints the given boolean model

Defined in compileWrite.c 

void 
Compile_WriteBoolSpecs_udg(
  FILE* out, 
  BddEnc_ptr  enc, 
  FlatHierarchy_ptr  hierarchy 
)
Prints into the specified file the booleanized specifications of an SMV model. NOTE: a temporary layer will be created during the dumping for determinization variables that derived from the booleanization of the specifications. These variable declarations will be printed after the specs.

Defined in compileWriteUdg.c 

void 
Compile_WriteBoolSpecs(
  FILE* out, 
  BddEnc_ptr  enc, 
  FlatHierarchy_ptr  hierarchy 
)
Prints into the specified file the booleanized specifications of an SMV model. NOTE: a temporary layer will be created during the dumping for determinization variables that derived from the booleanization of the specifications. These variable declarations will be printed after the specs.

Defined in compileWrite.c 

void 
Compile_WriteFlattenFsm_udg(
  FILE* out, 
  const SymbTable_ptr  st, 
  const array_t* layer_names, 
  const char* fsm_name, 
  FlatHierarchy_ptr  hierarchy 
)
Prints on the specified file the flatten FSM of an SMV model, i.e. a list of all variable, defines, and all constrains (INIT, TRANS, INVAR, ASSIGNS, JUSTICE, COMPASSION). Specifications are NOT printed. layer_names is an array of names of layers that is typically obtained from the symbol table. fsm_name is a name of the output structure, usually it is "MODULE main".

Defined in compileWriteUdg.c 

void 
Compile_WriteFlattenFsm(
  FILE* out, 
  const SymbTable_ptr  st, 
  const array_t* layer_names, 
  const char* fsm_name, 
  FlatHierarchy_ptr  hierarchy, 
  boolean  force_flattening 
)
Prints on the specified file the flatten FSM of an SMV model, i.e. a list of all variable, defines, and all constrains (INIT, TRANS, INVAR, ASSIGNS, JUSTICE, COMPASSION). Specifications are NOT printed. layer_names is an array of names of layers that is typically obtained from the symbol table. fsm_name is a name of the output structure, usually it is "MODULE main".

Defined in compileWrite.c 

void 
Compile_WriteFlattenModel_udg(
  FILE* out, 
  const SymbTable_ptr  st, 
  const array_t* layer_names, 
  const char* fsm_name, 
  FlatHierarchy_ptr  hierarchy 
)

Defined in compileWriteUdg.c 

void 
Compile_WriteFlattenModel(
  FILE* out, 
  const SymbTable_ptr  st, 
  const array_t* layer_names, 
  const char* fsm_name, 
  FlatHierarchy_ptr  hierarchy, 
  boolean  force_flattening 
)

Defined in compileWrite.c 

void 
Compile_WriteFlattenSpecs_udg(
  FILE* out, 
  const SymbTable_ptr  st, 
  FlatHierarchy_ptr  hierarchy 
)
Prints into the specified file the flatten specifications.

Defined in compileWriteUdg.c 

void 
Compile_WriteFlattenSpecs(
  FILE* out, 
  const SymbTable_ptr  st, 
  FlatHierarchy_ptr  hierarchy, 
  boolean  force_flattening 
)
Prints into the specified file the flatten specifications.

Defined in compileWrite.c 

void 
Compile_WriteObfuscatedFlattenModel(
  FILE* out, 
  const SymbTable_ptr  st, 
  const array_t* layer_names, 
  const char* fsm_name, 
  FlatHierarchy_ptr  hierarchy, 
  boolean  print_map, 
  boolean  force_flattening 
)

Defined in compileWrite.c 

void 
Compile_WriteRestrictedFlattenModel(
  FILE* out, 
  const SymbTable_ptr  st, 
  const array_t* layer_names, 
  const char* fsm_name, 
  FlatHierarchy_ptr  hierarchy, 
  boolean  force_flattening 
)
Dumps the flatten model on the given FILE. The dumped model is restricted to the set of variables defined in the given FlatHierarchy

Defined in compileWrite.c 

int 
Compile_check_if_bool_model_was_built(
  FILE* err, 
  boolean  forced 
)
Returns 0 if constructed, 1 otherwise. If given file is not NULL, an error message is also printed out to it (typically, you will use nusmv_stderr). If forced is true, thatn the model is requested to be built even when COI is enabled.

Defined in compileUtil.c 

int 
Compile_check_if_encoding_was_built(
  FILE* err 
)
Returns 0 if constructed, 1 otherwise. If given file is not NULL, an error message is also printed out to it (typically, you will use nusmv_stderr)

Defined in compileUtil.c 

int 
Compile_check_if_flat_model_was_built(
  FILE* err, 
  boolean  forced 
)
Returns 0 if constructed, 1 otherwise. If given file is not NULL, an error message is also printed out to it (typically, you will use nusmv_stderr). If forced is true, than the model is requested to be built even when COI is enabled.

Defined in compileUtil.c 

int 
Compile_check_if_flattening_was_built(
  FILE* err 
)
Returns 0 if constructed, 1 otherwise. If given file is not NULL, an error message is also printed out to it (typically, you will use nusmv_stderr)

Defined in compileUtil.c 

int 
Compile_check_if_model_was_built(
  FILE* err, 
  boolean  forced 
)
Returns 0 if constructed, 1 otherwise. If given file is not NULL, an error message is also printed out to it (typically, you will use nusmv_stderr). Use this function from commands that require the model to be constructed for being executed.

Defined in compileUtil.c 

void 
Compile_check_input_next(
  const SymbTable_ptr  st, 
  node_ptr  expr, 
  node_ptr  context 
)
It outputs an error message (and rises an exception) iff the expression contains a next statement which itself has an input variable in it.

Defined in compileCheck.c 

void 
Compile_check_next(
  const SymbTable_ptr  st, 
  node_ptr  expr, 
  node_ptr  context, 
  boolean  is_one_next_allowed 
)
Checks that given expression contains either no nested next, or no next operator at all.

Defined in compileCheck.c 

void 
Compile_cleanup_booleanizer_cache_about(
  SymbTable_ptr  st, 
  NodeList_ptr  symbs 
)
Called by BoolEnc class when removing a layer

Defined in compileBEval.c 

node_ptr 
Compile_convert_to_dag_udg(
  SymbTable_ptr  symb_table, 
  node_ptr  expr, 
  hash_ptr  dag_hash, 
  hash_ptr  defines 
)
Top level function to create dags from expressions

Defined in compileWriteUdg.c 

node_ptr 
Compile_convert_to_dag(
  SymbTable_ptr  symb_table, 
  node_ptr  expr, 
  hash_ptr  dag_hash, 
  hash_ptr  defines 
)
Top level function to create dags from expressions

Defined in compileWrite.c 

void 
Compile_destroy_dag_info_udg(
  hash_ptr  dag_info, 
  hash_ptr  defines 
)
Warning: the hashes are not freed, only the content

Defined in compileWriteUdg.c 

void 
Compile_destroy_dag_info(
  hash_ptr  dag_info, 
  hash_ptr  defines 
)
Warning: the hashes are not freed, only the content

Defined in compileWrite.c 

Expr_ptr 
Compile_detexpr2bexpr_list(
  BddEnc_ptr  enc, 
  Expr_ptr  expr 
)
This function is exactly like Compile_detexpr2bexpr except that the input expressions is expected to be a list of expressions. The only purpose of this function wrt Compile_detexpr2bexpr is efficiency. For big model list of expressions may be huge and stack overflow may happen in Compile_detexpr2bexpr because the expressions are processed recursively whereas here top-level expressions are processed in loop. expr has to be a RIGHT-connected list of elements (i.e. car is head and cdr is tail). The connecting nodes have to be of type AND or CONS with the semantics of AND. The returned expression is a list of the same order but with the booleanized expressions and AND used as connector. NOTE: some simplifications are done, e.g. if FALSE is met among elements then FALSE is returned. NOTE: when the function see on the right a node of a type other than AND and CONS then right child is considered as the last element in the list. NOTE: special case: if NEXT is met at the top then its sub-expression is processed as a list. TODO: if in future is will be necessary to process lists of different connector kind, e.g. OR, it will be necessary to provided the kind as parameter. Still AND and CONS have to dealt the same way because in traces it is unspecified if AND or CONS is used in var=value lists.

Side Effects None

See Also Compile_detexpr2bexpr Compile_expr2bexpr expr2bexpr_recur
Defined in compileBEval.c 

Expr_ptr 
Compile_detexpr2bexpr(
  BddEnc_ptr  enc, 
  Expr_ptr  expr 
)
Takes an scalar expression intended to evaluate to boolean, maps through booleans down to the atomic scalar propositions, builds the corresponding boolean function, and returns the resulting boolean expression. The conversion of atomic scalar proposition is currently performed by generating the corresponding ADD, and then printing it in terms of binary variables. An error is returned if determinization variables are introduced in the booleanization process. The input expression will be processed with Nil context (for flattened expr this does not matter).

Side Effects None

See Also Compile_expr2bexpr expr2bexpr_recur Compile_detexpr2bexpr_list
Defined in compileBEval.c 

Expr_ptr 
Compile_expr2bexpr(
  BddEnc_ptr  enc, 
  SymbLayer_ptr  det_layer, 
  Expr_ptr  expr 
)
Takes an scalar expression intended to evaluate to boolean, maps through booleans down to the atomic scalar propositions, builds the corresponding boolean function, and returns the resulting boolean expression. The conversion of atomic scalar proposition is currently performed by generating the corresponding ADD, and then printing it in terms of binary variables. If one or more determinization variable must be created (i.e. non-determinism must be allowed) then det_layer is the SymbLayer instance to be filled with the newly created determinization variables. If non-determinism is not allowed, specify NULL as det_layer value. In this case you can use detexpr2bexpr as well. The input expression will be processed with Nil context (for flattened expr this does not matter).

Side Effects None

See Also Compile_detexpr2bexpr expr2bexpr_recur
Defined in compileBEval.c 

FsmBuilder_ptr 
Compile_get_global_fsm_builder(
    
)
See fsm/FsmBuilder.h for more info

Defined in compileStruct.c 

PredicateNormaliser_ptr 
Compile_get_global_predicate_normaliser(
    
)
See PredicateNormaliser.h for more info on predication normaliser.

Defined in compileStruct.c 

hash_ptr 
Compile_get_obfuscation_map(
  const SymbTable_ptr  symb_table 
)
Generates the obfuscation map

Defined in compileWrite.c 

void 
Compile_init_cmd(
    
)
Initializes the commands provided by this package

Defined in compileCmd.c 

void 
Compile_init(
    
)
Initializes the compile package. The set of commands must be explicitly initialized later by calling Compile_InitCmd.

Defined in compileCmd.c 

boolean 
Compile_is_expr_booleanizable(
  Expr_ptr  expr, 
  const SymbTable_ptr  st, 
  boolean  word_unbooleanizable, 
  hash_ptr  cache 
)
Check if an expr is of a finite range type. REMARK: Words are considered finite only if word_unbooleanizable is set to false If cache is not null whenever we encounter a formula in the cache we simply return the previously computed value, otherwise an internal and temporary map is used. NOTE: the internal representation of cache is private so the user should provide only caches generated by this function!

Side Effects none

Defined in compileBEval.c 

node_ptr 
Compile_make_dag_info_udg(
  node_ptr  expr, 
  hash_ptr  hash 
)
Returns a node COLON(NUMBER count, NUMBER depth)

Defined in compileWriteUdg.c 

node_ptr 
Compile_make_dag_info(
  node_ptr  expr, 
  hash_ptr  hash 
)
Returns a node COLON(NUMBER count, NUMBER depth)

Defined in compileWrite.c 

Set_t 
Compile_make_sorted_vars_list_from_order(
  const SymbTable_ptr  st, 
  const NodeList_ptr  vars, 
  const NodeList_ptr  vars_order 
)
This function can be used to construct an ordered list of symbols. The set of symbols is provided by the input list 'vars', whereas the ordering is provided by the 'vars_order' list, that can be an intersecting set over 'vars'. The resulting list will contain those symbols that occur in vars_order (respecting their order), plus all the symbols in vars that do not occur in vars_order, pushed at the end of the list. All duplicates (if any) will not occur into the resulting list. The returned set must be destroyed by the caller.

Defined in compileUtil.c 

node_ptr 
Compile_obfuscate_expression(
  const SymbTable_ptr  symb_table, 
  node_ptr  expr, 
  const hash_ptr  obfuscation_map 
)
Apply the obfuscation over an expression

Defined in compileWrite.c 

node_ptr 
Compile_pop_distrib_ops(
  node_ptr  prop 
)
Transformation rules are: 1) a :-> a 2) ( a) * ( b) :-> (a * b); 3) ( (a * b)) :-> (a * b); 4) ( ( a * b)) :-> (a * b); 5) ( ( a * b)) :-> (a * b); Where can be either: G|AG|H for * := & F|AF|O for * := | Given property can be both flattened or unflattened.

Defined in compileUtil.c 

void 
Compile_print_array_define_udg(
  FILE* out, 
  const node_ptr  n 
)
Prints a array define node to out file. This function is exported so the hrc package can use it.

Defined in compileWriteUdg.c 

void 
Compile_print_array_define(
  FILE* out, 
  const node_ptr  n 
)
Prints a array define node to out file. This function is exported so the hrc package can use it.

Defined in compileWrite.c 

void 
Compile_quit(
    
)
Shut down the compile package

Defined in compileCmd.c 

void 
Compile_write_dag_defines_udg(
  FILE* out, 
  hash_ptr  defines 
)

Defined in compileWriteUdg.c 

void 
Compile_write_dag_defines(
  FILE* out, 
  hash_ptr  defines 
)

Defined in compileWrite.c 

Set_t 
ComputeCOIFixpoint(
  const SymbTable_ptr  symb_table, 
  const FlatHierarchy_ptr  hierarchy, 
  const Expr_ptr  expression, 
  const int  steps, 
  boolean* reached_fixpoint 
)
Computes the COI of a given expression, up to step "steps" (or fixpoint if steps = -1). If not NULL, if the fixpoint has been reached (ie: there are no more dependencies), reached_fixpoint is set to true.

Defined in compileCone.c 

Set_t 
ComputeCOI(
  const SymbTable_ptr  symb_table, 
  Set_t  base 
)
Computes the COI of a given set of variables, defined within the given symb_table. Returned Set must be disposed by the caller

Defined in compileCone.c 

node_ptr 
Flatten_GetDefinition(
  const SymbTable_ptr  symb_table, 
  node_ptr  atom 
)
Gets the flattened version of an atom. If the atom is a define then it is expanded. If the definition mode is set to "expand", then the expanded flattened version is returned, otherwise, the atom is returned.

Side Effects The flatten_def_hash is modified in order to memoize previously computed definition expansion.

Defined in compileFlatten.c 

void 
Flatten_remove_symbol_info(
  node_ptr  name 
)
This method is used when removing symbols (for example, when removing a layer) as some information about that symbol may be chached internally to this module. For example this is the case of defines, whose flatten body are privately cached within this module. If the symbol is not cached or have no associated information, no action is taken.

Defined in compileFlatten.c 

Set_t 
Formula_GetConstants(
  const SymbTable_ptr  symb_table, 
  node_ptr  formula, 
  node_ptr  context 
)
Given a formula the set of constants occurring in them is computed and returned. Returned set must be disposed by the caller

Defined in compileCone.c 

Set_t 
Formula_GetDependenciesByType(
  const SymbTable_ptr  symb_table, 
  node_ptr  formula, 
  node_ptr  context, 
  SymbFilterType  filter, 
  boolean  preserve_time 
)
The set of dependencies of a given formula are computed, as in Formula_GetDependencies, but the variable type filters the dependency collection. If flag preserve_time is true, then entries in the returned set will preserve the time they occur within the formula. For example, formula 'a & next(b) = 2 & attime(c, 2) < 4' returns {a,b,c} if preserve_time is false, and {a, next(b), attime(c, 2)} if preserve_time is true. Returned set must be disposed by the caller

See Also formulaGetDependenciesByTypeAux formulaGetDefinitionDependencies
Defined in compileCone.c 

Set_t 
Formula_GetDependencies(
  const SymbTable_ptr  symb_table, 
  node_ptr  formula, 
  node_ptr  context 
)
The set of dependencies of a given formula are computed. A traversal of the formula is performed. Each time a variable is encountered, it is added to the so far computed set. When a formula depends on a next variable, then the corresponding current variable is added to the set. When an atom is found a call to formulaGetDefinitionDependencies is performed to compute the dependencies. Returned set must be disposed by the caller

See Also formulaGetDefinitionDependencies
Defined in compileCone.c 

Set_t 
Formulae_GetDependencies(
  const SymbTable_ptr  symb_table, 
  node_ptr  formula, 
  node_ptr  justice, 
  node_ptr  compassion 
)
Given a formula and a list of fairness constraints, the set of variables occurring in them is computed. Returned Set must be disposed by the caller

Defined in compileCone.c 

static int 
UsageWriteCoiModel(
    
)
Prints the usage for the write_coi_command

Defined in compileCmd.c 

node_ptr 
__create_define_name(
  SymbTable_ptr  st, 
  const char * prefix, 
  node_ptr  body 
)
Creates a meaningful name for defines needed for dag printing

Defined in compileWrite.c 

static Set_t 
_coi_get_var_coi0(
  SymbTable_ptr  st, 
  FlatHierarchy_ptr  hierarchy, 
  node_ptr  var, 
  boolean * nonassign, 
  boolean  use_cache 
)
Given a variable it returns the cone at depth 0. If use_cache is true, then the result is memoized on the cache. When use_cache is true, it is assumed the hierarchy to be the mainFlatHierarchy. An assertion enforces this condition.

Side Effects required

See Also optional
Defined in compileCone.c 

static void 
check_assign_both(
  node_ptr  v, 
  int  node_type, 
  int  lineno 
)
Checks if there exists in the model an assignments of type node_type for variable v. If such an assignment exists, then an error is generated.

Defined in compileCheck.c 

static void 
check_assign(
  const SymbTable_ptr  symb_table, 
  node_ptr  n, 
  node_ptr  context, 
  int  mode 
)
This function detects either multiple or circular assignments in "context" regarding to "mode". If mode is equal to 0 (zero) then it checks for multiple assignments or symbols redefinition. Otherwise it performs checks for circular assignments.

Defined in compileCheck.c 

static void 
check_circular_assign(
  const SymbTable_ptr  symb_table, 
  node_ptr  n, 
  node_ptr  context, 
  boolean  is_next, 
  boolean  is_lhs, 
  boolean  lhs_is_next 
)
Checks for circular assignments in the model. If there are any, then an error is generated. NEXT operator, if any, must be stripped away from given expression 'n', and in that case is_next must be set to true. Parameter is_lhs is true at the first call (done with the first left-hand-side value (the assigned value)

Defined in compileCheck.c 

static void 
check_circ(
  const SymbTable_ptr  symb_table, 
  node_ptr  n, 
  node_ptr  context, 
  boolean  is_next, 
  boolean  lhs_is_next 
)
This function checks for circular definition of any kind. This function is able to detect circularity of the following kinds: where alpha(x) (alpha(next(x))) is a formula in which the variable x (next(x)) occurs. Notice that next(alpha(x)) can be rewritten in term of next(x), since the next operator distributes along all kind of operators.
Here we check also the case where we have next(x), and x is a symbol declared as DEFINE whose body contain a next(v). These kind of formulas cannot be checked at parsing time, since, it would require to knowledge of part of the model that might be possibly parsed later. And removing next from the body of DEFINE is a too restrictive choice.

Defined in compileCheck.c 

cmp_struct_ptr 
cmp_struct_init(
    
)
Initializes the cmp structure

Defined in compileStruct.c 

void 
cmp_struct_quit(
  cmp_struct_ptr  cmp 
)
Free the cmp structure

Defined in compileStruct.c 

static void 
coiInit(
  const SymbTable_ptr  symb_table, 
  FlatHierarchy_ptr  hierarchy 
)
Computes the COI of all the variables occurring within the symbol table

See Also ComputeCOI
Defined in compileCone.c 

static void 
compileCheckAssignForInputVars(
  SymbTable_ptr  symb_table, 
  node_ptr  assign, 
  FlatHierarchy_ptr  hierarchy 
)
If the flattened assign statement contains input variables then this function will print out an error message. Note that input variables are allowed in some parts of an assign statement. They're not allowed anywhere in an init section and cannot be contained within a next statement inside a next declaration.

Defined in compileCheck.c 

void 
compileCheckForInputVars(
  const SymbTable_ptr  symb_table, 
  node_ptr  trans_expr, 
  node_ptr  init_expr, 
  node_ptr  invar_expr, 
  node_ptr  assign_expr, 
  FlatHierarchy_ptr  hierarchy 
)
Checks the TRANS, INIT, INVAR and ASSIGN statements to make sure that input variables are not used where they should not be. That is, anywhere in a TRANS, INIT or INVAR statement and within next expressions in the init and next sections of an ASSIGN statement.

Defined in compileCheck.c 

static void 
compileCheckInitForInputVars(
  SymbTable_ptr  symb_table, 
  node_ptr  init 
)
If the flattened init statement contains input variables then this function will print out an error message.

Defined in compileCheck.c 

static void 
compileCheckInvarForInputVars(
  SymbTable_ptr  symb_table, 
  node_ptr  invar 
)
If the flattened invar statement contains input variables then this function will print out an error message.

Defined in compileCheck.c 

static void 
compileCheckNoNextInputs(
  SymbTable_ptr  symb_table, 
  node_ptr  expr, 
  node_ptr  ctx 
)
It outputs an error message (and rises an exception) iff the expression contains a next statement which itself has an input variable in it.

Defined in compileCheck.c 

static void 
compileCheckTransForInputVars(
  SymbTable_ptr  symb_table, 
  node_ptr  trans 
)
If the flattened trans statement contains input variables within next() statements then this function will print out an error message.

Defined in compileCheck.c 

static void 
compileFlattenProcessRecur(
  const SymbTable_ptr  symb_table, 
  node_ptr  assign, 
  node_ptr  context, 
  node_ptr  running, 
  FlatHierarchy_ptr  flatHierarchy 
)
Recursive definition of compileFlattenProcess. If running is Nil there are no processes => no need to create data structure with CASEs (for next-assignments).

Defined in compileFlatten.c 

static node_ptr 
compileFlattenProcess(
  const SymbTable_ptr  symb_table, 
  node_ptr  proc_assign_list, 
  FlatHierarchy_ptr  flattenHierarchy 
)
This functions takes in input the list of process names and their assignments resulting from the instantiation step and fills in the hash table (parameter assign_hash) with the associations the following form:
  • init(var) -> (init_assign)
    where init_assign is the right side of the initialization assignement of the variable var.
  • next(var) -> (case P1.running : next_assign_1; case P2.running : next_assign_2; ... var)
    where next_assign_i is the right side of the next assignement for the variable var in process i. When other processes not affecting the variable are running, the variable stutter. If there are no processes the data structure will degenerate into next(var) -> next_assign.
  • var -> (normal_assign)
    where normal_assign is the right side of the normal (invariant) assignement for the variable var.
The parameter proc_assignment_list is a list of pairs (process_name, a list of assignment in the process).

Defined in compileFlatten.c 

static node_ptr 
compileFlattenSexpRecur(
  const SymbTable_ptr  symb_table, 
  node_ptr  sexp, 
  node_ptr  context 
)
DOCUMENTATION ABOUT ARRAY: In NuSMV ARRAY has 2 meanings, it can be a part of identifier (which we call identifier-with-brackets) or a part of expression. For example, VAR v[5

See Also Compile_FlattenSexp Compile_FlattenSexpExpandDefine
Defined in compileFlatten.c 

void 
compile_add_vars_to_hierarhcy(
  node_ptr  name, 
  SymbType_ptr  type, 
  FlatHierarchy_ptr  fh 
)
Given a fully resolved array name and its type the function adds all the variables in the array to the hierarchy

Defined in compileFlatten.c 

void 
compile_build_model(
  boolean  force_build 
)
Builds the BDD fsm.

Defined in compileCmd.c 

void 
compile_check_print_io_atom_stack_assign(
  FILE * fd 
)

Defined in compileCheck.c 

node_ptr 
compile_cmd_get_var_type(
  SymbType_ptr  type 
)
Creates an internal representaion of the symbol type. The representation of the type returned is intended to be used only with the compile_cmd_print_type procedure. If 2 types are the same, the same node is returned

Defined in compileCmd.c 

void 
compile_cmd_print_type(
  FILE * file, 
  node_ptr  ntype, 
  int  threshold 
)
Prints the given type to the given stream. The type must be created with the compile_cmd_get_var_type function. If the type is scalar, then values are printed until "threshold" number of characters are reached. If some values are missing because of the threshold, then "other # values" is added in output

Defined in compileCmd.c 

Expr_ptr 
compile_cmd_remove_assignments(
  Expr_ptr  expr 
)
Removes expression in the form "a := b" from the given expression. The new expression is returned

Defined in compileCmd.c 

void 
compile_cmd_write_coi_prop_fsm(
  FlatHierarchy_ptr  fh, 
  Set_t  cone, 
  Set_t  props, 
  FILE* output_file 
)
Dumps the model applied to COI for the given property

Defined in compileCmd.c 

void 
compile_cmd_write_coi_prop(
  Set_t  cone, 
  Set_t  props, 
  FILE* output_file 
)
Dumps the COI for the given property

Defined in compileCmd.c 

void 
compile_cmd_write_global_coi_fsm(
  FlatHierarchy_ptr  hierarchy, 
  Prop_Type  prop_type, 
  FILE* output_file 
)
Dumps on output_file the FSM built using the union of all properties cone of influence. Properties can be filtered by type using prop_type: if prop_type == Prop_NoType, all properties are used

Defined in compileCmd.c 

int 
compile_cmd_write_properties_coi(
  FlatHierarchy_ptr  hierarchy, 
  Prop_Type  prop_type, 
  boolean  only_dump_coi, 
  const char* file_name 
)
Dumps properties shared COI informations. If only_dump_coi is true, only the set of variables in the cone of each property is dumped. Otherwise, an FSM is created and dumped. Properties with the same COI will appear in the same FSM. Properties can be filtered by type using prop_type: if prop_type == Prop_NoType, all properties are used

Defined in compileCmd.c 

node_ptr 
compile_concat_contexts(
  node_ptr  ctx1, 
  node_ptr  ctx2 
)
Since contexts are organized bottom-up ("a.b.c" becomes DOT / \ DOT c / \ a b ) ctx2 is appended to ctx1 by concatenating ctx1 to ctx2. For example if ctx1="c.d.e" and ctx2="a.b.c", node 'a' is searched in ctx2, and then substituted by / ... DOT / \ ->> DOT b / \ (ctx1) a Important: nodes in ctx2 are traversed and possibly recreated with find_node

Defined in compileFlatten.c 

node_ptr 
compile_convert_to_dag_aux_udg(
  SymbTable_ptr  symb_table, 
  node_ptr  expr, 
  hash_ptr  hash, 
  unsigned int  num_thres, 
  unsigned int  dep_thres, 
  hash_ptr  defines, 
  const char* defines_prefix 
)
Private service of function Compile_convert_to_dag_udg

Defined in compileWriteUdg.c 

node_ptr 
compile_convert_to_dag_aux(
  SymbTable_ptr  symb_table, 
  node_ptr  expr, 
  hash_ptr  hash, 
  unsigned int  num_thres, 
  unsigned int  dep_thres, 
  hash_ptr  defines, 
  const char* defines_prefix 
)
Private service of function Compile_convert_to_dag

Defined in compileWrite.c 

void 
compile_create_boolean_model(
    
)
The newly created layer will be committed to both the boolean and bdd encodings. Warning: it is assumed here that the flat model has been already created

Defined in compileCmd.c 

hash_ptr 
compile_create_dag_info_from_hierarchy_udg(
  SymbTable_ptr  st, 
  FlatHierarchy_ptr  hierarchy, 
  SymbLayer_ptr  det_layer, 
  BddEnc_ptr  enc 
)
If det_layer is not NULL, then hierarchy is to be considered boolean, and specifications will be booleanized, If det_layer is null, then also enc can be null

Defined in compileWriteUdg.c 

hash_ptr 
compile_create_dag_info_from_hierarchy(
  SymbTable_ptr  st, 
  FlatHierarchy_ptr  hierarchy, 
  SymbLayer_ptr  det_layer, 
  BddEnc_ptr  enc, 
  boolean  force_flattening, 
  hash_ptr  cdh 
)
If det_layer is not NULL, then hierarchy is to be considered boolean, and specifications will be booleanized, If det_layer is null, then also enc can be null

Defined in compileWrite.c 

void 
compile_create_flat_model(
    
)
creates the master scalar fsm if needed

Defined in compileCmd.c 

int 
compile_encode_variables(
    
)
Encodes variables in the model (BDD only).

Defined in compileCmd.c 

node_ptr 
compile_flatten_build_word_toint_ith_bit_case(
  node_ptr  wexpr, 
  int  bit, 
  boolean  is_neg 
)
Creates the following expression: wexpr[bit:bit

Defined in compileFlatten.c 

node_ptr 
compile_flatten_eval_number(
  SymbTable_ptr  st, 
  node_ptr  n, 
  node_ptr  context 
)
This is a private service of function CompileFlatten_resolve_number

Defined in compileFlatten.c 

int 
compile_flatten_get_int(
  node_ptr  value 
)
It is an error if overflow/underflow happens

Defined in compileFlatten.c 

node_ptr 
compile_flatten_normalise_value_list(
  node_ptr  old_value_list 
)
The normalisation includes: all TRUE and FALSE constants are substituted by 1 and 0 numbers

Defined in compileFlatten.c 

node_ptr 
compile_flatten_rewrite_word_toint_cast(
  node_ptr  body, 
  SymbType_ptr  type 
)
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

Defined in compileFlatten.c 

int 
compile_flatten_smv(
  boolean  calc_vars_constrains 
)
Traverses the parse tree coming from the smv parser and flattens the smv file.

Defined in compileCmd.c 

assoc_retval 
compile_free_define_udg(
  char * key, 
  char * data, 
  char * arg 
)
Internal service of Compile_destroy_dag_info_udg

Defined in compileWriteUdg.c 

assoc_retval 
compile_free_define(
  char * key, 
  char * data, 
  char * arg 
)
Internal service of Compile_destroy_dag_info

Defined in compileWrite.c 

assoc_retval 
compile_free_node_udg(
  char * key, 
  char * data, 
  char * arg 
)
Internal service of Compile_destroy_dag_info_udg

Defined in compileWriteUdg.c 

assoc_retval 
compile_free_node(
  char * key, 
  char * data, 
  char * arg 
)
Internal service of Compile_destroy_dag_info

Defined in compileWrite.c 

node_ptr 
compile_get_rid_of_define_chain(
  SymbTable_ptr  st, 
  node_ptr  expr, 
  hash_ptr  cdh 
)
Get rids of chain of defines until it reaches a DEFINE whose body is not atomic (i.e. a variable, a constant, or a complex expression). It assumes the expression being flattened.

Defined in compileWrite.c 

void 
compile_insert_assign_hrc(
  HrcNode_ptr  hrc_result, 
  node_ptr  cur_decl 
)
Add an assign declaration in hrc_result. The type of assign is inferred by the node type found.

Side Effects Contents of hrc_result is changed adding an assign constraint.

Defined in compileFlatten.c 

void 
compile_instantiate_by_name(
  SymbTable_ptr  st, 
  SymbLayer_ptr  layer, 
  node_ptr  module_name, 
  node_ptr  instance_name, 
  node_ptr  actual, 
  node_ptr * assign, 
  FlatHierarchy_ptr  result, 
  HrcNode_ptr  hrc_result, 
  hash_ptr  instances 
)
module_name is the name of the module being instantiated. The name of the module instance is instance_name. First checks if the module exists. Then it checks if the module is recursively defined, and if the case an error is printed out. If these checks are passed, then it proceeds in the instantiation of the body of the module.

Defined in compileFlatten.c 

void 
compile_instantiate_vars(
  SymbTable_ptr  st, 
  SymbLayer_ptr  layer, 
  node_ptr  var_list, 
  node_ptr  mod_name, 
  node_ptr * assign, 
  FlatHierarchy_ptr  result, 
  HrcNode_ptr  hrc_result, 
  hash_ptr  instances 
)
Recursively applies compile_instantiate_var to a given list of variables declaration, and performs some check for multiple variable definitions.

See Also compile_instantiate_var
Defined in compileFlatten.c 

void 
compile_instantiate_var(
  SymbTable_ptr  st, 
  SymbLayer_ptr  layer, 
  node_ptr  name, 
  node_ptr  type, 
  node_ptr  context, 
  node_ptr * assign, 
  FlatHierarchy_ptr  result, 
  HrcNode_ptr  hrc_result, 
  hash_ptr  instances 
)
It takes as input a variable and a context, and depending on the type of the variable some operation are performed in order to instantiate it in the given context:

  • BOOLEAN
    if the variable is of type boolean, then we add an entry in symbol_hash saying that the variable values are {0,1}.
  • RANGE
    if the variable is a range of the form M..N, then we add an entry in the symbol_hash saying that the variable values are {M, M+1, ..., N-1, N}. If M is less or equal to N, than an error occurs.
  • ENUMERATION
    if the variable is a scalar variable whose possible values are {a1, a2, ..., aN}, then we add an entry in the symbol_hash saying that the variable values are {a1, ..., aN}.
  • ARRAY
    for each element of the array it is created the corresponding symbol. Suppose you have the following definition "VAR x : array 1..4 of boolean;". We call this function for 4 times, asking at each call i (i from 1 to 4) to declare the boolean variable x[i].
  • MODULE
    If the variable is an instantiation of a module, than their arguments (if any) are contextualized, and passed as actual parameter to instantiate_by_name with the name of the instantiated module as root name (to extract its definition) and as variable name as the name of the module (to perform flattening).
  • PROCESS
    If the variable is of type process, than we extract the module name and args, we perform the contextualization of the process arguments and we perform a call to Compile_ConstructHierarchy using the variable name as process name (to perform flattening), the module name as root name (to extract its definition) and the computed actual parameters.

Depending on the kind of variable instantiation mode the variables of type boolean, scalar, and array are appended to input_variables, frozen_variables or state_variables, respectively.

See Also compile_instantiate_vars
Defined in compileFlatten.c 

void 
compile_instantiate(
  SymbTable_ptr  st, 
  SymbLayer_ptr  layer, 
  node_ptr  mod_def, 
  node_ptr  mod_name, 
  node_ptr  actual, 
  node_ptr * assign, 
  FlatHierarchy_ptr  result, 
  HrcNode_ptr  hrc_result, 
  hash_ptr  instances 
)
This function is responsible of the instantiation of the body of a module. The module definition (parameter and body) is mod_def and the module instance name mod_name are passed as arguments. First we instantiate the arguments of the given module. Then it loops over the module definition searching for defined symbols (i.e. those introduced by the keyword DEFINE) and inserts their definition in the symbol_hash. After this preliminary phase it loops again over module body in order to performs the other instantiation, and to extract all the information needed to compile the automaton, i.e. the list of processes, the TRANS statements, the INIT statements, ... and so on. NB: After parsing and creating the module hash table, the order of declarations is correct (not reversed). This function reverse the order of SPEC, LTLSPEC, PSLSPEC, INVARSPEC, COMPUTE, JUSTICE AND COMPATION

See Also compile_instantiate_var compile_instantiate_vars
Defined in compileFlatten.c 

boolean 
compile_is_booleanizable_aux(
  Expr_ptr  expr, 
  const SymbTable_ptr  st, 
  boolean  word_unbooleanizable, 
  hash_ptr  cache 
)
Private service of compile_is_booleanizable. To represent 'true' in cache we use the constant 2 for 'false' we use 1 to avoid representation problems wrt Nil

Side Effects cache can be updated

Defined in compileBEval.c 

node_ptr 
compile_make_dag_info_aux_udg(
  node_ptr  expr, 
  hash_ptr  hash 
)
Returns a node COLON(NUMBER count, NUMBER depth)

Defined in compileWriteUdg.c 

node_ptr 
compile_make_dag_info_aux(
  node_ptr  expr, 
  hash_ptr  hash 
)
Returns a node COLON(NUMBER count, NUMBER depth)

Defined in compileWrite.c 

node_ptr 
compile_pack_dag_info_udg(
  unsigned int  count, 
  unsigned int  depth 
)
Packs given count and depth into a node

Defined in compileWriteUdg.c 

node_ptr 
compile_pack_dag_info(
  unsigned int  count, 
  unsigned int  depth, 
  boolean  admissible 
)
Packs given count and depth into a node

Defined in compileWrite.c 

void 
compile_print_assign_udg(
  SymbTable_ptr  st, 
  FILE * out, 
  node_ptr  lhs, 
  node_ptr  rhs, 
  hash_ptr  dag_info, 
  hash_ptr  defines 
)
Prints an assignement statement

Defined in compileWriteUdg.c 

void 
compile_print_assign(
  SymbTable_ptr  st, 
  FILE * out, 
  node_ptr  lhs, 
  node_ptr  rhs, 
  hash_ptr  dag_info, 
  hash_ptr  defines 
)
Prints an assignement statement

Defined in compileWrite.c 

void 
compile_set_dag_info_udg(
  node_ptr  info, 
  unsigned int  count, 
  unsigned int  depth 
)
Sets count and depth

Defined in compileWriteUdg.c 

void 
compile_set_dag_info(
  node_ptr  info, 
  unsigned int  count, 
  unsigned int  depth, 
  boolean  admissible 
)
Sets count and depth

Defined in compileWrite.c 

void 
compile_symbtype_obfuscated_print(
  SymbType_ptr  type, 
  FILE* out, 
  const SymbTable_ptr  symb_table, 
  hash_ptr  obfuscation_map 
)
Prints the obfuscation of the given type

Defined in compileWrite.c 

void 
compile_unpack_dag_info_udg(
  node_ptr  info, 
  unsigned int* count, 
  unsigned int* depth 
)
Unpacks given node to count and deptch

Defined in compileWriteUdg.c 

void 
compile_unpack_dag_info(
  node_ptr  info, 
  unsigned int* count, 
  unsigned int* depth, 
  boolean* admissible 
)
Unpacks given node to count and deptch

Defined in compileWrite.c 

void 
compile_write_bool_fsm(
  FILE* out, 
  const SymbTable_ptr  symb_table, 
  NodeList_ptr  layers, 
  const char* fsm_name, 
  BoolSexpFsm_ptr  bool_sexp_fsm, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  boolean  force_flattening, 
  hash_ptr  cdh 
)
Prints into the specified file the boolean FSM of an SMV model. bool_sexp_fsm should be a boolean Sexp FSM. layer_names is an array of layers whose variables will be printed, usually this parameter is a list of all layers committed to enc. The array should be ended by a NULL element.

Defined in compileWrite.c 

void 
compile_write_bool_specs(
  FILE* out, 
  BddEnc_ptr  enc, 
  SymbLayer_ptr  det_layer, 
  FlatHierarchy_ptr  hierarchy, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  hash_ptr  cdh 
)
Prints into the specified file the booleanized specifications of an SMV model. NOTE: a temporary layer will be created during the dumping for determinization variables that derived from the booleanization of the specifications. These variable declarations will be printed after the specs.

Defined in compileWrite.c 

void 
compile_write_bool_spec(
  FILE* out, 
  BddEnc_ptr  enc, 
  node_ptr  spec, 
  const char* msg, 
  SymbLayer_ptr  det_layer, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  hash_ptr  cdh 
)
Private service to print a boolean specification

Defined in compileWrite.c 

int 
compile_write_constants(
  const SymbTable_ptr  symb_table, 
  FILE* out 
)
Returns 1 if at least one char have been written, 0 otherwise

Defined in compileWrite.c 

int 
compile_write_flat_array_define_udg(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  const NodeList_ptr  names, 
  hash_ptr  dag_info, 
  hash_ptr  defines 
)
Writes ARRAY DEFINE declarations in SMV format on a file.

Defined in compileWriteUdg.c 

int 
compile_write_flat_asgn(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  const NodeList_ptr  vars, 
  FlatHierarchy_ptr  hierarchy, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  hash_ptr  cdh 
)
Writes flattened ASSIGN declarations in SMV format on a file.

Defined in compileWrite.c 

int 
compile_write_flat_define_aux(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  name, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  hash_ptr  printed_arrays, 
  boolean  force_flattening 
)
If a define happens to be an array define's element then array is output (and remembered in printed_arrays) instead of the original identifiers.

Defined in compileWrite.c 

int 
compile_write_flat_define(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  const NodeList_ptr  names, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  boolean  force_flattening 
)
Writes DEFINE declarations in SMV format on a file.

Defined in compileWrite.c 

void 
compile_write_flat_fsm(
  FILE* out, 
  const SymbTable_ptr  symb_table, 
  const array_t* layer_names, 
  const char* fsm_name, 
  FlatHierarchy_ptr  hierarchy, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  boolean  force_flattening, 
  hash_ptr  cdh 
)
Prints on the specified file the flatten FSM of an SMV model, i.e. a list of all variable, defines, and all constrains (INIT, TRANS, INVAR, ASSIGNS, JUSTICE, COMPASSION). Specifications are NOT printed. layer_names is an array of names of layers that is typically obtained from the symbol table. fsm_name is a name of the output structure, usually it is "MODULE main".

Defined in compileWrite.c 

void 
compile_write_flat_specs(
  FILE* out, 
  const SymbTable_ptr  st, 
  FlatHierarchy_ptr  hierarchy, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  boolean  force_flattening, 
  hash_ptr  cdh 
)
Prints into the specified file the specifications of an SMV model.

Defined in compileWrite.c 

void 
compile_write_flat_spec(
  FILE* out, 
  const SymbTable_ptr  symb_table, 
  node_ptr  spec, 
  const char* msg, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  boolean  force_flattening, 
  hash_ptr  cdh 
)
Prints into the specified file the flatten specifications.

Defined in compileWrite.c 

int 
compile_write_flatten_bfexpr(
  BddEnc_ptr  enc, 
  const SymbTable_ptr  symb_table, 
  SymbLayer_ptr  det_layer, 
  FILE* out, 
  node_ptr  n, 
  const char* s, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  hash_ptr  cdh 
)
Writes a generic expression prefixed by a given string in SMV format on a file. The given layer is intended to hold the determization variables that are created by the booleanization process of the properties, that are kept not booleanized within the system.

Defined in compileWrite.c 

int 
compile_write_flatten_bool_vars(
  const SymbTable_ptr  symb_table, 
  const BoolEnc_ptr  bool_enc, 
  FILE* out, 
  NodeList_ptr  vars 
)
Writes boolean VAR, FROZENVAR and IVAR declarations in SMV format on a file. Non boolean vars are dumped as defines for the sake of readability of conterexamples.

Defined in compileWrite.c 

int 
compile_write_flatten_expr_pair(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  l, 
  const char* s, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  boolean  force_flattening, 
  hash_ptr  cdh 
)
Writes a list of flattened expression pairs prefixed by a given string in SMV format on a file.

Defined in compileWrite.c 

int 
compile_write_flatten_expr_split(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  n, 
  const char* s, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  boolean  force_flattening, 
  hash_ptr  cdh 
)
Writes a generic expression prefixed by a given string in SMV format on a file.

Defined in compileWrite.c 

int 
compile_write_flatten_expr(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  n, 
  const char* s, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  boolean  force_flattening, 
  hash_ptr  cdh 
)
Writes a generic expression prefixed by a given string in SMV format on a file. Returns true if at least one character was printed, and false otherwise.

Defined in compileWrite.c 

int 
compile_write_flatten_psl(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  n, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  hash_ptr  cdh 
)
Writes PSL properties as they are.

Defined in compileWrite.c 

int 
compile_write_flatten_spec_split(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  n, 
  const char* s, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  boolean  force_flattening, 
  hash_ptr  cdh 
)
Writes a generic spec prefixed by a given string in SMV format on a file.

Defined in compileWrite.c 

int 
compile_write_flatten_spec(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  n, 
  const char* s, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  boolean  force_flattening, 
  hash_ptr  cdh 
)
Writes a generic spec prefixed by a given string in SMV format on a file. Returns true if at least one character was printed, and false otherwise.

Defined in compileWrite.c 

int 
compile_write_flatten_vars_aux(
  const SymbTable_ptr  symb_table, 
  const node_ptr  name, 
  FILE* out, 
  hash_ptr  printed 
)
If the identifier contains an index subscript in its name then at first the identifier check for being a part of an array. In this case array is output (and remembered in "printed") instead of the var. Otherwise, the identifier is output.

Defined in compileWrite.c 

int 
compile_write_flatten_vars(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  NodeList_ptr  vars 
)
Writes VAR, FROZENVAR, and IVAR declarations in SMV format on a file.

Defined in compileWrite.c 

NodeList_ptr 
compile_write_get_restricted_vars(
  Set_t  keep_vars, 
  NodeList_ptr  all_vars 
)
Processes the intersection between the given set and the given list

Defined in compileWrite.c 

int 
compile_write_obfuscated_constants(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  hash_ptr  obfuscation_map 
)
Returns 1 if at least one char have been written, 0 otherwise

Defined in compileWrite.c 

void 
compile_write_obfuscated_dag_defines(
  FILE* out, 
  const SymbTable_ptr  st, 
  hash_ptr  defines, 
  hash_ptr  obfuscation_map 
)

Defined in compileWrite.c 

int 
compile_write_obfuscated_flat_asgn(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  const NodeList_ptr  vars, 
  FlatHierarchy_ptr  hierarchy, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  hash_ptr  obfuscation_map, 
  hash_ptr  cdh 
)
Writes flattened ASSIGN declarations in SMV format on a file.

Defined in compileWrite.c 

int 
compile_write_obfuscated_flat_define_aux(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  name, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  hash_ptr  printed_arrays, 
  hash_ptr  obfuscation_map, 
  boolean  force_flattening 
)
This function behaves example like compile_write_flat_define_aux except that identifiers are obfuscated before being printed.

See Also compile_write_flat_define_aux
Defined in compileWrite.c 

int 
compile_write_obfuscated_flat_define(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  const NodeList_ptr  names, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  hash_ptr  obfuscation_map, 
  boolean  force_flattening 
)
This function behaves exactly like compile_write_flat_define except that identifiers a re obfuscated before.

Defined in compileWrite.c 

void 
compile_write_obfuscated_flat_fsm(
  FILE* out, 
  const SymbTable_ptr  symb_table, 
  const array_t* layer_names, 
  const char* fsm_name, 
  FlatHierarchy_ptr  hierarchy, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  hash_ptr  obfuscation_map, 
  boolean  force_flattening, 
  hash_ptr  cdh 
)
Prints the obfuscated flatten version of FSM of an SMV model.

See Also compile_write_flat_fsm
Defined in compileWrite.c 

void 
compile_write_obfuscated_flat_specs(
  FILE* out, 
  const SymbTable_ptr  st, 
  FlatHierarchy_ptr  hierarchy, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  hash_ptr  obfuscation_map, 
  boolean  force_flattening, 
  hash_ptr  cdh 
)
Prints the obfuscated flatten specifications of an SMV model.

See Also compile_write_flat_specs
Defined in compileWrite.c 

void 
compile_write_obfuscated_flat_spec(
  FILE* out, 
  const SymbTable_ptr  symb_table, 
  node_ptr  spec, 
  const char* msg, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  hash_ptr  obfuscation_map, 
  boolean  force_flattening, 
  hash_ptr  cdh 
)
Prints into the specified file the flatten specifications.

Defined in compileWrite.c 

int 
compile_write_obfuscated_flatten_expr_pair(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  l, 
  const char* s, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  hash_ptr  obfuscation_map, 
  boolean  force_flattening, 
  hash_ptr  cdh 
)
Writes a list of flattened expression pairs prefixed by a given string in SMV format on a file.

Defined in compileWrite.c 

int 
compile_write_obfuscated_flatten_expr_split(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  n, 
  const char* s, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  hash_ptr  obfuscation_map, 
  boolean  force_flattening, 
  hash_ptr  cdh 
)
Writes a generic expression prefixed by a given string in SMV format on a file.

Defined in compileWrite.c 

int 
compile_write_obfuscated_flatten_expr(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  n, 
  const char* s, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  hash_ptr  obfuscation_map, 
  boolean  force_flattening, 
  hash_ptr  cdh 
)
Writes a generic expression prefixed by a given string in SMV format on a file. Returns true if at least one character was printed, and false otherwise.

Defined in compileWrite.c 

int 
compile_write_obfuscated_flatten_spec_split(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  n, 
  const char* s, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  hash_ptr  obfuscation_map, 
  boolean  force_flattening, 
  hash_ptr  cdh 
)
Writes a generic spec prefixed by a given string in SMV format on a file.

Defined in compileWrite.c 

int 
compile_write_obfuscated_flatten_spec(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  n, 
  const char* s, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  hash_ptr  obfuscation_map, 
  boolean  force_flattening, 
  hash_ptr  cdh 
)
Writes a generic spec prefixed by a given string in SMV format on a file. Returns true if at least one character was printed, and false otherwise.

Defined in compileWrite.c 

boolean 
compile_write_obfuscated_flatten_vars_aux(
  const SymbTable_ptr  symb_table, 
  const node_ptr  name, 
  FILE* out, 
  hash_ptr  printed, 
  hash_ptr  obfuscation_map 
)
The function works exactly like compile_write_flatten_vars_aux but all identifiers are obfuscated before being printed.

See Also compile_write_flatten_vars_aux
Defined in compileWrite.c 

int 
compile_write_obfuscated_flatten_vars(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  NodeList_ptr  vars, 
  hash_ptr  obfuscation_map 
)
Writes VAR, FROZENVAR, and IVAR declarations in SMV format on a file.

Defined in compileWrite.c 

void 
compile_write_restricted_flat_fsm(
  FILE* out, 
  const SymbTable_ptr  symb_table, 
  const array_t* layer_names, 
  const char* fsm_name, 
  FlatHierarchy_ptr  hierarchy, 
  hash_ptr  dag_info, 
  hash_ptr  defines, 
  boolean  force_flattening, 
  hash_ptr  cdh 
)
Prints on the specified file the flatten FSM of an SMV model, i.e. a list of restricted variables, defines, and all constrains (INIT, TRANS, INVAR, ASSIGNS, JUSTICE, COMPASSION) restricted to the set of variables in the FlatHierarchy. Specifications are NOT printed. layer_names is an array of names of layers that is typically obtained from the symbol table. fsm_name is a name of the output structure, usually it is "MODULE main".

Defined in compileWrite.c 

void 
compile_write_udg_bool_fsm(
  FILE* out, 
  const SymbTable_ptr  symb_table, 
  NodeList_ptr  layers, 
  const char* fsm_name, 
  BoolSexpFsm_ptr  bool_sexp_fsm, 
  hash_ptr  dag_info, 
  hash_ptr  defines 
)
Prints into the specified file the boolean FSM of an SMV model. bool_sexp_fsm should be a boolean Sexp FSM. layer_names is an array of layers whose variables will be printed, usually this parameter is a list of all layers committed to enc. The array should be ended by a NULL element.

Defined in compileWriteUdg.c 

void 
compile_write_udg_bool_specs(
  FILE* out, 
  BddEnc_ptr  enc, 
  SymbLayer_ptr  det_layer, 
  FlatHierarchy_ptr  hierarchy, 
  hash_ptr  dag_info, 
  hash_ptr  defines 
)
Prints into the specified file the booleanized specifications of an SMV model. NOTE: a temporary layer will be created during the dumping for determinization variables that derived from the booleanization of the specifications. These variable declarations will be printed after the specs.

Defined in compileWriteUdg.c 

void 
compile_write_udg_bool_spec(
  FILE* out, 
  BddEnc_ptr  enc, 
  node_ptr  spec, 
  const char* msg, 
  SymbLayer_ptr  det_layer, 
  hash_ptr  dag_info, 
  hash_ptr  defines 
)
Private service to print a boolean specification

Defined in compileWriteUdg.c 

int 
compile_write_udg_constants(
  const SymbTable_ptr  symb_table, 
  FILE* out 
)
Returns 1 if at least one char have been written, 0 otherwise

Defined in compileWriteUdg.c 

int 
compile_write_udg_flat_asgn(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  const NodeList_ptr  vars, 
  FlatHierarchy_ptr  hierarchy, 
  hash_ptr  dag_info, 
  hash_ptr  defines 
)
Writes flattened ASSIGN declarations in SMV format on a file.

Defined in compileWriteUdg.c 

int 
compile_write_udg_flat_define(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  const NodeList_ptr  names, 
  hash_ptr  dag_info, 
  hash_ptr  defines 
)
Writes DEFINE declarations in SMV format on a file.

Defined in compileWriteUdg.c 

void 
compile_write_udg_flat_fsm(
  FILE* out, 
  const SymbTable_ptr  symb_table, 
  const array_t* layer_names, 
  const char* fsm_name, 
  FlatHierarchy_ptr  hierarchy, 
  hash_ptr  dag_info, 
  hash_ptr  defines 
)
Prints on the specified file the flatten FSM of an SMV model, i.e. a list of all variable, defines, and all constrains (INIT, TRANS, INVAR, ASSIGNS, JUSTICE, COMPASSION). Specifications are NOT printed. layer_names is an array of names of layers that is typically obtained from the symbol table. fsm_name is a name of the output structure, usually it is "MODULE main".

Defined in compileWriteUdg.c 

void 
compile_write_udg_flat_specs(
  FILE* out, 
  const SymbTable_ptr  st, 
  FlatHierarchy_ptr  hierarchy, 
  hash_ptr  dag_info, 
  hash_ptr  defines 
)
Prints into the specified file the specifications of an SMV model.

Defined in compileWriteUdg.c 

node_ptr 
compile_write_udg_flatten_array_define(
  SymbTable_ptr  st, 
  node_ptr  body, 
  node_ptr  context 
)
Writes DEFINE declarations in SMV format on a file.

Defined in compileWriteUdg.c 

int 
compile_write_udg_flatten_bfexpr(
  BddEnc_ptr  enc, 
  const SymbTable_ptr  symb_table, 
  SymbLayer_ptr  det_layer, 
  FILE* out, 
  node_ptr  n, 
  const char* s, 
  hash_ptr  dag_info, 
  hash_ptr  defines 
)
Writes a generic expression prefixed by a given string in SMV format on a file. The given layer is intended to hold the determization variables that are created by the booleanization process of the properties, that are kept not booleanized within the system.

Defined in compileWriteUdg.c 

int 
compile_write_udg_flatten_bool_vars(
  const SymbTable_ptr  symb_table, 
  const BoolEnc_ptr  bool_enc, 
  FILE* out, 
  NodeList_ptr  vars 
)
Writes boolean VAR, FROZENVAR and IVAR declarations in SMV format on a file. Non boolean vars are dumped as defines for the sake of readability of conterexamples.

Defined in compileWriteUdg.c 

int 
compile_write_udg_flatten_expr_pair(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  l, 
  ModelSectionTag  mst, 
  hash_ptr  dag_info, 
  hash_ptr  defines 
)
Writes a list of flattened expression pairs prefixed by a given string in SMV format on a file.

Defined in compileWriteUdg.c 

int 
compile_write_udg_flatten_expr_split(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  n, 
  ModelSectionTag  mst, 
  hash_ptr  dag_info, 
  hash_ptr  defines 
)
Writes a generic expression prefixed by a given string in SMV format on a file.

Defined in compileWriteUdg.c 

int 
compile_write_udg_flatten_expr(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  n, 
  ModelSectionTag  mst, 
  hash_ptr  dag_info, 
  hash_ptr  defines 
)
Writes a generic expression prefixed by a given string in SMV format on a file. Returns true if at least one character was printed, and false otherwise.

Defined in compileWriteUdg.c 

int 
compile_write_udg_flatten_psl(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  n, 
  hash_ptr  dag_info, 
  hash_ptr  defines 
)
Writes PSL properties as they are.

Defined in compileWriteUdg.c 

int 
compile_write_udg_flatten_spec_split(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  n, 
  ModelSectionTag  mst, 
  hash_ptr  dag_info, 
  hash_ptr  defines 
)
Writes a generic spec prefixed by a given string in SMV format on a file.

Defined in compileWriteUdg.c 

int 
compile_write_udg_flatten_spec(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  n, 
  ModelSectionTag  mst, 
  hash_ptr  dag_info, 
  hash_ptr  defines 
)
Writes a generic spec prefixed by a given string in SMV format on a file. Returns true if at least one character was printed, and false otherwise.

Defined in compileWriteUdg.c 

int 
compile_write_udg_flatten_vars(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  NodeList_ptr  vars 
)
Writes VAR, FROZENVAR, and IVAR declarations in SMV format on a file.

Defined in compileWriteUdg.c 

inline int 
compile_write_udg_print_1_ary(
  FILE* buffer, 
  node_ptr  code, 
  const char* str, 
  boolean  close, 
  boolean  shared, 
  const char* color1 
)
Printer in udg format for a node with a child

Defined in compileWriteUdg.c 

inline int 
compile_write_udg_print_2_arya(
  FILE* buffer, 
  node_ptr  code, 
  const char* str, 
  boolean  close, 
  boolean  shared 
)
Printer in udg format for a node with children arity equal to 2

Defined in compileWriteUdg.c 

inline int 
compile_write_udg_print_2_ary(
  FILE* buffer, 
  node_ptr  code, 
  const char* str, 
  boolean  close, 
  boolean  shared, 
  const char* color1, 
  const char* color2 
)
Printer in udg format for a node with children arity equal to 2

Defined in compileWriteUdg.c 

inline int 
compile_write_udg_print_3_aryc_color(
  FILE* buffer, 
  node_ptr  code, 
  const char* str, 
  node_ptr  fst, 
  node_ptr  snd, 
  node_ptr  trd, 
  boolean  close, 
  boolean  shared, 
  const char* color1, 
  const char* color2, 
  const char* color3 
)
The children are provided explicitly

Defined in compileWriteUdg.c 

inline int 
compile_write_udg_print_3_aryc(
  FILE* buffer, 
  node_ptr  code, 
  const char* str, 
  node_ptr  fst, 
  node_ptr  snd, 
  node_ptr  trd, 
  boolean  close, 
  boolean  shared 
)
The children are provided explicitly

Defined in compileWriteUdg.c 

int 
compile_write_udg_print_node(
  FILE* out, 
  node_ptr  n, 
  boolean  close, 
  boolean  shared, 
  const char* style 
)
Menthod that prints the given node in udg format

Defined in compileWriteUdg.c 

static Set_t 
computeCoiVar(
  SymbTable_ptr  st, 
  FlatHierarchy_ptr  fh, 
  node_ptr  var 
)
optional

Side Effects required

See Also optional
Defined in compileCone.c 

static node_ptr 
construct_array_multiplexer(
  node_ptr  array, 
  node_ptr  index, 
  boolean  is_array_next, 
  SymbTable_ptr  symb_table 
)
This function takes index-access expression with dynamic index and returns if-then-else expression with all indexes are constants E.g.: a[i

Defined in compileFlatten.c 

static void 
create_process_symbolic_variables(
  SymbTable_ptr  symb_table, 
  SymbLayer_ptr  layer, 
  node_ptr  process_name_list 
)
Creates an input variable to denote the internal process selector, and the defines to denote the corresponding 'running' symbols. 'process_name_list' is a list of existing processes names. If the list contains just one element ("main") no variables and defines are declared (no need). This happens if there is no "process" modules or the modules were flattened (which also removes "process" things). NB for developers: the internal process selector variable is by default positioned at the top of the ordering. It is attached to input_variables and all_variables too.

Side Effects input_variables and all_variables are affected.

Defined in compileFlatten.c 

void 
error_bit_selection_assignment_not_supported(
  node_ptr  name 
)
Error message for unsupported feature

Defined in compileFlatten.c 

static node_ptr 
expr2bexpr_get_shift_def_value(
  BddEnc_ptr  enc, 
  SymbLayer_ptr  det_layer, 
  node_ptr  context, 
  boolean  in_next, 
  node_ptr  a, 
  node_ptr  b, 
  int  numWidth, 
  node_ptr  defaultBit 
)
creates a default error case. numWidth is the width of b or -1 if b is not a word. defaultBit is a default value of a bit. Typically it is 0 and the highest bit of a for right signed shift.

Defined in compileBEval.c 

static node_ptr 
expr2bexpr_ite(
  BddEnc_ptr  enc, 
  SymbLayer_ptr  det_layer, 
  node_ptr  expr, 
  node_ptr  context, 
  boolean  in_next 
)
Private sesrvice called by expr2bexpr_recur

Side Effects None

See Also expr2bexpr_word_ite_aux
Defined in compileBEval.c 

static node_ptr 
expr2bexpr_recur_binary(
  BddEnc_ptr  enc, 
  SymbLayer_ptr  det_layer, 
  node_ptr  expr, 
  node_ptr  context, 
  boolean  in_next 
)
For words: at first convert to boolean the arguments and then apply a corresponding word function. For all other types if the kind of an expression is arithmetic or relational converte the exp down to an ADD, and then back to a node_ptr to booleanize it. Otherwise process the arguments and create a new expression of the same kind with find_node.

Side Effects None

Defined in compileBEval.c 

static node_ptr 
expr2bexpr_recur_unary(
  BddEnc_ptr  enc, 
  SymbLayer_ptr  det_layer, 
  node_ptr  expr, 
  node_ptr  context, 
  boolean  in_next 
)
This function booleanize an unary expression in a standard way: at first process the argument. Then for words apply a corresponding unary word function, for all other type just create exp of the same kind with find_node.

Side Effects None

Defined in compileBEval.c 

static node_ptr 
expr2bexpr_recur(
  BddEnc_ptr  enc, 
  SymbLayer_ptr  det_layer, 
  node_ptr  expr, 
  node_ptr  context, 
  boolean  in_next 
)
Takes an expression intended to evaluate to boolean, maps through booleans down to the atomic scalar propositions, builds the corresponding boolean function, and returns the resulting boolean expression. The conversion of atomic scalar proposition is currently performed by generating the corresponding ADD, and then printing it in terms of binary variables. The introduction of determinization variables is allowed only if flag allow_nondet is set to true. The input expression may be normal (not flattened), flattened or expanded. Parameter 'context' is used if the expression is not flattened.

Side Effects None

See Also Compile_expr2bexpr detexpr2bexpr
Defined in compileBEval.c 

static node_ptr 
expr2bexpr_rotate(
  BddEnc_ptr  enc, 
  SymbLayer_ptr  det_layer, 
  node_ptr  expr, 
  node_ptr  context, 
  boolean  in_next 
)
This function is called directly by the booleanizer

Defined in compileBEval.c 

static node_ptr 
expr2bexpr_shift_left(
  BddEnc_ptr  enc, 
  SymbLayer_ptr  det_layer, 
  node_ptr  context, 
  boolean  in_next, 
  node_ptr  a, 
  node_ptr  b, 
  node_ptr  def_case, 
  int  numWidth 
)
numWidth is the width of b or -1 if b is not a word (it can be a number)

Defined in compileBEval.c 

static node_ptr 
expr2bexpr_shift_right(
  BddEnc_ptr  enc, 
  SymbLayer_ptr  det_layer, 
  node_ptr  context, 
  boolean  in_next, 
  node_ptr  a, 
  node_ptr  b, 
  node_ptr  def_case, 
  int  numWidth 
)
Creates the encoding of the unsigned right-shifting circuit for words

Side Effects numWidth is the width of b or -1 if b is not a word (it can be a number)

Defined in compileBEval.c 

static node_ptr 
expr2bexpr_shift(
  BddEnc_ptr  enc, 
  SymbLayer_ptr  det_layer, 
  node_ptr  expr, 
  node_ptr  context, 
  boolean  in_next 
)
This function is called directly by the booleanizer

Defined in compileBEval.c 

static node_ptr 
expr2bexpr_word_ite_aux(
  BddEnc_ptr  enc, 
  SymbLayer_ptr  det_layer, 
  node_ptr  expr, 
  node_ptr  context, 
  boolean  in_next 
)
Creates the resulting WORD encoding as: Encoding complexity is N*C (N=word width, C=num of cases)

Defined in compileBEval.c 

static void 
flatten_declare_constants_within_list(
  SymbTable_ptr  symb_table, 
  SymbLayer_ptr  layer, 
  node_ptr  value_list 
)
Constants will occur within the given layer

Defined in compileFlatten.c 

static Set_t 
formulaGetDefinitionDependencies(
  const SymbTable_ptr  symb_table, 
  node_ptr  formula, 
  SymbFilterType  filter, 
  boolean  preserve_time, 
  int  time 
)
This function computes the dependencies of an atom. If the atom corresponds to a variable then the singleton with the variable is returned. If the atom corresponds to a "running" condition the singleton with variable PROCESS_SELECTOR_VAR_NAME is returned. Otherwise if the atom corresponds to a defined symbol the dependency set corresponding to the body of the definition is computed and returned. filter specifies what variables we are interested to, as in Formula_GetDependenciesByType, and is_inside_next is supposed to be true if the atom is inside a Next, false otherwise. Returned set must be disposed by the caller

Side Effects The define_dep_hash is modified in order to memoize previously computed dependencies of defined symbols.

See Also Formula_GetDependencies
Defined in compileCone.c 

static Set_t 
formulaGetDependenciesRecur(
  const SymbTable_ptr  symb_table, 
  node_ptr  formula, 
  node_ptr  context, 
  SymbFilterType  filter, 
  boolean  preserve_time, 
  int  time 
)
Recursive call to Formula_GetDependenciesByType. Returned set must be released by the caller.

See Also formulaGetDefinitionDependencies Formula_GetDependenciesByType
Defined in compileCone.c 

static int 
get_bits(
  const SymbTable_ptr  st, 
  const NodeList_ptr  lst 
)
Computes the total bit number of symbols in the given list

Defined in compileCmd.c 

static HrcNode_ptr 
get_hrc_root_node(
  HrcNode_ptr  node 
)
Get the HRC root node from a child

Defined in compileFlatten.c 

static void 
init_check_program(
  node_ptr  l 
)
The input should be a list of processes names. Loops over the list of process names and inserts the process symbolic name in the check_constant_hash.

Defined in compileCheck.c 

static inline int 
insert_assoc_w(
  hash_ptr  hash, 
  node_ptr  key, 
  node_ptr  value 
)
Virtual menthod that prints the given node (core nodes are handled here)

Defined in compileWriteUdg.c 

static void 
instantiate_array_define(
  SymbTable_ptr  st, 
  SymbLayer_ptr  layer, 
  node_ptr  name, 
  node_ptr  mod_name, 
  node_ptr  definition 
)
For every cell and every dimension create a correct binding in the symbol layer

Side Effects Elements are added to the layer an the symbol table

Defined in compileFlatten.c 

static boolean 
is_array_define_cell_udg(
  const SymbTable_ptr  st, 
  const node_ptr  name 
)
Print to the given file the array define represerntation

Defined in compileWriteUdg.c 

static boolean 
is_array_define_element(
  const SymbTable_ptr  symb_table, 
  const node_ptr  name 
)
If name refers to an array element the index has to be a NUMBER. The name has to be a define or array define identifier.

Defined in compileWrite.c 

static boolean 
is_array_var_element(
  const SymbTable_ptr  symb_table, 
  const node_ptr  name 
)
If name refers to an array element the index has to be a NUMBER. The name has to be a var or array var identifier.

Defined in compileWrite.c 

static void 
make_params_hrc(
  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 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.

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

Defined in compileFlatten.c 

static void 
make_params(
  SymbLayer_ptr  layer, 
  node_ptr  basename, 
  node_ptr  actual_list, 
  node_ptr  formal_list 
)
Builds the parameters of a module from the list of formal parameters of the module itself and a basename.
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.

Side Effects In the symbol table the new parameter is associated to the old one.

Defined in compileFlatten.c 

static node_ptr 
push_array_index_down(
  node_ptr  array, 
  node_ptr  index, 
  boolean  is_array_next, 
  SymbTable_ptr  st 
)
An index-access operator can be applied to if-then-else expression. In such case this function is used to push the index-access operator down. E.g. (a ? b : c)[i

Defined in compileFlatten.c 

static node_ptr 
put_in_context(
  node_ptr  v 
)
Put a variable in the current "context", which is stored in param_context.

Side Effects None

See Also param_context
Defined in compileFlatten.c 

static void 
resolve_range(
  SymbTable_ptr  st, 
  node_ptr  range, 
  node_ptr  context, 
  int* low, 
  int* high 
)
If it is not possible to resolve the bounds to numbers, an error is issued.

Defined in compileFlatten.c 

static node_ptr 
scalar_atom2bexpr(
  BddEnc_ptr  enc, 
  SymbLayer_ptr  det_layer, 
  node_ptr  expr, 
  node_ptr  context, 
  boolean  in_next 
)
Takes an atomic expression and converts it into a corresponding boolean expression. The introduction of determinization variables is allowed only if the layer det_layer is not NULL

Side Effects A new boolean variable might be introduced.

Defined in compileBEval.c 

node_ptr 
sym_intern(
  char * s 
)
Builds an internal representation for a given string. If the conversion has been performed in the past, then the hashed value is returned back, else a new one is created, hashed and returned. We hash this in order to allow the following: 
  VAR
     x : {a1, a2, a3};
     y : {a3, a4, a5};

  ASSIGN
     next(x) := case
                 x = y    : a2;
                 !(x = y) : a1;
                 1        : a3;
                esac;
i.e. to allow the equality test between x and y. This can be performed because we internally have a unique representation of the atom a3.

See Also find_atom
Defined in compileUtil.c 

static int 
up_log2(
  int  a 
)
Computes the log2 of the given argument rounding the result to the closest upper integer

Defined in compileCmd.c 

 
(
    
)
Indicates that the body of a define is under the flattening, it is usde to discover possible recursive definitions.

See Also Flatten_GetDefinition
Defined in compileFlatten.c 

 
(
    
)
A utility used by internal clean up code for hash tables

Defined in compileFlatten.c 

 
(
    
)
Clears and frees (with entries) given hash

Defined in compileCone.c 

 
(
    
)
Indicates that no dependency has been yet computed.

Defined in compileCone.c 

 
(
    
)
Indicates that the COI computation should be verbose.

Defined in compileCone.c 

 
(
    
)
The value used during the building of dependencies of defined symbols to keep track that compuation is ongoing to discover circular definitions.

Defined in compileCone.c 

 
(
    
)
Indicates that the dependency is empty

Defined in compileCone.c 

 
(
    
)
Private macros for the sake of readability of the function Compile_pop_global

Defined in compileUtil.c 

 
(
    
)
Use this macro to recursively recall print_node

Defined in compileWriteUdg.c 

 
(
    
)
Short way of print a node with sharing

Defined in compileWriteUdg.c 

 
(
    
)
Short way of print a node without sharing

Defined in compileWriteUdg.c 

 
(
    
)
Short way of print a node. The sharing depends on shared variable

Defined in compileWriteUdg.c 

 
(
    
)
Use this name when creating the layer of model symbols

Defined in compile.h
Last updated on 2011/04/06 21h:12