SignCSP.hs revision d3c9318c22fcf44d9135a3b2c64f880b9a785bab
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
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyimport CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME,
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly PROCESS(..), CommAlpha, CommType(..), TypedChanName(..))
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyimport CASL.AS_Basic_CASL (CASLFORMULA, SORT, TERM)
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reillyimport CASL.Sign (CASLSign, emptySign, Sign, extendedInfo, sortRel)
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettimport Common.Lib.Rel (predecessors)
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maederimport qualified Data.Map as Map
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maederimport qualified Data.Set as Set
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- | A process has zero or more parameter sorts, and a communication
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblettdata ProcProfile = ProcProfile [SORT] CommAlpha
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder deriving (Eq, Ord, Show)
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimbletttype ChanNameMap = Map.Map CHANNEL_NAME SORT
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimbletttype ProcNameMap = Map.Map PROCESS_NAME ProcProfile
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimbletttype ProcVarMap = Map.Map SIMPLE_ID SORT
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillytype ProcVarList = [(SIMPLE_ID, SORT)]
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Close a communication alphabet under CASL subsort
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettcloseCspCommAlpha :: CspCASLSign -> CommAlpha -> CommAlpha
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycloseCspCommAlpha sig =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Set.unions . Set.toList . Set.map (closeOneCspComm sig)
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Close one CommType under CASL subsort
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettcloseOneCspComm :: CspCASLSign -> CommType -> CommAlpha
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaedercloseOneCspComm sig x = let
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder mkTypedChan c s = CommTypeChan $ TypedChanName c s
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly subsorts s' =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Set.singleton s' `Set.union` predecessors (sortRel sig) s'
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly CommTypeSort s ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Set.map CommTypeSort (subsorts s)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly CommTypeChan (TypedChanName c s) ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Set.map CommTypeSort (subsorts s)
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder `Set.union` Set.map (mkTypedChan c) (subsorts s)
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett{- Will probably be useful, but doesn't appear to be right now.
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Extract the sorts from a process alphabet
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaederprocAlphaSorts :: CommAlpha -> Set.Set SORT
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaederprocAlphaSorts a = stripMaybe $ Set.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
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaederprocAlphaChans :: CommAlpha -> Set.Set TypedChanName
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaederprocAlphaChans a = stripMaybe $ Set.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
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaederstripMaybe :: Ord a => Set.Set (Maybe a) -> Set.Set a
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaederstripMaybe x = Set.fromList $ Maybe.catMaybes $ Set.toList x
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- Close a set of sorts under a subsort relation
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaedercspSubsortCloseSorts :: CspCASLSign -> Set.Set SORT -> Set.Set SORT
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettcspSubsortCloseSorts sig sorts =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly where subsort_sets =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Set.toList $ Set.map (cspSubsortPreds sig) sorts
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- | CSP process signature.
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblettdata CspSign = CspSign
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett { chans :: ChanNameMap
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , procSet :: ProcNameMap
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -- | Added for uniformity to the CASL static analysis. After
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -- static analysis this is the empty list.
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly , ccSentences :: [Named CspCASLSen]
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder } deriving (Eq, Ord, Show)
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | A CspCASL signature is a CASL signature with a CSP process
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- signature in the extendedInfo part.
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimbletttype CspCASLSign = Sign () CspSign
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'ReillyccSig2CASLSign :: CspCASLSign -> CASLSign
cdf1545bdcd39a9d53c00761ffa42e7b1174b91eLiam O'ReillyccSig2CASLSign sigma = sigma { extendedInfo = () }
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Projection from CspCASL signature to Csp signature
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyccSig2CspSign :: CspCASLSign -> CspSign
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyccSig2CspSign sigma = extendedInfo sigma
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | Empty CspCASL signature.
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettemptyCspCASLSign :: CspCASLSign
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettemptyCspCASLSign = emptySign emptyCspSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | Empty CSP process signature.
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettemptyCspSign :: CspSign
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettemptyCspSign = CspSign
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly , ccSentences =[]
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | Compute union of two CSP process signatures.
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettaddCspProcSig :: CspSign -> CspSign -> CspSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettaddCspProcSig a b =
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett a { chans = chans a `Map.union` chans b
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , procSet = procSet a `Map.union` procSet b
f08f7774e4c47012f3c349205310750198cdc434Liam O'Reilly-- | Compute difference of two CSP process signatures.
f08f7774e4c47012f3c349205310750198cdc434Liam O'ReillydiffCspProcSig :: CspSign -> CspSign -> CspSign
f08f7774e4c47012f3c349205310750198cdc434Liam O'ReillydiffCspProcSig a b =
f08f7774e4c47012f3c349205310750198cdc434Liam O'Reilly a { chans = chans a `Map.difference` chans b
f08f7774e4c47012f3c349205310750198cdc434Liam O'Reilly , procSet = procSet a `Map.difference` procSet b
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- XXX looks incomplete!
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettisInclusion :: CspSign -> CspSign -> Bool
1df33829303cbf924aa018ac5ce9a28e69c17d22Till MossakowskiisInclusion _ _ = True
eaf34cf96fbfcdcce7f3bdb322c4ea7ebd1fd220Liam O'Reilly-- | Pretty printing for CspCASL signatures
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyinstance Pretty CspSign where
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly pretty = printCspSign
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillyprintCspSign :: CspSign -> Doc
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillyprintCspSign sigma =
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly chan_part $+$ proc_part
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly where chan_part =
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly case (Map.size $ chans sigma) of
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly 1 -> (keyword channelS) <+> printChanNameMap (chans sigma)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly _ -> (keyword channelsS) <+> printChanNameMap (chans sigma)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly proc_part = (keyword processS) <+> printProcNameMap (procSet sigma)
eaf34cf96fbfcdcce7f3bdb322c4ea7ebd1fd220Liam O'Reilly-- | Pretty printing for channel name maps
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyinstance Pretty ChanNameMap where
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly pretty = printChanNameMap
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillyprintChanNameMap :: ChanNameMap -> Doc
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillyprintChanNameMap chanMap =
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly vcat $ punctuate semi $ map printChan $ Map.toList chanMap
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly where printChan (chanName, sort) =
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly (pretty chanName) <+> colon <+> (pretty sort)
eaf34cf96fbfcdcce7f3bdb322c4ea7ebd1fd220Liam O'Reilly-- | Pretty printing for process name maps
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyinstance Pretty ProcNameMap where
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly pretty = printProcNameMap
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillyprintProcNameMap :: ProcNameMap -> Doc
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillyprintProcNameMap procNameMap =
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly vcat $ punctuate semi $ map printProcName $ Map.toList procNameMap
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly where printProcName (procName, procProfile) =
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly (pretty procName) <+> pretty procProfile
eaf34cf96fbfcdcce7f3bdb322c4ea7ebd1fd220Liam O'Reilly-- | Pretty printing for process profiles
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyinstance Pretty ProcProfile where
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly pretty = printProcProfile
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillyprintProcProfile :: ProcProfile -> Doc
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillyprintProcProfile (ProcProfile sorts commAlpha) =
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly printArgs sorts <+> colon <+> (ppWithCommas $ Set.toList commAlpha)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly where printArgs [] = empty
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly printArgs args = parens $ ppWithCommas args
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | FQProcVarList should only contain fully qualified CASL variables
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- which are TERMs i.e. constructed via the TERM constructor
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillytype FQProcVarList = [TERM ()]
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly-- | A CspCASl senetence is either a CASL formula or a Procsses
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly-- equation. A process equation has on the LHS a process name, a
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly-- list of parameters which are qualified variables (which are
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- terms), a constituent( or is it permitted ?) communication
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- alphabet and finally on the RHS a fully qualified process.
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillydata CspCASLSen
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly = CASLSen (CASLFORMULA)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly | ProcessEq PROCESS_NAME FQProcVarList CommAlpha PROCESS
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly deriving (Show, Eq, Ord)
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maederinstance GetRange CspCASLSen
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyinstance Pretty CspCASLSen where
b3449e90e6fd4696f423b39e295d1786e122a505Liam O'Reilly pretty(CASLSen f) = pretty f
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly pretty(ProcessEq pn varList commAlpha proc) =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly let varDoc = if (null varList)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly else parens $ sepByCommas $ map pretty varList
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly commAlphaDoc = brackets ((text "CommAlpha:") <+>
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly (text $ show commAlpha))
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly in pretty pn <+> varDoc <+> commAlphaDoc <+>
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly equals <+> pretty proc
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Empty CspCASL sentence
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyemptyCCSen :: CspCASLSen
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly let emptyProcName = mkSimpleId "empty"
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly emptyVarList = []
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly emptyAlphabet = Set.empty
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly emptyProc = Skip nullRange
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly in ProcessEq emptyProcName emptyVarList emptyAlphabet emptyProc -- BUG - this is incorrect
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Test if a CspCASL sentence is a CASL sentence
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyisCASLSen :: CspCASLSen -> Bool
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyisCASLSen (CASLSen _) = True
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyisCASLSen _ = False
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Test if a CspCASL sentence is a Process Equation.
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyisProcessEq :: CspCASLSen -> Bool
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyisProcessEq (ProcessEq _ _ _ _) = True
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyisProcessEq _ = False