SignCSP.hs revision 06dd4e7c29f33f6122a910719e3bd9062256e397
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
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettimport qualified Data.Set as Set
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblettimport CASL.AS_Basic_CASL (SORT, VAR)
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport CASL.Sign (emptySign, Sign)
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport CASL.Morphism (Morphism)
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettimport qualified Common.Doc as Doc
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettimport qualified Common.DocUtils as DocUtils
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblettimport CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME)
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- | A process has zero or more parameter sorts, and a communication
b22c258cca179a5ffe777b64b32e10687c5f6b2cAndy Gimblettdata ProcProfile = ProcProfile
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett { procArgs :: [SORT]
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett , procAlphabet :: ProcAlpha
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett } deriving (Eq, Show)
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett-- | A process communication alphabet consists of a set of sort names
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett-- and a set of channel names.
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettdata ProcAlpha = ProcAlpha
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett { procAlphaSorts :: Set.Set SORT
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett , procAlphaChannels :: Set.Set CHANNEL_NAME
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett } deriving (Eq, Show)
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimbletttype ChanNameMap = Map.Map CHANNEL_NAME SORT
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimbletttype ProcNameMap = Map.Map PROCESS_NAME ProcProfile
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimbletttype ProcVarMap = Map.Map VAR SORT
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- | CSP process signature.
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettdata CspProcSign = CspProcSign
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett { chans :: ChanNameMap
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett , procs :: ProcNameMap
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett } deriving (Eq, Show)
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | A CspCASL signature is a CASL signature with a CSP process
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- signature in the extendedInfo part.
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimbletttype CspSign = Sign () CspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | Empty CspCASL signature.
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettemptyCspSign :: CspSign
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettemptyCspSign = emptySign emptyCspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | Empty CSP process signature.
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettemptyCspProcSign :: CspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettemptyCspProcSign = CspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | Compute union of two CSP process signatures.
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettaddCspProcSig :: CspProcSign -> CspProcSign -> CspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettaddCspProcSig a b =
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett a { chans = chans a `Map.union` chans b
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett , procs = procs a `Map.union` procs b
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- XXX looks incomplete!
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettisInclusion :: CspProcSign -> CspProcSign -> Bool
1df33829303cbf924aa018ac5ce9a28e69c17d22Till MossakowskiisInclusion _ _ = True
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- XXX morphisms between CSP process signatures?
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblettdata CspAddMorphism = CspAddMorphism
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett { channelMap :: Map.Map Id Id
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett , processMap :: Map.Map Id Id
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder } deriving (Eq, Show)
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimbletttype CspMorphism = Morphism () CspProcSign CspAddMorphism
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettemptyCspAddMorphism :: CspAddMorphism
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettemptyCspAddMorphism = CspAddMorphism
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder { channelMap = Map.empty -- ???
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett , processMap = Map.empty
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski-- dummy instances, need to be elaborated!
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettinstance DocUtils.Pretty CspProcSign where
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett pretty = Doc.text . show
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblettinstance DocUtils.Pretty CspAddMorphism where
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett pretty = Doc.text . show