Current version is 1.0.5 released on 2014/06/27

Support for Epispin is not available anymore, alas.

EpiSpin is an Eclipse plug-in for editing and verifying Promela models using the Spin model checker, developed using the Spoofax language workbench. It allows you to edit Promela models in Eclipse, using the well known Eclipse features such as

Furthermore, it is possible to call the Spin verifier and simulator from within EpiSpin.

In case of any questions or remarks, do not hesitate to contact me at b.devos-1@student.tudelft.nl or leave a message at the EpiSpin issuetracker on YellowGrass. More information can also be found in the EpiSpin Paper.


EpiSpin can be installed with the standard Eclipse update site mechanism, using the URL: http://epispin.ewi.tudelft.nl/update. It is recommended to customize the Eclipse configuration file as is explained on the update site. Detailed installation instructions can be found here as well. A changelog is also available.
Please note that you need to have Eclipse 4.3 or 4.4 installed. Older versions are not officially supported, but if you have problems installing EpiSpin for older versions, please let me know using the YellowGrass issue tracker and I'll see what I can do for yous. Also spin and gcc should be installed and they should be in your PATH.s

To edit a Promela model, first create a new Eclipse Project (File > New > Project and select Project from General). Then start the EpiSpin wizard (File > New > Other and select EpiSpin) to create a new Promela file and a corresponding option screen. You can also create these files yourself by creating a new file with the .pml extension. When you want to use the Spin verifier and simulator, create a new file with the same name as the Promela file and the .opt extension. This way, you ensure that the option screen belongs to the right Promela file (you can also specify the filename of the Promela file manually in the text field below the run button). Make sure the Console view is opened to see the textual output from verification and simulation (Window > Show View > Console).

From source

To install EpiSpin from source, follow these steps:
  1. Download the source code and unzip it
  2. Start Eclipse and download the latest unstable release of Spoofax following these steps.
  3. In Eclipse, go to File -> Import and select Existing Projects into Workspace from the General folder and click Next
  4. In the next window, browse to the unpacked folder in the Select root directory field and click Finish. EpiSpin will now be imported in Eclipse and an initial built is started (go to Project -> Build project if the initial built is not started automatically).
  5. You can now make changes to the source code and click Project -> Build project (or use the shortcut Ctrl+Alt+B) to build the modified sources. If you want to use EpiSpin in a new editor, click right on the project and go to Run As -> Eclipse application.

Graphical User Interface

The user interface to call the Spin verifier and simulator is written in SWT and is only accessible by opening a file with the *.opt extension in EpiSpin. The filename of such a file is loaded in the text fields in the option window (see the Figure below). Therefore the easiest way to run a Spin simulation or verification is by creating a .opt file for every Promela file (using the wizard as described above or by creating a .opt file with the same filename as the Promela model yourself). In the future it will be possible for these Option-screen files to remember your settings for a specification or simulation run.

A screenshot of the GUI

Static Communication Analyzer

The Static Communication Analyzer (SCA) in EpiSpin is a tool that generates DOT code for a communication graph that is derived from the currently opened Promela model. In this graph, the relations between processes, global variables and channels are indicated using the following notationns:

To generate DOT code for a Promela file, click 'Transform' in the menu bar and click 'Generate Dot code' from the submenu. The DOT code is then saved in a file filename.dot. Now you can use Graphiz to compile this DOT code into an image or pdf file. This can be done by opening a Terminal screen, browse to the workspace and execute dot -Tpng filename.dot -o filename.png to create a png file. Change 'png' to another output format when another format is required.

I would recommand you to create an 'External Tools Configuration' in Eclipse. By running this configuration, the DOT program is called and a graph is created of the selected *.dot file. To create this, first select the *.dot file in the package explorer. Then go to Run > External Tools > External Tools Configurations, click on Program in the left part of the screen and press the 'New' button. Now insert the following values:

Name:               DOT
Location:           /usr/bin/dot 
Working Directory:  ${project_loc}
Arguments:          -Tpng ${selected_resource_loc} -o ${selected_resource_name}.png
Please note that if your DOT program is installed in another folder, you should change the Location field. You can find out where DOT is installed by typing which dot in the terminal.
Now click Run and the new *.png file should appear in the package explorer. When you want to run DOT again, select the *.dot file and select Run > External Tools > DOT from the menu or just click on the icon in the menu bar.

vBulletin analytics