StatAnaCSP.hs revision 9582375827616730f146b77f9d5a4fd0cc78bc47
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederDescription : static analysis for CspCASL
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiCopyright : (c) Markus Roggenbach, Till Mossakowski, Uni Bremen 2004-2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : M.Roggenbach@swansea.ac.uk
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiStatic analysis for CSP-CASL
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskiimport qualified Control.Monad as Monad
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Data.Map as Map
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Data.Maybe as Maybe
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Data.Set as S
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maederimport CASL.AS_Basic_CASL (SORT, TERM, VAR)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.Lib.Rel as Rel
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Common.Id (simpleIdToId)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport CspCASL.LocalTop (Obligation(..), unmetObs)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederbasicAnalysisCspCASL :: (CspBasicSpec, CspSign, GlobalAnnos)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -> Result (CspBasicSpec, ExtSign CspSign (), [Named ()])
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederbasicAnalysisCspCASL (cc, sigma, _ga) = do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let (_, accSig) = runState (ana_BASIC_CSP cc) sigma
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let ds = reverse $ envDiags accSig
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Result ds (Just ()) -- insert diagnostics
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (cc, mkExtSign accSig, [])
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiana_BASIC_CSP :: CspBasicSpec -> State CspSign ()
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiana_BASIC_CSP cc = do checkLocalTops
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski mapM anaChanDecl (channels cc)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski mapM anaProcItem (proc_items cc)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- Analysis of local top elements
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- | Check CspCASL signature for local top elements in subsorts.
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedercheckLocalTops :: State CspSign ()
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedercheckLocalTops = do
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let obs = unmetObs $ Rel.toList $ Rel.transClosure $ sortRel sig
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski addDiags (map lteError obs)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | Add diagnostic error for every unmet local top element obligation.
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederlteError :: Obligation SORT -> Diagnosis
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederlteError (Obligation x y z) = mkDiag Error msg ()
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski where msg = ("local top element obligation ("
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder ++ (show x) ++ "<" ++ (show y) ++ "," ++ (show z)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ++ ") unfulfilled")
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- Analysis of channel declarations
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederanaChanDecl :: CHANNEL_DECL -> State CspSign CHANNEL_DECL
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederanaChanDecl (ChannelDecl chanNames chanSort) = do
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski checkSorts [chanSort] -- check channel sort is known
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let ext = extendedInfo sig
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder oldChanMap = chans ext
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder newChanMap <- Monad.foldM (anaChannelName chanSort) oldChanMap chanNames
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder vds <- gets envDiags
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder put sig { extendedInfo = ext { chans = newChanMap }
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder , envDiags = vds
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return (ChannelDecl chanNames chanSort)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederanaChannelName :: SORT -> ChanNameMap -> CHANNEL_NAME ->
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder State CspSign ChanNameMap
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederanaChannelName s m chanName = do
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder if (show chanName) `S.member` (S.map show (sortSet sig))
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder then do let err = "channel name already in use as a sort name"
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder addDiags [mkDiag Error err chanName]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski else case Map.lookup chanName m of
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Nothing -> return (Map.insert chanName s m) -- insert new.
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder then do let warn = "channel redeclared with same sort"
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder addDiags [mkDiag Warning warn chanName]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder return m -- already declared with this sort.
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder else do let err = "channel declared with multiple sorts"
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder addDiags [mkDiag Error err chanName]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder-- Analysis of process items
10a2cf8d9887524acde19d4ea59f8fea3a7f3258Till MossakowskianaProcItem :: PROC_ITEM -> State CspSign ()
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskianaProcItem procItem =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski case procItem of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (Proc_Decl name argSorts alpha) -> anaProcDecl name argSorts alpha
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (Proc_Eq parmProcName procTerm) -> anaProcEq parmProcName procTerm
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- Analysis of process declarations
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederanaProcDecl :: PROCESS_NAME -> PROC_ARGS -> PROC_ALPHABET
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder -> State CspSign ()
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaederanaProcDecl name argSorts (ProcAlphabet commTypes _) = do
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder let ext = extendedInfo sig
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder oldProcDecls = procSet ext
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder newProcDecls <-
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder if name `Map.member` oldProcDecls
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder then do -- duplicate process declaration
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let err = "process name declared more than once"
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder addDiags [mkDiag Error err name]
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return oldProcDecls
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder else do -- new process declation
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder checkSorts argSorts -- check argument sorts are known
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- build alphabet: set of CommType values
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder alpha <- Monad.foldM (anaCommType sig) S.empty commTypes
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let profile = (ProcProfile argSorts alpha)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return (Map.insert name profile oldProcDecls)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder vds <- gets envDiags
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder put sig { extendedInfo = ext {procSet = newProcDecls }
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , envDiags = vds
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- Analysis of process equations
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederanaProcEq :: PARM_PROCNAME -> PROCESS -> State CspSign ()
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederanaProcEq (ParmProcname pn vs) proc = do
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let ext = extendedInfo sig
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder procDecls = procSet ext
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski prof = pn `Map.lookup` procDecls
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- Only analyse a process if its name (and thus profile) is known
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Just (ProcProfile procArgs procAlpha) ->
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder do gVars <- anaProcVars pn procArgs vs -- compute global vars
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder termAlpha <- anaProcTerm proc procAlpha gVars Map.empty
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski checkCommAlphaSub termAlpha procAlpha proc "process equation"
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski do addDiags [mkDiag Error "process equation for unknown process" pn]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder vds <- gets envDiags
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder put sig { envDiags = vds }
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder-- Analysis of process variable names.
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederanaProcVars :: PROCESS_NAME -> [SORT] -> [VAR] -> State CspSign ProcVarMap
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederanaProcVars pn ss vs = do
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder case (compare (length ss) (length vs)) of
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder LT -> do addDiags [mkDiag Error "too many process arguments" pn]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder GT -> do addDiags [mkDiag Error "not enough process arguments" pn]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski EQ -> Monad.foldM anaProcVar Map.empty (zip vs ss)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskianaProcVar :: ProcVarMap -> (VAR, SORT) -> State CspSign ProcVarMap
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederanaProcVar old (v, s) = do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski then do addDiags [mkDiag Error "process arg declared more than once" v]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski else return (Map.insert v s old)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- Analysis of process terms
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskianaProcTerm :: PROCESS -> CommAlpha -> ProcVarMap ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ProcVarMap -> State CspSign CommAlpha
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskianaProcTerm proc alpha gVars lVars = do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski NamedProcess _ _ _ ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do addDiags [mkDiag Debug "Named process" proc]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- XXX do this
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do addDiags [mkDiag Debug "Skip" proc]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder do addDiags [mkDiag Debug "Stop" proc]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do addDiags [mkDiag Debug "Div" proc]
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder do addDiags [mkDiag Debug "Run" proc]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski comms <- anaEventSet es
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Chaos es _ ->
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder do addDiags [mkDiag Debug "Chaos" proc]
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder comms <- anaEventSet es
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder PrefixProcess e p _ ->
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder do addDiags [mkDiag Debug "Prefix" proc]
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (evComms, rcvMap) <- anaEvent e (lVars `Map.union` gVars)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski comms <- anaProcTerm p alpha gVars (rcvMap `Map.union` lVars)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (comms `S.union` evComms)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski InternalPrefixProcess v s p _ ->
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder do addDiags [mkDiag Debug "Internal prefix" proc]
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder checkSorts [s] -- check sort is known
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski comms <- anaProcTerm p alpha gVars (Map.insert v s lVars)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return (S.insert (CommTypeSort s) comms)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder ExternalPrefixProcess v s p _ ->
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder do addDiags [mkDiag Debug "External prefix" proc]
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder checkSorts [s] -- check sort is known
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder comms <- anaProcTerm p alpha gVars (Map.insert v s lVars)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return (S.insert (CommTypeSort s) comms)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Sequential p q _ ->
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder do addDiags [mkDiag Debug "Sequential" proc]
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder pComms <- anaProcTerm p alpha gVars lVars
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder qComms <- anaProcTerm q alpha gVars Map.empty
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return (pComms `S.union` qComms)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder InternalChoice p q _ ->
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder do addDiags [mkDiag Debug "InternalChoice" proc]
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder pComms <- anaProcTerm p alpha gVars lVars
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder qComms <- anaProcTerm q alpha gVars lVars
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return (pComms `S.union` qComms)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder ExternalChoice p q _ ->
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder do addDiags [mkDiag Debug "ExternalChoice" proc]
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder pComms <- anaProcTerm p alpha gVars lVars
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder qComms <- anaProcTerm q alpha gVars lVars
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (pComms `S.union` qComms)
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder Interleaving p q _ ->
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder do addDiags [mkDiag Debug "Interleaving" proc]
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder pComms <- anaProcTerm p alpha gVars lVars
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder qComms <- anaProcTerm q alpha gVars lVars
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder return (pComms `S.union` qComms)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder SynchronousParallel p q _ ->
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder do addDiags [mkDiag Debug "Synchronous" proc]
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder pComms <- anaProcTerm p alpha gVars lVars
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder qComms <- anaProcTerm q alpha gVars lVars
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder return (pComms `S.union` qComms)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder GeneralisedParallel p es q _ ->
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder do addDiags [mkDiag Debug "Generalised parallel" proc]
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder pComms <- anaProcTerm p alpha gVars lVars
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder synComms <- anaEventSet es
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder qComms <- anaProcTerm q alpha gVars lVars
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder return (S.unions [pComms, qComms, synComms])
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder AlphabetisedParallel p esp esq q _ ->
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder do addDiags [mkDiag Debug "Alphabetised parallel" proc]
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder pComms <- anaProcTerm p alpha gVars lVars
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder pSynComms <- anaEventSet esp
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder checkCommAlphaSub pSynComms pComms proc "alphabetised parallel, left"
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder qSynComms <- anaEventSet esq
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder qComms <- anaProcTerm q alpha gVars lVars
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder checkCommAlphaSub qSynComms qComms proc "alphabetised parallel, right"
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder return (pComms `S.union` qComms)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Hiding p es _ ->
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder do addDiags [mkDiag Debug "Hiding" proc]
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder pComms <- anaProcTerm p alpha gVars lVars
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski hidComms <- anaEventSet es
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (pComms `S.union` hidComms)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski RelationalRenaming p _ _ ->
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder do addDiags [mkDiag Debug "Renaming" proc]
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -- XXX renaming needs fixing
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski anaProcTerm p alpha gVars lVars
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ConditionalProcess _ p q _ ->
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder do addDiags [mkDiag Debug "Conditional" proc]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder pComms <- anaProcTerm p alpha gVars lVars
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder qComms <- anaProcTerm q alpha gVars lVars
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder let fComms = S.empty -- XXX get formula sorts here
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder return (S.unions [pComms, qComms, fComms])
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederanaEventSet :: EVENT_SET -> State CspSign CommAlpha
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederanaEventSet (EventSet es _) = do
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder comms <- Monad.foldM (anaCommType sig) S.empty es
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder vds <- gets envDiags
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder put sig { envDiags = vds }
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederanaCommType :: CspSign -> CommAlpha -> COMM_TYPE -> State CspSign CommAlpha
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederanaCommType sig alpha ct =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder if ctSort `S.member` (sortSet sig)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder then -- ct is a sort name; insert sort into alpha
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder do return (S.insert (CommTypeSort ctSort) alpha)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski else -- ct not a sort name, so should be a channel name
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder case Map.lookup ct (chans $ extendedInfo sig) of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Just s -> -- ct is a channel name; insert typed chan name into alpha
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return (S.insert (mkTypedChan ct s) alpha)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Nothing -> do let err = "not a sort or channel name"
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder addDiags [mkDiag Error err ct]
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder where ctSort = simpleIdToId ct
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder mkTypedChan c s = CommTypeChan $ TypedChanName c s
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaederanaEvent :: EVENT -> ProcVarMap -> State CspSign (CommAlpha, ProcVarMap)
5e46b572ed576c0494768998b043d9d340594122Till MossakowskianaEvent e vars = case e of
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder TermEvent t _ -> anaTermEvent t vars
578b677874296e4ba48e57b5e4b4b0270d995603Christian Maeder ChanSend c t _ -> anaChanSend c t vars
578b677874296e4ba48e57b5e4b4b0270d995603Christian Maeder ChanNonDetSend c v s _ -> anaChanBinding c v s
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ChanRecv c v s _ -> anaChanBinding c v s
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederanaTermEvent :: (TERM ()) -> ProcVarMap ->
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder State CspSign (CommAlpha, ProcVarMap)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederanaTermEvent t vars = do
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder anaTermCspCASL t vars
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder let alpha = [] -- XXX Need to implement term sort computation
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederanaChanSend :: CHANNEL_NAME -> (TERM ()) -> ProcVarMap ->
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder State CspSign (CommAlpha, ProcVarMap)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederanaChanSend c t vars = do
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski let ext = extendedInfo sig
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder case c `Map.lookup` (chans ext) of
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder Nothing -> do
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder addDiags [mkDiag Error "unknown channel" c]
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder Just _ -> do -- XXX _ is to be chanSort
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder anaTermCspCASL t vars
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder -- XXX Need to implement term casting
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder let alpha = []
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederanaChanBinding :: CHANNEL_NAME -> VAR -> SORT ->
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder State CspSign (CommAlpha, ProcVarMap)
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederanaChanBinding c v s = do
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder checkSorts [s] -- check sort is known
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder let ext = extendedInfo sig
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder case c `Map.lookup` (chans ext) of
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder Nothing -> do
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski addDiags [mkDiag Error "unknown channel" c]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Just chanSort -> do
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder if s `S.member` (subsorts chanSort)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski then do let alpha = [CommTypeSort s
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder ,CommTypeChan (TypedChanName c s)]
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder let binding = [(v, s)]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski return (S.fromList alpha, Map.fromList binding)
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder else do let err = "sort not a subsort of channel's sort"
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski addDiags [mkDiag Error err s]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski where subsorts = Rel.predecessors (sortRel sig)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski-- Analysis of communication alphabet subsort-closed subset relationships.
5e46b572ed576c0494768998b043d9d340594122Till MossakowskicheckCommAlphaSub :: CommAlpha -> CommAlpha -> PROCESS -> String ->
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski State CspSign ()
5e46b572ed576c0494768998b043d9d340594122Till MossakowskicheckCommAlphaSub sub super proc context = do
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski let extras = ((closeCspCommAlpha sig sub) `S.difference`
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (closeCspCommAlpha sig super))
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski then do return ()
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski else do let err = ("Communication alphabet subset violations (" ++
a938729e277da5c7742bb88946ab2c150416fd5dTill Mossakowski context ++ "): " ++ (show $ S.toList extras))
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski addDiags [mkDiag Error err proc]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski-- Analysis of term appearing in CspCASL context
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederanaTermCspCASL :: (TERM ()) -> ProcVarMap -> State CspSign ()
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederanaTermCspCASL _ _ = do return () -- XXX not yet implemented