On top of the interactive shell a graphical user interface (GUI from now on) was developed. The GUI is a separate process and communicates with NUSMV via the interactive shell.
From the GUI it is possible to edit and to modify the file containing the model description. The editor window provides the user with basic editing functionalities, such as copy and paste of blocks of text. Figure 7 gives a snapshot of the editor window. The NUSMV GUI allows for the modification of the options in a menu driven way. A snapshot of the window for setting system options is the small window in Figure 9. Moreover, the GUI offers a formula editor that helps the user in writing new specifications (see Figure 8). Depending on the kind of formula to verify, various buttons corresponding to temporal modalities and/or boolean connectives are activated. For instance in Figure 8 a CTL specification was chosen (the radio-button relative to CTL formulas is selected), and all the boolean connectives and the CTL operator buttons are active.
>
