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).


void 
Ltl_Init(
    
)
Initializes the ltl package.

Side Effects None


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.


Last updated on 2009/01/30 15h:04