CSPM.CoreLanguage.Process

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.

Documentation

type family Prefix i

A prefix expression.

type family ExtProcess i

A process that has not yet been switched on.

class BE i => BL i where

Minimal complete definition

prefixNext, switchOn

Methods

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

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

switchOn :: ExtProcess i -> Process i

data Process i

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