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.


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.


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

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


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

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

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.


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.


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.


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.


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


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


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.


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.


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


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


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


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


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


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


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 
)


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


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.


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)


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.


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)


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.


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.


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.


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


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


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


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


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


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

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

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

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


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


hash_ptr 
Compile_get_obfuscation_map(
  const SymbTable_ptr  symb_table 
)
Generates the obfuscation map


void 
Compile_init_cmd(
    
)
Initializes the commands provided by this package


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


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


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


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


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.


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


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.


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.


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.


void 
Compile_quit(
    
)
Shut down the compile package


void 
Compile_write_dag_defines_udg(
  FILE* out, 
  hash_ptr  defines 
)


void 
Compile_write_dag_defines(
  FILE* out, 
  hash_ptr  defines 
)


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


void 
compile_build_model(
  boolean  force_build 
)
Builds the BDD fsm.


void 
compile_check_print_io_atom_stack_assign(
  FILE * fd 
)


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


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


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


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


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


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


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


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


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


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


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


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


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


void 
compile_create_flat_model(
    
)
creates the master scalar fsm if needed


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


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


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


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


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


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


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


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


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


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


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


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.


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.


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.


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

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:


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

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

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


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


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


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


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


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


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


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


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


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


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


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


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.


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.


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


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


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.


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.


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.


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.


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


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.


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.


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.


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.


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.


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.


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.


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.


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.


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.


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.


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.


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


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


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


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.


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

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.


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

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

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.


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.


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.


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.


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.


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.


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

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.


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


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.


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.


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


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


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.


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.


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


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.


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.


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.


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.


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.


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.


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.


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.


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.


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.


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.


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


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


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


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


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


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


Last updated on 2011/04/06 21h:13