int
CommandCheckLtlSpec(
int argc,
char ** argv
)
- Performs LTL model checking
- Side Effects None
- Defined in
ltlCmd.c
void
Ltl_CheckLtlSpec(
Prop_ptr prop
)
- The main routine to perform LTL model checking. It
first takes the LTL formula, prints it in a file. It calls the LTL2SMV
translator on it an reads in the generated tableau. The tableau is
instantiated, compiled and then conjoined with the original model
(both the set of fairness conditions and the transition relation are
affected by this operation, for this reason we save the current
model, and after the verification of the property we restore the
original one).
- Defined in
ltl.c
void
Ltl_Init(
)
- Initializes the ltl package.
- Side Effects None
- Defined in
ltlCmd.c
node_ptr
Ltl_RewriteInput(
SymbTable_ptr symb_table,
node_ptr expr,
SymbLayer_ptr layer,
node_ptr* init,
node_ptr* invar,
node_ptr* trans
)
- The function takes an LTL formula and rewrite it such a
way that it will not contain input variables any more. See the
description of this file for more details.
"layer" is the later where new state variables are defined (if it is
required).
"init", "invar", "trans" point to expressions corresponding to
initial condition, invariant and transition relations of the
hierarchy, respect. This expressions are added new expression if required.
The returned expressions (the LTL formula and parts of hierarchy)
are newly created node_ptr constructs and have to be freed by the
invoker.
NOTE ABOUT MEMORY: New expressions are created exactly the same way
as it is done by Compile_FlattenSexpExpandDefine.
Precondition: input expression has to be already flattened.
- Defined in
ltlRewrite.c
void
Ltl_StructCheckLtlSpec_build(
Ltl_StructCheckLtlSpec_ptr self
)
- Initialize the structure by computing the tableau for
the LTL property and computing the cross-product with the FSM of the model.
- Defined in
ltl.c
void
Ltl_StructCheckLtlSpec_check(
Ltl_StructCheckLtlSpec_ptr self
)
- Perform the check to see wether the property holds or not.
Assumes the Ltl_StructcCheckLtlSpec structure being initialized before with
Ltl_StructCheckLtlSpec_build.
If compassion is present it calls the check method for compassion,
otherwise the check method dedicated to the algorithm given by the
value of the oreg_justice_emptiness_bdd_algorithm option.
- See Also
ltl_stuctcheckltlspec_check_compassion
ltl_structcheckltlspec_check_el_bwd
ltl_structcheckltlspec_check_el_fwd
- Defined in
ltl.c
Ltl_StructCheckLtlSpec_ptr
Ltl_StructCheckLtlSpec_create(
)
- Create an empty Ltl_StructCheckLtlSpec structure.
- Defined in
ltl.c
void
Ltl_StructCheckLtlSpec_destroy(
Ltl_StructCheckLtlSpec_ptr self
)
- Desrtroy an Ltl_StructCheckLtlSpec structure.
- Defined in
ltl.c
void
Ltl_StructCheckLtlSpec_explain(
Ltl_StructCheckLtlSpec_ptr self,
NodeList_ptr symbols
)
- Perform the computation of a witness for a property.
Assumes the Ltl_StructcCheckLtlSpec structure being initialized before with
Ltl_StructCheckLtlSpec_build, and that Ltl_StructCheckLtlSpec_build has been
invoked.
- Defined in
ltl.c
bdd_ptr
Ltl_StructCheckLtlSpec_get_clean_s0(
Ltl_StructCheckLtlSpec_ptr self
)
- Get the s0 field of an Ltl_StructCheckLtlSpec structure
purified by tableu variables
- Defined in
ltl.c
bdd_ptr
Ltl_StructCheckLtlSpec_get_s0(
Ltl_StructCheckLtlSpec_ptr self
)
- Get the s0 field of an Ltl_StructCheckLtlSpec structure
- Defined in
ltl.c
void
Ltl_StructCheckLtlSpec_print_result(
Ltl_StructCheckLtlSpec_ptr self
)
- Prints the result of the Ltl_StructCheckLtlSpec_check fun
- Defined in
ltl.c
void
Ltl_StructCheckLtlSpec_set_do_rewriting(
Ltl_StructCheckLtlSpec_ptr self,
boolean do_rewriting
)
- Set the do_rewriting field of an Ltl_StructCheckLtlSpec
structure
- Defined in
ltl.c
void
Ltl_StructCheckLtlSpec_set_ltl2smv(
Ltl_StructCheckLtlSpec_ptr self,
Ltl_StructCheckLtlSpec_ltl2smv ltl2smv
)
- Set the ltl2smv field of an Ltl_StructCheckLtlSpec structure
- Defined in
ltl.c
void
Ltl_StructCheckLtlSpec_set_negate_formula(
Ltl_StructCheckLtlSpec_ptr self,
boolean negate_formula
)
- Set the negate_formula field of an Ltl_StructCheckLtlSpec structure
- Defined in
ltl.c
void
Ltl_StructCheckLtlSpec_set_oreg2smv(
Ltl_StructCheckLtlSpec_ptr self,
Ltl_StructCheckLtlSpec_oreg2smv oreg2smv
)
- Set the oreg2smv field of an Ltl_StructCheckLtlSpec structure
- Defined in
ltl.c
void
Ltl_StructCheckLtlSpec_set_prop(
Ltl_StructCheckLtlSpec_ptr self,
Prop_ptr prop
)
- Set the prop field of an Ltl_StructCheckLtlSpec structure
- Defined in
ltl.c
Expr_ptr
Ltl_apply_input_vars_rewriting(
Expr_ptr spec,
SymbTable_ptr st,
SymbLayer_ptr layer,
FlatHierarchy_ptr outfh
)
- Rewriting makes side-effect on given hierarchy, and
can declare new variables inside given layer.
The resulting expression is flattened and define expanded.
Invoker has to free returned expression exactly as if it was created by
Compile_FlattenSexpExpandDefine.
- Side Effects layer and outfh are expected to get changed
- See Also
Compile_FlattenSexpExpandDefine
- Defined in
ltl.c
bdd_ptr
feasible(
BddFsm_ptr fsm,
BddEnc_ptr enc
)
- Checks whether the model has a fair path and returns
the initial state of the path.
- Defined in
ltlCompassion.c
static node_ptr
fill_path_with_inputs(
BddFsm_ptr fsm,
BddEnc_ptr enc,
node_ptr path
)
- Fills a path with inputs.
- Defined in
ltlCompassion.c
static void
ltlPropAddTableau(
Prop_ptr prop,
SymbLayer_ptr tableau_layer,
FlatHierarchy_ptr hierarchy
)
- The bdd fsm into the property will change
- Defined in
ltl.c
bdd_ptr
ltl_clean_bdd(
Ltl_StructCheckLtlSpec_ptr self,
bdd_ptr bdd
)
- Quantify out tableau variables
- Side Effects required
- See Also
optional
- Defined in
ltl.c
node_ptr
ltl_create_substitution(
SymbTable_ptr symb_table,
node_ptr expr,
NodeList_ptr new_var_exprs
)
- The purpose of the function is to create a substitution
for the given expression in an LTL formula.
Returns the new identifiers.
- Defined in
ltlRewrite.c
LtlInputKind
ltl_rewrite_input(
SymbTable_ptr symb_table,
node_ptr* expr,
NodeList_ptr new_var_exprs
)
- A copy of the provided expression is created and
returned in the same pointer "expr". The copy may be exact or
already rewritten (to remove inputs in temporal expressions).
"new_var_exprs" is a list of pairs (CONS) of a new state var
introduced during rewriting and an expression associated with that
state variable.
Precondition: the expression have to be correctly typed.
NOTE FOR DEVELOPERS: This function creates new expression using the
same approach as compileFlattenSexpRecur, i.e. consts and ids are
find_atom-ed and operations are new_node-ed. Both functions should be
changed synchronously.
- See Also
LtlInputKind
- Defined in
ltlRewrite.c
int
ltl_structcheckltlspec_build_tableau_and_prop_fsm(
Ltl_StructCheckLtlSpec_ptr self
)
- Creates the tableau for a LTL property. The FSM of the
property contains the tableau. Returns 1 if an error is encountered
during the tableau generation, 0 otherwise
- Side Effects The bdd fsm into the prop will change
- Defined in
ltl.c
void
ltl_structcheckltlspec_check_compassion(
Ltl_StructCheckLtlSpec_ptr self
)
- Assumes the Ltl_StructcCheckLtlSpec structure being
initialized before with Ltl_StructCheckLtlSpec_build.
- Defined in
ltl.c
void
ltl_structcheckltlspec_check_el_bwd(
Ltl_StructCheckLtlSpec_ptr self
)
- Assumes the Ltl_StructcCheckLtlSpec structure being
initialized before with Ltl_StructCheckLtlSpec_build.
- Defined in
ltl.c
void
ltl_structcheckltlspec_check_el_fwd(
Ltl_StructCheckLtlSpec_ptr self
)
- Assumes the Ltl_StructcCheckLtlSpec structure being
initialized before with Ltl_StructCheckLtlSpec_build.
- Defined in
ltl.c
void
ltl_structcheckltlspec_deinit(
Ltl_StructCheckLtlSpec_ptr self
)
- optional
- Side Effects required
- See Also
optional
- Defined in
ltl.c
void
ltl_structcheckltlspec_init(
Ltl_StructCheckLtlSpec_ptr self
)
- optional
- Side Effects required
- See Also
optional
- Defined in
ltl.c
void
ltl_structcheckltlspec_remove_layer(
Ltl_StructCheckLtlSpec_ptr self
)
- Private service that removes the given layer from
the symbol table, and from both the boolean and bdd encodings.
- Defined in
ltl.c
static node_ptr
path(
BddEnc_ptr enc,
bdd_ptr source,
bdd_ptr dest,
bdd_ptr R
)
- Computes a path given the bdds representind the source
states, the target states, and the transition relation.
- Defined in
ltlCompassion.c
static bdd_ptr
predecessors(
BddEnc_ptr enc,
bdd_ptr relation,
bdd_ptr to
)
- Given a state to and a transition relation, compute the
direct and indirect predecessor states (transitive closure of
predecessor).
- Defined in
ltlCompassion.c
static bdd_ptr
predecessor(
BddEnc_ptr enc,
bdd_ptr relation,
bdd_ptr to
)
- Given a state to and a transition relation, compute the
direct predecessor state.
- Defined in
ltlCompassion.c
void
print_ltlspec(
FILE* file,
Prop_ptr prop
)
- Print the LTL specification.
- Defined in
ltl.c
static bdd_ptr
successors(
BddEnc_ptr enc,
bdd_ptr from,
bdd_ptr relation
)
- Given a state from and transition relation, compute the
direct and indirect successor states (transitive closure of
successor).
- Defined in
ltlCompassion.c
static bdd_ptr
successor(
BddEnc_ptr enc,
bdd_ptr from,
bdd_ptr relation
)
- Given a state from and transition relation, compute the
direct successor state.
- Defined in
ltlCompassion.c
node_ptr
witness(
BddFsm_ptr fsm,
BddEnc_ptr enc,
bdd_ptr feasib
)
- Computes fair path from one of the states
passed as parameter.
- Defined in
ltlCompassion.c
(
)
- Takes a formula (with context) and constructs the flat
hierarchy from it.
Description [
- Side Effects layer and outfh are expected to get changed
- Defined in
ltl.c