Copyright | (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | a.m.gimblett@swan.ac.uk |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe-Inferred |
Abstract syntax of CSP-CASL processes.
- type CHANNEL_NAME = Id
- type CommAlpha = Set CommType
- data CommType
- data EVENT
- = TermEvent (TERM ()) Range
- | ExternalPrefixChoice VAR SORT Range
- | InternalPrefixChoice VAR SORT Range
- | ChanSend CHANNEL_NAME (TERM ()) Range
- | ChanNonDetSend CHANNEL_NAME VAR SORT Range
- | ChanRecv CHANNEL_NAME VAR SORT Range
- | FQTermEvent (TERM ()) Range
- | FQExternalPrefixChoice (TERM ()) Range
- | FQInternalPrefixChoice (TERM ()) Range
- | FQChanSend (CHANNEL_NAME, SORT) (TERM ()) Range
- | FQChanNonDetSend (CHANNEL_NAME, SORT) (TERM ()) Range
- | FQChanRecv (CHANNEL_NAME, SORT) (TERM ()) Range
- data EVENT_SET = EventSet [CommType] Range
- data FQ_PROCESS_NAME
- data PROCESS
- = Skip Range
- | Stop Range
- | Div Range
- | Run EVENT_SET Range
- | Chaos EVENT_SET Range
- | PrefixProcess EVENT PROCESS Range
- | Sequential PROCESS PROCESS Range
- | ExternalChoice PROCESS PROCESS Range
- | InternalChoice PROCESS PROCESS Range
- | Interleaving PROCESS PROCESS Range
- | SynchronousParallel PROCESS PROCESS Range
- | GeneralisedParallel PROCESS EVENT_SET PROCESS Range
- | AlphabetisedParallel PROCESS EVENT_SET EVENT_SET PROCESS Range
- | Hiding PROCESS EVENT_SET Range
- | RenamingProcess PROCESS RENAMING Range
- | ConditionalProcess (FORMULA ()) PROCESS PROCESS Range
- | NamedProcess FQ_PROCESS_NAME [TERM ()] Range
- | FQProcess PROCESS CommAlpha Range
- type PROCESS_NAME = Id
- type PROC_ARGS = [SORT]
- data PROC_ALPHABET = ProcAlphabet [CommType]
- procNameToSimpProcName :: FQ_PROCESS_NAME -> PROCESS_NAME
- data ProcProfile = ProcProfile PROC_ARGS CommAlpha
- data RenameKind
- data Rename = Rename Id (Maybe (RenameKind, Maybe (SORT, SORT)))
- data RENAMING = Renaming [Rename]
- splitCASLVar :: TERM () -> (VAR, SORT)
- data TypedChanName = TypedChanName CHANNEL_NAME SORT
Documentation
type CHANNEL_NAME = Id
data CommType
data EVENT
TermEvent (TERM ()) Range |
|
ExternalPrefixChoice VAR SORT Range |
|
InternalPrefixChoice VAR SORT Range |
|
ChanSend CHANNEL_NAME (TERM ()) Range |
|
ChanNonDetSend CHANNEL_NAME VAR SORT Range |
|
ChanRecv CHANNEL_NAME VAR SORT Range |
|
FQTermEvent (TERM ()) Range |
|
FQExternalPrefixChoice (TERM ()) Range |
|
FQInternalPrefixChoice (TERM ()) Range |
|
FQChanSend (CHANNEL_NAME, SORT) (TERM ()) Range |
|
FQChanNonDetSend (CHANNEL_NAME, SORT) (TERM ()) Range |
|
FQChanRecv (CHANNEL_NAME, SORT) (TERM ()) Range |
|
data EVENT_SET
Event sets are sets of communication types.
data FQ_PROCESS_NAME
A process name is either a fully qualified process name or a plain process name.
PROCESS_NAME PROCESS_NAME | A non-fully qualified process name |
FQ_PROCESS_NAME PROCESS_NAME ProcProfile | A name with parameter sorts and communication ids from the parser. This is where the user has tried to specify a fully qualified process name |
data PROCESS
CSP-CASL process expressions.
Skip Range |
|
Stop Range |
|
Div Range |
|
Run EVENT_SET Range |
|
Chaos EVENT_SET Range |
|
PrefixProcess EVENT PROCESS Range |
|
Sequential PROCESS PROCESS Range |
|
ExternalChoice PROCESS PROCESS Range |
|
InternalChoice PROCESS PROCESS Range |
|
Interleaving PROCESS PROCESS Range |
|
SynchronousParallel PROCESS PROCESS Range |
|
GeneralisedParallel PROCESS EVENT_SET PROCESS Range |
|
AlphabetisedParallel PROCESS EVENT_SET EVENT_SET PROCESS Range |
|
Hiding PROCESS EVENT_SET Range |
|
RenamingProcess PROCESS RENAMING Range |
|
ConditionalProcess (FORMULA ()) PROCESS PROCESS Range |
|
NamedProcess FQ_PROCESS_NAME [TERM ()] Range | Named process |
FQProcess PROCESS CommAlpha Range | Fully qualified process. The range here shall be the same as in the process. |
type PROCESS_NAME = Id
data PROC_ALPHABET
data ProcProfile
Fully qualified process names have parameter sorts, and a communication alphabet (a Set of sorts). The CommAlpha here should always contain the minimal super sorts only. The communication over subsorts is implied
Eq ProcProfile | |
Data ProcProfile | |
Ord ProcProfile | |
Show ProcProfile | |
ShATermConvertible ProcProfile | |
GetRange ProcProfile | |
Pretty ProcProfile | Pretty printing for process profiles |
Typeable * ProcProfile |
data RenameKind
data Rename
data RENAMING
CSP renamings are predicate names or op names.
splitCASLVar :: TERM () -> (VAR, SORT)
data TypedChanName
A process communication alphabet consists of a set of sort names and typed channel names.