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:

The following will make life easier:

If you’re using Chocolately, this can all be installed with:

1choco install 7zip git everything

Downloading/Extracting Spin

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.

Download the latest prebuilt version of Spin
Download the latest prebuilt version of Spin

Once that’s downloaded, use 7zip to extract the archive.

Extract the archive with 7zip
Extract the archive with 7zip

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).

Install the base MinGW package
Install the base MinGW package

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:

1choco install mingw

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”.

Download the GUI file for Spin
Download the GUI file for Spin

Save this wherever you like.

Now, the GUI needs to know where spin.exe is. There are two options.

  1. Add spin.exe to your PATH. Recommended
  2. Edit ispin.tcl on line 19 to replace
    1set SPIN    spin   ;# essential
    
    with something like
    1set SPIN	"C:/Program\ Files\ \(x86\)/spin650_windows64/bin/spin";# essential
    
    to 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.

wish.exe showing up in Everything
Tcl/Tk is often included with Git for Windows

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”.

Selecting a default program association for .tcl files
Selecting a default program association for .tcl files

With that, you should be able to launch the GUI for Spin by double-clicking on ispin.tcl.

Spin GUI
Spin GUI

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:

1choco install graphviz

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.

Spin GUI automata view
Spin GUI automata view

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.