SignCSP.hs revision de16f2cd7bef567000c39b40e6f7b0b263e49d12
967e5f3c25249c779575864692935627004d3f9eChristian MaederModule : $Header$
650bafe7709533bc5f82bb9daf8fa06f431cd963Christian MaederDescription : CspCASL signatures
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
967e5f3c25249c779575864692935627004d3f9eChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
967e5f3c25249c779575864692935627004d3f9eChristian MaederMaintainer : M.Roggenbach@swansea.ac.uk
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaederStability : provisional
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : portable
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maedersignatures for CSP-CASL
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maederimport qualified CspCASL.LocalTop as LocalTop
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederimport Common.Lib.Rel (Rel, predecessors)
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederimport qualified Data.Map as Map
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederimport qualified Data.Set as Set
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maedertype ChanNameMap = Map.Map CHANNEL_NAME (Set.Set SORT)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maedertype ProcNameMap = Map.Map PROCESS_NAME (Set.Set ProcProfile)
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maedertype ProcVarMap = Map.Map SIMPLE_ID SORT
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maedertype ProcVarList = [(SIMPLE_ID, SORT)]
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder-- | Add a process name and its profile to a process name map. exist.
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian MaederaddProcNameToProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder -> ProcNameMap
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian MaederaddProcNameToProcNameMap name profile =
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder Map.insertWith Set.union name (Set.singleton profile)
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder-- | Test if a simple process name with a profile is in the process name map.
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaederisNameInProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap -> Bool
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederisNameInProcNameMap name profile =
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder Set.member profile . Map.findWithDefault Set.empty name
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder{- | Given a simple process name and a required number of parameters, find a
d5c415f6373274fed04d83b9322891f3b82e9c26Christian Maederunqiue profile with that many parameters if possible. If this is not possible
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder(i.e., name does not exist, or no profile with the required number of
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederarguments or not unique profile for the required number of arguments), then
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederthe functions returns a failed result with a helpful error message. failure. -}
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedergetUniqueProfileInProcNameMap :: PROCESS_NAME -> Int -> ProcNameMap ->
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder Result ProcProfile
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaedergetUniqueProfileInProcNameMap name numParams pm =
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder let profiles = Map.findWithDefault Set.empty name pm
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder isMatch (ProcProfile argSorts _) =
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder length argSorts == numParams
d48085f765fca838c1d972d2123601997174583dChristian Maeder matchedProfiles = Set.filter isMatch profiles
d48085f765fca838c1d972d2123601997174583dChristian Maeder in case Set.toList matchedProfiles of
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder [] -> mkError ("Process name not in signature with "
d48085f765fca838c1d972d2123601997174583dChristian Maeder ++ show numParams ++ " parameters:") name
d48085f765fca838c1d972d2123601997174583dChristian Maeder [p] -> return p
d48085f765fca838c1d972d2123601997174583dChristian Maeder _ -> mkError ("Process name not unique in signature with "
d48085f765fca838c1d972d2123601997174583dChristian Maeder ++ show numParams ++ " parameters:") name
717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedercloseProcs :: Rel SORT -> CspSign -> CspSign
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaedercloseProcs r s = s { procSet = closeProcNameMapSortRel r $ procSet s }
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder{- | Close a proc name map under a sub-sort relation. Assumes all the proc
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maederprofile's comms are in the sub sort relation and simply makes the comms
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederdownward closed under the sub-sort relation. -}
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaedercloseProcNameMapSortRel :: Rel SORT -> ProcNameMap -> ProcNameMap
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedercloseProcNameMapSortRel sig =
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder Map.map (Set.map $ closeProcProfileSortRel sig)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder{- | Close a profile under a sub-sort relation. Assumes the proc profile's
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maedercomms are in the sub sort relation and simply makes the comms downward closed
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederunder the sub-sort relation. -}
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedercloseProcProfileSortRel :: Rel SORT -> ProcProfile -> ProcProfile
c66a930944d9e4d64a8f0f38c748fdad0831ff87Christian MaedercloseProcProfileSortRel sig (ProcProfile argSorts comms) =
c66a930944d9e4d64a8f0f38c748fdad0831ff87Christian Maeder ProcProfile argSorts (closeCspCommAlpha sig comms)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-- Close a communication alphabet under CASL subsort
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedercloseCspCommAlpha :: Rel SORT -> CommAlpha -> CommAlpha
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedercloseCspCommAlpha sr =
a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maeder Set.unions . Set.toList . Set.map (closeOneCspComm sr)
967e5f3c25249c779575864692935627004d3f9eChristian Maeder-- Close one CommType under CASL subsort
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedercloseOneCspComm :: Rel SORT -> CommType -> CommAlpha
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedercloseOneCspComm sr x = let
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder mkTypedChan c s = CommTypeChan $ TypedChanName c s
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder subsorts s' = Set.insert s' $ predecessors sr s'
20e16bdd7481741d0b6b14f952aea42ee7a65efbChristian Maeder CommTypeSort s ->
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder Set.map CommTypeSort (subsorts s)
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder CommTypeChan (TypedChanName c s) ->
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder Set.map CommTypeSort (subsorts s)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder `Set.union` Set.map (mkTypedChan c) (subsorts s)
a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maeder-- | CSP process signature.
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maederdata CspSign = CspSign
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder { chans :: ChanNameMap
650bafe7709533bc5f82bb9daf8fa06f431cd963Christian Maeder , procSet :: ProcNameMap
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder } deriving (Eq, Ord, Show)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-- | plain union
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedercspSignUnion :: CspSign -> CspSign -> CspSign
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaedercspSignUnion sign1 sign2 = emptyCspSign
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder { chans = addMapSet (chans sign1) (chans sign2)
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski , procSet = addMapSet (procSet sign1) (procSet sign2) }
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder{- | A CspCASL signature is a CASL signature with a CSP process
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maedersignature in the extendedInfo part. -}
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maedertype CspCASLSign = Sign CspSen CspSign
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskiccSig2CASLSign :: CspCASLSign -> CASLSign
842eedc62639561781b6c33533d1949693ef6cc5Christian MaederccSig2CASLSign sigma = sigma { extendedInfo = (), sentences = [] }
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder-- | Projection from CspCASL signature to Csp signature
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian MaederccSig2CspSign :: CspCASLSign -> CspSign
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian MaederccSig2CspSign = extendedInfo
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski-- | Empty CspCASL signature.
967e5f3c25249c779575864692935627004d3f9eChristian MaederemptyCspCASLSign :: CspCASLSign
967e5f3c25249c779575864692935627004d3f9eChristian MaederemptyCspCASLSign = emptySign emptyCspSign
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder-- | Empty CSP process signature.
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederemptyCspSign :: CspSign
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederemptyCspSign = CspSign
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-- | Compute union of two CSP CASL signatures.
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederunionCspCASLSign :: CspCASLSign -> CspCASLSign -> Result CspCASLSign
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederunionCspCASLSign s1 s2 = do
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder -- Compute the unioned data signature ignoring the csp signatures
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder let newDataSig = addSig (\ _ _ -> emptyCspSign) s1 s2
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder -- Check that the new data signature has local top elements
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder rel = sortRel newDataSig
967e5f3c25249c779575864692935627004d3f9eChristian Maeder -- Compute the unioned csp signature with respect to the new data signature
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder newCspSign = unionCspSign rel (extendedInfo s1) (extendedInfo s2)
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder {- Only error will be added if there are any probelms. If there are no
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder problems no errors will be added and hets will continue as normal. -}
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder appendDiags diags'
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder -- put both the new data signature and the csp signature back together
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder return $ newDataSig {extendedInfo = newCspSign}
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder{- | Compute union of two CSP signatures assuming the new already computed data
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederunionCspSign :: Rel SORT -> CspSign -> CspSign -> CspSign
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederunionCspSign sr a b = cspSignUnion (closeProcs sr a) (closeProcs sr b)
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder-- | Compute difference of two CSP process signatures.
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederdiffCspSig :: CspSign -> CspSign -> CspSign
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederdiffCspSig a b = emptyCspSign
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder { chans = diffMapSet (chans a) $ chans b
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder , procSet = diffMapSet (procSet a) $ procSet b
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder-- | Is one CspCASL Signature a sub signature of another
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederisCspCASLSubSig :: CspCASLSign -> CspCASLSign -> Bool
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederisCspCASLSubSig =
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder -- Normal casl subsignature and our extended csp part
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder isSubSig isCspSubSign
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder {- Also the sorts and sub-sort rels should be equal. If they are not then we
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder cannot just add the processes in as their profiles need to be donward closed
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder under the new sort-rels, but we do not check this here. -}
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder{- | Is one Csp Signature a sub signature of another assuming the same data
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maedersignature for now. -}
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederisCspSubSign :: CspSign -> CspSign -> Bool
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederisCspSubSign a b =
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder isSubMapSet (chans a) (chans b) &&
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder -- Check for each profile that the set of names are included.
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder isSubMapSet (procSet a) (procSet b)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-- | Pretty printing for CspCASL signatures
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederinstance Pretty CspSign where
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder pretty = printCspSign
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaedermapSetToList :: (Ord a, Ord b) => Map.Map a (Set.Set b) -> [(a, b)]
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedermapSetToList = concatMap (\ (c, ts) -> map (\ t -> (c, t)) $ Set.toList ts)
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederprintCspSign :: CspSign -> Doc
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederprintCspSign sigma =
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder case mapSetToList $ chans sigma of
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder s -> keyword (channelS ++ appendS s) <+> printChanList s
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder $+$ case mapSetToList $ procSet sigma of
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder ps -> keyword processS <+> printProcList ps
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder-- | Pretty printing for channels
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian MaederprintChanList :: [(CHANNEL_NAME, SORT)] -> Doc
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian MaederprintChanList l = let
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder gl = groupBy (\ (_, s1) (_, s2) -> s1 == s2) $ sortBy (comparing snd) l
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder printChan cl = case cl of
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder [] -> empty -- should not happen
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder (_, s) : _ -> fsep [ppWithCommas (map fst cl), colon <+> pretty s]
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder in sepBySemis $ map printChan gl
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder-- | Pretty printing for processes
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaederprintProcList :: [(PROCESS_NAME, ProcProfile)] -> Doc
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederprintProcList = sepBySemis . map
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder (\ (procName, procProfile) -> pretty procName <+> pretty procProfile)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-- * overload relations
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaederrelatedSorts :: CspCASLSign -> SORT -> SORT -> Bool
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaederrelatedSorts sig s1 s2 = haveCommonSupersorts True sig s1 s2
TERMs i.e. constructed via the TERM constructor Qual_var. -}