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