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