This module contains all the central monads in the CHP library.
- type CHP = CHPSpecT (StateT CHPState IO)
- class Monad m => MonadCHP m where
- liftIO_CHP :: Serial a => IO a -> CHP a
- liftIO_CHP' :: Serial a => String -> IO a -> CHP a
- foreverP :: CHP a -> CHP b
- specify :: Bool -> CHP () -> IO String
- class Process p
- process :: Process p => String -> p -> p
- subProcess :: Process p => String -> p -> p
- onPoisonTrap :: forall a. CHP a -> CHP a -> CHP a
- onPoisonRethrow :: CHP a -> CHP () -> CHP a
- throwPoison :: CHP a
- class Poisonable c where
- poisonAll :: (Poisonable c, MonadCHP m) => [c] -> m ()
- skip :: CHP ()
- stop :: CHP a
The central monad of the library. You can use
specify function to model programs written with this monad.
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
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/
Models processes that run forever.
Anything following a
foreverP call in sequence will not be modelled.
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.
A class with instances for CHP processes of the form
a -> b -> .. -> CHP r.
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' = ...
Allows you to provide a handler for sections with poison. Since poison is
not currently modelled, this acts like
const at the moment.