ltl.h
External header file
ltlInt.h
Internal header file
ltl.c
Routines to perform reduction of LTL model checking to CTL model checking.
ltlCmd.c
Shell commands to deal with the LTL model checking.
ltlCompassion.c
Routines to perform strongly fair LTL model checking
ltlRewrite.c
Rewrite formula to keep track of possible inputs

ltl.h

External header file

By: Marco Roveri

See Alsomc


ltlInt.h

Internal header file

By: Marco Roveri


ltl.c

Routines to perform reduction of LTL model checking to CTL model checking.

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()
The main routine to perform LTL model checking.
print_ltlspec()
Print the LTL specification.
Ltl_StructCheckLtlSpec_create()
Create an empty Ltl_StructCheckLtlSpec structure.
Ltl_StructCheckLtlSpec_destroy()
Desrtroy an Ltl_StructCheckLtlSpec structure.
Ltl_StructCheckLtlSpec_set_oreg2smv()
Set the oreg2smv 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_do_rewriting()
Set the do_rewriting field of an Ltl_StructCheckLtlSpec structure
Ltl_StructCheckLtlSpec_get_s0()
Get the s0 field of an Ltl_StructCheckLtlSpec structure
Ltl_StructCheckLtlSpec_get_clean_s0()
Get the s0 field purified by tableu variables
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_print_result()
Prints the result of the Ltl_StructCheckLtlSpec_check fun
Ltl_StructCheckLtlSpec_build_counter_example()
Perform the computation of a witness for a property
Ltl_StructCheckLtlSpec_explain()
Perform the computation of a witness for a property
ltlPropAddTableau()
Main routine to add the tableau to the FSM
Ltl_apply_input_vars_rewriting()
Takes a LTL formula and applies rewriting to get rid of input variables from the formula
()
Takes a formula (with context) and constructs the flat hierarchy from it. Description [
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_remove_layer()
Private service that removes the given layer from the symbol table, and from both the boolean and bdd encodings.
ltl_clean_bdd()
Quantify out tableau variables
ltl_structcheckltlspec_init()
required
ltl_structcheckltlspec_deinit()
required
ltl_structcheckltlspec_prepare()
Support function for the init function

ltlCmd.c

Shell commands to deal with the LTL model checking.

By: Marco Roveri

Shell commands to deal with the LTL model checking.

See Alsomc

Ltl_Init()
Initializes the ltl package.
CommandCheckLtlSpec()
Performs LTL model checking

ltlCompassion.c

Routines to perform strongly fair LTL model checking

By: Rik Eshuis

The technique adopted has been taken from [1

See Alsomc

feasible()
Check for feasability
witness()
Compute a withness of feasability
successor()
Compute the direct successor of a state
successors()
Compute the direct and indirect successors of a state
predecessor()
Compute the direct predecessor of a state
predecessors()
Compute the direct and indirect predecessors of a state
path()
Compute a path from source to destination
fill_path_with_inputs()
Fill a path with inputs.

ltlRewrite.c

Rewrite formula to keep track of possible 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. 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; INVAR 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"

Ltl_RewriteInput()
Rewrites an LTL formula to get rid of input variables in it present
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_create_substitution()
Creates a new state variable and add a pair to the list "new_var_exprs"

Last updated on 2011/04/06 21h:16