fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz{- |

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzModule : $Id$

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzDescription : CspCASL signatures

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzCopyright : (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzMaintainer : M.Roggenbach@swansea.ac.uk

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzStability : provisional

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzPortability : portable

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzsignatures for CSP-CASL

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz-}

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz-- todo: implement isInclusion, computeExt

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzmodule CspCASL.SignCSP where

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME,

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz PROCESS(..), CommAlpha(..), CommType(..), TypedChanName(..))

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport CspCASL.AS_CspCASL ()

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport CspCASL.Print_CspCASL

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport CASL.AS_Basic_CASL (FORMULA, SORT)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport CASL.Sign (emptySign, Sign, extendedInfo, sortRel)

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport CASL.Morphism (Morphism)

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Common.AS_Annotation (Named)

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Common.Doc

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Common.DocUtils

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Common.Id (Id, SIMPLE_ID, mkSimpleId, nullRange)

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savuimport Common.Lib.Rel (predecessors)

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savuimport Common.Result

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuimport Control.Monad (unless)

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savuimport qualified Data.Map as Map

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuimport qualified Data.Set as Set

239330cd665aac95fcf9cf95449594c96667cbc2Robert Savu

239330cd665aac95fcf9cf95449594c96667cbc2Robert Savu-- | A process has zero or more parameter sorts, and a communication

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu-- alphabet.

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata ProcProfile = ProcProfile [SORT] CommAlpha

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder deriving (Eq, Show)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savutype ChanNameMap = Map.Map CHANNEL_NAME SORT

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savutype ProcNameMap = Map.Map PROCESS_NAME ProcProfile

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedertype ProcVarMap = Map.Map SIMPLE_ID SORT

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savutype ProcVarList = [(SIMPLE_ID, SORT)]

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu-- Close a communication alphabet under CASL subsort

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercloseCspCommAlpha :: CspCASLSign -> CommAlpha -> CommAlpha

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercloseCspCommAlpha sig = Set.unions . Set.toList . Set.map (closeOneCspComm sig)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu-- Close one CommType under CASL subsort

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavucloseOneCspComm :: CspCASLSign -> CommType -> CommAlpha

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavucloseOneCspComm sig x = let

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mkTypedChan c s = CommTypeChan $ TypedChanName c s

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu subsorts s' = Set.singleton s' `Set.union` predecessors (sortRel sig) s'

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu in case x of

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu CommTypeSort s -> Set.map CommTypeSort (subsorts s)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu CommTypeChan (TypedChanName c s) -> Set.map CommTypeSort (subsorts s)

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu `Set.union` Set.map (mkTypedChan c) (subsorts s)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

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

3051a3502f027f3d7bb750a1d7a6b1b43cdd2a86Robert Savu

3051a3502f027f3d7bb750a1d7a6b1b43cdd2a86Robert Savu-- Extract the sorts from a process alphabet

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavuprocAlphaSorts :: CommAlpha -> Set.Set SORT

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavuprocAlphaSorts a = stripMaybe $ Set.map justSort a

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu where justSort n = case n of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (CommTypeSort s) -> Just s

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu _ -> Nothing

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu-- Extract the typed channel names from a process alphabet

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavuprocAlphaChans :: CommAlpha -> Set.Set TypedChanName

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprocAlphaChans a = stripMaybe $ Set.map justChan a

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu where justChan n = case n of

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu (CommTypeChan c) -> Just c

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu _ -> Nothing

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

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederstripMaybe :: Ord a => Set.Set (Maybe a) -> Set.Set a

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavustripMaybe x = Set.fromList $ Maybe.catMaybes $ Set.toList x

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu-- Close a set of sorts under a subsort relation

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspSubsortCloseSorts :: CspCASLSign -> Set.Set SORT -> Set.Set SORT

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspSubsortCloseSorts sig sorts =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Set.unions subsort_sets

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder where subsort_sets = Set.toList $ Set.map (cspSubsortPreds sig) sorts

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu-}

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | CSP process signature.

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savudata CspSign = CspSign

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder { chans :: ChanNameMap

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu , procSet :: ProcNameMap

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

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu -- static analysis this is the empty list.

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , ccSentences :: [Named CspCASLSen]

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder } deriving (Eq, Show)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | A CspCASL signature is a CASL signature with a CSP process

