-
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 13h:34