Core_CspCASL.hs revision 7703bbb85e121b1b4190179f4084683a31ae6ea9
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederDescription : Conversion to core CspCASL
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Andy Gimblett and Uni Bremen 2006
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederMaintainer : a.m.gimblett@swansea.ac.uk
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaederStability : provisional
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : portable
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederConverting sugared CspCASL to core CspCASL.
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian MaederThe following process types are core:
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder PrefixProcess ev p
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ExternalPrefixProcess v es p
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder InternalPrefixProcess v es p
d48085f765fca838c1d972d2123601997174583dChristian Maeder Sequential p q
47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder ExternalChoice p q
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder InternalChoice p q
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder GeneralisedParallel p es q
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder RelationalRenaming p RENAMING
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder NamedProcess pn evs
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder ConditionalProcess CSP_FORMULA p q
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder (Also the interrupt operator should be added, and core?)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedermodule CspCASL.Core_CspCASL (basicToCore) where
ce3928e71520030ad0275b72050a8f4377f9313cChristian MaederbasicToCore :: CspBasicSpec -> CspBasicSpec
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederbasicToCore c = CspBasicSpec (channels c) (core_procs)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder where core_procs = map procEqToCore (proc_items c)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder procEqToCore (ProcEq pn p) = (ProcEq pn (procToCore p))
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder procEqToCore x = x
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaederprocToCore :: PROCESS -> PROCESS
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederprocToCore proc = let p' = procToCore in case proc of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- First the core operators: we just need to recurse.
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder (Skip r) -> (Skip r)
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder (Stop r) -> (Stop r)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (PrefixProcess ev p r) -> (PrefixProcess ev (p' p) r)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (ExternalPrefixProcess v es p r) -> (ExternalPrefixProcess v es (p' p) r)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (InternalPrefixProcess v es p r) -> (InternalPrefixProcess v es (p' p) r)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (Sequential p q r) -> (Sequential (p' p) (p' q) r)
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder (ExternalChoice p q r) -> (ExternalChoice (p' p) (p' q) r)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (InternalChoice p q r) -> (InternalChoice (p' p) (p' q) r)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (GeneralisedParallel p es q r) -> (GeneralisedParallel (p' p) es (p' q) r)
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder (Hiding p es r) -> (Hiding (p' p) es r)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (RelationalRenaming p rn r) -> (RelationalRenaming (p' p) rn r)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (NamedProcess pn evs r) -> (NamedProcess pn evs r)
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder (ConditionalProcess f p q r) -> (ConditionalProcess f (p' p) (p' q) r)
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder -- Non-core, done.
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (Interleaving p q r) -> (GeneralisedParallel (p' p) (EmptyEventSet nullRange) (p' q) r)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- Non-core, not done yet.
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (Div r) -> (Div r)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (Run es r) -> (Run es r)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (Chaos es r) -> (Chaos es r)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (SynchronousParallel p q r) -> (SynchronousParallel (p' p) (p' q) r)
92aa1b88f02d2a413da60dba78acd34312e6f29aChristian Maeder (AlphabetisedParallel p esp esq q r) ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (AlphabetisedParallel (p' p) esp esq (p' q) r)