239330cd665aac95fcf9cf95449594c96667cbc2Robert Savu-- signature in the extendedInfo part.

239330cd665aac95fcf9cf95449594c96667cbc2Robert Savutype CspCASLSign = Sign () CspSign

239330cd665aac95fcf9cf95449594c96667cbc2Robert Savu

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederccSig2CASLSign :: CspCASLSign -> Sign () ()

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavuccSig2CASLSign sigma = sigma { extendedInfo = () }

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederccSig2CspSign :: CspCASLSign -> CspSign

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuccSig2CspSign sigma = extendedInfo sigma

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu-- | Empty CspCASL signature.

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederemptyCspCASLSign :: CspCASLSign

b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuemptyCspCASLSign = emptySign emptyCspSign

0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz

0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz-- | Empty CSP process signature.

0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst SchulzemptyCspSign :: CspSign

0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst SchulzemptyCspSign = CspSign

0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz { chans = Map.empty

, procSet = Map.empty

, ccSentences =[]

}

-- | Compute union of two CSP process signatures.

addCspProcSig :: CspSign -> CspSign -> CspSign

addCspProcSig a b =

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

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

}

-- XXX looks incomplete!

isInclusion :: CspSign -> CspSign -> Bool

isInclusion _ _ = True

-- XXX morphisms between CSP process signatures?

data CspAddMorphism = CspAddMorphism

{ channelMap :: Map.Map Id Id

, processMap :: Map.Map Id Id

} deriving (Eq, Show)

composeIdMaps :: Map.Map Id Id -> Map.Map Id Id -> Map.Map Id Id

composeIdMaps m1 m2 = Map.foldWithKey (\ i j -> case Map.lookup j m2 of

Nothing -> error "SignCsp.composeIdMaps"

Just k -> Map.insert i k) Map.empty m1

composeCspAddMorphism :: CspAddMorphism -> CspAddMorphism

-> Result CspAddMorphism

composeCspAddMorphism m1 m2 = return emptyCspAddMorphism

{ channelMap = composeIdMaps (channelMap m1) $ channelMap m2

, processMap = composeIdMaps (processMap m1) $ processMap m2 }

inverseCspAddMorphism :: CspAddMorphism -> Result CspAddMorphism

inverseCspAddMorphism cm = do

let chL = Map.toList $ channelMap cm

prL = Map.toList $ processMap cm

swap = map $ \ (a, b) -> (b, a)

isInj l = length l == Set.size (Set.fromList $ map snd l)

unless (isInj chL) $ fail "invertCspAddMorphism.channelMap"

unless (isInj prL) $ fail "invertCspAddMorphism.processMap"

return emptyCspAddMorphism

{ channelMap = Map.fromList $ swap chL

, processMap = Map.fromList $ swap prL }

type CspMorphism = Morphism () CspSign CspAddMorphism

emptyCspAddMorphism :: CspAddMorphism

emptyCspAddMorphism = CspAddMorphism

{ channelMap = Map.empty -- ???

, processMap = Map.empty

}

-- dummy instances, need to be elaborated!

instance Pretty CspSign where

pretty = text . show

instance Pretty CspAddMorphism where

pretty = text . show

-- Sentences

-- 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 communication alphabet and finally on the RHS a fully

-- qualified process.

data CspCASLSen = CASLSen (FORMULA ())

| ProcessEq PROCESS_NAME ProcVarList CommAlpha PROCESS

deriving (Show, Eq, Ord)

instance Pretty CspCASLSen where

-- Not implemented yet - the pretty printing of the casl sentences

pretty(CASLSen _) = text "Pretty printing for CASLSen not implemented yet"

pretty(ProcessEq pn varList alpha proc) =

let varDoc = if (null varList)

then empty

else parens $ sepByCommas $ map pretty (map fst varList)

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

emptyCCSen :: CspCASLSen

emptyCCSen =

let emptyProcName = mkSimpleId "empty"

emptyVarList = []

emptyAlphabet = Set.empty

emptyProc = Skip nullRange

in ProcessEq emptyProcName emptyVarList emptyAlphabet emptyProc

isCASLSen :: CspCASLSen -> Bool

isCASLSen (CASLSen _) = True

isCASLSen _ = False

isProcessEq :: CspCASLSen -> Bool

isProcessEq (ProcessEq _ _ _ _) = True

isProcessEq _ = False