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). If already set (The Scalar and the Bdd ones, the FSMs used for verification are taken from within the property. Otherwise, global FSMs are set within the property and then used for verification.


void 
Ltl_Init(
    
)
Initializes the ltl package.

Side Effects None


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.


Trace_ptr 
Ltl_StructCheckLtlSpec_build_counter_example(
  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.


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.


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

Ltl_StructCheckLtlSpec_ptr 
Ltl_StructCheckLtlSpec_create(
  Prop_ptr  prop 
)
Create an empty Ltl_StructCheckLtlSpec structure.


void 
Ltl_StructCheckLtlSpec_destroy(
  Ltl_StructCheckLtlSpec_ptr  self 
)
Desrtroy an Ltl_StructCheckLtlSpec structure.


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.


bdd_ptr 
Ltl_StructCheckLtlSpec_get_clean_s0(
  Ltl_StructCheckLtlSpec_ptr  self 
)
Get the s0 field of an Ltl_StructCheckLtlSpec structure purified by tableu variables


bdd_ptr 
Ltl_StructCheckLtlSpec_get_s0(
  Ltl_StructCheckLtlSpec_ptr  self 
)
Get the s0 field of an Ltl_StructCheckLtlSpec structure


void 
Ltl_StructCheckLtlSpec_print_result(
  Ltl_StructCheckLtlSpec_ptr  self 
)
Prints the result of the Ltl_StructCheckLtlSpec_check fun


void 
Ltl_StructCheckLtlSpec_set_do_rewriting(
  Ltl_StructCheckLtlSpec_ptr  self, 
  boolean  do_rewriting 
)
Set the do_rewriting field of an Ltl_StructCheckLtlSpec structure


void 
Ltl_StructCheckLtlSpec_set_ltl2smv(
  Ltl_StructCheckLtlSpec_ptr  self, 
  Ltl_StructCheckLtlSpec_ltl2smv  ltl2smv 
)
Set the ltl2smv field of an Ltl_StructCheckLtlSpec structure


void 
Ltl_StructCheckLtlSpec_set_negate_formula(
  Ltl_StructCheckLtlSpec_ptr  self, 
  boolean  negate_formula 
)
Set the negate_formula field of an Ltl_StructCheckLtlSpec structure


void 
Ltl_StructCheckLtlSpec_set_oreg2smv(
  Ltl_StructCheckLtlSpec_ptr  self, 
  Ltl_StructCheckLtlSpec_oreg2smv  oreg2smv 
)
Set the oreg2smv field of an Ltl_StructCheckLtlSpec structure


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

bdd_ptr 
ltl_clean_bdd(
  Ltl_StructCheckLtlSpec_ptr  self, 
  bdd_ptr  bdd 
)
Quantify out tableau variables

Side Effects required

See Also optional

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.


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

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


void 
ltl_structcheckltlspec_check_compassion(
  Ltl_StructCheckLtlSpec_ptr  self 
)
Assumes the Ltl_StructcCheckLtlSpec structure being initialized before with Ltl_StructCheckLtlSpec_build.


void 
ltl_structcheckltlspec_check_el_bwd(
  Ltl_StructCheckLtlSpec_ptr  self 
)
Assumes the Ltl_StructcCheckLtlSpec structure being initialized before with Ltl_StructCheckLtlSpec_build.


void 
ltl_structcheckltlspec_check_el_fwd(
  Ltl_StructCheckLtlSpec_ptr  self 
)
Assumes the Ltl_StructcCheckLtlSpec structure being initialized before with Ltl_StructCheckLtlSpec_build.


void 
ltl_structcheckltlspec_deinit(
  Ltl_StructCheckLtlSpec_ptr  self 
)
optional

Side Effects required

See Also optional

void 
ltl_structcheckltlspec_init(
  Ltl_StructCheckLtlSpec_ptr  self, 
  Prop_ptr  prop 
)
optional

Side Effects required

See Also optional

void 
ltl_structcheckltlspec_prepare(
  Ltl_StructCheckLtlSpec_ptr  self 
)
Support function for the init function

See Also ltl_structcheckltlspec_init

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.


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