The Adelaide Refinement Checker (ARC) is a Communicating Sequential Processes (CSP)
model checking environment. CSP scripts consist of definitions, including those of
processes and assertion statements where assertion statements define properties of
processes or relationships between processes. With ARC CSP scripts can be edited, parsed,
type checked, viewed, checked for data independent types and finally model checked.
The functionality of ARC has been restricted to editing, parsing, type checking and exploration of CSP scripts.
ARC is written in the Java 2 language and requires either the Java runtime
environment (JRE) or the Java software development kit (SDK) to be installed on the
machine on which it is to run. Either Java environment can be obtained from the following
web site: http://www.javasoft.com/j2se/*
If Java is already installed on your machine please ascertain that you have the correct version installed by entering java -version in a command or terminal window. The version information returned should be greater than version 1.2.
ARC is available in two compressed forms: a zip file for PCs and a tar, gzip file for Unix machines. To be able to run ARC decompress the downloaded file into an empty directory. Once decompressed you will find a Java jar file and a directory of example CSP scripts.
To start ARC first ensure that your current directory contains the arc.jar file. Then in a terminal window enter:
java -jar arc.jar
When ARC successfully starts a splash screen will appear. This will be followed by ARC window appearing. Please note that the command line above may be appended with the name of a CSP script.
Click here for the Unix version
Click here for the PC version