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.
ltlInsertModuleHashReadModule()
Add the tableau module to the list of know modules
ltlPropAddTableau()
Main routine to add the tableau to the FSM
ltlBuildTableauAndPropFsm()
Creates the tableau
ltl_remove_layer()
Private service that removes the given layer from the symbol table, and from both the boolean and bdd encodings.

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

This file provide a mechanism to rewrite an LTL formula containing inputs in a way that the inputs are interpreted correctly. Let us suppose that a formula Phi speak about an input boolean variable i. The i refers to the input received to move from the previous state if any to the current state. That is we observe it in the next state as the result of the transition executed. Thus we build a new formula Phi' such that Phi' = Phi[i/_pi

See Alsooptional

ltlRewriteWffIfInputPresent()
Rewrites an LTL formula if inputs are present
ltlHandleInputsVars()
Add the variables introduced by the rewriting
ltlFreeWFFR_TYPE()
Free memory in the rewrite structure
extract_inputs()
Extracts the set of inputs from a formula
expand_input()
Rewrites an LTL formula
expr_subst_all()
Subst occurrence of s with d
expr_is_wff()
checks wheter the formula is a wff
expr_is_term()
checks wheter the formula is a term
expr_is_constant()
checks wheter the formula is a constant
build_input_vars_assoc()
Builds assoc variables
get_var_values()
Retrieves values of new var associated to name
get_var_name()
Retrieves name of new var associated to name
get_var_trans()
Retrieves transition relation of new var associated to name
get_digits()
Retrieves numbers of digit of a number
free_assoc_data_aux()
Retrieves numbers of digit of a number

Last updated on 2009/03/04 13h:34