The Prototype Haskell Circal System

The Haskell Circal System is a modelling and verification tool for the Circal Process Algebra, embedded in the standard lazy purely functional programming language Haskell. Circal processes are defined in Haskell source code, using a set of process construction combinators. The Circal structural operators are provided directly as functions; behavioural processes are defined by writing down their transition systems. Higher-order functions provide powerful tools for defining complex paramaterised families of processes and systems -- even more so than the Circal system, since XCircal's embedding language XTC is cumbersome for complex symbolic manipulation. Features of the Haskell Circal system include:

• An equivalence and preorder checker for trace and testing equivalence ("may" and "must" preorders). In the case of failed checks, diagnostic traces are generated which highlight the inequivalence.
• Algorithms for analysing labelled transition systems: printing, nondeterminisim removal, state minimisation (these last two are not present in the Circal System).
• On-the-fly state space exploration. Only the parts of a system's state space actually needed for analysis are generated. Our experiments have shown that this makes possible some modelling and analysis techniques where constraint processes are composed with a large system in order to study aspects of the system's full behaviour.
• Function for translating Haskell-built Circal models into XTC code, to take advantage of the Circal System's fast equivalence checking engine.
• Poor time performance compared to the Circal System (on the order of 100 times slower). Haskell Circal seems to have better memory performance though, it can complete some large computations (albeit slowly) that the Circal System is unable to complete.

The Haskell Circal System is being developed as a prototype of an updated Circal System. This work is likely to include:

• A portable interchange data format for Circal models, allowing decoupling and separate development of tools.
• An equivalence checking engine based on the generation of C code written specifically for each particular computation (an approach used in the SPIN system). This should be faster than the current Circal System engine and have memory usage better than the current Haskell Circal System. The Haskell Circal system already performs a partial evalution transformation of Circal models internally to generate something like the sequential code needed.
• A BDD based equivalence-checking engine.
• A visual programming interface for the construction of behavioural and structural Circal models.
• A growing library of documented generic processes in a number of problem domains.

Distribution

The Haskell Circal System is still an experimental prototype, but a version can be made available for academic use (only) upon request.

If you wish to obtain a copy of Haskell Circal, please email joel@csse.uwa.edu.au. Haskell Circal is currently entirely Haskell 98 standard source code, so you will need a Haskell compiler and/or interpreter (eg ghc) and familiarity with Haskell.

Documentation

Unfortunately, there is no documentation (apart from the source code and examples) at this time. If you are interested in the system, let us know what documentation you would most like to have.

Examples

Here are some examples of X-Circal code:

• Fischer mutual-exclusion protocol: Fischer.hs
• Synchronous bus arbiter: Arbiter.hs This uses GateProcesses.hs. This example is older and in a messier style, but does correspond fairly closely with XCircal code for the same synchronous bus arbiter system.