Here is the list of examples:

inteq.sp: a simple example illustrating how to write concurrent program specifications. It specifies a concurrent program for finding integer solutions to the equation w^2 = x^2 + y^2 + z^2.


test2.sp: This is a test file intended to check the code generation module. It generates a process that creates periodically a thread until it terminates. There are synchronizations between the process and the threads it generates. 


The test3  files below consider the dining philosopher problem.

test3a.sp: Tests that the deadlock prevention function works fine when no deadlock is possible. Only one philosopher with two resources. 

test3c.sp: A test involving 5 philosophers. 

test3d.sp: A test involving 5 philosophers. Here, the resources (chopsticks) are defined as supervisor components, not as threads. 


reader.sp: this is a reader/deleter/inserter example. It illustrates more complex marking and firing vector constraints.


The examples test2.sp, test3a, test3c, and test3d were converted to the current specification format by Micah Martin and Basil Hall. 
