chp-spec-1.0.0: A mirror implementation of chp that generates a specification of the program




This module contains all the central monads in the CHP library.


CHP Monad

type CHP = CHPSpecT (StateT CHPState IO)Source

The central monad of the library. You can use the specify function to model programs written with this monad.

class Monad m => MonadCHP m whereSource


liftCHP :: CHP a -> m aSource


liftIO_CHP :: Serial a => IO a -> CHP aSource

Like liftIO_CHP', but with an empty label.

liftIO_CHP' :: Serial a => String -> IO a -> CHP aSource

Models the lifting of an IO action into the CHP monad.

The IO computation itself is completely ignored. The label (first parameter) is used to label various different dummy events, which arise from exploring the return type of the IO computation. To support this exploration, the return type must be an instance of Serial.

More details and a full explanation of how IO events are modelled are available in this blog post:

foreverP :: CHP a -> CHP bSource

Models processes that run forever.

Anything following a foreverP call in sequence will not be modelled.

specify :: Bool -> CHP () -> IO StringSource

The top-level function in this library, to be used in place of runCHP in your program. You pass it a boolean (True if you want to leave the dummy IO events exposed, False if you want them hidden) and a CHP process that you want to specify. The result is a String containing a CSP-M specification that can be written out to a file and read in to other tools, such as FDR, PRoBE and others.

class Process p Source

A class with instances for CHP processes of the form a -> b -> .. -> CHP r.

The return value of the process must support Typeable, and the arguments of the process must support Typeable and Eq.


Typeable a => Process (CHP a) 
(Eq a, Typeable a, Process b) => Process (a -> b) 

process :: Process p => String -> p -> pSource

An annotation to put around a top-level process. This annotation must be inside the recursive knot. You can either place it as:

 foo :: Int -> String -> CHP ()
 foo = process "foo" $ \n s -> ...

Or as follows:

 foo :: Int -> String -> CHP ()
 foo = process "foo" foo'
     foo' n s = ...

The annotation must capture all the parameters to the process. What you must not do is place it such that there are free parameters not captured, for example this is wrong:

 foo :: Int -> String -> CHP ()
 foo n s = process "foo" foo'
     foo' = ...

If you do want to have recursive processes that have outer parameters and not pass them, you must wrap the outer process in process and the inner process(es) in subProcess.

subProcess :: Process p => String -> p -> pSource

onPoisonTrap :: forall a. CHP a -> CHP a -> CHP aSource

Allows you to provide a handler for sections with poison. Since poison is not currently modelled, this acts like const at the moment.

onPoisonRethrow :: CHP a -> CHP () -> CHP aSource

Like onPoisonTrap, this function allows you to provide a handler for poison. Since poison is not currently modelled, this acts like const at the moment.

throwPoison :: CHP aSource

Throws a poison exception. Poison is not currently modelled.

class Poisonable c whereSource


poison :: MonadCHP m => c -> m ()Source

checkForPoison :: MonadCHP m => c -> m ()Source


poisonAll :: (Poisonable c, MonadCHP m) => [c] -> m ()Source

Primitive actions