acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder{-# LANGUAGE TypeSynonymInstances #-}

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder{- |

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederModule : $Id$

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederDescription : CspCASL signatures

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

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederMaintainer : M.Roggenbach@swansea.ac.uk

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederStability : provisional

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederPortability : portable

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedersignatures for CSP-CASL

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-}

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedermodule CspCASL.SignCSP where

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport CASL.AS_Basic_CASL

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport CASL.Sign

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport CASL.ToDoc

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport CspCASL.AS_CspCASL_Process

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport CspCASL.AS_CspCASL ()

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport CspCASL.CspCASL_Keywords

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederimport qualified CspCASL.LocalTop as LocalTop

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport CspCASL.Print_CspCASL ()

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport Common.AnnoState

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport Common.Doc

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport Common.DocUtils

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederimport Common.Id

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederimport Common.Lib.Rel (Rel, predecessors)

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederimport Common.Result

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport qualified Data.Map as Map

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport qualified Data.Set as Set

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maedertype ChanNameMap = Map.Map CHANNEL_NAME (Set.Set SORT)

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedertype ProcNameMap = Map.Map PROCESS_NAME (Set.Set ProcProfile)

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedertype ProcVarMap = Map.Map SIMPLE_ID SORT

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maedertype ProcVarList = [(SIMPLE_ID, SORT)]

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder-- | Add a process name and its profile to a process name map. exist.

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederaddProcNameToProcNameMap :: PROCESS_NAME -> ProcProfile ->

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder ProcNameMap -> ProcNameMap

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederaddProcNameToProcNameMap name profile pm =

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder let l = Map.findWithDefault Set.empty name pm

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder in Map.insert name (Set.insert profile l) pm

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- | Test if a simple process name with a profile is in the process name map.

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederisNameInProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap -> Bool

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederisNameInProcNameMap name profile pm =

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder let l = Map.findWithDefault Set.empty name pm

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder in Set.member profile l

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder{- | Given a simple process name and a required number of parameters, find a

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederunqiue profile with that many parameters if possible. If this is not possible

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder(i.e., name does not exist, or no profile with the required number of

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederarguments or not unique profile for the required number of arguments), then

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederthe functions returns a failed result with a helpful error message. failure. -}

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedergetUniqueProfileInProcNameMap :: PROCESS_NAME -> Int -> ProcNameMap ->

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Result ProcProfile

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedergetUniqueProfileInProcNameMap name numParams pm =

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder let profiles = Map.findWithDefault Set.empty name pm

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder isMatch (ProcProfile argSorts _) =

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder length argSorts == numParams

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder matchedProfiles = Set.filter isMatch profiles

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder in case Set.toList matchedProfiles of

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder [] -> mkError ("Process name not in signature with "

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder ++ show numParams ++ " parameters:") name

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder [p] -> return p

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder _ -> mkError ("Process name not unique in signature with "

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder ++ show numParams ++ " parameters:") name

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercloseProcs :: Rel SORT -> CspSign -> CspSign

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercloseProcs r s = s { procSet = closeProcNameMapSortRel r $ procSet s }

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder{- | Close a proc name map under a sub-sort relation. Assumes all the proc

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederprofile's comms are in the sub sort relation and simply makes the comms

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederdownward closed under the sub-sort relation. -}

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercloseProcNameMapSortRel :: Rel SORT -> ProcNameMap -> ProcNameMap

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercloseProcNameMapSortRel sig =

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Map.map (Set.map $ closeProcProfileSortRel sig)

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder{- | Close a profile under a sub-sort relation. Assumes the proc profile's

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedercomms are in the sub sort relation and simply makes the comms downward closed

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederunder the sub-sort relation. -}

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedercloseProcProfileSortRel :: Rel SORT -> ProcProfile -> ProcProfile

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercloseProcProfileSortRel sig (ProcProfile argSorts comms) =

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder ProcProfile argSorts (closeCspCommAlpha sig comms)

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- Close a communication alphabet under CASL subsort

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercloseCspCommAlpha :: Rel SORT -> CommAlpha -> CommAlpha

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercloseCspCommAlpha sr =

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Set.unions . Set.toList . Set.map (closeOneCspComm sr)

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- Close one CommType under CASL subsort

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercloseOneCspComm :: Rel SORT -> CommType -> CommAlpha

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercloseOneCspComm sr x = let

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder mkTypedChan c s = CommTypeChan $ TypedChanName c s

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder subsorts s' =

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Set.singleton s' `Set.union` predecessors sr s'

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder in case x of

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder CommTypeSort s ->

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder Set.map CommTypeSort (subsorts s)

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder CommTypeChan (TypedChanName c s) ->

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Set.map CommTypeSort (subsorts s)

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

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

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

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- Extract the sorts from a process alphabet

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederprocAlphaSorts :: CommAlpha -> Set.Set SORT

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaederprocAlphaSorts a = stripMaybe $ Set.map justSort a

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder where justSort n = case n of

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (CommTypeSort s) -> Just s

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder _ -> Nothing

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- Extract the typed channel names from a process alphabet

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederprocAlphaChans :: CommAlpha -> Set.Set TypedChanName

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederprocAlphaChans a = stripMaybe $ Set.map justChan a

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder where justChan n = case n of

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder (CommTypeChan c) -> Just c

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder _ -> Nothing

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

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederstripMaybe :: Ord a => Set.Set (Maybe a) -> Set.Set a

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederstripMaybe x = Set.fromList $ Maybe.catMaybes $ Set.toList x

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- Close a set of sorts under a subsort relation

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedercspSubsortCloseSorts :: 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

} deriving (Eq, Ord, Show)

