"Case Study: Replicated Workers Framework (RWF)"

This directory contains the following files:
------------------------------------------------------------------------------

RW.ada_original - original RWF ada code as modified by John Hatcliff.

RW.a		- RWF ada code used by me (I ran cfg-to-sedl on it);
		- it has stubs and driver; list unmodeled

RW.inca		- the inca equivalent of rw.a

RW1.prom	- promela code obtained from RW.inca for checking property1 
		(never1)
RW23.prom	- promela code obtained from RW.inca for checking property2 
		(never2) and property3 (never3)

RW4.prom	- promela code obtained from RW.inca for checking property4
		(never4)

RW5.prom	- promela code obtained from RW.inca for checking property5
		(never5)


RWlist.inca	- the inca code for RWF with 2-ordered abstraction

RWlist6.prom	- promela code obtained from RWlist.inca for checking property6
		(never6)

RWlist78.prom	- promela code obtained from RWlist.inca for checking property7
		(never7) and property8 (never8)

*.query		- query files for the corresponding *.inca files.

never*		- never claims for the corresponding properties 
		- "f" indicates filter

------------------------------------------------------------------------------