SignCSP.hs revision afd6ed16928bbd774b6c6c5b3f440a917dd638a1
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{- |
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy GimblettModule : $Id$
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
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : M.Roggenbach@swansea.ac.uk
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : portable
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maedersignatures for CSP-CASL
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblett
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-}
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
fbb2d28086a1860850f661fbf4af531322bac405Christian Maeder-- todo: implement isInclusion, computeExt
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachmodule CspCASL.SignCSP where
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettimport qualified CASL.AS_Basic_CASL as AS_Basic_CASL
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettimport qualified CASL.Sign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettimport qualified CASL.Morphism
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettimport qualified Common.Doc as Doc
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettimport qualified Common.DocUtils as DocUtils
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettimport qualified Common.Id as Id
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | A CSP process signature contains information on channels and
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- processes.
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettdata CspProcSign = CspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett { chans :: Map.Map Id.Id AS_Basic_CASL.SORT
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett , procs :: Map.Map Id.Id (Maybe AS_Basic_CASL.SORT)
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett } deriving (Eq, Show)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | A CspCASL signature is a CASL signature with a CSP process
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- signature in the extendedInfo part.
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimbletttype CSPSign = CASL.Sign.Sign () CspProcSign
929190acb9f2b2f5857dce841c5a389710895515Andy Gimblett
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | Empty CspCASL signature.
929190acb9f2b2f5857dce841c5a389710895515Andy GimblettemptyCSPSign :: CSPSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettemptyCSPSign = CASL.Sign.emptySign emptyCspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | Empty CSP process signature.
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettemptyCspProcSign :: CspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettemptyCspProcSign = CspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett { chans = Map.empty
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett , procs = Map.empty
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett }
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | Compute difference between two CSP process signatures.
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettdiffCspProcSig :: CspProcSign -> CspProcSign -> CspProcSign
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettdiffCspProcSig a b =
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett a { chans = chans a `Map.difference` chans b
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett , procs = procs a `Map.difference` procs b
e99df192a380bfa91e3261c911751bb034c09a17Till Mossakowski }
e99df192a380bfa91e3261c911751bb034c09a17Till Mossakowski
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
eca4db63ed0bdbd93b62678feea6e3eb80aa47bbChristian Maeder }
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- XXX looks incomplete!
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettisInclusion :: CspProcSign -> CspProcSign -> Bool
1df33829303cbf924aa018ac5ce9a28e69c17d22Till MossakowskiisInclusion _ _ = True
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- XXX morphisms between CSP process signatures?
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederdata CSPAddMorphism = CSPAddMorphism
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett { channelMap :: Map.Map Id.Id Id.Id
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett , processMap :: Map.Map Id.Id Id.Id
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder } deriving (Eq, Show)
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimbletttype CSPMorphism = CASL.Morphism.Morphism () CspProcSign CSPAddMorphism
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederemptyCSPAddMorphism :: CSPAddMorphism
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederemptyCSPAddMorphism = CSPAddMorphism
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder { channelMap = Map.empty -- ???
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett , processMap = Map.empty
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett }
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski-- dummy instances, need to be elaborated!
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettinstance DocUtils.Pretty CspProcSign where
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett pretty = Doc.text . show
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettinstance DocUtils.Pretty CSPAddMorphism where
afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett pretty = Doc.text . show