-- | plain union

cspSignUnion :: CspSign -> CspSign -> CspSign

cspSignUnion sign1 sign2 = emptyCspSign

{ chans = addMapSet (chans sign1) (chans sign2)

, procSet = addMapSet (procSet sign1) (procSet sign2) }

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

signature in the extendedInfo part. -}

type CspCASLSign = Sign CspSen CspSign

ccSig2CASLSign :: CspCASLSign -> CASLSign

ccSig2CASLSign sigma = sigma { extendedInfo = (), sentences = [] }

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

-- | Compute union of two CSP CASL signatures.

unionCspCASLSign :: CspCASLSign -> CspCASLSign -> Result CspCASLSign

unionCspCASLSign s1 s2 = do

-- Compute the unioned data signature ignoring the csp signatures

let newDataSig = addSig (\ _ _ -> emptyCspSign) s1 s2

-- Check that the new data signature has local top elements

rel = sortRel newDataSig

diags' = LocalTop.checkLocalTops rel

-- Compute the unioned csp signature with respect to the new data signature

newCspSign = unionCspSign rel (extendedInfo s1) (extendedInfo s2)

{- Only error will be added if there are any probelms. If there are no

problems no errors will be added and hets will continue as normal. -}

appendDiags diags'

-- put both the new data signature and the csp signature back together

return $ newDataSig {extendedInfo = newCspSign}

{- | Compute union of two CSP signatures assuming the new already computed data

signature. -}

unionCspSign :: Rel SORT -> CspSign -> CspSign -> CspSign

unionCspSign sr a b = cspSignUnion (closeProcs sr a) (closeProcs sr b)

-- | Compute difference of two CSP process signatures.

diffCspSig :: CspSign -> CspSign -> CspSign

diffCspSig a b = emptyCspSign

{ chans = diffMapSet (chans a) $ chans b

, procSet = diffMapSet (procSet a) $ procSet b

}

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

isCspCASLSubSig :: CspCASLSign -> CspCASLSign -> Bool

isCspCASLSubSig =

-- Normal casl subsignature and our extended csp part

isSubSig isCspSubSign

{- Also the sorts and sub-sort rels should be equal. If they are not then we

cannot just add the processes in as their profiles need to be donward closed

under the new sort-rels, but we do not check this here. -}

{- | Is one Csp Signature a sub signature of another assuming the same data

signature for now. -}

isCspSubSign :: CspSign -> CspSign -> Bool

isCspSubSign a b =

isSubMapSet (chans a) (chans b) &&

-- Check for each profile that the set of names are included.

isSubMapSet (procSet a) (procSet b)

-- | Pretty printing for CspCASL signatures

instance Pretty CspSign where

pretty = printCspSign

mapSetToList :: (Ord a, Ord b) => Map.Map a (Set.Set b) -> [(a, b)]

mapSetToList = concatMap (\ (c, ts) -> map (\ t -> (c, t)) $ Set.toList ts)

. Map.toList

printCspSign :: CspSign -> Doc

printCspSign sigma =

case mapSetToList $ chans sigma of

[] -> empty

s -> keyword (channelS ++ appendS s) <+> printChanList s

$+$ case mapSetToList $ procSet sigma of

[] -> empty

ps -> keyword processS <+> printProcList ps

-- | Pretty printing for channels

printChanList :: [(CHANNEL_NAME, SORT)] -> Doc

printChanList =

vcat . punctuate semi . map printChan

where printChan (chanName, sort) =

pretty chanName <+> colon <+> pretty sort

-- | Pretty printing for processes

printProcList :: [(PROCESS_NAME, ProcProfile)] -> Doc

printProcList =

vcat . punctuate semi . map printProc

where printProc (procName, procProfile) = pretty procName <+>

pretty procProfile

-- 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 CspSen = ProcessEq FQ_PROCESS_NAME FQProcVarList CommAlpha PROCESS

deriving (Show, Eq, Ord)

type CspCASLSen = FORMULA CspSen

instance GetRange CspSen

instance Pretty CspSen where

pretty (ProcessEq pn varList _commAlpha proc) =

let varDoc = if null varList

then empty

else parens $ ppWithCommas varList

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

instance FormExtension CspSen where

prefixExt (ProcessEq pn _ _ _) = case pn of

PROCESS_NAME _ -> (keyword processS <+>)

FQ_PROCESS_NAME {} -> id

instance TermExtension CspSen

instance TermParser CspSen

isProcessEq :: CspCASLSen -> Bool

isProcessEq f = case f of

ExtFORMULA _ -> True

_ -> False