How to install Spin model checker on Ubuntu 16.04 LTS.

Installing Spin on your machine can be a bit tough as the documentation is not up to date. So, in order to overcome that hurdle, simply follow the steps below.

1. Download the .gz file into your system from the spin official website.
2. Next, carry out the below steps before installing anything or making any changes.

sudo apt-get update 
sudo apt-get install build-essential

3. Then move the spin6.4.6.tar.gz file to /opt/ file. (The version I got at the time of writing this is Spin 6.4.6. hence why it’s used throughout. Change it accordingly).

mv spin6.4.6.tar.gz /opt/

4. Next, extract the .tar file there by simply typing

tar -zxvf spin6.4.6.tar.gz

5. Next, go inside the extracted Spin folder and go into the Src folder. You might get it with a version number attached so make sure to type your version. Else press tab and Ubuntu will complete the path for you.

cd /opt/Spin/Spin6.4.6/Src

6. Next to compile the source files while in the Src folder,

make

7. If you get an error here fix it with,

sudo apt-get install byacc flex
make

8. Next, you need to set the path for Spin to work correctly. You have to move the executable file which is in the Src folder shown in green (shown below) to /usr/local/bin as shown;

cp spin /usr/local/bin

Make sure that after you do it, you can see spin in the path as below;

*You have to restart/take a new terminal after this.

9. Next, go back to the Spin folder and type ls. You’ll see that there is an Example folder. So let's check if our installation works!

cd ..
cd Examples
spin hello.pml

10. If you get an error here saying spin is not installed and to install it a line of code, do just that!

sudo apt install staden

11.To run the .pml files using ispin, go to iSpin folder which is in the same directory as Examples; That’s it!

cd ../iSpin
sudo sh install.sh

UPDATE;

To open a file using ispin,

ispin hello.pml

Possible errors you might encounter after this point:

1. Spin opens up instead. Only when you close the spin window does iSpin opens up.
2. iSpin opens up but gives the error “spin preprocessing failed” in the output window when you try to run a .pml file.

In both these cases, just run the .pml file with sudo, cause you have nothing else to lose ;)

3. iSpin opens up but when you are run a .pml file, nothing happens and no output. Chances are there's something wrong with the path. Make sure you do Step 8 correctly.

That’s it, folks. Hope this helps! :)