SignCSP.hs revision 33bdce26495121cdbce30331ef90a1969126a840
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder{- |
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederModule : $Id$
3a6c7a7ff823616f56cd3d205fc44664a683effdChristian MaederDescription : CspCASL signatures
73dfcef93ee2ba07fedf4f3c74bace31853d1b9fChristian MaederCopyright : (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederMaintainer : M.Roggenbach@swansea.ac.uk
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederStability : provisional
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederPortability : portable
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskisignatures for CSP-CASL
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-}
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- todo: implement isInclusion, computeExt
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedermodule CspCASL.SignCSP where
85ebda7270c6883b503d3bde4757033c09c25644Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME,
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz PROCESS(..), CommAlpha, CommType(..), TypedChanName(..))
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport CspCASL.AS_CspCASL ()
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport CspCASL.CspCASL_Keywords
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulzimport CspCASL.Print_CspCASL ()
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulzimport CASL.AS_Basic_CASL (CASLFORMULA, SORT, TERM)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport CASL.Sign (CASLSign, emptySign, Sign, extendedInfo, sortRel)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport Common.AS_Annotation (Named)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport Common.Doc
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maederimport Common.DocUtils
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederimport Common.Id (SIMPLE_ID, mkSimpleId, nullRange)
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maederimport Common.Lib.Rel (predecessors)
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maederimport qualified Data.Map as Map
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maederimport qualified Data.Set as Set
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- | A process has zero or more parameter sorts, and a communication
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder-- alphabet.
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederdata ProcProfile = ProcProfile [SORT] CommAlpha
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving (Eq, Ord, Show)
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maedertype ChanNameMap = Map.Map CHANNEL_NAME SORT
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedertype ProcNameMap = Map.Map PROCESS_NAME ProcProfile
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedertype ProcVarMap = Map.Map SIMPLE_ID SORT
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maedertype ProcVarList = [(SIMPLE_ID, SORT)]
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski-- Close a communication alphabet under CASL subsort
6abfd7000f15635fd29746bd841b4c36819e552bTill MossakowskicloseCspCommAlpha :: CspCASLSign -> CommAlpha -> CommAlpha
6abfd7000f15635fd29746bd841b4c36819e552bTill MossakowskicloseCspCommAlpha sig =
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski Set.unions . Set.toList . Set.map (closeOneCspComm sig)
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski-- Close one CommType under CASL subsort
6abfd7000f15635fd29746bd841b4c36819e552bTill MossakowskicloseOneCspComm :: CspCASLSign -> CommType -> CommAlpha
6abfd7000f15635fd29746bd841b4c36819e552bTill MossakowskicloseOneCspComm sig x = let
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder mkTypedChan c s = CommTypeChan $ TypedChanName c s
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder subsorts s' =
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Set.singleton s' `Set.union` predecessors (sortRel sig) s'
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder in case x of
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder CommTypeSort s ->
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski Set.map CommTypeSort (subsorts s)
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder CommTypeChan (TypedChanName c s) ->
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Set.map CommTypeSort (subsorts s)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder `Set.union` Set.map (mkTypedChan c) (subsorts s)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder{- Will probably be useful, but doesn't appear to be right now.
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- Extract the sorts from a process alphabet
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederprocAlphaSorts :: CommAlpha -> Set.Set SORT
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederprocAlphaSorts a = stripMaybe $ Set.map justSort a
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder where justSort n = case n of
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder (CommTypeSort s) -> Just s
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder _ -> Nothing
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- Extract the typed channel names from a process alphabet
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederprocAlphaChans :: CommAlpha -> Set.Set TypedChanName
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederprocAlphaChans a = stripMaybe $ Set.map justChan a
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder where justChan n = case n of
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (CommTypeChan c) -> Just c
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder _ -> Nothing
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder-- Given a set of Maybes, filter to keep only the Justs
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederstripMaybe :: Ord a => Set.Set (Maybe a) -> Set.Set a
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederstripMaybe x = Set.fromList $ Maybe.catMaybes $ Set.toList x
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- Close a set of sorts under a subsort relation
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercspSubsortCloseSorts :: CspCASLSign -> Set.Set SORT -> Set.Set SORT
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercspSubsortCloseSorts sig sorts =
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Set.unions subsort_sets
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder where subsort_sets =
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski Set.toList $ Set.map (cspSubsortPreds sig) sorts
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski-}
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski-- | CSP process signature.
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowskidata CspSign = CspSign
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski { chans :: ChanNameMap
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski , procSet :: ProcNameMap
b20cc520e698253354303b7bf3bc17f84240b213Klaus Luettich -- | Added for uniformity to the CASL static analysis. After
da955132262baab309a50fdffe228c9efe68251dCui Jian -- static analysis this is the empty list.
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder , ccSentences :: [Named CspCASLSen]
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder } deriving (Eq, Ord, Show)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- | A CspCASL signature is a CASL signature with a CSP process
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- signature in the extendedInfo part.
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedertype CspCASLSign = Sign () CspSign
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaederccSig2CASLSign :: CspCASLSign -> CASLSign
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederccSig2CASLSign sigma = sigma { extendedInfo = () }
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- | Projection from CspCASL signature to Csp signature
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederccSig2CspSign :: CspCASLSign -> CspSign
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederccSig2CspSign sigma = extendedInfo sigma
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- | Empty CspCASL signature.
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst SchulzemptyCspCASLSign :: CspCASLSign
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst SchulzemptyCspCASLSign = emptySign emptyCspSign
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz-- | Empty CSP process signature.
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst SchulzemptyCspSign :: CspSign
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst SchulzemptyCspSign = CspSign
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz { chans = Map.empty
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz , procSet = Map.empty
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz , ccSentences =[]
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder }
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- | Compute union of two CSP process signatures.
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederaddCspProcSig :: CspSign -> CspSign -> CspSign
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederaddCspProcSig a b =
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder a { chans = chans a `Map.union` chans b
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder , procSet = procSet a `Map.union` procSet b
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder }
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- | Compute difference of two CSP process signatures.
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederdiffCspProcSig :: CspSign -> CspSign -> CspSign
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederdiffCspProcSig a b =
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder a { chans = chans a `Map.difference` chans b
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder , procSet = procSet a `Map.difference` procSet b
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder }
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- XXX looks incomplete!
07baaf27fc0029203075ed916999006dcc619ef0Christian MaederisInclusion :: CspSign -> CspSign -> Bool
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederisInclusion _ _ = True
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- | Pretty printing for CspCASL signatures
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederinstance Pretty CspSign where
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder pretty = printCspSign
3a6decfd748f532d5cb03fbcb7a42fa37b0faab3Christian Maeder
07baaf27fc0029203075ed916999006dcc619ef0Christian MaederprintCspSign :: CspSign -> Doc
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederprintCspSign sigma =
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder chan_part $+$ proc_part
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder where chan_part =
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder case (Map.size $ chans sigma) of
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder 0 -> empty
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder 1 -> (keyword channelS) <+> printChanNameMap (chans sigma)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder _ -> (keyword channelsS) <+> printChanNameMap (chans sigma)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder proc_part = (keyword processS) <+> printProcNameMap (procSet sigma)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder-- | Pretty printing for channel name maps
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederinstance Pretty ChanNameMap where
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder pretty = printChanNameMap
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederprintChanNameMap :: ChanNameMap -> Doc
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaederprintChanNameMap chanMap =
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder vcat $ punctuate semi $ map printChan $ Map.toList chanMap
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder where printChan (chanName, sort) =
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski (pretty chanName) <+> colon <+> (pretty sort)
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski-- | Pretty printing for process name maps
999f839e42d594e4ae288208fec398626837c41cTill Mossakowskiinstance Pretty ProcNameMap where
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski pretty = printProcNameMap
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian MaederprintProcNameMap :: ProcNameMap -> Doc
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian MaederprintProcNameMap procNameMap =
ad69cb3627839ed3d33f13d71c81378b65a24b35Till Mossakowski vcat $ punctuate semi $ map printProcName $ Map.toList procNameMap
ad69cb3627839ed3d33f13d71c81378b65a24b35Till Mossakowski where printProcName (procName, procProfile) =
(pretty procName) <+> pretty procProfile
-- | Pretty printing for process profiles
instance Pretty ProcProfile where
pretty = printProcProfile
printProcProfile :: ProcProfile -> Doc
printProcProfile (ProcProfile sorts commAlpha) =
printArgs sorts <+> colon <+> (ppWithCommas $ Set.toList commAlpha)
where printArgs [] = empty
printArgs args = parens $ ppWithCommas args
-- Sentences
-- | FQProcVarList should only contain fully qualified CASL variables
-- which are TERMs i.e. constructed via the TERM constructor
-- Qual_var.
type FQProcVarList = [TERM ()]
-- | A CspCASl senetence is either a CASL formula or a Procsses
-- equation. A process equation has on the LHS a process name, a
-- list of parameters which are qualified variables (which are
-- terms), a constituent( or is it permitted ?) communication
-- alphabet and finally on the RHS a fully qualified process.
data CspCASLSen
= CASLSen (CASLFORMULA)
| ProcessEq PROCESS_NAME FQProcVarList CommAlpha PROCESS
deriving (Show, Eq, Ord)
instance Pretty CspCASLSen where
pretty(CASLSen f) = pretty f
pretty(ProcessEq pn varList commAlpha proc) =
let varDoc = if (null varList)
then empty
else parens $ sepByCommas $ map pretty varList
commAlphaDoc = brackets ((text "CommAlpha:") <+>
(text $ show commAlpha))
in pretty pn <+> varDoc <+> commAlphaDoc <+>
equals <+> pretty proc
-- | Empty CspCASL sentence
emptyCCSen :: CspCASLSen
emptyCCSen =
let emptyProcName = mkSimpleId "empty"
emptyVarList = []
emptyAlphabet = Set.empty
emptyProc = Skip nullRange
in ProcessEq emptyProcName emptyVarList emptyAlphabet emptyProc -- BUG - this is incorrect
-- | Test if a CspCASL sentence is a CASL sentence
isCASLSen :: CspCASLSen -> Bool
isCASLSen (CASLSen _) = True
isCASLSen _ = False
-- | Test if a CspCASL sentence is a Process Equation.
isProcessEq :: CspCASLSen -> Bool
isProcessEq (ProcessEq _ _ _ _) = True
isProcessEq _ = False