Ever tried to do model verification using iSpin (on Windows) on a click of a button but couldn’t manage to get it to work? I had the same problem. Apparently, there aren’t good resources that solve this problem. Follow these steps to get it to work. This has been tested to work on Widnows 7 and Windows 8.
I assume you have iSpin and SPIN installed on you system. Now let’s proceed with the necessary components. While doing the command line verification, most probably you used Cygwin’s gcc. or if you haven’t done any model verification so far, please first download and install Cygwin (note that you can also use MinGW instead of Cygwin – but this solution works for both). Then download and install gcc – C, C++ compiler package. When the installation completes, click on the Start menu, then right click on Computer and click on Properties. On the left navigation, click on Advanced system settings — a dialog will appear. On the dialog, click on Environmental Variables. Now a new dialog will open. Under the System variables section, locate the variable Path, select it and click on Edit. At the end of Variable value, add semi-colon (;) and add the path where you installed Cygwin plus Bin folder. That is, if you installed Cygwin in C:\Cygwin, then add the following
C:\Cygwin\Bin\
If you’re using the MinGW version of gcc rather than Cygwin, use instead the following (assuming MinGW is installed in C:\MinGW\)
C:\MinGW\bin\
and click on OK. Then click on OK on the previous dialogs.
Now, navigate to the path where you installed SPIN. Locate iSpin, then open it in a text editor (I used Notepad++). Now locate the line that reads the following:
set CC gcc
Add the following line just under it (select the one that applies for you)
set CC “C:/Cygwin/bin/gcc” ; for Cygwin users
set CC “C:/MinGW/bin/gcc” ; for MinGW users
That’s it. Save the file and close it. Now as a test, open iSpin and then open some model. Then write the LTL properties you want to verify inside the model, save it, and reopen it. Then go to the verification tab and adjust the commands to be used as per your requirements. Then click on the Run button. After some time, you should see the result on the Verification result window (the dark windows on the right bottom).
Cheers!
C:\Windows\Help 