| Portability | GHC-only |
|---|---|
| Stability | experimental |
| Maintainer | fontaine@cs.uni-duesseldorf.de |
| Safe Haskell | Safe-Inferred |
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.
- 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 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) |