7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder{-# LANGUAGE MultiParamTypeClasses #-}

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder{- |

81d182b21020b815887e9057959228546cf61b6bChristian MaederModule : $Header$

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaederDescription : Symbols and signature morphisms for the CspCASL logic

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

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder

7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederMaintainer : csliam@swansea.ac.uk

2ac1742771a267119f1d839054b5e45d0a468085Christian MaederStability : provisional

7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederPortability : portable

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederSymbols and signature morphisms for the CspCASL logic

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder-}

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maedermodule CspCASL.Morphism

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder ( CspCASLMorphism

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , CspAddMorphism (..)

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder , ChanMap

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , ProcessMap

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder , mapProcProfile

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , cspSubsigInclusion

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , emptyCspAddMorphism

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder , cspAddMorphismUnion

8197d0be8b81692f311ad5ca34e125e2cf9eecb8Christian Maeder , cspMorphismToCspSymbMap

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder , inducedCspSign

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder , mapSen

d42a01c4eb6892fe23ca9eff107bb29f4a229480Christian Maeder ) where

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederimport CspCASL.AS_CspCASL_Process

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maederimport CspCASL.SignCSP

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederimport CspCASL.Symbol

2ac1742771a267119f1d839054b5e45d0a468085Christian Maederimport qualified CspCASL.LocalTop as LT

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport CASL.AS_Basic_CASL (FORMULA, TERM, SORT, SORT_ITEM (..))

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maederimport CASL.Sign as CASL_Sign

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederimport CASL.Morphism as CASL_Morphism

2ac1742771a267119f1d839054b5e45d0a468085Christian Maederimport qualified CASL.MapSentence as CASL_MapSen

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

2ac1742771a267119f1d839054b5e45d0a468085Christian Maederimport Common.Doc

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Common.DocUtils

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederimport Common.Id

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maederimport Common.Result

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederimport Common.Utils (composeMap, isSingleton)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport qualified Common.Lib.MapSet as MapSet

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maederimport qualified Common.Lib.Rel as Rel

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder

2ac1742771a267119f1d839054b5e45d0a468085Christian Maederimport qualified Data.Map as Map

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederimport qualified Data.Set as Set

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder-- Morphisms

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder

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

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

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

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

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maedercommunications alphabet of the profile. This is because the argument sorts of

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

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

2ac1742771a267119f1d839054b5e45d0a468085Christian Maedercommunications alphabet of the source profile must be downward closed with

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

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

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

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maedertype ProcessMap =

d48085f765fca838c1d972d2123601997174583dChristian Maeder Map.Map (PROCESS_NAME, ProcProfile) (PROCESS_NAME, CommAlpha)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maedertype ChanMap = Map.Map (CHANNEL_NAME, SORT) CHANNEL_NAME

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder

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

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maederdata CspAddMorphism = CspAddMorphism

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

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

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

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

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder { channelMap :: ChanMap

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder , processMap :: ProcessMap

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder } deriving (Eq, Ord, Show)

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder-- | The empty CspAddMorphism.

b1bd8688a1ce545444792a307412711c2c61df5fChristian MaederemptyCspAddMorphism :: CspAddMorphism

b1bd8688a1ce545444792a307412711c2c61df5fChristian MaederemptyCspAddMorphism = CspAddMorphism

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

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

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder then the application is the identity function. Thus empty maps

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder are used to form the empty morphism. -}

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder { channelMap = Map.empty

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder , processMap = Map.empty

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder }

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder

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

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maederaccording to CspCASL.SignCSP.isCspCASLSubSig) compute the inclusion morphism. -}

2ac1742771a267119f1d839054b5e45d0a468085Christian MaedercspSubsigInclusion :: CspCASLSign -> CspCASLSign -> Result CspCASLMorphism

2ac1742771a267119f1d839054b5e45d0a468085Christian MaedercspSubsigInclusion sign = checkResultMorphismIsLegal .

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder CASL_Morphism.sigInclusion emptyCspAddMorphism sign

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

7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maederwill embed channel names and process names properly. -}

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaedercheckResultMorphismIsLegal :: Result CspCASLMorphism -> Result CspCASLMorphism

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaedercheckResultMorphismIsLegal rmor = do

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder mor <- rmor

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder legalMorphismExtension mor

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return mor

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder-- | lookup a typed channel

840b2a6f37ec58f3281da16fafbc4121462c856aChristian MaedermapChan :: Sort_map -> ChanMap -> (CHANNEL_NAME, SORT) -> (CHANNEL_NAME, SORT)

