ltl.h
ltlInt.h
ltl.c
ltlCmd.c
ltlCompassion.c
ltlRewrite.c
By: Marco Roveri
See Alsomc
By: Marco Roveri
By: Marco Roveri
Here we perform the reduction of LTL model checking to CTL model checking. The technique adopted has been taken from [1
See Alsomc
Ltl_CheckLtlSpec()
print_ltlspec()
Ltl_StructCheckLtlSpec_create()
Ltl_StructCheckLtlSpec_destroy()
Ltl_StructCheckLtlSpec_set_oreg2smv()
Ltl_StructCheckLtlSpec_set_ltl2smv()
Ltl_StructCheckLtlSpec_set_negate_formula()
Ltl_StructCheckLtlSpec_set_do_rewriting()
Ltl_StructCheckLtlSpec_get_s0()
Ltl_StructCheckLtlSpec_get_clean_s0()
Ltl_StructCheckLtlSpec_build()
Ltl_StructCheckLtlSpec_check()
Ltl_StructCheckLtlSpec_print_result()
Ltl_StructCheckLtlSpec_build_counter_example()
Ltl_StructCheckLtlSpec_explain()
ltlPropAddTableau()
Ltl_apply_input_vars_rewriting()
()
ltl_structcheckltlspec_build_tableau_and_prop_fsm()
ltl_structcheckltlspec_check_compassion()
ltl_structcheckltlspec_check_el_bwd()
ltl_structcheckltlspec_check_el_fwd()
ltl_structcheckltlspec_remove_layer()
ltl_clean_bdd()
ltl_structcheckltlspec_init()
ltl_structcheckltlspec_deinit()
ltl_structcheckltlspec_prepare()
By: Marco Roveri
Shell commands to deal with the LTL model checking.
See Alsomc
Ltl_Init()
CommandCheckLtlSpec()
By: Rik Eshuis
The technique adopted has been taken from [1
See Alsomc
feasible()
witness()
successor()
successors()
predecessor()
predecessors()
path()
fill_path_with_inputs()
By: Marco Roveri, changed by Andrei Tchaltsev
The algorithm to check an LTL formula cannot deal with input variables. Thus it is necessary to rewrite LTL formula to get rid from input variables. This is done by introducing fresh state variables. The idea is the following: let's assume we have an LTL formula which contains a non-temporal boolean sub-formula Phi over state and input variables. LTL_REWRITE_STANDARD method: The LTL formula is rewritten by substituting a fresh boolean state variable sv for Phi and adding a new transition relation TRANS sv <-> Phi. For example, LTL formula G (s < i); becomes G sv; and the model is augmented by VAR sv : boolean; TRANS sv <-> (s < i); Note 1: new deadlocks are introduced after the rewriting (because new vars are assigned a value before the value of input vars are known). For example, with "TRANS s Phi" and a new initial condition "INIT sv"; For example, LTL formula G (s < i) becomes G (X sv) and the model is augmented by VAR sv : boolean; INIT sv; TRANS next(sv) <-> (s < i);
Ltl_RewriteInput()
ltl_rewrite_input()
ltl_create_substitution()