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 
CommandShowVars(
  int  argc, 
  char ** argv 
)
Shows model's symbolic variables and their values

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 
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_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_value_list 
)
The normalisation includes: all TRUE and FALSE constants are substituted by 1 and 0 numbers. If the range includes just 0 and 1, it became the boolean_range.

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_name(
  const SymbTable_ptr  symb_table, 
  node_ptr  name, 
  node_ptr  context 
)
Takes an expression representing an identifier and recursively evaluates it. This function is responsible of building the symbolic name of the given symbol n in module instance context. If the given symbol is a formal parameter of the module instance, than the actual parameter is built. If the given symbol is an array, than the expression referring to the element of the array must evaluate to an unique integer (not to a set of integers) in the range of array bound. NULL is returned if the given expression is not syntactically an identifier. NOTE: param symb_table is used only when the name is an array whose index is not a constant number. If the caller is sure that this is not the case, it is possible to pass NULL instead.

See Also compile_flatten_resolve_name_recur
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, otherwise NULL is returned

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

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

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

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.

Defined in compileFlatten.c

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.

Defined in compileWrite.c

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.

Defined in compileWrite.c

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

Defined in compileWrite.c

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.

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

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

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

Defined in compileCheck.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

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

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.

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

Defined in compileCmd.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

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_GetDependenciesByType(
  const SymbTable_ptr  symb_table, 
  node_ptr  formula, 
  node_ptr  context, 
  VarFilterType  filter 
)
The set of dependencies of a given formula are computed, as in Formula_GetDependencies, but the variable type filters the dependency collection:
VFT_CURRENT
filters the current variables
VFT_NEXT
filters out the next variables
VFT_INPUT
filters out the input variables
VFT_STATE
filters out the state variables
VFT_ALL
filters out all the variables
Combined modes can be obtained by bit-or: for example VFT_NEXT | VFT_INPUT will enable the search for the variables which are next or input variables.

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.

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.

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

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

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

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

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

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

boolean 
compileExpressionHasNextInputs(
  SymbTable_ptr  symb_table, 
  node_ptr  expr 
)
Returns true if the expression contains a next statement which itself has an input variable in it.

Defined in compileCheck.c

static Set_t 
compileFlattenConstantSexpCheck(
  const SymbLayer_ptr  layer, 
  node_ptr  expr, 
  int  type 
)
If the constant is trivially true, it is skipped; otherwise it will be associated to each fsm of all state variables occurring within the given layer

Side Effects required

See Also optional
Defined in compileFlatten.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 thier 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 void 
compileFlattenSexpModelAux(
  const SymbTable_ptr  symb_table, 
  const SymbLayer_ptr  layer, 
  node_ptr  expr, 
  int  type, 
  FlatHierarchy_ptr  flatHierarchy 
)
see compileFlattenSexpModel

Defined in compileFlatten.c

static void 
compileFlattenSexpModelRecur(
  const SymbTable_ptr  symb_table, 
  const SymbLayer_ptr  layer, 
  node_ptr  expr, 
  int  type, 
  FlatHierarchy_ptr  flatHierarchy 
)
see compileFlattenSexpModel

Defined in compileFlatten.c

static void 
compileFlattenSexpModel(
  const SymbTable_ptr  symb_table, 
  const SymbLayer_ptr  layer, 
  node_ptr  init_expr, 
  node_ptr  invar_expr, 
  node_ptr  trans_expr, 
  FlatHierarchy_ptr  flatHierarchy 
)
For every variable var-name in the given expressions the function creates association between: 1. var-name and and the INVAR expression list the variable occur. 2. init(var-name) and INIT expression list 3. next(var-name) and TRANS expression list. The result is remembered by flatHierarchy. The function compileFlattenProcess works similarly but with assignments.

See Also compileFlattenProcess
Defined in compileFlatten.c

static node_ptr 
compileFlattenSexpRecur(
  const SymbTable_ptr  symb_table, 
  node_ptr  sexp, 
  node_ptr  context 
)
Recursive function for flattenig a sexp.

See Also Compile_FlattenSexp Compile_FlattenSexpExpandDefine
Defined in compileFlatten.c

void 
compile_check_print_io_atom_stack_assign(
  FILE * fd 
)

Defined in compileCheck.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

void 
compile_create_flat_model(
    
)
creates the master scalar fsm if needed

Defined in compileCmd.c

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

Defined in compileFlatten.c

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
Defined in compileFlatten.c

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.

Defined in compileFlatten.c

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
Defined in compileFlatten.c

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:

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

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
Defined in compileFlatten.c

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
Defined in compileFlatten.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_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.

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 and IVARS declarations in SMV format on a file.

Defined in compileWrite.c

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.

Defined in compileWrite.c

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.

Defined in compileWrite.c

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.

Defined in compileWrite.c

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

Defined in compileWrite.c

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.

Defined in compileWrite.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  wb 
)
creates a default error case. wb is -1 if b is not a word.

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, 
  NPFNN  op 
)
If operands are not words and the expression is not a leaf, the expression is converted down to an ADD, and then back to a node_ptr to booleanize it.

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, 
  NPFN  op 
)
Applied unary operand to booleanize depending on the operand type. Operation is passed through 'op'. Operation can be a closure W->W

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  wb 
)
wb is -1 if b is not a word (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  wb 
)
Creates the encoding of the right-shifting circuit for words

Side Effects wb is -1 if b is not a word (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(
  node_ptr  value_list, 
  SymbLayer_ptr  layer 
)
Constnats will occur within the given layer

Defined in compileFlatten.c

static Set_t 
formulaGetDefinitionDependencies(
  const SymbTable_ptr  symb_table, 
  node_ptr  formula, 
  VarFilterType  filter 
)
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.

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, 
  VarFilterType  filter 
)
Recursive call to Formula_GetDependenciesByType

See Also formulaGetDefinitionDependencies Formula_GetDependenciesByType
Defined in compileCone.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 void 
make_params(
  node_ptr  basename, 
  node_ptr  actual, 
  node_ptr  formal 
)
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 and formal parameters. If the number of elements of the lists are different then, an error occurs.

Side Effects In the param_hash, the new parameter is associated to the old one.

Defined in compileFlatten.c

static void 
print_assign(
  FILE * out, 
  node_ptr  lhs, 
  node_ptr  rhs 
)
[Prints an assignement statement

Defined in compileWrite.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 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 const char* 
type_to_string(
  int  type 
)
optional

See Also optional
Defined in compileFlatten.c

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

Defined in compileWrite.c

static int 
write_flatten_define(
  const SymbTable_ptr  symb_table, 
  FILE* out, 
  const NodeList_ptr  names 
)
Writes DEFINE declarations in SMV format on a file.

Defined in compileWrite.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 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

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

Defined in compileUtil.c

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

Defined in compile.h

Last updated on 2009/01/30 15h:04