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


Last updated on 2005/11/21 16h:42