-
CommandBuildBooleanModel()
- Compiles the flattened hierarchy into boolean SEXP
-
CommandBuildFlatModel()
- Compiles the flattened hierarchy into SEXP
-
CommandBuildModel()
- Compiles the flattened hierarchy into BDD
-
CommandCPPrintClusterInfo()
- Prints out information about the clustering.
** DEPRECATED in 2.4 **
-
CommandEncodeVariables()
- Builds the BDD variables necessary to compile the
model into BDD.
-
CommandFlattenHierarchy()
- Flattens the hierarchy of modules
-
CommandGetInternalStatus()
- Implements the get_internal_status command
-
CommandGoBmc()
- Implements the go_bmc command
-
CommandGo()
- Implements the go command
-
CommandIwls95PrintOption()
- Prints the Iwls95 Options.
-
CommandPrintFsmStats()
- Prints out information about the fsm and clustering.
-
CommandProcessModel()
- Performs the batch steps and then returns
control to the interactive shell.
-
CommandShowVars()
- Shows model's symbolic variables and their values
-
CommandWriteModelFlatBool()
- Writes a flat and boolean model of a given SMV file
-
CommandWriteModelFlat()
- Writes the currently loaded SMV model in the
specified file, after having flattened it
-
CommandWriteOrder()
- Writes variable order to file.
-
CompileFlatten_expand_range()
- Returns a range going from a to b
-
CompileFlatten_init_flattener()
- Inits the flattener module
-
CompileFlatten_normalise_value_list()
- Takes a list of values and returns the same
list being normalised
-
CompileFlatten_quit_flattener()
- Quits the flattener module
-
CompileFlatten_resolve_name()
- Takes an expression representing an identifier
and recursively evaluates it.
-
CompileFlatten_resolve_number()
- Resolves the given symbol to be a number
-
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
-
ComputeCOI()
- Computes the COI of a given set of variables, defined
within the given symb_table
-
Flatten_GetDefinition()
- Gets the flattened version of an atom.
-
Flatten_remove_symbol_info()
- Resets the hashed information about the given symbol
-
Formula_GetDependenciesByType()
- Computes the dependencies of an SMV expression by type
-
Formula_GetDependencies()
- Computes dependencies of a given SMV expression
-
Formulae_GetDependencies()
- Compute the dependencies of two set of formulae
-
check_assign_both()
- Given a variable, it checks if there are
multiple assignments to it.
-
check_assign()
- Checks for multiple or circular assignments.
-
check_circular_assign()
- Performs circular assignment checking
-
check_circ()
- Checks for circular definitions.
-
cmp_struct_init()
- Initializes the cmp structure
-
coiInit()
- Pre-compute the COI of the variables
-
compileCheckAssignForInputVars()
- Checks flattened assign statement for input variables
-
compileCheckForInputVars()
- Checks expressions for illegal occurrences of input vars
-
compileCheckInitForInputVars()
- Checks flattened init statement for input variables
-
compileCheckInvarForInputVars()
- Checks flattened invar statement for input variables
-
compileCheckTransForInputVars()
- Checks flattened trans statement for input variables
-
compileExpressionHasNextInputs()
- Checks expression for input variables in next statements
-
compileFlattenConstantSexpCheck()
- Called when a constant has been found in INVAR, INIT or
TRANS
-
compileFlattenProcessRecur()
- Recursive definition of compileFlattenProcess
-
compileFlattenProcess()
- Flatten a hierarchy of SMV processes.
-
compileFlattenSexpModelAux()
-
-
compileFlattenSexpModelRecur()
-
-
compileFlattenSexpModel()
- Creates association between variables and all the expressions
the variables occur in.
-
compileFlattenSexpRecur()
- Recursive function for flattenig a sexp.
-
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.
-
create_process_symbolic_variables()
- Creates the internal process selector variable, within
the given layer
-
error_bit_selection_assignment_not_supported()
- Error message for unsupported feature
-
expr2bexpr_get_shift_def_value()
- Private service for shifting operations
-
expr2bexpr_ite()
- Creates an encoding for CASE node. If CASE evaluates to
a word, a WORD encoding is created.
-
expr2bexpr_recur_binary()
- Applied to binary operands to booleanize depending
on the operands types. Operation is passed through 'op'. Operation can
be a closure WxW->W or a predicate over words WxW->Bool
-
expr2bexpr_recur_unary()
- Applied unary operand to booleanize depending
on the operand type. Operation is passed through 'op'. Operation can
be a closure W->W
-
expr2bexpr_recur()
- Converts a generic expression into a boolean expression.
-
expr2bexpr_rotate()
- High-level function for rotating words
-
expr2bexpr_shift_left()
- Creates the encoding of the left-shifting circuit for
words
-
expr2bexpr_shift_right()
- Creates the encoding of the right-shifting circuit for
words
-
expr2bexpr_shift()
- High-level function for shifting operations
-
expr2bexpr_word_ite_aux()
- Service of expr2bexpr_word_ite, that creates the word encoding
-
flatten_declare_constants_within_list()
- Traverses the list of values, and declare all constants (leaves) it
finds
-
formulaGetDefinitionDependencies()
- Compute the dependencies of an atom
-
formulaGetDependenciesRecur()
- Recursive call to Formula_GetDependenciesByType
-
init_check_program()
- Initializes the data structure to perform semantic
checks.
-
make_params()
- Builds the parameters of a module from the list of formal
parameters of the module itself.
-
print_assign()
- Prints an assignement statement
-
put_in_context()
- Put a variable in the current "context"
-
scalar_atom2bexpr()
- Converts an atomic expression into the corresponding
(boolean) expression.
-
sym_intern()
- Builds an internal representation for a given string.
-
type_to_string()
- required
-
write_flatten_assign()
- Writes flattened ASSIGN declarations in SMV format on a
file.
-
write_flatten_define()
- Writes DEFINE declarations in SMV format on a
file.
-
()
- Body of define in evaluation
-
()
- Cleans and frees the hash
-
()
- Clears and frees (with entries) given hash
-
()
- Indicates that the COI computation should be verbose.
-
()
- Indicates that the dependency computation is ongoing.
-
()
- Private macros for the sake of readability of the function
Compile_pop_global
-
()
- The name of the standard layer dedicated to model symbols
Last updated on 2009/03/04 12h:51