Portability	GHC-only
Stability	experimental
Maintainer	fontaine@cs.uni-duesseldorf.de

CSPM.CoreLanguage.Process

Description

This modules defines a FDR-compatible CSP core language. The core language deals with CSP related constructs like processes and events, but abstracts, e.g. from the underlying functional programming language.

The implementation of the underlying language must provide instances for the type families Prefix and 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 whereSource

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 iSource

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 uses 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)

isOmega :: Process i -> Bool Source