| 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, ExtProcess
and class BL.
- type family Prefix i
- type family ExtProcess i
- class BE i => BL i where
- prefixNext :: Prefix i -> Event i -> Maybe (Process i)
- switchOn :: ExtProcess i -> Process i
- data Process i
- = 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
- | 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
Documentation
type family ExtProcess i Source
A process that has not yet been switched on.
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) | |
| Exception (EventSet i) (Process i) (Process i) |