ConcurrencySuite Files

                 ConcurrencySuite
  Tools for teaching concurrency and nondeterminism
            http://sourceforge.net/projects/pcdp/

               Mordechai (Moti) Ben-Ari
            http://stwww.weizmann.ac.il/g-cs/benari/

Concurrency and nondeterminism are two of the most challenging topics in 
computer science. Concurrency is difficult because you cannot test 
a concurrent program so formal verification techniques are indispensable.
Nondeterminism is difficult because it is unnatural to students who have 
studied deterministic algorithms and programming.
From this site you can download a suite of software tools 
for teaching and learning these subjects:

jSpin - A development environment for the Spin model checker.

SpinSpider - A tool for automatically creating state transition
  diagrams of concurrent programs. (SpinSpider is integrated
  into jSpin and is not downloaded separately.)

iDot - A program for incremental visualization of Dot graphs
  such as those generated by SpinSpider.

VN - A software tool for visualizing and "experiencing" nondeterminism.

DAJ - An interactive program for studying distributed algorithms.

The tools are described in more detail below.

The programs are written in Java and are available under the 
GNU General Public License.
Other tools that are needed (Spin, Graphviz/dot, an ANSI C 
compiler, JFLAP) can be freely downloaded
as described in the documentation of each tool.

The tools are coordinated with my textbooks:

Principles of Concurrent and Distributed Programming (Second Edition), 
  Addison-Wesley, 2006.

Principles of Spin. Springer, 2007.

See also:
Gerard J. Holzmann. The Spin Model Checker, Addison-Wesley, 2004.

Spin

Spin was developed by Gerard J. Holzmann for verifying communications 
protocols; it earned him the ACM Software System Award for 2001. 
Concurrent programs are written in a simple C-like language called Promela,
and simulation and verification are carried out by Spin.

jSpin

jSpin is a development environment for Spin. Additionally,
jSpin filters the scenario data that is generated by Spin so that 
it can be flexibly displayed.

SpinSpider

The semantics of concurrent programs are defined in terms of automata, 
displayed graphically as state transition diagrams. SpinSpider is a tool that 
uses data available from Spin to construct the state transition diagram, which 
is then written in the dot language of Graphviz. The dot tool is called to 
layout the graph.

VN

Nondeterminism appears in several contexts such as nondeterministic 
finite automata (NDFA) and nondeterministic algorithms. VN is a 
software tool that leverages the nondeterministic execution of a 
Promela program by Spin and the graph layout capabilities of dot 
to enable the student "experience" the nondeterminism of an NDFA. VN can 
run in three modes: (1) random resolution of nondeterminism;
(2) interactive resolution of nondeterminism;
(3) verification mode to find an accepting computation if one exists.

DAJ

Distributed Algorithms in Java (DAJ) is designed for studying distributed
algorithms like the Byzantine Generals algorithm for consensus and
the Ricart-Agrawala algorithm for distributed mutual exclusion.
The data stored at each node is displayed and the student
can create scenarios interactively.