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_counter_example()
Perform the computation of a witness for a property
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_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_prepare()
Support function for the init function
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 2012/11/18 14h:37