Compile_CheckAssigns()
Semantic checks on assignments of the modele.
Compile_ConstructHierarchy()
Traverses the module hierarchy and extracts the information needed to compile the automaton.
Compile_FlattenHierarchy()
Traverse the module hierarchy, collect all required the informations and flatten the hierarchy.
Compile_FlattenSexpExpandDefine()
Flattens an expression and expands defined symbols.
Compile_FlattenSexp()
Builds the flattened version of an expression.
Compile_ProcessHierarchy()
This function processes a hierarchy after collecting all its subparts.
Compile_WriteBoolFsm()
Prints the boolean FSM of an SMV model.
Compile_WriteBoolSpecs()
Prints the boolean specifications of an SMV model.
Compile_WriteFlattenFsm()
Prints the flatten version of FSM of an SMV model.
Compile_WriteFlattenSpecs()
Prints the flatten specifications.
Compile_check_if_bool_model_was_built()
Checks if boolean model has been constructed
Compile_check_if_encoding_was_built()
Checks if the variables enconding has been constructed
Compile_check_if_flat_model_was_built()
Checks if flat model has been constructed
Compile_check_if_flattening_was_built()
Checks if the flattening has been carried out
Compile_check_if_model_was_built()
Checks if bdd model has been constructed
Compile_cleanup_booleanizer_cache_about()
Cleans those hashed entries that are about a symbol that is being removed
Compile_detexpr2bexpr()
Converts a scalar expression into a boolean expression.
Compile_expr2bexpr()
Converts a scalar expression into a boolean expression.
Compile_get_expression_dependencies()
Gets list of variables in the expression
Compile_get_global_fsm_builder()
Returns the global fsm builder
Compile_get_global_predicate_normaliser()
Returns a global predicate normaliser
Compile_init_cmd()
Initializes the commands provided by this package
Compile_init()
Initializes the compile package.
Compile_make_sorted_vars_list_from_order()
This function creates a new list of variables that will contain the same symbols into 'vars', but ordered wrt to 'vars_order' content
Compile_pop_distrib_ops()
Simplifies the given property by exploiting the distributivity of G, AG and H over AND, and distributivity of F, AF and O over OR
Compile_quit()
Shut down the compile package
compile_check_print_io_atom_stack_assign()
compile_create_boolean_model()
Creates the master boolean fsm if needed. A new layer called DETERM_LAYER_NAME will be added if the bool fsm is created.
compile_create_flat_model()
creates the master scalar fsm if needed
compile_flatten_eval_number()
Simple evaluator for positive and negative constant numbers
compile_flatten_resolve_name_recur()
Performs the recursive step of CompileFlatten_resolve_name. Returns TYPE_ERROR if not resolvable name
compile_instantiate_by_name()
Starts the flattening from a given point in the module hierarchy.
compile_instantiate_vars()
Recursively applies compile_instantiate_var.
compile_instantiate_var()
Instantiates the given variable.
compile_instantiate()
Instantiates all in the body of a module.
compile_write_constants()
Writes the set of non-numeric constants as CONSTANTS statement
compile_write_flatten_bfexpr()
Writes flattened expression in SMV format on a file.
compile_write_flatten_bool_vars()
Writes boolean VAR and IVAR declarations in SMV format on a file. Non boolean vars are dumped as defines for the sake of readability of conterexamples.
compile_write_flatten_expr_pair()
Writes flattened expression pairs in SMV format on a file.
compile_write_flatten_expr_split()
Writes flattened expression in SMV format on a file.
compile_write_flatten_expr()
Writes flattened expression in SMV format on a file.
compile_write_flatten_psl()
Writes PSL properties as they are.
compile_write_flatten_vars()
Writes VAR and IVAR declarations in SMV format on a file.

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