LTL module.

The LTL module is a separate module that calls an external program that translates the LTL formula into a tableau suitable to be loaded into NUSMV. This program also generates a new CTL formula to be verified on the synchronous product of the original system and the generated tableau. This module was plugged in on top of the other modules (e.g., the Parser, the Encoder, the FSM Compiler, the Model Checking and the Explanation modules), thus reusing a lot of the functionalities already present in the architecture.