7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Id$

81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : Static analysis of CspCASL

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaederCopyright : (c) Andy Gimblett, Liam O'Reilly Markus Roggenbach,

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu Swansea University 2008

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder

7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederMaintainer : a.m.gimblett@swansea.ac.uk

2ac1742771a267119f1d839054b5e45d0a468085Christian MaederStability : provisional

7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederPortability : portable

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederStatic analysis of CSP-CASL specifications, following "Tool Support

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederfor CSP-CASL", MPhil thesis by Andy Gimblett, 2008.

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder<http://www.cs.swan.ac.uk/~csandy/mphil/>

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder-}

950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maedermodule CspCASL.StatAnaCSP where

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport qualified Control.Monad as Monad

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maederimport qualified Data.Map as Map

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as S

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport CASL.AS_Basic_CASL (FORMULA(..), OpKind(..), SORT, TERM(..), VAR,

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder VAR_DECL(..))

8197d0be8b81692f311ad5ca34e125e2cf9eecb8Christian Maederimport CASL.MixfixParser

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport CASL.Overload (minExpFORMULA, oneExpTerm)

a6f84880cea4485fba85b521d122eba73b0df70bChristian Maederimport CASL.Sign

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maederimport CASL.StaticAna (allConstIds, allOpIds, allPredIds)

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maederimport Common.AS_Annotation

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maederimport Common.Result

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maederimport Common.GlobalAnnotations

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maederimport Common.ConvertGlobalAnnos

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maederimport qualified Common.Lib.Rel as Rel

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederimport Common.Id (getRange, Id, nullRange, simpleIdToId)

878ac75d7acbbb06412e82a4c95356ce60f942deChristian Maederimport Common.Lib.State

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederimport Common.ExtSign

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport CspCASL.AS_CspCASL

2ac1742771a267119f1d839054b5e45d0a468085Christian Maederimport CspCASL.AS_CspCASL_Process

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport qualified CspCASL.LocalTop as LocalTop

2ac1742771a267119f1d839054b5e45d0a468085Christian Maederimport CspCASL.Print_CspCASL ()

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport CspCASL.SignCSP

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport CspCASL.Symbol

6b1153c560b677f9f5da2a60ee8a10de75ff90c5Christian Maederimport CspCASL.Morphism(makeChannelNameSymbol, makeFQProcNameSymbol)

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport qualified Data.Set as Set

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- | The first element of the returned pair (CspBasicSpec) is the same

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder-- as the inputted version just with some very minor optimisations -

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder-- none in our case, but for CASL - brackets are otimized. This all

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-- that happens, the mixfixed terms are still mixed fixed terms in

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder-- the returned version.

2ac1742771a267119f1d839054b5e45d0a468085Christian MaederbasicAnalysisCspCASL :: (CspBasicSpec, CspCASLSign, GlobalAnnos)

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol,

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder [Named CspCASLSen])

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederbasicAnalysisCspCASL (cc, sigma, ga) =

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder let Result es mga = mergeGlobalAnnos ga $ globAnnos sigma

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder (_, accSig) = runState (ana_BASIC_CSP cc) $ case mga of

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Nothing -> sigma

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Just nga -> sigma { globAnnos = nga }

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ds = reverse $ envDiags accSig

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder -- Extract process equations only.

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder ext = extendedInfo accSig

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder ccsents = reverse $ ccSentences ext

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder -- Clean signature here

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder cleanSig = accSig

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder { extendedInfo = ext { ccSentences = []}}

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder in Result (es ++ ds) $ Just (cc

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder , ExtSign cleanSig $ Set.map caslToCspSymbol $ declaredSymbols accSig

522913d1d69be804c9579bbc77868ec6b501b608Christian Maeder , ccsents)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

b1bd8688a1ce545444792a307412711c2c61df5fChristian MaedercaslToCspSymbol :: Symbol -> CspSymbol

b1bd8688a1ce545444792a307412711c2c61df5fChristian MaedercaslToCspSymbol sy = CspSymbol (symName sy) $ CaslSymbType $ symbType sy

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maederana_BASIC_CSP :: CspBasicSpec -> State CspCASLSign ()

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maederana_BASIC_CSP cc = do checkLocalTops

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder mapM anaChanDecl (channels cc)

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder mapM anaProcItem (proc_items cc)

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder return ()

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder-- Analysis of local top elements

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder-- | Check a CspCASL signature for local top elements in its subsort

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder-- relation.

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian MaedercheckLocalTops :: State CspCASLSign ()

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian MaedercheckLocalTops = do

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder sig <- get

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder let diags' = LocalTop.checkLocalTops $ sortRel sig

