CommandCheckLtlSpec()
Performs LTL model checking
Ltl_CheckLtlSpec()
The main routine to perform LTL model checking.
Ltl_Init()
Initializes the ltl package.
build_input_vars_assoc()
Builds assoc variables
expand_input()
Rewrites an LTL formula
expr_is_constant()
checks wheter the formula is a constant
expr_is_term()
checks wheter the formula is a term
expr_is_wff()
checks wheter the formula is a wff
expr_subst_all()
Subst occurrence of s with d
extract_inputs()
Extracts the set of inputs from a formula
feasible()
Check for feasability
fill_path_with_inputs()
Fill a path with inputs.
free_assoc_data_aux()
Retrieves numbers of digit of a number
get_digits()
Retrieves numbers of digit of a number
get_var_name()
Retrieves name of new var associated to name
get_var_trans()
Retrieves transition relation of new var associated to name
get_var_values()
Retrieves values of new var associated to name
ltlBuildTableauAndPropFsm()
Creates the tableau
ltlFreeWFFR_TYPE()
Free memory in the rewrite structure
ltlHandleInputsVars()
Add the variables introduced by the rewriting
ltlInsertModuleHashReadModule()
Add the tableau module to the list of know modules
ltlPropAddTableau()
Main routine to add the tableau to the FSM
ltlRewriteWffIfInputPresent()
Rewrites an LTL formula if inputs are present
ltl_remove_layer()
Private service that removes the given layer from the symbol table, and from both the boolean and bdd encodings.
path()
Compute a path from source to destination
predecessors()
Compute the direct and indirect predecessors of a state
predecessor()
Compute the direct predecessor of a state
print_ltlspec()
Print the LTL specification.
successors()
Compute the direct and indirect successors of a state
successor()
Compute the direct successor of a state
witness()
Compute a withness of feasability

Last updated on 2009/03/04 13h:34