4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{-# LANGUAGE TypeSynonymInstances #-}

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{- |

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederModule : $Id$

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederDescription : CspCASL signatures

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederCopyright : (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederMaintainer : M.Roggenbach@swansea.ac.uk

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederStability : provisional

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederPortability : portable

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedersignatures for CSP-CASL

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-}

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedermodule CspCASL.SignCSP where

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME,

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder PROCESS (..), CommAlpha, CommType (..), TypedChanName (..))

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport CspCASL.AS_CspCASL ()

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport CspCASL.CspCASL_Keywords

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport CspCASL.Print_CspCASL ()

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport CASL.AS_Basic_CASL (CASLFORMULA, SORT, TERM)

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport CASL.Sign (CASLSign, emptySign, Sign, extendedInfo, sortRel)

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Common.AS_Annotation (Named)

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Common.Doc

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Common.DocUtils

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Common.Id

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Common.Lib.Rel (predecessors)

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport qualified Data.Map as Map

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport qualified Data.Set as Set

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | A process has zero or more parameter sorts, and a communication

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- alphabet.

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederdata ProcProfile = ProcProfile [SORT] CommAlpha

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder deriving (Eq, Ord, Show)

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedertype ChanNameMap = Map.Map CHANNEL_NAME SORT

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedertype ProcNameMap = Map.Map PROCESS_NAME ProcProfile

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedertype ProcVarMap = Map.Map SIMPLE_ID SORT

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedertype ProcVarList = [(SIMPLE_ID, SORT)]

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- Close a communication alphabet under CASL subsort

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedercloseCspCommAlpha :: CspCASLSign -> CommAlpha -> CommAlpha

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedercloseCspCommAlpha sig =

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Set.unions . Set.toList . Set.map (closeOneCspComm sig)

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- Close one CommType under CASL subsort

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedercloseOneCspComm :: CspCASLSign -> CommType -> CommAlpha

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedercloseOneCspComm sig x = let

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder mkTypedChan c s = CommTypeChan $ TypedChanName c s

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder subsorts s' =

fd28ce71068bc46a4e1bba587a978206959c62abChristian Maeder Set.singleton s' `Set.union` predecessors (sortRel sig) s'

fd28ce71068bc46a4e1bba587a978206959c62abChristian Maeder in case x of

fd28ce71068bc46a4e1bba587a978206959c62abChristian Maeder CommTypeSort s ->

fd28ce71068bc46a4e1bba587a978206959c62abChristian Maeder Set.map CommTypeSort (subsorts s)

fd28ce71068bc46a4e1bba587a978206959c62abChristian Maeder CommTypeChan (TypedChanName c s) ->

fd28ce71068bc46a4e1bba587a978206959c62abChristian Maeder Set.map CommTypeSort (subsorts s)

ec676ed8bdc0f0a1d52793db1d75eb0c8d6f0f05Christian Maeder `Set.union` Set.map (mkTypedChan c) (subsorts s)

ec676ed8bdc0f0a1d52793db1d75eb0c8d6f0f05Christian Maeder

ec676ed8bdc0f0a1d52793db1d75eb0c8d6f0f05Christian Maeder{- Will probably be useful, but doesn't appear to be right now.

ec676ed8bdc0f0a1d52793db1d75eb0c8d6f0f05Christian Maeder

ec676ed8bdc0f0a1d52793db1d75eb0c8d6f0f05Christian Maeder-- Extract the sorts from a process alphabet

procAlphaSorts :: CommAlpha -> Set.Set SORT

procAlphaSorts a = stripMaybe $ Set.map justSort a

where justSort n = case n of

(CommTypeSort s) -> Just s

_ -> Nothing

-- Extract the typed channel names from a process alphabet

procAlphaChans :: CommAlpha -> Set.Set TypedChanName

procAlphaChans a = stripMaybe $ Set.map justChan a

where justChan n = case n of

(CommTypeChan c) -> Just c

_ -> Nothing

-- Given a set of Maybes, filter to keep only the Justs

stripMaybe :: Ord a => Set.Set (Maybe a) -> Set.Set a

stripMaybe x = Set.fromList $ Maybe.catMaybes $ Set.toList x

-- Close a set of sorts under a subsort relation

cspSubsortCloseSorts :: CspCASLSign -> Set.Set SORT -> Set.Set SORT

cspSubsortCloseSorts sig sorts =

Set.unions subsort_sets

where subsort_sets =

Set.toList $ Set.map (cspSubsortPreds sig) sorts

-}

-- | CSP process signature.

data CspSign = CspSign

{ chans :: ChanNameMap

, procSet :: ProcNameMap

-- | Added for uniformity to the CASL static analysis. After

-- static analysis this is the empty list.

, ccSentences :: [Named CspCASLSen]

} deriving (Eq, Ord, Show)

-- | I dont know if this is implemented correctly. Always prefers sign1 if there

-- are clashes in chans or procSet. BUG?

cspSignUnion :: CspSign -> CspSign -> CspSign

cspSignUnion sign1 sign2 =

CspSign { chans = Map.union (chans sign1) (chans sign2)

, procSet = Map.union (procSet sign1) (procSet sign2)

, ccSentences = ccSentences sign1 ++ ccSentences sign2

}

-- | A CspCASL signature is a CASL signature with a CSP process

-- signature in the extendedInfo part.

type CspCASLSign = Sign () CspSign

ccSig2CASLSign :: CspCASLSign -> CASLSign

ccSig2CASLSign sigma = sigma { extendedInfo = () }

-- | Projection from CspCASL signature to Csp signature

ccSig2CspSign :: CspCASLSign -> CspSign

ccSig2CspSign = extendedInfo

-- | Empty CspCASL signature.

emptyCspCASLSign :: CspCASLSign

emptyCspCASLSign = emptySign emptyCspSign

-- | Empty CSP process signature.

emptyCspSign :: CspSign

emptyCspSign = CspSign

{ chans = Map.empty

, procSet = Map.empty

, ccSentences = []

}

-- | Compute union of two CSP process signatures.

addCspProcSig :: CspSign -> CspSign -> CspSign

addCspProcSig a b = emptyCspSign

{ chans = chans a `Map.union` chans b

, procSet = procSet a `Map.union` procSet b

}

-- | Compute difference of two CSP process signatures.

diffCspProcSig :: CspSign -> CspSign -> CspSign

diffCspProcSig a b = emptyCspSign

{ chans = chans a `Map.difference` chans b

, procSet = procSet a `Map.difference` procSet b

}

-- | Is one Csp Signature a sub signature of another

isCspSubSign :: CspSign -> CspSign -> Bool

isCspSubSign a b =

chans a `Map.isSubmapOf` chans b &&

procSet a `Map.isSubmapOf` procSet b

-- | Pretty printing for CspCASL signatures

instance Pretty CspSign where

pretty = printCspSign

printCspSign :: CspSign -> Doc

printCspSign sigma =

chan_part $+$ proc_part

where chan_part =

case Map.size $ chans sigma of

0 -> empty

s -> keyword (if s > 1 then channelsS else channelS)

<+> printChanNameMap (chans sigma)

proc_part = keyword processS <+>

printProcNameMap (procSet sigma)

-- | Pretty printing for channel name maps

instance Pretty ChanNameMap where

pretty = printChanNameMap

printChanNameMap :: ChanNameMap -> Doc

printChanNameMap chanMap =

vcat $ punctuate semi $ map printChan $ Map.toList chanMap

where printChan (chanName, sort) =

pretty chanName <+> colon <+> pretty sort

-- | Pretty printing for process name maps

instance Pretty ProcNameMap where

pretty = printProcNameMap

printProcNameMap :: ProcNameMap -> Doc

printProcNameMap procNameMap =

vcat $ punctuate semi $ map printProcName $ Map.toList procNameMap

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 GetRange CspCASLSen

instance Pretty CspCASLSen where

pretty (CASLSen f) = pretty f

pretty (ProcessEq pn varList _commAlpha proc) =

let varDoc = if null varList

then empty

else parens $ ppWithCommas varList

in pretty pn <+> varDoc <+> equals <+> pretty proc

-- | Empty CspCASL sentence

emptyCCSen :: CspCASLSen

emptyCCSen =

let emptyProcName = mkSimpleId "empty"

emptyVarList = []

emptyAlphabet = Set.empty

emptyProc = Skip nullRange

-- BUG - this is incorrect

in ProcessEq emptyProcName emptyVarList emptyAlphabet emptyProc

-- | 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