SignCSP.hs revision 2650e8a56cc2381719bd2390fdf82402e0c696d8
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiModule : $Header$
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiDescription : CspCASL signatures
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiCopyright : (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiLicense : GPLv2 or higher, see LICENSE.txt
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiMaintainer : M.Roggenbach@swansea.ac.uk
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiStability : provisional
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiPortability : portable
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskisignatures for CSP-CASL
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiimport qualified CspCASL.LocalTop as LocalTop
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiimport Common.Lib.Rel (Rel, predecessors)
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescuimport qualified Data.Map as Map
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescuimport qualified Data.Set as Set
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescutype ChanNameMap = Map.Map CHANNEL_NAME (Set.Set SORT)
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescutype ProcNameMap = Map.Map PROCESS_NAME (Set.Set ProcProfile)
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescutype ProcVarMap = Map.Map SIMPLE_ID SORT
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Langetype ProcVarList = [(SIMPLE_ID, SORT)]
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu-- | Add a process name and its profile to a process name map. exist.
c57bde4abc9029546fa396c4eccacf969e126b96Mihai CodescuaddProcNameToProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu -> ProcNameMap
c57bde4abc9029546fa396c4eccacf969e126b96Mihai CodescuaddProcNameToProcNameMap name profile =
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz Map.insertWith Set.union name (Set.singleton profile)
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz-- | Test if a simple process name with a profile is in the process name map.
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst SchulzisNameInProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap -> Bool
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst SchulzisNameInProcNameMap name profile =
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz Set.member profile . Map.findWithDefault Set.empty name
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz{- | Given a simple process name and a required number of parameters, find a
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulzunqiue profile with that many parameters if possible. If this is not possible
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange(i.e., name does not exist, or no profile with the required number of
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulzarguments or not unique profile for the required number of arguments), then
356f33e31a1cf98a878f069e9e2e1cbea4a06e81Ewaryst Schulzthe functions returns a failed result with a helpful error message. failure. -}
356f33e31a1cf98a878f069e9e2e1cbea4a06e81Ewaryst SchulzgetUniqueProfileInProcNameMap :: PROCESS_NAME -> Int -> ProcNameMap ->
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz Result ProcProfile
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst SchulzgetUniqueProfileInProcNameMap name numParams pm =
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz let profiles = Map.findWithDefault Set.empty name pm
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz isMatch (ProcProfile argSorts _) =
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange length argSorts == numParams
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu matchedProfiles = Set.filter isMatch profiles
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu in case Set.toList matchedProfiles of
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu [] -> mkError ("Process name not in signature with "
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu ++ show numParams ++ " parameters:") name
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu [p] -> return p
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu _ -> mkError ("Process name not unique in signature with "
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu ++ show numParams ++ " parameters:") name
de55550f7d117195f127481d18ec2d5e8d2317ffMihai CodescucloseProcs :: Rel SORT -> CspSign -> CspSign
de55550f7d117195f127481d18ec2d5e8d2317ffMihai CodescucloseProcs r s = s { procSet = closeProcNameMapSortRel r $ procSet s }
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu{- | Close a proc name map under a sub-sort relation. Assumes all the proc
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescuprofile's comms are in the sub sort relation and simply makes the comms
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescudownward closed under the sub-sort relation. -}
de55550f7d117195f127481d18ec2d5e8d2317ffMihai CodescucloseProcNameMapSortRel :: Rel SORT -> ProcNameMap -> ProcNameMap
de55550f7d117195f127481d18ec2d5e8d2317ffMihai CodescucloseProcNameMapSortRel sig =
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu Map.map (Set.map $ closeProcProfileSortRel sig)
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu{- | Close a profile under a sub-sort relation. Assumes the proc profile's
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescucomms are in the sub sort relation and simply makes the comms downward closed
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescuunder the sub-sort relation. -}
de55550f7d117195f127481d18ec2d5e8d2317ffMihai CodescucloseProcProfileSortRel :: Rel SORT -> ProcProfile -> ProcProfile
de55550f7d117195f127481d18ec2d5e8d2317ffMihai CodescucloseProcProfileSortRel sig (ProcProfile argSorts comms) =
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu ProcProfile argSorts (closeCspCommAlpha sig comms)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- Close a communication alphabet under CASL subsort
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskicloseCspCommAlpha :: Rel SORT -> CommAlpha -> CommAlpha
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskicloseCspCommAlpha sr =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Set.unions . Set.toList . Set.map (closeOneCspComm sr)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- Close one CommType under CASL subsort
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskicloseOneCspComm :: Rel SORT -> CommType -> CommAlpha
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskicloseOneCspComm sr x = let
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski mkTypedChan c s = CommTypeChan $ TypedChanName c s
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski subsorts s' = Set.insert s' $ predecessors sr s'
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski CommTypeSort s ->
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Set.map CommTypeSort (subsorts s)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski CommTypeChan (TypedChanName c s) ->
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Set.map CommTypeSort (subsorts s)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski `Set.union` Set.map (mkTypedChan c) (subsorts s)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | CSP process signature.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskidata CspSign = CspSign
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski { chans :: ChanNameMap
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski , procSet :: ProcNameMap
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski } deriving (Eq, Ord, Show)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | plain union
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskicspSignUnion :: CspSign -> CspSign -> CspSign
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskicspSignUnion sign1 sign2 = emptyCspSign
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski { chans = addMapSet (chans sign1) (chans sign2)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski , procSet = addMapSet (procSet sign1) (procSet sign2) }
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski{- | A CspCASL signature is a CASL signature with a CSP process
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskisignature in the extendedInfo part. -}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitype CspCASLSign = Sign CspSen CspSign
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiccSig2CASLSign :: CspCASLSign -> CASLSign
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiccSig2CASLSign sigma = sigma { extendedInfo = (), sentences = [] }
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | Projection from CspCASL signature to Csp signature
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiccSig2CspSign :: CspCASLSign -> CspSign
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiccSig2CspSign = extendedInfo
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | Empty CspCASL signature.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiemptyCspCASLSign :: CspCASLSign
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiemptyCspCASLSign = emptySign emptyCspSign
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | Empty CSP process signature.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiemptyCspSign :: CspSign
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiemptyCspSign = CspSign
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | Compute union of two CSP CASL signatures.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiunionCspCASLSign :: CspCASLSign -> CspCASLSign -> Result CspCASLSign
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiunionCspCASLSign s1 s2 = do
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski -- Compute the unioned data signature ignoring the csp signatures
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski let newDataSig = addSig (\ _ _ -> emptyCspSign) s1 s2
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski -- Check that the new data signature has local top elements
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski rel = sortRel newDataSig
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski -- Compute the unioned csp signature with respect to the new data signature
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski newCspSign = unionCspSign rel (extendedInfo s1) (extendedInfo s2)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski {- Only error will be added if there are any probelms. If there are no
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski problems no errors will be added and hets will continue as normal. -}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski appendDiags diags'
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski -- put both the new data signature and the csp signature back together
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski return $ newDataSig {extendedInfo = newCspSign}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski{- | Compute union of two CSP signatures assuming the new already computed data
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiunionCspSign :: Rel SORT -> CspSign -> CspSign -> CspSign
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiunionCspSign sr a b = cspSignUnion (closeProcs sr a) (closeProcs sr b)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | Compute difference of two CSP process signatures.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskidiffCspSig :: CspSign -> CspSign -> CspSign
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskidiffCspSig a b = emptyCspSign
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski { chans = diffMapSet (chans a) $ chans b
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski , procSet = diffMapSet (procSet a) $ procSet b
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | Is one CspCASL Signature a sub signature of another
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiisCspCASLSubSig :: CspCASLSign -> CspCASLSign -> Bool
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiisCspCASLSubSig =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski -- Normal casl subsignature and our extended csp part
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski isSubSig isCspSubSign
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski {- Also the sorts and sub-sort rels should be equal. If they are not then we
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski cannot just add the processes in as their profiles need to be donward closed
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski under the new sort-rels, but we do not check this here. -}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski{- | Is one Csp Signature a sub signature of another assuming the same data
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskisignature for now. -}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiisCspSubSign :: CspSign -> CspSign -> Bool
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiisCspSubSign a b =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski isSubMapSet (chans a) (chans b) &&
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski -- Check for each profile that the set of names are included.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski isSubMapSet (procSet a) (procSet b)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | Pretty printing for CspCASL signatures
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiinstance Pretty CspSign where
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski pretty = printCspSign
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskimapSetToList :: (Ord a, Ord b) => Map.Map a (Set.Set b) -> [(a, b)]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskimapSetToList = concatMap (\ (c, ts) -> map (\ t -> (c, t)) $ Set.toList ts)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiprintCspSign :: CspSign -> Doc
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiprintCspSign sigma =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski case mapSetToList $ chans sigma of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski s -> keyword (channelS ++ appendS s) <+> printChanList s
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski $+$ case mapSetToList $ procSet sigma of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski ps -> keyword processS <+> printProcList ps
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | Pretty printing for channels
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiprintChanList :: [(CHANNEL_NAME, SORT)] -> Doc
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiprintChanList l = let
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski gl = groupBy (\ (_, s1) (_, s2) -> s1 == s2) $ sortBy (comparing snd) l
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski printChan cl = case cl of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski [] -> empty -- should not happen
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (_, s) : _ -> fsep [ppWithCommas (map fst cl), colon <+> pretty s]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in sepBySemis $ map printChan gl
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | Pretty printing for processes
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiprintProcList :: [(PROCESS_NAME, ProcProfile)] -> Doc
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiprintProcList = sepBySemis . map
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (\ (procName, procProfile) -> pretty procName <+> pretty procProfile)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski{- | FQProcVarList should only contain fully qualified CASL variables which are
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiTERMs i.e. constructed via the TERM constructor Qual_var. -}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitype FQProcVarList = [TERM ()]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski{- | A CspCASl senetence is either a CASL formula or a Procsses equation. A
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiprocess equation has on the LHS a process name, a list of parameters which
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiare qualified variables (which are terms), a constituent( or is it permitted
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski?) communication alphabet and finally on the RHS a fully qualified process. -}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskidata CspSen = ProcessEq FQ_PROCESS_NAME FQProcVarList CommAlpha PROCESS
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski deriving (Show, Eq, Ord)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitype CspCASLSen = FORMULA CspSen
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiinstance GetRange CspSen
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiinstance Pretty CspSen where
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski pretty (ProcessEq pn varList _commAlpha proc) =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski let varDoc = if null varList
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski else parens $ ppWithCommas varList
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in fsep [pretty pn, varDoc, equals <+> pretty proc]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiinstance FormExtension CspSen where
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski prefixExt (ProcessEq pn _ _ _) = case pn of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski PROCESS_NAME _ -> (keyword processS <+>)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski FQ_PROCESS_NAME {} -> id
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiinstance TermExtension CspSen
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiinstance TermParser CspSen
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiisProcessEq :: CspCASLSen -> Bool
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiisProcessEq f = case f of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski ExtFORMULA _ -> True