AS_CspCASL_Process.der.hs revision 293d1430cbd764408a2565ce95380ee9aedd26c4
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : Abstract syntax of CSP-CASL processes
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiCopyright : (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : a.m.gimblett@swan.ac.uk
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiAbstract syntax of CSP-CASL processes.
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski CHANNEL_NAME,
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder EVENT_SET(..),
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder PROCESS_NAME,
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder RENAMING (..),
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder CommType(..),
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder TypedChanName(..)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport CASL.AS_Basic_CASL (FORMULA, SORT, TERM, VAR)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangimport qualified Data.Set as Set
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder-- DrIFT command
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder{-! global: GetRange !-}
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder -- | @t -> p@ - Term prefix
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder = TermEvent (TERM ()) Range
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder -- | @[] var :: s -> p@ - External nondeterministic prefix choice
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder | ExternalPrefixChoice VAR SORT Range
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- | @|~| var :: s -> p@ - Internal nondeterministic prefix choice
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | InternalPrefixChoice VAR SORT Range
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -- | @c ! t -> p@ - Channel send
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | ChanSend CHANNEL_NAME (TERM ()) Range
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich -- | @c ! var :: s -> p@ - Channel nondeterministic send
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder | ChanNonDetSend CHANNEL_NAME VAR SORT Range
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich -- | @c ? var :: s -> p@ - Channel recieve
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich | ChanRecv CHANNEL_NAME VAR SORT Range
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich -- | A fully qualified event contains the (non-fully qualified)
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich -- event being qualified. There other parameters depend on the
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich -- underlying type of the event.
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder -- For TermEvent, the fully qualified channel should be nothing
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- and the fully qualified term should be the fully qualified
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- CASL term version of the term being communicated in the inner
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder -- For ExternalPrefixChoice and InternalPrefixChoice, the fully
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu -- qualified channel should be nothing and the fully qualified
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski -- term should be the fully qualified CASL variable version (a
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski -- term) of the inner process's variable.
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder -- For ChanSend, the fully qualified channel should be the fully
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder -- qualified channel of the underlying event and the fully
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder -- qualified term should be the fully qualified CASL term
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder -- version of the term being communicated in the inner process.
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder -- For ChanNonDetSend and ChanRecv, the fully qualified channel
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder -- should be the fully qualified channel of the underlying event
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder -- and the fully qualified CASL variable version (a term) of the
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- inner process's variable
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder | FQEvent EVENT (Maybe (CHANNEL_NAME, SORT)) (TERM ()) Range
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder deriving (Show,Ord, Eq)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- | Event sets are sets of communication types.
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederdata EVENT_SET = EventSet [COMM_TYPE] Range
4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maeder -- | FQEvent set distinguishes between channel names and Sorts
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder | FQEventSet [CommType] Range
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder deriving (Show,Ord, Eq)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski-- | CSP renamings are predicate names or op names.
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskidata RENAMING = Renaming [Id]
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder | FQRenaming [TERM ()]
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder deriving (Show,Ord, Eq)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maedertype CHANNEL_NAME = SIMPLE_ID
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maedertype PROCESS_NAME = SIMPLE_ID
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maedertype COMM_TYPE = SIMPLE_ID
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder-- | A process communication alphabet consists of a set of sort names
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- and typed channel names.
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederdata TypedChanName = TypedChanName CHANNEL_NAME SORT
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski deriving (Eq, Ord, Show)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskidata CommType = CommTypeSort SORT
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder | CommTypeChan TypedChanName
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder deriving (Eq, Ord)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maederinstance Show CommType where
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder show (CommTypeSort s) = show s
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder show (CommTypeChan (TypedChanName c s)) = show (c, s)
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maedertype CommAlpha = Set.Set CommType
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder-- | CSP-CASL process expressions.
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder -- | @Skip@ - Terminate immediately
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- | @Stop@ - Do nothing
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder -- | @div@ - Divergence
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder -- | @Run es@ - Accept any event in es, forever
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | Run EVENT_SET Range
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- | @Chaos es@ - Accept\/refuse any event in es, forever
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | Chaos EVENT_SET Range
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- | @event -> p@ - Prefix process
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | PrefixProcess EVENT PROCESS Range
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- | @p ; q@ - Sequential process
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | Sequential PROCESS PROCESS Range
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- | @p [] q@ - External choice
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | ExternalChoice PROCESS PROCESS Range
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- | @p |~| q@ - Internal choice
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | InternalChoice PROCESS PROCESS Range
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- | @p ||| q@ - Interleaving
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | Interleaving PROCESS PROCESS Range
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- | @p || q @ - Synchronous parallel
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | SynchronousParallel PROCESS PROCESS Range
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- | @p [| a |] q@ - Generalised parallel
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | GeneralisedParallel PROCESS EVENT_SET PROCESS Range
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- | @p [ a || b ] q@ - Alphabetised parallel
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | AlphabetisedParallel PROCESS EVENT_SET EVENT_SET PROCESS Range
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- | @p \\ es@ - Hiding
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | Hiding PROCESS EVENT_SET Range
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- | @p [[r]]@ - Renaming
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder | RenamingProcess PROCESS RENAMING Range
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski -- | @if f then p else q@ - Conditional
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder | ConditionalProcess (FORMULA ()) PROCESS PROCESS Range
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder -- | Named process
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski | NamedProcess PROCESS_NAME [TERM ()] Range
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder -- | Fully qualified process. The range here shall be the same as
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder -- | in the process.
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder | FQProcess PROCESS CommAlpha Range
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder deriving (Eq, Ord, Show)