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

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport CASL.AS_Basic_CASL (SORT)

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

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport Common.Id (Id)

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblettimport CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME)

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- | A process has zero or more parameter sorts, and a communication

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- sort.

b22c258cca179a5ffe777b64b32e10687c5f6b2cAndy Gimblettdata ProcProfile = ProcProfile

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett { procArgs :: [SORT]

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett , procSort :: SORT

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett } deriving (Eq, Show)

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimbletttype ChanNameMap = Map.Map CHANNEL_NAME SORT

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- | CSP process signature.

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettdata CspProcSign = CspProcSign

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett { chans :: Map.Map CHANNEL_NAME SORT

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett , procs :: Map.Map PROCESS_NAME ProcProfile

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.

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimbletttype CspSign = Sign () CspProcSign

929190acb9f2b2f5857dce841c5a389710895515Andy Gimblett

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | Empty CspCASL signature.

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettemptyCspSign :: CspSign

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettemptyCspSign = 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 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

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblettdata CspAddMorphism = CspAddMorphism

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett { channelMap :: Map.Map Id Id

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett , processMap :: Map.Map Id Id

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder } deriving (Eq, Show)

b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimbletttype CspMorphism = Morphism () CspProcSign CspAddMorphism

b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettemptyCspAddMorphism :: CspAddMorphism

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettemptyCspAddMorphism = 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

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblettinstance DocUtils.Pretty CspAddMorphism where

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett pretty = Doc.text . show