hets/CspCASL/AS_CspCASL_Process.der.hs

	AS_CspCASL_Process.der.hs revision 9582375827616730f146b77f9d5a4fd0cc78bc47
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder{- |
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederModule      :  $Id$
81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription :  Abstract syntax of CSP-CASL processes
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaederCopyright   :  (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer  :  a.m.gimblett@swan.ac.uk
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederStability   :  provisional
fbb66ee3e170624835b99f7aa91980753cb5b472Christian MaederPortability :  portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederAbstract syntax of CSP-CASL processes.
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder-}
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maedermodule CspCASL.AS_CspCASL_Process (
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder    CHANNEL_NAME,
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder    COMM_TYPE,
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder    EVENT(..),
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder    EVENT_SET(..),
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder    CSP_FORMULA(..),
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder    PROCESS(..),
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder    PROCESS_NAME,
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder    RENAMING,
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder) where
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport CASL.AS_Basic_CASL (FORMULA, SORT, TERM, VAR)
33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maederimport Common.Id
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder-- DrIFT command
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder{-! global: UpPos !-}
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maederdata EVENT
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder    = TermEvent (TERM ()) Range
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder    | ChanSend CHANNEL_NAME (TERM ()) Range
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder    | ChanNonDetSend CHANNEL_NAME VAR SORT Range
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski    | ChanRecv CHANNEL_NAME VAR SORT Range
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder    deriving (Show,Eq)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski-- |Event sets are sets of communication types.
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederdata EVENT_SET = EventSet [COMM_TYPE] Range
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder    deriving (Show,Eq)
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- |Formulas.  These are basically just CASL formulas.
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maederdata CSP_FORMULA
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder    = Formula (FORMULA ()) Range
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder    deriving (Show,Eq)
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder-- |CSP renamings are predicate names or op names.
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maedertype RENAMING = [Id]
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder
c44c23429c72f3a709e22a18f2ed6f05fc8cc765Christian Maeder
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maedertype CHANNEL_NAME = SIMPLE_ID
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maedertype PROCESS_NAME = SIMPLE_ID
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maedertype COMM_TYPE = SIMPLE_ID
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder-- |CSP-CASL process expressions.
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederdata PROCESS
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder    -- | @Skip@ - Terminate immediately
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder    = Skip Range
3c62e6ef442caf092adcbecf6fccd957dcd72689Christian Maeder    -- | @Stop@ - Do nothing
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder    | Stop Range
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder    -- | @div@ - Divergence
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder    | Div Range
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder    -- | @Run es@ - Accept any event in es, forever
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder    | Run EVENT_SET Range
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder    -- | @Chaos es@ - Accept\/refuse any event in es, forever
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder    | Chaos EVENT_SET Range
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder    -- | @es -> p@ - Prefix process
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder    | PrefixProcess EVENT PROCESS Range
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder    -- | @[] var : es -> p@ - External nondeterministic prefix choice
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder    | ExternalPrefixProcess VAR SORT PROCESS Range
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder    -- | @|~| var : es -> p@ - Internal nondeterministic prefix choice
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder    | InternalPrefixProcess VAR SORT PROCESS Range
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder    -- | @p ; q@ - Sequential process
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder    | Sequential PROCESS PROCESS Range
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian Maeder    -- | @p [] q@ - External choice
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder    | ExternalChoice PROCESS PROCESS Range
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder    -- | @p |~| q@ - Internal choice
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder    | InternalChoice PROCESS PROCESS Range
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder    -- | @p ||| q@ - Interleaving
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder    | Interleaving PROCESS PROCESS Range
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder    -- | @p || q @ - Synchronous parallel
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian Maeder    | SynchronousParallel PROCESS PROCESS Range
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder    -- | @p [| a |] q@ - Generalised parallel
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder    | GeneralisedParallel PROCESS EVENT_SET PROCESS Range
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder    -- | @p [ a || b ] q@ - Alphabetised parallel
149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder    | AlphabetisedParallel PROCESS EVENT_SET EVENT_SET PROCESS Range
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder    -- | @p \\ es@ - Hiding
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder    | Hiding PROCESS EVENT_SET Range
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder    -- | @p [[r]]@ - Renaming
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder    | RelationalRenaming PROCESS RENAMING Range
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder    -- | @if f then p else q@ - Conditional
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder    | ConditionalProcess CSP_FORMULA PROCESS PROCESS Range
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder    -- | Named process
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian Maeder    | NamedProcess PROCESS_NAME [EVENT] Range
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder    deriving (Eq, Show)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder