-
Ltl_CheckLtlSpec()
- The main routine to perform LTL model checking.
-
Ltl_Init()
- Initializes the ltl package.
-
Ltl_RewriteInput()
- Rewrites an LTL formula to get rid of input variables
in it present
-
Ltl_StructCheckLtlSpec_build()
- Initialize the structure by computing the tableau for
the LTL property
-
Ltl_StructCheckLtlSpec_check()
- Perform the check to see wether the property holds or not
-
Ltl_StructCheckLtlSpec_create()
- Create an empty Ltl_StructCheckLtlSpec structure.
-
Ltl_StructCheckLtlSpec_destroy()
- Desrtroy an Ltl_StructCheckLtlSpec structure.
-
Ltl_StructCheckLtlSpec_explain()
- Perform the computation of a witness for a property
-
Ltl_StructCheckLtlSpec_get_clean_s0()
- Get the s0 field purified by tableu variables
-
Ltl_StructCheckLtlSpec_get_s0()
- Get the s0 field of an Ltl_StructCheckLtlSpec structure
-
Ltl_StructCheckLtlSpec_print_result()
- Prints the result of the Ltl_StructCheckLtlSpec_check fun
-
Ltl_StructCheckLtlSpec_set_do_rewriting()
- Set the do_rewriting field of an Ltl_StructCheckLtlSpec
structure
-
Ltl_StructCheckLtlSpec_set_ltl2smv()
- Set the ltl2smv field of an Ltl_StructCheckLtlSpec structure
-
Ltl_StructCheckLtlSpec_set_negate_formula()
- Set the negate_formula field of an Ltl_StructCheckLtlSpec structure
-
Ltl_StructCheckLtlSpec_set_oreg2smv()
- Set the oreg2smv field of an Ltl_StructCheckLtlSpec structure
-
Ltl_StructCheckLtlSpec_set_prop()
- Set the prop field of an Ltl_StructCheckLtlSpec structure
-
Ltl_apply_input_vars_rewriting()
- Takes a LTL formula and applies rewriting to get rid of
input variables from the formula
-
ltl_clean_bdd()
- Quantify out tableau variables
-
ltl_create_substitution()
- Creates a new state variable and add a pair
to the list "new_var_exprs"
-
ltl_rewrite_input()
- Recursively walk over the expressions and returns
the kind of the expression, i.e. if it is temporal or with input vars.
-
ltl_structcheckltlspec_build_tableau_and_prop_fsm()
- Creates the tableau
-
ltl_structcheckltlspec_check_compassion()
- Perform the check to see wether the property holds or
not using an algorithm for strong fairness
-
ltl_structcheckltlspec_check_el_bwd()
- Perform the check to see wether the property holds or
not using the backward Emerson-Lei algorithm
-
ltl_structcheckltlspec_check_el_fwd()
- Perform the check to see wether the property holds or
not using the forward Emerson-Lei algorithm
-
ltl_structcheckltlspec_deinit()
- required
-
ltl_structcheckltlspec_init()
- required
-
ltl_structcheckltlspec_remove_layer()
- Private service that removes the given layer from
the symbol table, and from both the boolean and bdd encodings.
Last updated on 2010/05/19 22h:25