Table of Contents
Introduction
For a class, I was trying to install the Spin
formal verification tool somehow on my Windows computer. I couldn’t find
a good guide, so this is what I figured out.
While you can do this with WSL, Spin has prebuilt Windows
binaries available, so I think this is easier than trying to get
X11 working (as of Sept 2020).
Prerequisites
You’ll need the following software installed:
- 7zip
The following will make life easier:
- Git for Windows
- Everything
If you’re using Chocolately,
this can all be installed with:
1choco install 7zip git everything
First, go to the Spin GitHub page. If you
already have Git installed, you can just clone this. Or, if you’d like,
you can go to Bin directory,
and click on the latest version of
spin<ver>_windows64.exe.gz. Click “Download” on the right side to get
only this file.
Once that’s downloaded, use 7zip to extract the archive.
Inside the directory it extracted into will be an executable. Rename this to spin.exe.
GCC
Next, Spin needs the GCC compiler in order to compile the generated C verifier.
The easiest way to get this is with MinGW
which is a project that has ported GCC to Windows.
Download and run the installer,
and select the base MinGW package (this includes GCC).
You may need to add C:\MinGW\bin\ to your PATH after it installs GCC.
You can verify it is setup correctly by running gcc in a shell and making sure
you don’t get a “gcc not found” error.
If you’re using Chocolately,
this can alternatively be installed with:
This will setup your PATH for you.
Now, if you only want the command-line version of Spin, you’re basically done.
You’ll need to use the full path to the spin.exe executable (unless you
add spin.exe to your PATH).
GUI
Now, if you’d like to use the GUI, complete the following steps. Buckle up.
First, you’ll need to download
ispin.tcl
from the optional_gui directory on the Spin GitHub page. The easiest way to do
this is to right-click “Raw” and then “Save link as”.
Save this wherever you like.
Now, the GUI needs to know where spin.exe is. There are two options.
- Add
spin.exeto your PATH. Recommended - Edit
ispin.tclon line 19 to replace1set SPIN spin ;# essentialwith something like
1set SPIN "C:/Program\ Files\ \(x86\)/spin650_windows64/bin/spin";# essentialto point where ever you put
spin.exe. Make sure properly escape the Windows path characters.
The next problem is getting Tcl/Tk installed,
which is needed to run this file.
Git for Windows
If you have installed Git for Windows, it likely already has already installed Tcl/Tk
(or another program may have installed it).
An easy way to check is to open up Everything,
and look for wish.exe.
All you need to do is right-click on ispin.tcl, choose “Open With”,
and select the wish.exe you found. Make sure to set
“Always use this app to open .tcl files”.
With that, you should be able to launch the GUI for Spin
by double-clicking on ispin.tcl.
Tcl/Tk Distributions
Let’s say you don’t have Git installed. There are other ways to get Tcl/Tk.
The easiest is ActiveTCL as
this will automatically setup all the proper file associations. However, they require
you to create an account to download it.
Another option is
Magicsplat,
but this does not setup the file associations, so you’ll have to do it manually, like
I described above, after finding wish.exe.
Graphviz
This last part is optional. If you want the automata view to work, you’ll need
to install Graphviz. Go to the
downloads page and get the
latest .zip file.
Extract this and put it somewhere useful like C:\Program Files (x86)\.
You can add the bin directory to your PATH if you like.
If you’re using Chocolately,
this can alternatively be installed with:
Lastly, you’ll need to edit ispin.tcl again. Comment out line 21, and uncomment
line 22, and adjust the path to dot as needed. For example:
1# set DOT dot ;# recommended, for automata view
2 set DOT "C:/Program\ Files\ \(x86\)/graphviz-2.44.1-win32/Graphviz/bin/dot";
(Even if dot.exe is added to your PATH, I’ve found it will still not work without doing this)
You should be all set now.
Conclusion
This is all you need to run Spin with the GUI on Windows! While it may
seem a bit complicated, you should really only have to do this once.
I really do recommend using Chocolately to make
installing everything easier. Installing the vast majority of the dependencies
becomes one command:
1choco install 7zip git everything mingw graphviz
If this seems like a lot of work, I’ve found another Spin GUI
available: jspin.
This has its own installation challenges (needing a Java runtime and requiring
some PATH configuration in its config.cfg file), but it seems
to work similarly and be far easier to get setup.
Spin is able to run on any Windows machine that supports Windows Subsystem Linux v2 (WLS2). This is a feature developed by Microsoft that allows you to run a Linux distribution on your Windows machine. It is supported in updated versions of Windows 10 and Windows 11.
Spin requires a working Windows installation with Docker installed. There are two popular methods to install Docker on Windows:
- Install
docker-ceon Windows Subsystem Linux v2 (WSL2) [recommended] - Install Docker Desktop on Windows with WSL2 backend
Optional software
You may want to consider installing this software to improve your development experience (this is what we use).
- Windows Terminal — This is a great terminal application that will give you tab support for your CLIs.
Both options require installing WSL2. We can follow the principles discussed in the official WSL2 documentation and prepare our machine to run «Windows Subsystem Linux v2» (WSL2). We prefer Ubuntu as our distribution. So if you’re happy with that recommendation, run this command in PowerShell as administrator to install WSL2.
A restart may be required.
After a reboot, you may be prompted to create a username and password for your new Ubuntu installation. This is a separate user from your Windows user.
Once configured, you can confirm is working by opening a new PowerShell window and running:
⚠️ Always be aware of what shell you’re in (Windows or Ubuntu). You can always tell by the prompt.
What a Windows shell looks like
You can tell you’re in a Windows shell by the prompt when you see the PS prefix and the C:\ prefix.
What a Linux shell looks like
When you’re in a Linux shell, you’ll see the different colors and things like /mnt/c for your Windows drive.
To go back to your Windows shell, type exit and press enter.
⚠️ Always run spin from the Linux shell. You’ll need to run wsl from a Windows prompt to enter the Linux shell, then you can run spin after you complete the installation.
Installing docker-ce within Linux allows you to run the open source versions of Docker without installing any proprietary software.
If this option interests you, run wsl to enter a Linux shell and then follow our instructions for installing Spin on Linux.
Install Docker Community Edition to Linux (WSL2) →
If you prefer to install Docker Desktop with the WSL2 backend, you’ll need to download Docker Desktop from Docker’s website.
Installation
Double click the setup file to begin the installation.
Configuration
If prompted, leave the default options checked.
Another restart may be required.
After the installation completes, you may be prompted to reboot your machine. If so, go ahead and do that.
Accept the terms
Once your computer comes back online, click on the Docker Desktop icon. The application will initialize and be sure to accept the terms.
Configuring your Docker Account
You will be prompted to login to your Docker account. If you don’t have one, you can create one for free. For most cases, you can use Docker without creating an account.
It should return version information.
It should return something like this.
⚠️ Be sure to run wsl to enter the Linux shell before running the following commands.
Run the installer with this simple command in your terminal
The above script will install spin at the user level in ~/.spin, using less than 300KB of storage.
Spin will prompt you if you want Spin to modify your PATH variable. If you press «Yes» follow the instructions on the screen. If you press «No» you will need to manually add Spin to your PATH.
If you did not add spin to your PATH during the installation, you can manually add it to your PATH by adding this to your shell profile:
Run echo $0 in your terminal to figure out which shell you are using.
In order to apply the changes to your current terminal session, you will need to run the source command.
You should be able to run this and get a result 🥳
Provide feedback
Saved searches
Use saved searches to filter your results more quickly
Sign up
Appearance settings
Education |
Version Control |
Introduction to Programming |
Unit Testing
Research |
A Broadcast Calculus |
Model Checking |
VSR
Model Checking Using SPIN[]
- http://spinroot.com/spin/whatispin.html
Installation[]
Installing SPIN on UBUNTU[]
Pre-requisites[]
- yacc
Installation[]
- Download http://spinroot.com/spin/Src/spin524.tar.gz
gunzip *.tar.gz tar -xf *.tar cd Spin/Src* make # or, on older distributions: make -f make_unix sudo cp spin /usr/local/bin
Installing SPIN on Windows XP[]
Download the releavant zip file and unzip into C:\Program Files\Spin.
- Download http://spinroot.com/spin/Src/pc_spin524.zip
- Unzip pc_spin524.zip in C:\Program Files\Spin
- Test the installation by running spin
C:> CD "Program Files"\Spin C:\Program Files\Spin>spin -V Spin Version 5.2.4 -- 2 December 2009
- Run the hello program.
C:\Program Files\Spin>spin hello passed first test! 1 process created
Using Spin[]
Hello World[]
active proctype main()
{
printf ("hello, world\n")
}
Run this:
$ spin hello.pml
hello, world
1 process created
1. Install supporting Software
Install gcc
Download cygwin setup file from https://cygwin.com/install.html and Install cygwin by double clicking on setup file.
Select gcc-c++ from package list
Look here for complete step
Then include ‘c:\cygwin\bin’ to PATH environment variable (https://www3.ntu.edu.sg/home/ehchua/programming/howto/Cygwin_HowTo.html)
Install TCL/tk software
Download the installation file from here and install it.
Install graphviz
Download latest graphviz setup file from here and install it.
2. Spin and Ispin installation
- Download spin executable from http://spinroot.com/spin/Src/index.html (select Windows PC executable, iSpin, and documentation, but no sources) and unzip it. It contains executables and examples.
- Select appropriate spin exe(include 64 and 32 bit) and rename into spin.exe.
- Copy spin.exe and ispin.tcl to «c:\cygwin\bin'( Assume default installation drive is C)
- Create a shortcut for «c:\cygwin\bin\ispin.tcl».
- Now you can access spin gui using ispin shortcut.
Known Issues
1.gcc error
Solution
1. Open cygwin-terminal and create link for gcc-3 and gcc-4
cd /bin ln gcc-3 gcc ln gcc-4 gcc