ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder{-# LANGUAGE MultiParamTypeClasses #-}

ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder{- |

c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederModule : $Header$

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederDescription : Symbols and signature morphisms for the CspCASL logic

ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederCopyright : (c) Liam O'Reilly, Markus Roggenbach, Swansea University 2008

eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian MaederLicense : GPLv2 or higher, see LICENSE.txt

ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder

c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederMaintainer : csliam@swansea.ac.uk

ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederStability : provisional

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : portable

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian MaederSymbols and signature morphisms for the CspCASL logic

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder-}

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maedermodule CspCASL.Morphism

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder ( CspCASLMorphism

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder , CspAddMorphism (..)

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , ChanMap

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder , ProcessMap

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder , mapProcProfile

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , cspSubsigInclusion

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , emptyCspAddMorphism

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder , cspAddMorphismUnion

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder , cspMorphismToCspSymbMap

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder , inducedCspSign

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder , mapSen

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder ) where

fc7df539e6d41b050161ed8f9ae6e444b1b5ab14Christian Maeder

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederimport CspCASL.AS_CspCASL_Process

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederimport CspCASL.SignCSP

2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maederimport CspCASL.Symbol

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport qualified CspCASL.LocalTop as LT

d3bca27d616c5741d0b18776c8a0848ec31c87f4Christian Maeder

2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maederimport CASL.AS_Basic_CASL (FORMULA, TERM, SORT, SORT_ITEM (..))

cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maederimport CASL.Sign as CASL_Sign

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maederimport CASL.Morphism as CASL_Morphism

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederimport qualified CASL.MapSentence as CASL_MapSen

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederimport Common.Doc

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederimport Common.DocUtils

04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport Common.Id

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederimport Common.Result

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederimport Common.Utils (composeMap, isSingleton)

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederimport qualified Common.Lib.MapSet as MapSet

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederimport qualified Common.Lib.Rel as Rel

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder

04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport qualified Data.Map as Map

ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maederimport qualified Data.Set as Set

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder-- Morphisms

cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder

cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder{- | This is the second component of a CspCASL signature moprhism, the process

cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maedername map. We map process name with a profile into new names and

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maedercommunications alphabet. We follow CASL here and instread of mapping to a new

cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maedername and a new profile, we map just to the new name and the new

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maedercommunications alphabet of the profile. This is because the argument sorts of

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederthe profile have no chocie they have to be the sorts resultsing from maping

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederthe original sorts in the profile with the data part map. Note: the

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maedercommunications alphabet of the source profile must be downward closed with

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederrespect to the CASL signature sub-sort relation (at source) and also the

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maedertarget communications alphabet must be downward closed with respect to the

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian MaederCASL signature sub-sort relation (at target). -}

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maedertype ProcessMap =

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder Map.Map (PROCESS_NAME, ProcProfile) (PROCESS_NAME, CommAlpha)

ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maedertype ChanMap = Map.Map (CHANNEL_NAME, SORT) CHANNEL_NAME

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder-- | CspAddMorphism - This is just the extended part

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maederdata CspAddMorphism = CspAddMorphism

8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maeder {- Note that when applying the CspAddMorphism to process names or channel

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder names, if the name is not in the map in the morphism, then the

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder application is the identity function. Thus empty maps are used to form

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder the empty morphism and the identity morphism. -}

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder { channelMap :: ChanMap

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , processMap :: ProcessMap

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder } deriving (Eq, Ord, Show)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | The empty CspAddMorphism.

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskiemptyCspAddMorphism :: CspAddMorphism

c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederemptyCspAddMorphism = CspAddMorphism

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder {- Note that when applying the CspAddMorphism to process names or

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder channel names, if the name is not in the map in the morphism,

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder then the application is the identity function. Thus empty maps

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder are used to form the empty morphism. -}

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder { channelMap = Map.empty

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , processMap = Map.empty

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder }

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder{- | Given two signatures (the first being a sub signature of the second

7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maederaccording to CspCASL.SignCSP.isCspCASLSubSig) compute the inclusion morphism. -}

c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedercspSubsigInclusion :: CspCASLSign -> CspCASLSign -> Result CspCASLMorphism

e76e6a43f51438215737d6fc176c89da05bb86daChristian MaedercspSubsigInclusion = CASL_Morphism.sigInclusion emptyCspAddMorphism

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder{- We use the empty morphism as it also represents the identity, thus this

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maederwill embed channel names and process names properly. -}

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder-- | lookup a typed channel

0b14ccc700093e203914052bf6aceda3164af730Christian MaedermapChan :: Sort_map -> ChanMap -> (CHANNEL_NAME, SORT) -> (CHANNEL_NAME, SORT)

0b14ccc700093e203914052bf6aceda3164af730Christian MaedermapChan sm cm p@(c, s) = (Map.findWithDefault c p cm, mapSort sm s)

0b14ccc700093e203914052bf6aceda3164af730Christian Maeder

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder-- | Apply a signature morphism to a channel name

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedermapChannel :: Morphism f CspSign CspAddMorphism -> (CHANNEL_NAME, SORT)

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder -> (CHANNEL_NAME, SORT)

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaedermapChannel mor = mapChan (sort_map mor) $ channelMap $ extended_map mor

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedermapCommTypeAux :: Sort_map -> ChanMap -> CommType -> CommType

c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedermapCommTypeAux sm cm ct = case ct of

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder CommTypeSort s -> CommTypeSort $ mapSort sm s

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder CommTypeChan (TypedChanName c s) -> let (d, t) = mapChan sm cm (c, s) in

d48085f765fca838c1d972d2123601997174583dChristian Maeder CommTypeChan $ TypedChanName d t

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder-- | Apply a signature morphism to a CommType

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedermapCommType :: Morphism f CspSign CspAddMorphism -> CommType -> CommType

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedermapCommType mor = mapCommTypeAux (sort_map mor) (channelMap $ extended_map mor)

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedermapCommAlphaAux :: Sort_map -> ChanMap -> CommAlpha -> CommAlpha

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedermapCommAlphaAux sm = Set.map . mapCommTypeAux sm

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder-- | Apply a signature morphism to a CommAlpha

c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedermapCommAlpha :: Morphism f CspSign CspAddMorphism -> CommAlpha -> CommAlpha

c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedermapCommAlpha = Set.map . mapCommType

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder

c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedermapProcProfile :: Sort_map -> ChanMap -> ProcProfile -> ProcProfile

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedermapProcProfile sm cm (ProcProfile sl cs) =

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder ProcProfile (map (mapSort sm) sl) $ mapCommAlphaAux sm cm cs

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder

793945d4ac7c0f22760589c87af8e71427c76118Christian MaedermapProcId :: Sort_map -> ChanMap -> ProcessMap

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder -> (PROCESS_NAME, ProcProfile) -> (PROCESS_NAME, ProcProfile)

c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedermapProcId sm cm pm (i, p) = let

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder n@(ProcProfile args _) = mapProcProfile sm cm p

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder in case Map.lookup (i, p) pm of

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder Nothing -> (i, n)

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder Just (j, alpha) -> (j, ProcProfile args alpha)

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder

793945d4ac7c0f22760589c87af8e71427c76118Christian MaedermapProcess :: Morphism f CspSign CspAddMorphism

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder -> (PROCESS_NAME, ProcProfile) -> (PROCESS_NAME, ProcProfile)

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaedermapProcess mor = let em = extended_map mor in

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder mapProcId (sort_map mor) (channelMap em) $ processMap em

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder-- | Compose two CspAddMorphisms

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaedercomposeCspAddMorphism :: Morphism f CspSign CspAddMorphism

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder -> Morphism f CspSign CspAddMorphism -> Result CspAddMorphism

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaedercomposeCspAddMorphism m1 m2 = let

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder sMap1 = sort_map m1

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder sMap2 = sort_map m2

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder sMap = composeMap (MapSet.setToMap $ sortSet src) sMap1 sMap2

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder src = msource m1

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder cSrc = extendedInfo src

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder cMap = MapSet.foldWithKey ( \ c s ->

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder let p = (c, s)

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder ni = fst $ mapChannel m2 $ mapChannel m1 p

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder in if c == ni then id else Map.insert p ni)

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder Map.empty $ chans cSrc

0b14ccc700093e203914052bf6aceda3164af730Christian Maeder pMap = MapSet.foldWithKey ( \ p pr@(ProcProfile _ a) ->

cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder let pp = (p, pr)

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder (ni, ProcProfile _ na) =

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder mapProcess m2 $ mapProcess m1 pp

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder oa = mapCommAlphaAux sMap cMap a

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder in if p == ni && oa == na then id else

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder Map.insert pp (ni, na))

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder Map.empty $ procSet cSrc

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder in return emptyCspAddMorphism

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder { channelMap = cMap

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder , processMap = pMap }

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder{- | A CspCASLMorphism is a CASL Morphism with the extended_map to be a

c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederCspAddMorphism. -}

0b14ccc700093e203914052bf6aceda3164af730Christian Maedertype CspCASLMorphism = CASL_Morphism.Morphism CspSen CspSign CspAddMorphism

0b14ccc700093e203914052bf6aceda3164af730Christian Maeder

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder{- | Check if a CspCASL signature morphism has the refl property i.e.,

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maedersigma(s1) <= sigma(s2) implies s1 <= s2 for all s1, s2 in S -}

15c12a3ac049a4528da05b1017b78145f308aeb0Christian MaedercheckReflCondition :: Morphism f CspSign CspAddMorphism -> Result ()

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian MaedercheckReflCondition mor =

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder let sig = msource mor

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder sig' = mtarget mor

cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder sm = sort_map mor

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder rel = sortRel sig

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder rel' = sortRel sig'

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder allPairs = LT.cartesian $ sortSet sig

cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder failures = Set.filter (not . test) allPairs

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder test (s1, s2) = if Rel.path (mapSort sm s1) (mapSort sm s2) rel' ||

cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder mapSort sm s1 == mapSort sm s2

f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder then Rel.path s1 s2 rel || s1 == s2

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder else True

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder in if Set.null failures

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder then return ()

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder else let produceDiag (s1, s2) =

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder let x = (mapSort sm s1)

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder y = (mapSort sm s2)

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder in Diag Error

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder ("CSP-CASL Signature Morphism Refl Property Violated:\n'"

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder ++ showDoc (Symbol x $ SubsortAsItemType y) "' but not\n'"

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder ++ showDoc (Symbol s1 $ SubsortAsItemType s2) "'")

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski nullRange

20fe556546c9277cf017931a07d90add61f199d9Christian Maeder allDiags = map produceDiag $ Set.toList failures

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder in Result allDiags Nothing -- failure with error messages

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder

20fe556546c9277cf017931a07d90add61f199d9Christian Maeder

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder{- | Check if a CspCASL signature morphism has the weak non extension property

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maederi.e.,

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maedersigma(s1) <= u' and sigma(s2) <= u' implies there exists t in S with

c9b711a46e5138b2742727817c8071960e673073Christian Maeders1 <= t and s2 <= t and sigma(t) <= u' for all s1,s2 in S and u' in S' -}

c9b711a46e5138b2742727817c8071960e673073Christian MaedercheckWNECondition :: Morphism f CspSign CspAddMorphism -> Result ()

c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedercheckWNECondition mor =

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder let sig = msource mor

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder sig' = mtarget mor

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder sm = sort_map mor

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder rel' = sortRel sig'

59c036af82aff7fbe074455dad50477b7878e2d8Christian Maeder supers s signature = Set.insert s $ supersortsOf s signature

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder allPairsInSource = LT.cartesian $ sortSet sig

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder commonSuperSortsInTarget s1 s2 = Set.intersection

59c036af82aff7fbe074455dad50477b7878e2d8Christian Maeder (supers (mapSort sm s1) sig')

59c036af82aff7fbe074455dad50477b7878e2d8Christian Maeder (supers (mapSort sm s2) sig')

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder {- Candidates are triples (s1,s2,u') such that

\sigma(s1),\sigma(s2) < u' -}

createCandidateTripples (s1, s2) =

Set.map (\ u' -> (s1, s2, u')) (commonSuperSortsInTarget s1 s2)

allCandidateTripples =

Set.unions $ Set.toList $ Set.map createCandidateTripples

allPairsInSource

testCandidate (s1, s2, u') =

let possibleWitnesses = Set.intersection (supers s1 sig) (supers s2 sig)

test t = Rel.path (mapSort sm t) u' rel' || mapSort sm t == u'

in or $ Set.toList $ Set.map test possibleWitnesses

failures = Set.filter (not . testCandidate) allCandidateTripples

in if Set.null failures

then return ()

else let produceDiag (s1, s2, u') =

let x = (mapSort sm s1)

y = (mapSort sm s2)

in Diag Error

("CSP-CASL Signature Morphism Weak Non-Extension Property "

++ "Violated:\n'"

++ showDoc

(Subsort_decl [x, y] u' nullRange :: SORT_ITEM ())

"'\nbut no common supersort for\n'"

++ showDoc

(Sort_decl [s1, s2] nullRange :: SORT_ITEM ()) "'")

nullRange

allDiags = map produceDiag $ Set.toList failures

in Result allDiags Nothing -- failure with error messages

-- | unite morphisms

cspAddMorphismUnion :: CspCASLMorphism -> CspCASLMorphism

-> Result CspAddMorphism

cspAddMorphismUnion mor1 mor2 = let

s1 = extendedInfo $ msource mor1

s2 = extendedInfo $ msource mor2

m1 = extended_map mor1

m2 = extended_map mor2

chan1 = channelMap m1

chan2 = channelMap m2

delChan (n, s) m = MapSet.delete n s m

uc1 = foldr delChan (chans s1) $ Map.keys chan1

uc2 = foldr delChan (chans s2) $ Map.keys chan2

uc = MapSet.union uc1 uc2

proc1 = processMap m1

proc2 = processMap m2

delProc (n, p) m = MapSet.delete n p m

up1 = foldr delProc (procSet s1) $ Map.keys proc1

up2 = foldr delProc (procSet s2) $ Map.keys proc2

up = MapSet.union up1 up2

showAlpha (i, s) l = shows i (if null l then "" else "(..)") ++ ":"

++ if isSingleton s then showDoc (Set.findMin s) "" else showDoc s ""

(cds, cMap) = foldr ( \ (isc@(i, s), j) (ds, m) ->

case Map.lookup isc m of

Nothing -> (ds, Map.insert isc j m)

Just k -> if j == k then (ds, m) else

(Diag Error

("incompatible mapping of channel " ++ shows i ":"

++ showDoc s " to " ++ shows j " and "

++ shows k "") nullRange : ds, m)) ([], chan1)

(Map.toList chan2 ++ concatMap ( \ (c, ts) -> map

( \ s -> ((c, s), c)) ts) (MapSet.toList uc))

(pds, pMap) =

foldr ( \ (isc@(i, pt@(ProcProfile args _)), j) (ds, m) ->

case Map.lookup isc m of

Nothing -> (ds, Map.insert isc j m)

Just k -> if j == k then (ds, m) else

(Diag Error

("incompatible mapping of process " ++ shows i " "

++ showDoc pt " to " ++ showAlpha j args ++ " and "

++ showAlpha k args) nullRange : ds, m)) (cds, proc1)

(Map.toList proc2 ++ concatMap ( \ (p, pts) -> map

( \ pt@(ProcProfile _ al) -> ((p, pt), (p, al))) pts)

(MapSet.toList up))

in if null pds then return emptyCspAddMorphism

{ channelMap = cMap

, processMap = pMap }

else Result pds Nothing

toCspSymbMap :: Bool -> Morphism f CspSign CspAddMorphism

-> Map.Map CspSymbol CspSymbol

toCspSymbMap b mor = let

src = extendedInfo $ msource mor

chanSymMap = MapSet.foldWithKey

( \ i t -> let

p = (i, t)

q@(j, _) = mapChannel mor p

in if b && i == j then id else

Map.insert (toChanSymbol p) $ toChanSymbol q)

Map.empty $ chans src

procSymMap = MapSet.foldWithKey

( \ i t@(ProcProfile _ al) -> let

p = (i, t)

al1 = mapCommAlpha mor al

q@(j, ProcProfile _ al2) = mapProcess mor p

in if b && i == j && al1 == al2 then id else

Map.insert (toProcSymbol p) $ toProcSymbol q)

Map.empty $ procSet src

in Map.union chanSymMap procSymMap

cspMorphismToCspSymbMap :: CspCASLMorphism -> Map.Map CspSymbol CspSymbol

cspMorphismToCspSymbMap mor =

Map.union (Map.fromList

. map (\ (a, b) -> (caslToCspSymbol a, caslToCspSymbol b))

$ Map.toList $ morphismToSymbMap mor)

$ toCspSymbMap False mor

-- | Instance for CspCASL signature extension

instance SignExtension CspSign where

isSubSignExtension = isCspSubSign

-- | a dummy instances used for the default definition

instance Pretty CspAddMorphism where

pretty m = pretty $ toCspSymbMap False

$ embedMorphism m emptyCspCASLSign emptyCspCASLSign

-- | Instance for CspCASL morphism extension (used for Category)

instance CASL_Morphism.MorphismExtension CspSign CspAddMorphism

where

ideMorphismExtension _ = emptyCspAddMorphism

composeMorphismExtension = composeCspAddMorphism

-- we omit inverses here

isInclusionMorphismExtension m =

Map.null (channelMap m) && Map.null (processMap m)

-- pretty printing for Csp morphisms

prettyMorphismExtension = printMap id sepByCommas pairElems

. toCspSymbMap True

legalMorphismExtension m =

joinResult (checkReflCondition m) (checkWNECondition m)

-- * induced signature extension

inducedChanMap :: Sort_map -> ChanMap -> ChanNameMap -> ChanNameMap

inducedChanMap sm cm = MapSet.foldWithKey

( \ i s ->

let (j, t) = mapChan sm cm (i, s)

in MapSet.insert j t) MapSet.empty

inducedProcMap :: Sort_map -> ChanMap -> ProcessMap -> ProcNameMap

-> ProcNameMap

inducedProcMap sm cm pm = MapSet.foldWithKey

( \ n p ->

let (m, q) = mapProcId sm cm pm (n, p)

in MapSet.insert m q) MapSet.empty

inducedCspSign :: InducedSign f CspSign CspAddMorphism CspSign

inducedCspSign sm _ _ m sig =

let csig = extendedInfo sig

cm = channelMap m

in emptyCspSign

{ chans = inducedChanMap sm cm $ chans csig

, procSet = inducedProcMap sm cm (processMap m) $ procSet csig }

-- * application of morhisms to sentences

-- | Apply a Signature Morphism to a CspCASL Sentence

mapSen :: CspCASLMorphism -> CspSen -> CspSen

mapSen mor sen =

if CASL_Morphism.isInclusionMorphism

CASL_Morphism.isInclusionMorphismExtension mor

then sen

else case sen of

ProcessEq procName fqVarList commAlpha proc ->

let {- Map the morphism over all the parts of the process

equation -}

newProcName = mapProcessName mor procName

newFqVarList = mapFQProcVarList mor fqVarList

newCommAlpha = mapCommAlpha mor commAlpha

newProc = mapProc mor proc

in ProcessEq newProcName newFqVarList

newCommAlpha newProc

-- | Apply a signature morphism to a Fully Qualified Process Variable List

mapFQProcVarList :: CspCASLMorphism -> FQProcVarList -> FQProcVarList

mapFQProcVarList mor =

-- As these are terms, just map the morphism over CASL TERMs

map (mapCASLTerm mor)

-- | Apply a signature morphism to a process

mapProc :: CspCASLMorphism -> PROCESS -> PROCESS

mapProc mor proc =

let mapProc' = mapProc mor

mapProcessName' = mapProcessName mor

mapEvent' = mapEvent mor

mapEventSet' = mapEventSet mor

mapRenaming' = mapRenaming mor

mapCommAlpha' = mapCommAlpha mor

mapCASLTerm' = mapCASLTerm mor

mapCASLFormula' = mapCASLFormula mor

in case proc of

Skip r -> Skip r

Stop r -> Stop r

Div r -> Div r

Run es r -> Run (mapEventSet' es) r

Chaos ev r -> Chaos (mapEventSet' ev) r

PrefixProcess e p r ->

PrefixProcess (mapEvent' e) (mapProc' p) r

Sequential p q r -> Sequential (mapProc' p) (mapProc' q) r

ExternalChoice p q r -> ExternalChoice (mapProc' p) (mapProc' q) r

InternalChoice p q r -> InternalChoice (mapProc' p) (mapProc' q) r

Interleaving p q r -> Interleaving (mapProc' p) (mapProc' q) r

SynchronousParallel p q r ->

SynchronousParallel (mapProc' p) (mapProc' q) r

GeneralisedParallel p es q r ->

GeneralisedParallel (mapProc' p) (mapEventSet' es) (mapProc' q) r

AlphabetisedParallel p les res q r ->

AlphabetisedParallel (mapProc' p) (mapEventSet' les)

(mapEventSet' res) (mapProc' q) r

Hiding p es r ->

Hiding (mapProc' p) (mapEventSet' es) r

RenamingProcess p re r ->

RenamingProcess (mapProc' p) (mapRenaming' re) r

ConditionalProcess f p q r ->

ConditionalProcess (mapCASLFormula' f)

(mapProc' p) (mapProc' q) r

NamedProcess pn fqParams r ->

NamedProcess (mapProcessName' pn) (map mapCASLTerm' fqParams) r

FQProcess p commAlpha r ->

FQProcess (mapProc' p) (mapCommAlpha' commAlpha) r

-- | Apply a signature morphism to an event set

mapEventSet :: CspCASLMorphism -> EVENT_SET -> EVENT_SET

mapEventSet mor (EventSet fqComms r) =

EventSet (map (mapCommType mor) fqComms) r

-- | Apply a signature morphism to an event

mapEvent :: CspCASLMorphism -> EVENT -> EVENT

mapEvent mor e =

let mapEvent' = mapEvent mor

mapCASLTerm' = mapCASLTerm mor

mapSort' = CASL_MapSen.mapSrt mor

mapChannelName' = mapChannel mor

in case e of

TermEvent t r ->

-- Just map the morphism over the event (a term)

TermEvent (mapCASLTerm' t) r

InternalPrefixChoice v s r ->

-- Just map the morphism over the sort, we keep the variable name

InternalPrefixChoice v (mapSort' s) r

ExternalPrefixChoice v s r ->

-- Just map the morphism over the sort, we keep the variable name

ExternalPrefixChoice v (mapSort' s) r

ChanSend c t r ->

-- Just map the morphism over the event (a term) and the channel name

ChanSend (fst $ mapChannelName' (c, sortOfTerm t)) (mapCASLTerm' t) r

ChanNonDetSend c v s r ->

{- Just map the morphism over the sort and the channel name, we keep

the variable name -}

ChanNonDetSend (fst $ mapChannelName' (c, s)) v (mapSort' s) r

ChanRecv c v s r ->

{- Just map the morphism over the sort and the channel name, we keep

the variable name -}

ChanRecv (fst $ mapChannelName' (c, s)) v (mapSort' s) r

FQEvent ev mfqc fqTerm r ->

-- Map the morphism over each part of the FQEvent

FQEvent (mapEvent' ev) (fmap mapChannelName' mfqc)

(mapCASLTerm' fqTerm) r

mapRenaming :: CspCASLMorphism -> RENAMING -> RENAMING

mapRenaming mor re =

case re of

Renaming _ ->

{- There should be no (non fully qualified) Renamings (only

FQRenamings) as the static analysis should have transformed

EventSets into FQEventSets -}

error "CspCASL.Morphism.mapRenaming: Unexpected Renaming"

FQRenaming rs -> FQRenaming $ map (mapCASLTerm mor) rs

cspCASLMorphism2caslMorphism :: CspCASLMorphism -> Morphism () () ()

cspCASLMorphism2caslMorphism m =

m { msource = ccSig2CASLSign $ msource m

, mtarget = ccSig2CASLSign $ mtarget m

, extended_map = () }

{- | Apply a signature morphism to a CASL TERM (for CspCASL only, i.e. a CASL

TERM that appears in CspCASL). -}

mapCASLTerm :: CspCASLMorphism -> TERM () -> TERM ()

mapCASLTerm =

{- The error here is not used. It is a function to map over the morphism,

CspCASL does not use this functionality. -}

CASL_MapSen.mapTerm (error "CspCASL.Morphism.mapCASLTerm")

. cspCASLMorphism2caslMorphism

{- | Apply a signature morphism to a CASL FORMULA (for CspCASL only, i.e. a CASL

FORMULA that appears in CspCASL). -}

mapCASLFormula :: CspCASLMorphism -> FORMULA () -> FORMULA ()

mapCASLFormula =

{- The error here is not used. It is a function to map over the morphism,

CspCASL does not use this functionality. -}

CASL_MapSen.mapSen (error "CspCASL.Morphism.mapCASLFormula")

. cspCASLMorphism2caslMorphism

-- | Apply a signature morphism to a process name

mapProcessName :: CspCASLMorphism -> FQ_PROCESS_NAME -> FQ_PROCESS_NAME

mapProcessName mor pn = case pn of

FQ_PROCESS_NAME pn' procProfilePn' ->

let (m, procProfileM) =

mapProcess mor (pn', procProfilePn')

in FQ_PROCESS_NAME m procProfileM

_ -> error "unqualifed FQ_PROCESS_NAME"