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/01/30 14h:53