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(
  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 
)
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.


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
)
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. NB: It is the invoker's responsibility to destroy the returned value. NB: The 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).

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

void 
Compile_ProcessHierarchy(
  SymbTable_ptr  symb_table, 
  SymbLayer_ptr  layer, 
  FlatHierarchy_ptr  hierarchy, 
  node_ptr  name, 
  boolean  create_process_variables 
)
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 dependenses 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(
  FILE* out, 
  const SymbTable_ptr  symb_table, 
  NodeList_ptr  layers, 
  const char* fsm_name, 
  SexpFsm_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_WriteBoolSpecs(
  FILE* out, 
  const SymbTable_ptr  symb_table, 
  BddEnc_ptr  enc, 
  node_ptr  spec, 
  node_ptr  compute, 
  node_ptr  ltlspec, 
  node_ptr  invarspec, 
  node_ptr  pslspec, 
  node_ptr  reachtarget, 
  node_ptr  avoidtarget, 
  node_ptr  reachdeadlock, 
  node_ptr  avoiddeadlock, 
  node_ptr  buchigame, 
  node_ptr  genreactivity 
)
Prints into the specified file the flattened boolead 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(
  FILE* out, 
  const SymbTable_ptr  symb_table, 
  const char** 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 terminated by NULL. fsm_name is a name of the output structure, usually it is "MODULE main".


void 
Compile_WriteFlattenSpecs(
  FILE* out, 
  const SymbTable_ptr  symb_table, 
  node_ptr  spec, 
  node_ptr  compute, 
  node_ptr  ltlspec, 
  node_ptr  invarspec, 
  node_ptr  pslspec, 
  node_ptr  reachtarget, 
  node_ptr  avoidtarget, 
  node_ptr  reachdeadlock, 
  node_ptr  avoiddeadlock, 
  node_ptr  buchigame, 
  node_ptr  genreactivity 
)
Prints into the specified file the flatten specifications. layer_names is an array of names of layers terminated by NULL.


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, thatn 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_cleanup_booleanizer_cache_about(
  SymbTable_ptr  st, 
  NodeList_ptr  symbs 
)
Called by BoolEnc class when removing a layer


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

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

NodeList_ptr 
Compile_get_expression_dependencies(
  const SymbTable_ptr  symb_table, 
  Expr_ptr  expression 
)
Calls Formula_GetDependencies to get the set of variables which appear in the expression. This is then converted to the type NodeList_ptr and returned. It is the responsibility of the caller to destroy the NodeList object

Side Effects NodeList object created


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.


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.


NodeList_ptr 
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 list must be destroyed by the caller.


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_quit(
    
)
Shut down the compile package


void 
compile_check_print_io_atom_stack_assign(
  FILE * fd 
)


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


void 
compile_create_flat_model(
    
)
creates the master scalar fsm if needed


node_ptr 
compile_flatten_eval_number(
  node_ptr  n, 
  boolean  pos 
)
Returns a NUMBER node, or Nil n is not a number. This is a private service of function CompileFlatten_resolve_number


node_ptr 
compile_flatten_resolve_name_recur(
  const SymbTable_ptr  symb_table, 
  node_ptr  n, 
  node_ptr  context 
)
Performs the recursive step of CompileFlatten_resolve_name.

See Also CompileFlatten_resolve_name

void 
compile_instantiate_by_name(
  SymbLayer_ptr  layer, 
  node_ptr  module_name, 
  node_ptr  instance_name, 
  node_ptr  actual, 
  node_ptr * assign, 
  FlatHierarchy_ptr  result 
)
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(
  SymbLayer_ptr  layer, 
  node_ptr  var_list, 
  node_ptr  mod_name, 
  node_ptr * assign, 
  FlatHierarchy_ptr  result 
)
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(
  SymbLayer_ptr  layer, 
  node_ptr  name, 
  node_ptr  type, 
  node_ptr  context, 
  node_ptr * assign, 
  FlatHierarchy_ptr  result 
)
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:


The variables of type boolean, scalar, and array depending the kind of variable instantiation mode are appended to input_variables or to state_variables.

See Also compile_instantiate_vars

void 
compile_instantiate(
  SymbLayer_ptr  layer, 
  node_ptr  mod_def, 
  node_ptr  mod_name, 
  node_ptr  actual, 
  node_ptr * assign, 
  FlatHierarchy_ptr  result 
)
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

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_flatten_bfexpr(
  BddEnc_ptr  enc, 
  const SymbTable_ptr  symb_table, 
  SymbLayer_ptr  det_layer, 
  FILE* out, 
  node_ptr  n, 
  char* s 
)
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 and IVARS declarations in SMV format on a file.


int 
compile_write_flatten_expr_pair(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  node_ptr  l, 
  char* s 
)
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, 
  char* s 
)
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, 
  char* s 
)
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 
)
Writes PSL properties as they are.


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


Last updated on 2009/03/04 12h:51