Copyright	(c) Fontaine 2011
License	BSD
Maintainer	fontaine@cs.uni-duesseldorf.de
Stability	experimental
Portability	GHC-only
Safe Haskell	Safe
Language	Haskell2010

CSPM.CoreLanguage.Process

Description

This modules defines an FDR-compatible CSP core language. The core language deals with CSP-related constructs like processes and events.

The implementation of the underlying language must provide instances for the type families Prefix, ExtProcess and class BL.

Synopsis

Documentation

type family Prefix i Source #

A prefix expression.

type family ExtProcess i Source #

A process that has not yet been switched on.

class BE i => BL i where Source #

Minimal complete definition

prefixNext, switchOn

Methods

prefixNext :: Prefix i -> Event i -> Maybe (Process i) Source #

Try to perform an Event return the successor Process or Nothing if the event is not possible.

switchOn :: ExtProcess i -> Process i Source #

data Process i Source #

A data type for CSPM processes. For efficiency, replicated alphabetized parallel has an explicit constructor. Other replicated operations get translated on the fly. For constructing processes one should rather use the wrappers from CSPM.CoreLanguage.ProcessWrappers.

Constructors

Prefix (Prefix i)
ExternalChoice (Process i) (Process i)
InternalChoice (Process i) (Process i)
Interleave (Process i) (Process i)
Interrupt (Process i) (Process i)
Timeout (Process i) (Process i)
Sharing (Process i) (EventSet i) (Process i)
AParallel (EventSet i) (EventSet i) (Process i) (Process i)
RepAParallel [(EventSet i, Process i)]
Seq (Process i) (Process i)
Hide (EventSet i) (Process i)
Stop
Skip
Omega
Chaos (EventSet i)
AProcess Int	Just for debugging.
SwitchedOff (ExtProcess i)
Renaming (RenamingRelation i) (Process i)
LinkParallel (RenamingRelation i) (Process i) (Process i)
Exception (EventSet i) (Process i) (Process i)

isOmega :: Process i -> Bool Source #