5ba383b1607c20c57e14324e72cee2c789436d5fChristian MaedermapChan sm cm p@(c, s) = (Map.findWithDefault c p cm, mapSort sm s)

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder-- | Apply a signature morphism to a channel name

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

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder -> (CHANNEL_NAME, SORT)

2ac1742771a267119f1d839054b5e45d0a468085Christian MaedermapChannel mor = mapChan (sort_map mor) $ channelMap $ extended_map mor

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedermapCommTypeAux :: Sort_map -> ChanMap -> CommType -> CommType

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaedermapCommTypeAux sm cm ct = case ct of

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder CommTypeSort s -> CommTypeSort $ mapSort sm s

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

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder CommTypeChan $ TypedChanName d t

55ea7f4cb33abac6a8d539741e457cf686d1f26cChristian Maeder

2118d66b6aa3c90458925019c9b2fb986e2b2aabChristian Maeder-- | Apply a signature morphism to a CommType

2118d66b6aa3c90458925019c9b2fb986e2b2aabChristian MaedermapCommType :: Morphism f CspSign CspAddMorphism -> CommType -> CommType

2118d66b6aa3c90458925019c9b2fb986e2b2aabChristian MaedermapCommType mor = mapCommTypeAux (sort_map mor) (channelMap $ extended_map mor)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedermapCommAlphaAux :: Sort_map -> ChanMap -> CommAlpha -> CommAlpha

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedermapCommAlphaAux sm = Set.map . mapCommTypeAux sm

d48085f765fca838c1d972d2123601997174583dChristian Maeder

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder-- | Apply a signature morphism to a CommAlpha

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaedermapCommAlpha :: Morphism f CspSign CspAddMorphism -> CommAlpha -> CommAlpha

d48085f765fca838c1d972d2123601997174583dChristian MaedermapCommAlpha = Set.map . mapCommType

d48085f765fca838c1d972d2123601997174583dChristian Maeder

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaedermapProcProfile :: Sort_map -> ChanMap -> ProcProfile -> ProcProfile

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedermapProcProfile sm cm (ProcProfile sl cs) =

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

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedermapProcId :: Sort_map -> ChanMap -> ProcessMap

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder -> (PROCESS_NAME, ProcProfile) -> (PROCESS_NAME, ProcProfile)

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedermapProcId sm cm pm (i, p) = let

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

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

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Nothing -> (i, n)

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Just (j, alpha) -> (j, ProcProfile args alpha)

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder

5ba383b1607c20c57e14324e72cee2c789436d5fChristian MaedermapProcess :: Morphism f CspSign CspAddMorphism

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

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedermapProcess mor = let em = extended_map mor in

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder mapProcId (sort_map mor) (channelMap em) $ processMap em

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder-- | Compose two CspAddMorphisms

2ac1742771a267119f1d839054b5e45d0a468085Christian MaedercomposeCspAddMorphism :: Morphism f CspSign CspAddMorphism

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder -> Morphism f CspSign CspAddMorphism -> Result CspAddMorphism

d93bbbec133697cc79d59f9d7cc8e97458976c15Christian MaedercomposeCspAddMorphism m1 m2 = let

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder sMap1 = sort_map m1

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder sMap2 = sort_map m2

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder sMap = composeMap (MapSet.setToMap $ sortSet src) sMap1 sMap2

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder src = msource m1

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder cSrc = extendedInfo src

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder cMap = MapSet.foldWithKey ( \ c s ->

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder let p = (c, s)

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder ni = fst $ mapChannel m2 $ mapChannel m1 p

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

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Map.empty $ chans cSrc

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

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder let pp = (p, pr)

8dcc70ff9afdfe4aff258676718677a4d7076fd0Christian Maeder (ni, ProcProfile _ na) =

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder mapProcess m2 $ mapProcess m1 pp

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder oa = mapCommAlphaAux sMap cMap a

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder in if p == ni && oa == na then id else

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Map.insert pp (ni, na))

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Map.empty $ procSet cSrc

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder in return emptyCspAddMorphism

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder { channelMap = cMap

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder , processMap = pMap }

d48085f765fca838c1d972d2123601997174583dChristian Maeder

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

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaederCspAddMorphism. -}

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maedertype CspCASLMorphism = CASL_Morphism.Morphism CspSen CspSign CspAddMorphism

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder

d93bbbec133697cc79d59f9d7cc8e97458976c15Christian 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 -}

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedercheckReflCondition :: Morphism f CspSign CspAddMorphism -> Result ()

