SignCSP.hs revision d04c328b10f17ec78001a94d694f7188ebd8c03c
e071fb22ea9923a2a4ff41184d80ca46b55ee932Till MossakowskiDescription : CspCASL signatures
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachCopyright : (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : M.Roggenbach@swansea.ac.uk
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maedersignatures for CSP-CASL
fbb2d28086a1860850f661fbf4af531322bac405Christian Maeder-- todo: implement isInclusion, computeExt
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettimport qualified Data.Set as S
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettimport CASL.Sign (emptySign, Sign, sortRel)
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport CASL.Morphism (Morphism)
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettimport qualified Common.Doc as Doc
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettimport qualified Common.DocUtils as DocUtils
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettimport Common.Id (Id, SIMPLE_ID)
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettimport Common.Lib.Rel (predecessors)
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblettimport CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME)
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- | A process has zero or more parameter sorts, and a communication
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblettdata ProcProfile = ProcProfile [SORT] CommAlpha
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett deriving (Eq, Show)
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett-- | A process communication alphabet consists of a set of sort names
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- and typed channel names.
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettdata TypedChanName = TypedChanName CHANNEL_NAME SORT
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett deriving (Eq, Ord, Show)
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettdata CommType = CommTypeSort SORT
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett | CommTypeChan TypedChanName
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett deriving (Eq, Ord)
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblettinstance Show CommType where
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett show (CommTypeSort s) = show s
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett show (CommTypeChan (TypedChanName c s)) = show (c, s)
9f6d67c9b0e2661e7967b435f17a27687929144fAndy Gimbletttype CommAlpha = S.Set CommType
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimbletttype ChanNameMap = Map.Map CHANNEL_NAME SORT
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimbletttype ProcNameMap = Map.Map PROCESS_NAME ProcProfile
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimbletttype ProcVarMap = Map.Map SIMPLE_ID SORT
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Close a communication alphabet under CASL subsort
9f6d67c9b0e2661e7967b435f17a27687929144fAndy GimblettcloseCspCommAlpha :: CspSign -> CommAlpha -> CommAlpha
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettcloseCspCommAlpha sig alpha =
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett S.unions $ S.toList $ S.map (closeOneCspComm sig) alpha
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Close one CommType under CASL subsort
9f6d67c9b0e2661e7967b435f17a27687929144fAndy GimblettcloseOneCspComm :: CspSign -> CommType -> CommAlpha
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettcloseOneCspComm sig x =
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (CommTypeSort s) -> S.map CommTypeSort (subsorts s)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (CommTypeChan (TypedChanName c s)) -> (S.map CommTypeSort (subsorts s))
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (S.map (mkTypedChan c) (subsorts s))
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett where mkTypedChan c s = CommTypeChan $ TypedChanName c s
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett subsorts s' = (S.singleton s') `S.union` predecessors (sortRel sig) s'
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett{- Will probably be useful, but doesn't appear to be right now.
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Extract the sorts from a process alphabet
9f6d67c9b0e2661e7967b435f17a27687929144fAndy GimblettprocAlphaSorts :: CommAlpha -> S.Set SORT
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettprocAlphaSorts a = stripMaybe $ S.map justSort a
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett where justSort n = case n of
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett (CommTypeSort s) -> Just s
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Extract the typed channel names from a process alphabet
9f6d67c9b0e2661e7967b435f17a27687929144fAndy GimblettprocAlphaChans :: CommAlpha -> S.Set TypedChanName
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettprocAlphaChans a = stripMaybe $ S.map justChan a
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett where justChan n = case n of
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett (CommTypeChan c) -> Just c
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Given a set of Maybes, filter to keep only the Justs
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettstripMaybe :: Ord a => S.Set (Maybe a) -> S.Set a
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettstripMaybe x = S.fromList $ Maybe.catMaybes $ S.toList x
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Close a set of sorts under a subsort relation
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettcspSubsortCloseSorts :: CspSign -> S.Set SORT -> S.Set SORT
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettcspSubsortCloseSorts sig sorts =
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett where subsort_sets = S.toList $ S.map (cspSubsortPreds sig) sorts
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- | CSP process signature.
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettdata CspProcSign = CspProcSign
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett { chans :: ChanNameMap
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , procSet :: ProcNameMap
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett } deriving (Eq, Show)
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | A CspCASL signature is a CASL signature with a CSP process
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- signature in the extendedInfo part.
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimbletttype CspSign = Sign () CspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | Empty CspCASL signature.
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettemptyCspSign :: CspSign
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettemptyCspSign = emptySign emptyCspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | Empty CSP process signature.
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettemptyCspProcSign :: CspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettemptyCspProcSign = CspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | Compute union of two CSP process signatures.
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettaddCspProcSig :: CspProcSign -> CspProcSign -> CspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettaddCspProcSig a b =
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett a { chans = chans a `Map.union` chans b
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , procSet = procSet a `Map.union` procSet b
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- XXX looks incomplete!
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettisInclusion :: CspProcSign -> CspProcSign -> Bool
1df33829303cbf924aa018ac5ce9a28e69c17d22Till MossakowskiisInclusion _ _ = True
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- XXX morphisms between CSP process signatures?
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblettdata CspAddMorphism = CspAddMorphism
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett { channelMap :: Map.Map Id Id
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett , processMap :: Map.Map Id Id
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder } deriving (Eq, Show)
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimbletttype CspMorphism = Morphism () CspProcSign CspAddMorphism
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettemptyCspAddMorphism :: CspAddMorphism
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettemptyCspAddMorphism = CspAddMorphism
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder { channelMap = Map.empty -- ???
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett , processMap = Map.empty
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski-- dummy instances, need to be elaborated!
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettinstance DocUtils.Pretty CspProcSign where
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett pretty = Doc.text . show
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblettinstance DocUtils.Pretty CspAddMorphism where
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett pretty = Doc.text . show