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

Last updated on 2010/05/19 15h:56