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

static hash_ptr 
build_input_vars_assoc(
  SymbTable_ptr  symb_table, 
  node_ptr  inputs 
)
optional

Side Effects required

See Also optional
Defined in ltlRewrite.c

static node_ptr 
expand_input(
  SymbTable_ptr  symb_table, 
  node_ptr  expr, 
  hash_ptr  assoc 
)
optional

Side Effects required

See Also optional
Defined in ltlRewrite.c

static boolean 
expr_is_constant(
  SymbTable_ptr  symb_table, 
  node_ptr  expr 
)
optional

Side Effects required

See Also optional
Defined in ltlRewrite.c

static boolean 
expr_is_term(
  node_ptr  expr 
)
optional

Side Effects required

See Also optional
Defined in ltlRewrite.c

static boolean 
expr_is_wff(
  node_ptr  expr 
)
optional

Side Effects required

See Also optional
Defined in ltlRewrite.c

static node_ptr 
expr_subst_all(
  SymbTable_ptr  symb_table, 
  node_ptr  expr, 
  node_ptr  s, 
  node_ptr  d 
)
optional

Side Effects required

See Also optional
Defined in ltlRewrite.c

static node_ptr 
extract_inputs(
  SymbTable_ptr  symb_table, 
  node_ptr  expr 
)
optional

Side Effects required

See Also optional
Defined in ltlRewrite.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 assoc_retval 
free_assoc_data_aux(
  char * key, 
  char * data, 
  char * arg 
)
optional

Side Effects required

See Also optional
Defined in ltlRewrite.c

static int 
get_digits(
  int  n 
)
optional

Side Effects required

See Also optional
Defined in ltlRewrite.c

static node_ptr 
get_var_name(
  hash_ptr  assoc, 
  node_ptr  name 
)
optional

Side Effects required

See Also optional
Defined in ltlRewrite.c

static node_ptr 
get_var_trans(
  hash_ptr  assoc, 
  node_ptr  name 
)
optional

Side Effects required

See Also optional
Defined in ltlRewrite.c

static node_ptr 
get_var_values(
  hash_ptr  assoc, 
  node_ptr  name 
)
optional

Side Effects required

See Also optional
Defined in ltlRewrite.c

static int 
ltlBuildTableauAndPropFsm(
  SymbTable_ptr  symb_table, 
  SymbLayer_ptr  tableau_layer, 
  Prop_ptr  prop 
)
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 
ltlFreeWFFR_TYPE(
  WFFR_TYPE  rw 
)
optional

Side Effects required

See Also optional
Defined in ltlRewrite.c

void 
ltlHandleInputsVars(
  SymbLayer_ptr  layer, 
  WFFR_TYPE  wr, 
  node_ptr* init, 
  node_ptr* invar, 
  node_ptr* trans 
)
Declares the new variables introduced by the rewriting and builds their transition relation

Side Effects required

See Also optional
Defined in ltlRewrite.c

static void 
ltlInsertModuleHashReadModule(
  node_ptr  ltl_parsed_module 
)
Add the tableau module to the list of know modules

Defined in ltl.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

WFFR_TYPE 
ltlRewriteWffIfInputPresent(
  SymbTable_ptr  symb_table, 
  node_ptr  expr 
)
optional

Side Effects required

See Also optional
Defined in ltlRewrite.c

void 
ltl_remove_layer(
  BddEnc_ptr  bdd_enc, 
  SymbLayer_ptr  layer 
)
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

Last updated on 2009/03/04 12h:51