AS_CspCASL_Process.der.hs revision bba1e274cf727c39b4f1dd8970539a2bb967f20f
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederDescription : Abstract syntax of CSP-CASL processes
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederCopyright : (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : a.m.gimblett@swan.ac.uk
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederPortability : portable
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaederAbstract syntax of CSP-CASL processes.
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder CHANNEL_NAME,
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder EVENT_SET(..),
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder PROCESS_NAME,
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder RENAMING (..),
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder CommType(..),
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder TypedChanName(..)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport CASL.AS_Basic_CASL (FORMULA, SORT, TERM, VAR)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport qualified Data.Set as Set
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- DrIFT command
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder{-! global: GetRange !-}
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder = TermEvent (TERM ()) Range
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder | ChanSend CHANNEL_NAME (TERM ()) Range
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder | ChanNonDetSend CHANNEL_NAME VAR SORT Range
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder | ChanRecv CHANNEL_NAME VAR SORT Range
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder -- | A fully qualified event contains the event being
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder -- qualified. The channel of the fully qualified event should be
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder -- nothing if the contained event is a TermEvent - as this does
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder -- not have a channel. The channel should match the contained
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder -- event's channel if the contained event is not a TermEvent,
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder -- where the sort of the channel is also recorded in the
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder -- pair. The fully qualified term's event should be the fully
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder -- qualified version of the contained events' term. The range of
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder -- the fully qualified event should always be the same as the
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder -- range of the contained event. In the case of a fully
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder -- qualified ChanNonDetSend and ChanRecv the variable becomes a
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder -- fully qualified CASL term based on the variable and its sort.
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder | FQEvent EVENT (Maybe (CHANNEL_NAME, SORT)) (TERM ()) Range
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder deriving (Show,Ord, Eq)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- |Event sets are sets of communication types.
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederdata EVENT_SET = EventSet [COMM_TYPE] Range
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder -- | FQEvent set distinguishes between channel names and Sorts
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder | FQEventSet [CommType] Range
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder deriving (Show,Ord, Eq)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- |CSP renamings are predicate names or op names.
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederdata RENAMING = Renaming [Id]
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder | FQRenaming [TERM ()]
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder deriving (Show,Ord, Eq)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedertype CHANNEL_NAME = SIMPLE_ID
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedertype PROCESS_NAME = SIMPLE_ID
ad270004874ce1d0697fb30d7309f180553bb315Christian Maedertype COMM_TYPE = SIMPLE_ID
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder-- | A process communication alphabet consists of a set of sort names
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski-- and typed channel names.
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangdata TypedChanName = TypedChanName CHANNEL_NAME SORT
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder deriving (Eq, Ord, Show)
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederdata CommType = CommTypeSort SORT
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder | CommTypeChan TypedChanName
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang deriving (Eq, Ord)
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederinstance Show CommType where
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder show (CommTypeSort s) = show s
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder show (CommTypeChan (TypedChanName c s)) = show (c, s)
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maedertype CommAlpha = Set.Set CommType
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- |CSP-CASL process expressions.
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich -- | @Skip@ - Terminate immediately
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich -- | @Stop@ - Do nothing
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- | @div@ - Divergence
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu -- | @Run es@ - Accept any event in es, forever
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder | Run EVENT_SET Range
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder -- | @Chaos es@ - Accept\/refuse any event in es, forever
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | Chaos EVENT_SET Range
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- | @es -> p@ - Prefix process
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder | PrefixProcess EVENT PROCESS Range
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- | @[] var : es -> p@ - External nondeterministic prefix choice
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder | ExternalPrefixProcess VAR SORT PROCESS Range
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder -- | @|~| var : es -> p@ - Internal nondeterministic prefix choice
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder | InternalPrefixProcess VAR SORT PROCESS Range
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder -- | @p ; q@ - Sequential process
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder | Sequential PROCESS PROCESS Range
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder -- | @p [] q@ - External choice
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder | ExternalChoice PROCESS PROCESS Range
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder -- | @p |~| q@ - Internal choice
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder | InternalChoice PROCESS PROCESS Range
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder -- | @p ||| q@ - Interleaving
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder | Interleaving PROCESS PROCESS Range
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder -- | @p || q @ - Synchronous parallel
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder | SynchronousParallel PROCESS PROCESS Range
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder -- | @p [| a |] q@ - Generalised parallel
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder | GeneralisedParallel PROCESS EVENT_SET PROCESS Range
e6dccba746efe07338d3107fed512e713fd50b28Christian Maeder -- | @p [ a || b ] q@ - Alphabetised parallel
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder | AlphabetisedParallel PROCESS EVENT_SET EVENT_SET PROCESS Range
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder -- | @p \\ es@ - Hiding
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder | Hiding PROCESS EVENT_SET Range
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder -- | @p [[r]]@ - Renaming
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder | RenamingProcess PROCESS RENAMING Range
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder -- | @if f then p else q@ - Conditional
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder | ConditionalProcess (FORMULA ()) PROCESS PROCESS Range
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder -- | Named process
9a6779c8495854bdf36e4a87f98f095e8d0a6e45Christian Maeder | NamedProcess PROCESS_NAME [TERM ()] Range
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder -- | Fully qualified process. The range here shall be the same as
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder -- | in the process.
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder | FQProcess PROCESS CommAlpha Range
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder deriving (Eq, Ord, Show)