-
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 12h:51