SignCSP.hs revision f08f7774e4c47012f3c349205310750198cdc434
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederDescription : CspCASL signatures
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederCopyright : (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederMaintainer : M.Roggenbach@swansea.ac.uk
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : provisional
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : portable
44fb55f639914f4f531641f32dd4904f15c510a4Till Mossakowskisignatures for CSP-CASL
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder-- todo: implement isInclusion, computeExt
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski PROCESS(..), CommAlpha(..), CommType(..), TypedChanName(..))
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport CASL.AS_Basic_CASL (FORMULA, SORT)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport CASL.Sign (emptySign, Sign, extendedInfo, sortRel)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport CASL.Morphism (Morphism)
9e2e744c6b967c3f5f581acf01c13769b6769285Till Mossakowskiimport Common.Id (Id, SIMPLE_ID, mkSimpleId, nullRange)
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maederimport Common.Lib.Rel (predecessors)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport qualified Data.Map as Map
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport qualified Data.Set as Set
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | A process has zero or more parameter sorts, and a communication
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata ProcProfile = ProcProfile [SORT] CommAlpha
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski deriving (Eq, Show)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskitype ChanNameMap = Map.Map CHANNEL_NAME SORT
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskitype ProcNameMap = Map.Map PROCESS_NAME ProcProfile
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maedertype ProcVarMap = Map.Map SIMPLE_ID SORT
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maedertype ProcVarList = [(SIMPLE_ID, SORT)]
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski-- Close a communication alphabet under CASL subsort
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till MossakowskicloseCspCommAlpha :: CspCASLSign -> CommAlpha -> CommAlpha
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till MossakowskicloseCspCommAlpha sig = Set.unions . Set.toList . Set.map (closeOneCspComm sig)
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski-- Close one CommType under CASL subsort
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till MossakowskicloseOneCspComm :: CspCASLSign -> CommType -> CommAlpha
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill MossakowskicloseOneCspComm sig x = let
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski mkTypedChan c s = CommTypeChan $ TypedChanName c s
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski subsorts s' = Set.singleton s' `Set.union` predecessors (sortRel sig) s'
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski CommTypeSort s -> Set.map CommTypeSort (subsorts s)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski CommTypeChan (TypedChanName c s) -> Set.map CommTypeSort (subsorts s)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski `Set.union` Set.map (mkTypedChan c) (subsorts s)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski{- Will probably be useful, but doesn't appear to be right now.
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder-- Extract the sorts from a process alphabet
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaederprocAlphaSorts :: CommAlpha -> Set.Set SORT
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaederprocAlphaSorts a = stripMaybe $ Set.map justSort a
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski where justSort n = case n of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (CommTypeSort s) -> Just s
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- Extract the typed channel names from a process alphabet
0e51a998b1b213654c7a9eca451562041971f100Till MossakowskiprocAlphaChans :: CommAlpha -> Set.Set TypedChanName
0e51a998b1b213654c7a9eca451562041971f100Till MossakowskiprocAlphaChans a = stripMaybe $ Set.map justChan a
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski where justChan n = case n of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (CommTypeChan c) -> Just c
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder-- Given a set of Maybes, filter to keep only the Justs
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaederstripMaybe :: Ord a => Set.Set (Maybe a) -> Set.Set a
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaederstripMaybe x = Set.fromList $ Maybe.catMaybes $ Set.toList x
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder-- Close a set of sorts under a subsort relation
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedercspSubsortCloseSorts :: CspCASLSign -> Set.Set SORT -> Set.Set SORT
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedercspSubsortCloseSorts sig sorts =
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder where subsort_sets = Set.toList $ Set.map (cspSubsortPreds sig) sorts
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder-- | CSP process signature.
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maederdata CspSign = CspSign
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder { chans :: ChanNameMap
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder , procSet :: ProcNameMap
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder -- | Added for uniformity to the CASL static analysis. After
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder -- static analysis this is the empty list.
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder , ccSentences :: [Named CspCASLSen]
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder } deriving (Eq, Show)
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder-- | A CspCASL signature is a CASL signature with a CSP process
586af0e9490a14dd3075095692b584c652584875Till Mossakowski-- signature in the extendedInfo part.
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowskitype CspCASLSign = Sign () CspSign
797595aad6dfd626bc1c9df52616f1ac4235c669Till MossakowskiccSig2CASLSign :: CspCASLSign -> Sign () ()
797595aad6dfd626bc1c9df52616f1ac4235c669Till MossakowskiccSig2CASLSign sigma = sigma { extendedInfo = () }
797595aad6dfd626bc1c9df52616f1ac4235c669Till MossakowskiccSig2CspSign :: CspCASLSign -> CspSign
797595aad6dfd626bc1c9df52616f1ac4235c669Till MossakowskiccSig2CspSign sigma = extendedInfo sigma
933baca0720dae81434de384b32a93b47e754d09Christian Maeder-- | Empty CspCASL signature.
8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskiemptyCspCASLSign :: CspCASLSign
8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskiemptyCspCASLSign = emptySign emptyCspSign
586af0e9490a14dd3075095692b584c652584875Till Mossakowski-- | Empty CSP process signature.
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian MaederemptyCspSign :: CspSign
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiemptyCspSign = CspSign
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , ccSentences =[]
933baca0720dae81434de384b32a93b47e754d09Christian Maeder-- | Compute union of two CSP process signatures.
933baca0720dae81434de384b32a93b47e754d09Christian MaederaddCspProcSig :: CspSign -> CspSign -> CspSign
933baca0720dae81434de384b32a93b47e754d09Christian MaederaddCspProcSig a b =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski a { chans = chans a `Map.union` chans b
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , procSet = procSet a `Map.union` procSet b
586af0e9490a14dd3075095692b584c652584875Till Mossakowski-- | Compute difference of two CSP process signatures.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskidiffCspProcSig :: CspSign -> CspSign -> CspSign
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskidiffCspProcSig a b =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski a { chans = chans a `Map.difference` chans b
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , procSet = procSet a `Map.difference` procSet b
933baca0720dae81434de384b32a93b47e754d09Christian Maeder-- XXX looks incomplete!
933baca0720dae81434de384b32a93b47e754d09Christian MaederisInclusion :: CspSign -> CspSign -> Bool
933baca0720dae81434de384b32a93b47e754d09Christian MaederisInclusion _ _ = True
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder-- XXX morphisms between CSP process signatures?
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maederdata CspAddMorphism = CspAddMorphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski { channelMap :: Map.Map Id Id
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski , processMap :: Map.Map Id Id
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski } deriving (Eq, Show)
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian MaedercomposeIdMaps :: Map.Map Id Id -> Map.Map Id Id -> Map.Map Id Id
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskicomposeIdMaps m1 m2 = Map.foldWithKey (\ i j -> case Map.lookup j m2 of
8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski Nothing -> error "SignCsp.composeIdMaps"
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian MaedercomposeCspAddMorphism :: CspAddMorphism -> CspAddMorphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -> Result CspAddMorphism
ca8550c6d47234042130bdc10a152806ecbc9832Christian MaedercomposeCspAddMorphism m1 m2 = return emptyCspAddMorphism
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder { channelMap = composeIdMaps (channelMap m1) $ channelMap m2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , processMap = composeIdMaps (processMap m1) $ processMap m2 }
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiinverseCspAddMorphism :: CspAddMorphism -> Result CspAddMorphism
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian MaederinverseCspAddMorphism cm = do
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let chL = Map.toList $ channelMap cm
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski prL = Map.toList $ processMap cm
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski swap = map $ \ (a, b) -> (b, a)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski isInj l = length l == Set.size (Set.fromList $ map snd l)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski unless (isInj chL) $ fail "invertCspAddMorphism.channelMap"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski unless (isInj prL) $ fail "invertCspAddMorphism.processMap"
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder return emptyCspAddMorphism
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder { channelMap = Map.fromList $ swap chL
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , processMap = Map.fromList $ swap prL }
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maedertype CspMorphism = Morphism () CspSign CspAddMorphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiemptyCspAddMorphism :: CspAddMorphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiemptyCspAddMorphism = CspAddMorphism
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder { channelMap = Map.empty -- ???
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski-- dummy instances, need to be elaborated!
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowskiinstance Pretty CspSign where
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski pretty = text . show
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowskiinstance Pretty CspAddMorphism where
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski pretty = text . show
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski-- | A CspCASl senetence is either a CASL formula or a Procsses
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski-- equation. A process equation has on the LHS a process name, a
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski-- list of parameters which are qualified variables (which are
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- terms), a constituent( or is it permitted ?) communication alphabet and
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- finally on the RHS a fully qualified process.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata CspCASLSen = CASLSen (FORMULA ())
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski | ProcessEq PROCESS_NAME ProcVarList CommAlpha PROCESS
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder deriving (Show, Eq, Ord)
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maederinstance Pretty CspCASLSen where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- Not implemented yet - the pretty printing of the casl sentences
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder pretty(CASLSen _) = text "Pretty printing for CASLSen not implemented yet"
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder pretty(ProcessEq pn varList alpha proc) =
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder let varDoc = if (null varList)
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski else parens $ sepByCommas $ map pretty (map fst varList)
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder in pretty pn <+> varDoc <+> equals <+> pretty proc
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian MaederemptyCCSen :: CspCASLSen
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder let emptyProcName = mkSimpleId "empty"
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski emptyVarList = []
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder emptyAlphabet = Set.empty
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski emptyProc = Skip nullRange
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder in ProcessEq emptyProcName emptyVarList emptyAlphabet emptyProc
9d34a8049237647d0188ee2ec88db2dc45f1f848Till MossakowskiisCASLSen :: CspCASLSen -> Bool
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaederisCASLSen (CASLSen _) = True
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaederisCASLSen _ = False
0e51a998b1b213654c7a9eca451562041971f100Till MossakowskiisProcessEq :: CspCASLSen -> Bool
933baca0720dae81434de384b32a93b47e754d09Christian MaederisProcessEq (ProcessEq _ _ _ _) = True