2ac1742771a267119f1d839054b5e45d0a468085Christian MaedercheckReflCondition mor =

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder let sig = msource mor

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder sig' = mtarget mor

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder sm = sort_map mor

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder rel = sortRel sig

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder rel' = sortRel sig'

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder allPairs = LT.cartesian $ sortSet sig

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

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

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder mapSort sm s1 == mapSort sm s2

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder then Rel.path s1 s2 rel || s1 == s2

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder else True

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder in if Set.null failures

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder then return ()

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder else let produceDiag (s1, s2) =

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder let x = (mapSort sm s1)

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder y = (mapSort sm s2)

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder in Diag Error

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder ("CSP-CASL Signature Morphism Refl Property Violated:\n'"

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder ++ showDoc (Symbol x $ SubsortAsItemType y)

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder "' in target but not in source\n'"

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

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder nullRange

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder allDiags = map produceDiag $ Set.toList failures

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

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder

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

2ac1742771a267119f1d839054b5e45d0a468085Christian Maederi.e.,

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

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

2ac1742771a267119f1d839054b5e45d0a468085Christian MaedercheckWNECondition :: Morphism f CspSign CspAddMorphism -> Result ()

2ac1742771a267119f1d839054b5e45d0a468085Christian MaedercheckWNECondition mor =

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder let sig = msource mor

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder sig' = mtarget mor

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder sm = sort_map mor

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder rel' = sortRel sig'

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder supers s signature = Set.insert s $ supersortsOf s signature

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder allPairsInSource = LT.cartesian $ sortSet sig

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder commonSuperSortsInTarget s1 s2 = Set.intersection

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder (supers (mapSort sm s1) sig')

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder (supers (mapSort sm s2) sig')

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

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

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder createCandidateTripples (s1, s2) =

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

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder allCandidateTripples =

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Set.unions $ Set.toList $ Set.map createCandidateTripples

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder allPairsInSource

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder testCandidate (s1, s2, u') =

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

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

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder in or $ Set.toList $ Set.map test possibleWitnesses

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder failures = Set.filter (not . testCandidate) allCandidateTripples

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder in if Set.null failures

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder then return ()

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder else let produceDiag (s1, s2, u') =

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder let x = (mapSort sm s1)

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder y = (mapSort sm s2)

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder in Diag Error

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder ("CSP-CASL Signature Morphism Weak Non-Extension Property "

27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder ++ "Violated:\n'"

27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder ++ showDoc

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

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder "'\nbut no common supersort for\n'"

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder ++ showDoc

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

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder nullRange

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder allDiags = map produceDiag $ Set.toList failures

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder in Result allDiags Nothing -- failure with error messages

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder-- | unite morphisms

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedercspAddMorphismUnion :: CspCASLMorphism -> CspCASLMorphism

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder -> Result CspAddMorphism

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedercspAddMorphismUnion mor1 mor2 = let

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder s1 = extendedInfo $ msource mor1

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder s2 = extendedInfo $ msource mor2

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder m1 = extended_map mor1

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder m2 = extended_map mor2

d48085f765fca838c1d972d2123601997174583dChristian Maeder chan1 = channelMap m1

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder chan2 = channelMap m2

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

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

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

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder uc = MapSet.union uc1 uc2

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder proc1 = processMap m1

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder proc2 = processMap m2

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder delProc (n, p) m = MapSet.delete n p m

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

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

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder up = MapSet.union up1 up2

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

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

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

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder case Map.lookup isc m of

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

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

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder (Diag Error

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ("incompatible mapping of channel " ++ shows i ":"

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ++ showDoc s " to " ++ shows j " and "

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

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

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

840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder (pds, pMap) =

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

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder case Map.lookup isc m of

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

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

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder (Diag Error

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

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

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

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

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

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder (MapSet.toList up))

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder in if null pds then return emptyCspAddMorphism

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder { channelMap = cMap

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder , processMap = pMap }

9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder else Result pds Nothing

9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder

9fb0db7f56cbb44c3df49552c04afc881267b84eChristian MaedertoCspSymbMap :: Bool -> Morphism f CspSign CspAddMorphism

9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder -> Map.Map CspSymbol CspSymbol

2ac1742771a267119f1d839054b5e45d0a468085Christian MaedertoCspSymbMap b mor = let

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder src = extendedInfo $ msource mor

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder chanSymMap = MapSet.foldWithKey

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder ( \ 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 = do

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"