Control.Concurrent.CHPSpec.Monad

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

CHP Monad

type CHP = CHPSpecT (StateT CHPState IO)

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

class Monad m => MonadCHP m where

Methods

liftCHP :: CHP a -> m a

Instances

MonadCHP CHP

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

Like liftIO_CHP', but with an empty label.

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

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: http://chplib.wordpress.com/2010/04/20/automatic-model-generation-part-3-choice-and-io/

foreverP :: CHP a -> CHP b

Models processes that run forever.

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

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

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

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.

Instances

Typeable a => Process (CHP a)

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

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

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'
   where
     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'
   where
     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 -> p

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

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 a

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 a

Throws a poison exception. Poison is not currently modelled.

class Poisonable c where

Methods

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

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

Instances

Poisonable (Chanout a)

Poisonable (Chanin a)

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

Primitive actions

skip :: CHP ()

stop :: CHP a