-
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_prop()
- Set the prop field of 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_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
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 2010/05/19 15h:56