These are files used in a course at Chalmers university.
(Close window) This cheat sheet is based on the Spin Reference Card by Mordechai Ben-Ari, under the CC 3.0 license.
Datatypes
bit (1 bit) Operators (descending precendence)
() [] .
! ~ ++ --
* / % +
- << >> Predefined
Constants - true, false Preprocessor
#define name (arguments) string Statements
mtype var; - variable declaration |
Statements (ctd)
skip - no operation Guarded commands
if :: guard -> statements :: .. fi Processes
Declaration - proctype procname (parameters) { ... } Channels
chan ch = [capacity] of { type, type, ... }
|
Channels (ctd)
Matching in a receive statement: constants and mtype Temporal logic
Remote references
Test the control state or value of a variable: LTL formulaltl name { ... }Variable declaration prefixeshidden - hide this variable from the system statelocal - a global var. is accessed only by one process Comments// single-line /* multi-line*/ |
This website provides an online interface to the Spin model checker and was developed to simplify its use in a course at Chalmers university.
Not all functionality of Spin and jSpin can be found here. Some operations such as running interactively are technically too complicated, but other functionality is left out to keep the interface simple for the purpose of the course.
If you find that the website malfunctions, please contact me about it
and specify which browser you are using:
vandeba (a) chalmers.se
This service is provided as is. Information you enter while using this site is not stored.
This interface was developed by Bart van Delft, 2013.
More information on Spin and its developers can be found at spinroot.com.
If you want to deploy or modify this website, the code (a mixture of DHTML and a small bit of PHP) is available on github with some documentation under the WTFPL license. The editor used is the ACE editor, which is distributed with the BSD license.
Select a file to edit. Note that you need to save changes back to a file on your local machine; they are not saved by the web service.
|