74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder -- Only error will be added if there are any probelms. If there are no

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

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder addDiags (diags')

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return ()

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder-- Static analysis of channel declarations

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder-- | Statically analyse a CspCASL channel declaration.

2ac1742771a267119f1d839054b5e45d0a468085Christian MaederanaChanDecl :: CHANNEL_DECL -> State CspCASLSign ()

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaederanaChanDecl (ChannelDecl chanNames chanSort) = do

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder checkSorts [chanSort] -- check channel sort is known

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder sig <- get

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder let ext = extendedInfo sig

7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maeder oldChanMap = chans ext

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder newChanMap <- Monad.foldM (anaChannelName chanSort) oldChanMap chanNames

4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder sig2 <- get

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder put sig2 { extendedInfo = ext { chans = newChanMap }}

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder-- | Statically analyse a CspCASL channel name.

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederanaChannelName :: SORT -> ChanNameMap -> CHANNEL_NAME ->

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder State CspCASLSign ChanNameMap

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederanaChannelName s m chanName = do

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder sig <- get

840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder if (show chanName) `S.member` (S.map show (sortSet sig))

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder then do let err = "channel name already in use as a sort name"

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder addDiags [mkDiag Error err chanName]

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder return m

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder else case Map.lookup chanName m of

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Nothing ->

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder -- Add the channel name as a symbol to the list of

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder -- newly defined symbols - which is stored in the CASL

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder -- signature

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder do addSymbol (makeChannelNameSymbol chanName)

72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder return (Map.insert chanName s m) -- insert new.

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder Just e ->

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder if e == s

72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder then do let warn = "channel redeclared with same sort"

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder addDiags [mkDiag Warning warn chanName]

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder return m -- already declared with this sort.

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder else do let err = "channel declared with multiple sorts"

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder addDiags [mkDiag Error err chanName]

32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder return m

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder

2118d66b6aa3c90458925019c9b2fb986e2b2aabChristian Maeder-- Static analysis of process items

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- | Statically analyse a CspCASL process item.

2ac1742771a267119f1d839054b5e45d0a468085Christian MaederanaProcItem :: (Annoted PROC_ITEM) -> State CspCASLSign ()

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian MaederanaProcItem annotedProcItem =

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder let procItem = item annotedProcItem

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder in case procItem of

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder (Proc_Decl name argSorts alpha) -> anaProcDecl name argSorts alpha

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder (Proc_Eq parmProcName procTerm) ->

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder anaProcEq annotedProcItem parmProcName procTerm

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder-- Static analysis of process declarations

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder

4805aaef9706fd26f102ffd712b99cb8778ba3c1Christian Maeder-- | Statically analyse a CspCASL process declaration.

4805aaef9706fd26f102ffd712b99cb8778ba3c1Christian MaederanaProcDecl :: SIMPLE_PROCESS_NAME -> PROC_ARGS -> PROC_ALPHABET

4805aaef9706fd26f102ffd712b99cb8778ba3c1Christian Maeder -> State CspCASLSign ()

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaederanaProcDecl name argSorts comms = do

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder sig <- get

89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian Maeder let ext = extendedInfo sig

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder oldProcDecls = procSet ext

cc584a730c98e711c2a244e51b102ba1821e531dChristian Maeder newProcDecls <- do

cc584a730c98e711c2a244e51b102ba1821e531dChristian Maeder -- new process declation

cc584a730c98e711c2a244e51b102ba1821e531dChristian Maeder profile <- anaProcAlphabet argSorts comms

cc584a730c98e711c2a244e51b102ba1821e531dChristian Maeder -- Add the process name as a symbol to the list of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- newly defined symbols - which is stored in the CASL

66f4f32855e7e2f0cf79b50ce6bd426598d9b166Christian Maeder -- signature

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder let fqPn = FQ_PROCESS_NAME name profile

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder addSymbol $ makeFQProcNameSymbol fqPn

d93bbbec133697cc79d59f9d7cc8e97458976c15Christian Maeder -- Check the name (with profile) is new (for warning only)

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder if isNameInProcNameMap name profile oldProcDecls

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder then -- name with profile already in signature

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder do let warn = "process name redeclared with same profile '" ++

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder show (printProcProfile profile) ++ "':"

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder addDiags [mkDiag Warning warn name]

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder return oldProcDecls

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder else -- New name with profile - add the name to the signature in the

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder -- state

d93bbbec133697cc79d59f9d7cc8e97458976c15Christian Maeder return $ addProcNameToProcNameMap name profile oldProcDecls

66f4f32855e7e2f0cf79b50ce6bd426598d9b166Christian Maeder sig2 <- get

66f4f32855e7e2f0cf79b50ce6bd426598d9b166Christian Maeder put sig2 { extendedInfo = ext {procSet = newProcDecls }}

66f4f32855e7e2f0cf79b50ce6bd426598d9b166Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- Static analysis of process equations

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- | Find a profile for a process name. Either the profile is given via a parsed

8dcc70ff9afdfe4aff258676718677a4d7076fd0Christian Maeder-- fully qualified process name, in which case we check everything is valid and

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-- the process name with the profile is known. Or its a plain process name where

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder-- we must deduce a unique profile is possible. We also know how many variables

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-- / parameters the process name has.

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaederfindProfileForProcName :: FQ_PROCESS_NAME -> Int -> ProcNameMap ->

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder State CspCASLSign (Maybe ProcProfile)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederfindProfileForProcName pn numParams procNameMap =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder case pn of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder FQ_PROCESS_NAME _ _ ->

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder -- We should not be trying to find a profile for a fully qualified process

d93bbbec133697cc79d59f9d7cc8e97458976c15Christian Maeder -- name

a6f84880cea4485fba85b521d122eba73b0df70bChristian Maeder error $ "CspCASL.StatAnaCsp.findProfileForProcName: Process name\

a6f84880cea4485fba85b521d122eba73b0df70bChristian Maeder \ already fully qualified: " ++ show pn

a6f84880cea4485fba85b521d122eba73b0df70bChristian Maeder PARSED_FQ_PROCESS_NAME pn' argSorts comms -> do

a6f84880cea4485fba85b521d122eba73b0df70bChristian Maeder profile <- anaProcAlphabet argSorts comms

a6f84880cea4485fba85b521d122eba73b0df70bChristian Maeder let profiles = Map.findWithDefault Set.empty pn' procNameMap

a6f84880cea4485fba85b521d122eba73b0df70bChristian Maeder if profile `Set.member` profiles

a6f84880cea4485fba85b521d122eba73b0df70bChristian Maeder then return $ Just profile

a6f84880cea4485fba85b521d122eba73b0df70bChristian Maeder else do

a6f84880cea4485fba85b521d122eba73b0df70bChristian Maeder addDiags [mkDiag Error

a6f84880cea4485fba85b521d122eba73b0df70bChristian Maeder "Fully qualified process name not in signature" pn]

a6f84880cea4485fba85b521d122eba73b0df70bChristian Maeder return Nothing

a6f84880cea4485fba85b521d122eba73b0df70bChristian Maeder PROCESS_NAME pn' ->

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder let resProfile = getUniqueProfileInProcNameMap pn' numParams procNameMap

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder in case resultToMaybe resProfile of

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder Nothing ->

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder do addDiags $ diags resProfile

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder return Nothing

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder Just profile' ->

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder return $ Just profile'

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder-- | Analyse a process name an return a fully qualified one if possible. We also

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder-- know how many variables / parameters the process name has.

2ac1742771a267119f1d839054b5e45d0a468085Christian MaederanaProcName :: FQ_PROCESS_NAME -> Int -> State CspCASLSign (Maybe FQ_PROCESS_NAME)

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaederanaProcName pn numParams= do

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder sig <- get

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder let ext = extendedInfo sig

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder procDecls = procSet ext

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder simpPn = procNameToSimpProcName pn

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder maybeProf <- findProfileForProcName pn numParams procDecls

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder case maybeProf of

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder Nothing -> return Nothing

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder Just profile ->

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder -- We now construct the real fully qualified process name

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder return $ Just $ FQ_PROCESS_NAME simpPn profile

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder-- | Statically analyse a CspCASL process equation.

2ac1742771a267119f1d839054b5e45d0a468085Christian MaederanaProcEq :: Annoted a -> PARM_PROCNAME -> PROCESS -> State CspCASLSign ()

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederanaProcEq a (ParmProcname pn vs) proc =

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder -- the 'annoted a' contains the annotation of the process equation. We do not

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder -- care what the underlying item is in the annotation (but it probably will be

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder -- the proc eq)

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder do

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder sig <- get

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder let ext = extendedInfo sig

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder ccsens = ccSentences ext

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder -- procDecls = procSet ext

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder maybeFqPn <- anaProcName pn (length vs)

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder case maybeFqPn of

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder -- Only analyse a process if its name and profile is known

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Nothing -> return ()

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Just fqPn ->

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder case fqPn of

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder PROCESS_NAME _ ->

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder error "CspCasl.StatAnaCSP.anaProcEq: Impossible case"

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder PARSED_FQ_PROCESS_NAME _ _ _ ->

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder error "CspCasl.StatAnaCSP.anaProcEq: Impossible case"

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder FQ_PROCESS_NAME _ prof ->

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder case prof of

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder ProcProfile procArgs procAlpha -> do

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder gVars <- anaProcVars pn

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder procArgs vs -- compute global

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder -- vars Change a procVarList to a FQProcVarList We do

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder -- not care about the range as we are building fully

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder -- qualified variables and they have already been

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder -- checked to be ok.

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder let mkFQProcVar (v,s) = Qual_var v s nullRange

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder let fqGVars = map mkFQProcVar gVars

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (termAlpha, fqProc) <-

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder anaProcTerm proc (Map.fromList gVars) Map.empty

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder checkCommAlphaSub termAlpha procAlpha proc "process equation"

0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder -- Save the diags from the checkCommAlphaSub

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder vds <- gets envDiags

d48085f765fca838c1d972d2123601997174583dChristian Maeder -- put CspCASL Sentences back in to the state with new sentence

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder -- BUG - What should the constituent alphabet be for this

bd6b297dcf467926715d0a6bd36e8d4071b6728eChristian Maeder -- process? probably the same as the inner one!

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder let namedSen = makeNamedSen $

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder -- We take the annotated item and replace the

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder -- inner item, thus preserving the annotations. We

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder -- then take this annotated sentence and make it a

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder -- named sentence in accordance to the (if

bd6b297dcf467926715d0a6bd36e8d4071b6728eChristian Maeder -- existing) name in the annotations.

bd6b297dcf467926715d0a6bd36e8d4071b6728eChristian Maeder a {item =

bd6b297dcf467926715d0a6bd36e8d4071b6728eChristian Maeder ProcessEq fqPn fqGVars procAlpha fqProc}

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder put sig {envDiags = vds, extendedInfo =

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder ext {ccSentences = namedSen:ccsens}

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder }

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder return ()

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return ()

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- | Statically analyse a CspCASL process equation's global variable

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- names.

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederanaProcVars :: FQ_PROCESS_NAME -> [SORT] -> [VAR] ->

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder State CspCASLSign ProcVarList

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederanaProcVars pn ss vs =

9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder do vars <-

840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder case (compare (length ss) (length vs)) of

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder LT -> do addDiags [mkDiag Error

3bffe0f10ad93403e36288a1a4a92d50356956b5Christian Maeder "Process name applied to too many arguments:"

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder pn]

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder return []

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder GT -> do addDiags [mkDiag Error

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder "process name not applied to enough arguments:"

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder pn]

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder return []

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder EQ -> Monad.foldM anaProcVar [] (zip vs ss)

840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder return $ reverse $ vars

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-- | Statically analyse a CspCASL process-global variable name.

bb13d067514a3f474166f345e098b81f3de11dbeChristian MaederanaProcVar :: ProcVarList -> (VAR, SORT) -> State CspCASLSign ProcVarList

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaederanaProcVar old (v, s) = do

9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder if v `elem` (map fst old)

9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder then do addDiags [mkDiag Error

9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder "Process argument declared more than once:" v]

9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder return old

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder else return ((v,s) : old)

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder-- Static analysis of process terms

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder

-- BUG in fucntion below

-- not returing FQProcesses

-- | Statically analyse a CspCASL process term.

-- The process that is returned is a fully qualified process.

anaProcTerm :: PROCESS -> ProcVarMap -> ProcVarMap ->

State CspCASLSign (CommAlpha, PROCESS)

anaProcTerm proc gVars lVars = case proc of

NamedProcess name args r ->

do addDiags [mkDiag Debug "Named process" proc]

(al, fqArgs) <- anaNamedProc proc name args (lVars `Map.union` gVars)

let fqProc = FQProcess (NamedProcess name fqArgs r) al r

return (al, fqProc)

Skip r ->

do addDiags [mkDiag Debug "Skip" proc]

let fqProc = FQProcess (Skip r) S.empty r

return (S.empty, fqProc)

Stop r ->

do addDiags [mkDiag Debug "Stop" proc]

let fqProc = FQProcess (Stop r) S.empty r

return (S.empty, fqProc)

Div r ->

do addDiags [mkDiag Debug "Div" proc]

let fqProc = FQProcess (Div r) S.empty r

return (S.empty, fqProc)

Run es r ->

do addDiags [mkDiag Debug "Run" proc]

(comms, fqEs) <- anaEventSet es

let fqProc = FQProcess (Run fqEs r) comms r

return (comms, fqProc)

Chaos es r ->

do addDiags [mkDiag Debug "Chaos" proc]

(comms, fqEs) <- anaEventSet es

let fqProc = FQProcess (Chaos fqEs r) comms r

return (comms, fqProc)

PrefixProcess e p r ->

do addDiags [mkDiag Debug "Prefix" proc]

(evComms, rcvMap, fqEvent) <- anaEvent e (lVars `Map.union` gVars)

(comms, pFQTerm) <- anaProcTerm p gVars (rcvMap `Map.union` lVars)

let newAlpha = comms `S.union` evComms

let fqProc = FQProcess (PrefixProcess fqEvent pFQTerm r) newAlpha r

return (newAlpha, fqProc)

Sequential p q r ->

do addDiags [mkDiag Debug "Sequential" proc]

(pComms, pFQTerm) <- anaProcTerm p gVars lVars

(qComms, qFQTerm) <- anaProcTerm q gVars Map.empty

let newAlpha = pComms `S.union` qComms

let fqProc = FQProcess (Sequential pFQTerm qFQTerm r) newAlpha r

return (newAlpha, fqProc)

InternalChoice p q r ->

do addDiags [mkDiag Debug "InternalChoice" proc]

(pComms, pFQTerm) <- anaProcTerm p gVars lVars

(qComms, qFQTerm) <- anaProcTerm q gVars lVars

let newAlpha = pComms `S.union` qComms

let fqProc = FQProcess (InternalChoice pFQTerm qFQTerm r) newAlpha r

return (newAlpha, fqProc)

ExternalChoice p q r ->

do addDiags [mkDiag Debug "ExternalChoice" proc]

(pComms, pFQTerm) <- anaProcTerm p gVars lVars

(qComms, qFQTerm) <- anaProcTerm q gVars lVars

let newAlpha = pComms `S.union` qComms

let fqProc = FQProcess (ExternalChoice pFQTerm qFQTerm r) newAlpha r

return (newAlpha, fqProc)

Interleaving p q r ->

do addDiags [mkDiag Debug "Interleaving" proc]

(pComms, pFQTerm) <- anaProcTerm p gVars lVars

(qComms, qFQTerm) <- anaProcTerm q gVars lVars

let newAlpha = pComms `S.union` qComms

let fqProc = FQProcess (Interleaving pFQTerm qFQTerm r) newAlpha r

return (newAlpha, fqProc)

SynchronousParallel p q r ->

do addDiags [mkDiag Debug "Synchronous" proc]

(pComms, pFQTerm) <- anaProcTerm p gVars lVars

(qComms, qFQTerm) <- anaProcTerm q gVars lVars

let newAlpha = pComms `S.union` qComms

let fqProc = FQProcess (SynchronousParallel pFQTerm

qFQTerm r) newAlpha r

return (newAlpha, fqProc)

GeneralisedParallel p es q r ->

do addDiags [mkDiag Debug "Generalised parallel" proc]

(pComms, pFQTerm) <- anaProcTerm p gVars lVars

(synComms, fqEs) <- anaEventSet es

(qComms, qFQTerm) <- anaProcTerm q gVars lVars

let newAlpha = S.unions [pComms, qComms, synComms]

let fqProc = FQProcess (GeneralisedParallel pFQTerm fqEs qFQTerm r)

newAlpha r

return (newAlpha, fqProc)

AlphabetisedParallel p esp esq q r ->

do addDiags [mkDiag Debug "Alphabetised parallel" proc]

(pComms, pFQTerm) <- anaProcTerm p gVars lVars

(pSynComms, fqEsp) <- anaEventSet esp

checkCommAlphaSub pSynComms pComms proc "alphabetised parallel, left"

(qSynComms, fqEsq) <- anaEventSet esq

(qComms, qFQTerm) <- anaProcTerm q gVars lVars

checkCommAlphaSub qSynComms qComms proc

"alphabetised parallel, right"

let newAlpha = pComms `S.union` qComms

let fqProc = FQProcess (AlphabetisedParallel pFQTerm fqEsp fqEsq

qFQTerm r) newAlpha r

return (newAlpha, fqProc)

Hiding p es r ->

do addDiags [mkDiag Debug "Hiding" proc]

(pComms, pFQTerm) <- anaProcTerm p gVars lVars

(hidComms, fqEs) <- anaEventSet es

return (pComms `S.union` hidComms, FQProcess (Hiding pFQTerm fqEs r)

(pComms `S.union` hidComms) r)

RenamingProcess p renaming r ->

do addDiags [mkDiag Debug "Renaming" proc]

(pComms, pFQTerm) <- anaProcTerm p gVars lVars

(renAlpha, fqRenaming) <- anaRenaming renaming

let newAlpha = pComms `S.union` renAlpha

let fqProc = FQProcess (RenamingProcess pFQTerm fqRenaming r)

(pComms `S.union` renAlpha) r

return (newAlpha, fqProc)

ConditionalProcess f p q r ->

do addDiags [mkDiag Debug "Conditional" proc]

(pComms, pFQTerm) <- anaProcTerm p gVars lVars

(qComms, qFQTerm) <- anaProcTerm q gVars lVars

-- mfs is the fully qualified formula version of f

mfs <- anaFormulaCspCASL (gVars `Map.union` lVars) f

let fFQ = case mfs of

Nothing -> f -- use old formula as the fully

-- qualified version - there is a

-- error in the spec anyway as the

-- formula could not be fully

-- qualified.

Just fs -> fs -- use the real fully qualified formula

let fComms = case mfs of

Nothing -> S.empty

Just fs -> formulaComms fs

let newAlpha = S.unions [pComms, qComms, fComms]

let fqProc = FQProcess (ConditionalProcess

(fFQ) pFQTerm qFQTerm r)

newAlpha r

return (newAlpha, fqProc)

FQProcess _ _ _ ->

error "CspCASL.StatAnaCSP.anaProcTerm: Unexpected FQProcess"

-- | Statically analyse a CspCASL "named process" term. Return the

-- permitted alphabet of the process and also a list of the fully qualified

-- version of the inputted terms.

-- BUG !!! the FQ_PROCESS_NAME may actually need to be a simple process name

anaNamedProc :: PROCESS -> FQ_PROCESS_NAME -> [TERM ()] -> ProcVarMap ->

State CspCASLSign (CommAlpha, [TERM ()])

anaNamedProc proc pn terms procVars = do

maybeFqPn <- anaProcName pn (length terms)

-- sig <- get

-- let ext = extendedInfo sig

-- procDecls = procSet ext

-- prof = error "NYI: CspCASL.StatAnaCSP.anaNamedProc: Sentence not\

-- \ implemented with new signatures\

-- \ yet" -- pn `Map.lookup` procDecls

case maybeFqPn of

Nothing ->

-- Return the empty alphabet and the original

-- terms. There is an error in the spec.

return (S.empty, terms)

Just fqPn ->

case fqPn of

PROCESS_NAME _ ->

error "CspCasl.StatAnaCSP.anaNamedProc: Impossible case"

PARSED_FQ_PROCESS_NAME _ _ _ ->

error "CspCasl.StatAnaCSP.anaNamedProc: Impossible case"

FQ_PROCESS_NAME _ (ProcProfile varSorts permAlpha) ->

if (length terms) == (length varSorts)

then do fqTerms <-

mapM (anaNamedProcTerm procVars) (zip terms varSorts)

-- Return the permitted alphabet of the process and

-- the fully qualifed terms

return (permAlpha, fqTerms)

else do let err = "Wrong number of arguments in named process"

addDiags [mkDiag Error err proc]

-- Return the empty alphabet and the original

-- terms. There is an error in the spec.

return (S.empty, terms)

-- | Statically analysis a CASL term occurring in a CspCASL "named

-- process" term.

anaNamedProcTerm :: ProcVarMap -> ((TERM ()), SORT) ->

State CspCASLSign (TERM ())

anaNamedProcTerm pm (t, expSort) = do

mt <- anaTermCspCASL pm t

case mt of

Nothing -> return t -- CASL term analysis failed. Use old term

-- as the fully qualified term, there is a

-- error in the spec anyway.

(Just at) -> do at' <- ccTermCast at expSort -- attempt cast;

case at' of

Nothing -> -- Use old term as the fully

-- qualified term, there is a error

-- in the spec anyway.

return t

(Just at'') -> return at'' -- Use the fully

-- qualified

-- (possibly cast)

-- term

-- Static analysis of event sets and communication types

-- | Statically analyse a CspCASL event set. Returns the alphabet of

-- the event set and a fully qualified version of the event set.

anaEventSet :: EVENT_SET -> State CspCASLSign (CommAlpha, EVENT_SET)

anaEventSet eventSet =

case eventSet of

EventSet es r ->

do sig <- get

-- fqEsElems is built the reversed order for efficiency.

(comms, fqEsElems) <- Monad.foldM (anaCommType sig)

(S.empty, []) es

vds <- gets envDiags

put sig { envDiags = vds }

-- reverse the list inside the event set

return (comms, FQEventSet (reverse fqEsElems) r)

FQEventSet _ _ ->

error "CspCASL.StatAnaCSP.anaEventSet: Unexpected FQEventSet"

-- | Statically analyse a proc alphabet (i.e., a list of channel and sort

-- identifiers) to yeild a list of sorts and typed channel names. We also check

-- the parameter sorts and actually construct a process profile.

anaProcAlphabet :: PROC_ARGS -> PROC_ALPHABET ->

State CspCASLSign ProcProfile

anaProcAlphabet argSorts (ProcAlphabet commTypes _) = do

sig <- get

checkSorts argSorts -- check argument sorts are known build alphabet: set of

-- CommType values. We do not need the fully qualfied commTypes that are

-- returned (these area used for analysing Event Sets)

(alpha, _ ) <- Monad.foldM (anaCommType sig) (S.empty, []) commTypes

let profile =

closeProcProfileSortRel (sortRel sig) (ProcProfile argSorts alpha)

return profile

-- | Statically analyse a CspCASL communication type. Returns the

-- extended alphabet and the extended list of fully qualified event

-- set elements - [CommType].

anaCommType :: CspCASLSign -> (CommAlpha, [CommType]) -> COMM_TYPE ->

State CspCASLSign (CommAlpha, [CommType])

anaCommType sig (alpha, fqEsElems) ct =

if ctSort `S.member` (sortSet sig)

then -- ct is a sort name; insert sort into alpha and add a sort

-- to the fully qualified event set elements.

do let newAlpha = S.insert (CommTypeSort ctSort) alpha

let newFqEsElems = (CommTypeSort ctSort) : fqEsElems

return (newAlpha, newFqEsElems)

else -- ct not a sort name, so should be a channel name

case Map.lookup ct (chans $ extendedInfo sig) of

Just s -> -- ct is a channel name; insert typed chan name

-- into alpha and add typed channel to the fully

-- qualified event set elemenets.

let newAlpha = S.insert (mkTypedChan ct s) alpha

newFqEsElems = (mkTypedChan ct s) : fqEsElems

in return (newAlpha, newFqEsElems)

Nothing -> do let err = "not a sort or channel name"

addDiags [mkDiag Error err ct]

-- failed, thus error in spec, return the

-- unmodified alphabet and the unmodifled

-- fully qualified event set elements.

return (alpha, fqEsElems)

where ctSort = simpleIdToId ct

mkTypedChan c s = CommTypeChan $ TypedChanName c s

-- Static analysis of events

-- | Statically analyse a CspCASL event. Returns a constituent

-- communication alphabet of the event, mapping for any new

-- locally bound variables and a fully qualified version of the event.

anaEvent :: EVENT -> ProcVarMap ->

State CspCASLSign (CommAlpha, ProcVarMap, EVENT)

anaEvent e vars =

case e of

TermEvent t range ->

do addDiags [mkDiag Debug "Term event" e]

(alpha, newVars, fqTerm) <- anaTermEvent t vars

let fqEvent = FQEvent e Nothing fqTerm range

return (alpha, newVars, fqEvent)

InternalPrefixChoice v s range ->

do addDiags [mkDiag Debug "Internal prefix event" e]

(alpha, newVars, fqVar) <- anaPrefixChoice v s

let fqEvent = FQEvent e Nothing fqVar range

return (alpha, newVars, fqEvent)

ExternalPrefixChoice v s range ->

do addDiags [mkDiag Debug "External prefix event" e]

(alpha, newVars, fqVar) <- anaPrefixChoice v s

let fqEvent = FQEvent e Nothing fqVar range

return (alpha, newVars, fqEvent)

ChanSend c t range ->

do addDiags [mkDiag Debug "Channel send event" e]

-- mfqChan is a maybe fully qualified

-- channel. It will be Nothing if

-- annChanSend failed - i.e. we forget

-- about the channel.

(alpha, newVars, mfqChan, fqTerm) <- anaChanSend c t vars

let fqEvent = FQEvent e mfqChan fqTerm range

return (alpha, newVars, fqEvent)

ChanNonDetSend c v s range ->

do addDiags [mkDiag Debug "Channel nondeterministic send event" e]

-- mfqChan is the same as in chanSend case.

-- fqVar is the fully qualfied version of the variable.

(alpha, newVars, mfqChan, fqVar) <- anaChanBinding c v s

let fqEvent = FQEvent e mfqChan fqVar range

return (alpha, newVars, fqEvent)

ChanRecv c v s range ->

do addDiags [mkDiag Debug "Channel receive event" e]

-- mfqChan is the same as in chanSend case.

-- fqVar is the fully qualfied version of the variable.

(alpha, newVars, mfqChan, fqVar) <- anaChanBinding c v s

let fqEvent = FQEvent e mfqChan fqVar range

return (alpha, newVars, fqEvent)

FQEvent _ _ _ _ ->

error "CspCASL.StatAnaCSP.anaEvent: Unexpected FQEvent"

-- | Statically analyse a CspCASL term event. Returns a constituent

-- communication alphabet of the event and a mapping for any new

-- locally bound variables and the fully qualified version of the

-- term.

anaTermEvent :: (TERM ()) -> ProcVarMap ->

State CspCASLSign (CommAlpha, ProcVarMap, TERM ())

anaTermEvent t vars = do

mt <- anaTermCspCASL vars t

let (alpha, t') = case mt of

-- return the alphabet and the fully qualified term

Just at -> ([(CommTypeSort (sortOfTerm at))], at)

-- return the empty alphabet and the original term

Nothing -> ([], t)

return (S.fromList alpha, Map.empty, t')

-- | Statically analyse a CspCASL internal or external prefix choice

-- event. Returns a constituent communication alphabet of the event

-- and a mapping for any new locally bound variables and the fully

-- qualified version of the variable.

anaPrefixChoice :: VAR -> SORT ->

State CspCASLSign (CommAlpha, ProcVarMap, TERM ())

anaPrefixChoice v s = do

checkSorts [s] -- check sort is known

let alpha = S.singleton $ CommTypeSort s

let binding = Map.singleton v s

let fqVar = Qual_var v s nullRange

return (alpha, binding, fqVar)

-- | Statically analyse a CspCASL channel send event. Returns a

-- constituent communication alphabet of the event, a mapping for

-- any new locally bound variables, a fully qualified channel (if

-- possible) and the fully qualified version of the term.

anaChanSend :: CHANNEL_NAME -> (TERM ()) -> ProcVarMap ->

State CspCASLSign (CommAlpha, ProcVarMap,

(Maybe (CHANNEL_NAME, SORT)), TERM ())

anaChanSend c t vars = do

sig <- get

let ext = extendedInfo sig

case c `Map.lookup` (chans ext) of

Nothing -> do

addDiags [mkDiag Error "unknown channel" c]

-- Use old term as the fully qualified term and forget about the

-- channel, there is an error in the spec

return (S.empty, Map.empty, Nothing, t)

Just chanSort -> do

mt <- anaTermCspCASL vars t

case mt of

Nothing -> -- CASL analysis failed. Use old term as the fully

-- qualified term and forget about the channel,

-- there is an error in the spec.

return (S.empty, Map.empty, Nothing, t)

(Just at) ->

do mc <- ccTermCast at chanSort

case mc of

Nothing -> -- cast failed. Use old term as the fully

-- qualified term, and forget about the

-- channel there is an error in the spec.

return (S.empty, Map.empty, Nothing, t)

(Just ct) ->

do let castSort = sortOfTerm ct

alpha = [CommTypeSort castSort

,CommTypeChan $ TypedChanName c castSort

]

-- Use the real fully qualified term. We do

-- not want to use a cast term here. A cast

-- must be possible, but we do not want to

-- force it!

return (S.fromList alpha, Map.empty,

Just (c, chanSort), at)

-- | Statically analyse a CspCASL "binding" channel event (which is

-- either a channel nondeterministic send event or a channel receive

-- event). Returns a constituent communication alphabet of the event,

-- a mapping for any new locally bound variables, a fully qualified

-- channel (if possible) and the fully qualified version of the

-- variable.

anaChanBinding :: CHANNEL_NAME -> VAR -> SORT ->

State CspCASLSign( CommAlpha,

ProcVarMap,

(Maybe (CHANNEL_NAME, SORT)), TERM ()

)

anaChanBinding c v s = do

checkSorts [s] -- check sort is known

sig <- get

let ext = extendedInfo sig

case c `Map.lookup` (chans ext) of

Nothing -> do

addDiags [mkDiag Error "unknown channel" c]

-- No fully qualified channel, use Nothing - there is a error in

-- the spec anyway. Use the real fully qualified variable

-- version with a nullRange.

return (S.empty, Map.empty, Nothing, (Qual_var v s nullRange))

Just chanSort -> do

if s `S.member` (chanSort `S.insert` (subsorts chanSort))

then do let alpha = [CommTypeSort s

,CommTypeChan (TypedChanName c s)]

let binding = [(v, s)]

-- Return the alphabet, var mapping, the fully

-- qualfied channel and fully qualfied

-- variable. Notice that the fully qualified

-- channel's sort should be the lowest sort we can

-- communicate in i.e. the sort of the variable.

return (S.fromList alpha, Map.fromList binding,

(Just (c,s)), (Qual_var v s nullRange))

else do let err = "sort not a subsort of channel's sort"

addDiags [mkDiag Error err s]

-- There is a error in the spec, but return

-- the alphabet, var mapping, the fully

-- qualfied channel and fully qualfied

-- variable - as we can.

return (S.empty, Map.empty, (Just (c,s)),

(Qual_var v s nullRange))

where subsorts = Rel.predecessors (sortRel sig)

-- Static analysis of renaming and renaming items

-- | Statically analyse a CspCASL renaming. Returns the alphabet and

-- | the fully qualified renaming.

anaRenaming :: RENAMING -> State CspCASLSign (CommAlpha, RENAMING)

anaRenaming renaming = case renaming of

Renaming r -> do

(al, fqRenamingTermsMaybes) <- Monad.foldM anaRenamingItem (S.empty, []) r

return (al, FQRenaming fqRenamingTermsMaybes)

FQRenaming _ ->

error "CspCASL.StatAnaCSP.anaRenaming: Unexpected FQRenaming"

-- | Statically analyse a CspCASL renaming item. Return the alphabet

-- | and the fully qualified list of renaming functions and predicates.

anaRenamingItem :: (CommAlpha, [TERM ()]) -> Id ->

State CspCASLSign (CommAlpha, [TERM ()])

anaRenamingItem (inAl, fqRenamingTerms) ri = do

-- BUG -- too many nothings - should only be one

totOps <- getUnaryOpsById ri Total

if (not $ S.null totOps)

then return (inAl `S.union` totOps, fqRenamingTerms)

else do

parOps <- getUnaryOpsById ri Partial

if not (S.null parOps)

then return (inAl `S.union` parOps, fqRenamingTerms)

else do

preds <- getBinPredsById ri

if not (S.null preds)

then return (inAl `S.union` preds, fqRenamingTerms)

else do

let err = "renaming item not a binary "

++ "operation or predicate name"

addDiags [mkDiag Error err ri]

-- return the original alphabet and the original fully

-- qualified terms (renamings) with out any modification

-- as there is an error in the spec.

return (inAl, fqRenamingTerms)

-- | Given a CASL identifier and a `function kind' (total or partial),

-- find all unary operations of that kind with that name in the CASL

-- signature, and return a set of corresponding communication types

-- for those operations.

getUnaryOpsById :: Id -> OpKind -> State CspCASLSign (S.Set CommType)

getUnaryOpsById ri kind = do

sig <- get

let opsWithId = Map.findWithDefault S.empty ri (opMap sig)

binOpsKind = S.filter (isBin kind) opsWithId

cts = S.map CommTypeSort $ S.fold opSorts S.empty binOpsKind

return cts

where isBin k ot = (k == opKind ot) && (1 == (length (opArgs ot)))

opSorts o inS = inS `S.union` (S.fromList ((opArgs o) ++ [opRes o]))

-- | Given a CASL identifier find all binary predicates with that name

-- in the CASL signature, and return a set of corresponding

-- communication types for those predicates.

getBinPredsById :: Id -> State CspCASLSign (S.Set CommType)

getBinPredsById ri = do

sig <- get

let predsWithId = Map.findWithDefault S.empty ri (predMap sig)

binPreds = S.filter isBin predsWithId

cts = S.map CommTypeSort $ S.fold predSorts S.empty binPreds

return cts

where isBin ot = (2 == (length (predArgs ot)))

predSorts p inS = inS `S.union` (S.fromList (predArgs p))

-- | Given two CspCASL communication alphabets, check that the first's

-- subsort closure is a subset of the second's subsort closure.

checkCommAlphaSub :: CommAlpha -> CommAlpha -> PROCESS -> String ->

State CspCASLSign ()

checkCommAlphaSub sub super proc context = do

sig <- get

let sr = sortRel sig

let extras = ((closeCspCommAlpha sr sub) `S.difference`

(closeCspCommAlpha sr super))

if S.null extras

then do return ()

else do let err = ("Communication alphabet subset violations (" ++

context ++ "): " ++ (show $ S.toList extras))

addDiags [mkDiag Error err proc]

return ()

-- Static analysis of CASL terms occurring in CspCASL process terms.

-- | Statically analyse a CASL term appearing in a CspCASL process;

-- any in-scope process variables are added to the signature before

-- performing the analysis.

anaTermCspCASL :: ProcVarMap -> (TERM ()) ->

State CspCASLSign (Maybe (TERM ()))

anaTermCspCASL pm t = do

sig <- get

let newVars = Map.union pm (varMap sig)

sigext = sig { varMap = newVars }

Result ds mt = anaTermCspCASL' sigext t

addDiags ds

return mt

idSetOfSig :: CspCASLSign -> IdSets

idSetOfSig sig =

unite [mkIdSets (allConstIds sig) (allOpIds sig) $ allPredIds sig]

-- | Statically analyse a CASL term in the context of a CspCASL

-- signature. If successful, returns a fully-qualified term.

anaTermCspCASL' :: CspCASLSign -> TERM () -> Result (TERM ())

anaTermCspCASL' sig trm = do

let ga = globAnnos sig

mix = extendMix (Map.keysSet $ varMap sig)

emptyMix { mixRules = makeRules ga $ idSetOfSig sig }

resT <- resolveMixfix (putParen mix) (mixResolve mix)

ga (mixRules mix) trm

oneExpTerm (const return) sig resT

-- | Attempt to cast a CASL term to a particular CASL sort.

ccTermCast :: (TERM ()) -> SORT -> State CspCASLSign (Maybe (TERM ()))

ccTermCast t cSort =

if termSort == (cSort)

then return (Just t)

else do sig <- get

if Rel.member termSort cSort (sortRel sig)

then do let err = "upcast term to " ++ (show cSort)

addDiags [mkDiag Debug err t]

return (Just (Sorted_term t cSort (getRange t)))

else if Rel.member cSort termSort (sortRel sig)

then do let err = "downcast term to " ++ (show cSort)

addDiags [mkDiag Debug err t]

return (Just (Cast t cSort (getRange t)))

else do let err = "can't cast term to sort " ++

(show cSort)

addDiags [mkDiag Error err t]

return Nothing

where termSort = (sortOfTerm t)

-- Static analysis of CASL formulae occurring in CspCASL process

-- terms.

-- | Statically analyse a CASL formula appearing in a CspCASL process;

-- any in-scope process variables are added to the signature before

-- performing the analysis.

anaFormulaCspCASL :: ProcVarMap -> (FORMULA ()) ->

State CspCASLSign (Maybe (FORMULA ()))

anaFormulaCspCASL pm f = do

addDiags [mkDiag Debug "anaFormulaCspCASL" f]

sig <- get

let newVars = Map.union pm (varMap sig)

sigext = sig { varMap = newVars }

Result ds mt = anaFormulaCspCASL' sigext f

addDiags ds

return mt

-- | Statically analyse a CASL formula in the context of a CspCASL

-- signature. If successful, returns a fully-qualified formula.

anaFormulaCspCASL' :: CspCASLSign -> FORMULA () -> Result (FORMULA ())

anaFormulaCspCASL' sig frm = do

let ga = globAnnos sig

mix = extendMix (Map.keysSet $ varMap sig)

emptyMix { mixRules = makeRules ga $ idSetOfSig sig }

resF <- resolveFormula (putParen mix) (mixResolve mix) ga (mixRules mix) frm

minExpFORMULA (const return) sig resF

-- | Compute the communication alphabet arising from a formula

-- occurring in a CspCASL process term.

formulaComms :: (FORMULA ()) -> CommAlpha

formulaComms f = case f of

Quantification _ varDecls f' _ ->

(formulaComms f') `S.union` S.fromList vdSorts

where vdSorts = (map (CommTypeSort . vdSort) varDecls)

vdSort (Var_decl _ s _) = s

Conjunction fs _ -> S.unions (map formulaComms fs)

Disjunction fs _ -> S.unions (map formulaComms fs)

Implication f1 f2 _ _ -> (formulaComms f1) `S.union` (formulaComms f2)

Equivalence f1 f2 _ -> (formulaComms f1) `S.union` (formulaComms f2)

Negation f' _ -> formulaComms f'

Definedness t _ -> S.singleton (CommTypeSort (sortOfTerm t))

Existl_equation t1 t2 _ -> S.fromList [CommTypeSort (sortOfTerm t1),

CommTypeSort (sortOfTerm t2)]

Strong_equation t1 t2 _ -> S.fromList [CommTypeSort (sortOfTerm t1),

CommTypeSort (sortOfTerm t2)]

Membership t s _ -> S.fromList [CommTypeSort (sortOfTerm t),

CommTypeSort s]

Mixfix_formula t -> S.singleton (CommTypeSort (sortOfTerm t))

_ -> S.empty