2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann{- |

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannModule : $Id$

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannDescription : static analysis for CspCASL

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCopyright : (c) Markus Roggenbach, Till Mossakowski, Uni Bremen 2004-2005

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannMaintainer : M.Roggenbach@swansea.ac.uk

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannStability : provisional

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannPortability : portable

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannstatic analysis for CSP-CASL

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann-}

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann{- todo:

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann most of the process and channel analysis missing

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann sentences are completely missing:

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann use equation systems of processes, like:

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann spec hugo =

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann data ...

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann channel ...

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann process A = a->A

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann process P = ...A...Q...

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Q = ...P....

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann R = a->P

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann reveal R

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannreveal R should keep CASL data part, and reveal process R

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann-}

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannmodule CspCASL.StatAnaCSP where

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport CASL.Sign

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport Common.AS_Annotation

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport Common.Result

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport Common.GlobalAnnotations

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport Common.Id

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport qualified Data.Map as Map

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport Common.Lib.State

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport CspCASL.AS_CspCASL (BASIC_CSP_CASL_SPEC(..))

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport CspCASL.AS_CspCASL_Process (PROCESS_DEFN(..),

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann CHANNEL_DECL(..),

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann CHANNEL_ITEM(..)

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann )

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport CspCASL.SignCSP

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann-- This is a very null analysis function, returning as it does

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann-- essentially unchanged data.

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannbasicAnalysisCspCASL :: (BASIC_CSP_CASL_SPEC, CSPSign, GlobalAnnos)

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann -> Result (BASIC_CSP_CASL_SPEC, CSPSign, [Named ()])

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannbasicAnalysisCspCASL (Basic_Csp_Casl_Spec dd p, sigma, _ga) =

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann do let ((ch',p'), accSig) = runState (ana_BASIC_CSP ((Channel_items []),(Process p))) sigma

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann ds = reverse $ envDiags accSig

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Result ds (Just ()) -- insert diags

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann return (Basic_Csp_Casl_Spec dd p, accSig, [])

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann-- | the main CspCASL analysis function

ana_BASIC_CSP :: (CHANNEL_DECL, PROCESS_DEFN)

-> State CSPSign (CHANNEL_DECL, PROCESS_DEFN)

ana_BASIC_CSP (ch, p) = do

ch' <- anaChannels ch

p' <- anaProcesses p

return (ch',p')

anaChannels :: CHANNEL_DECL -> State CSPSign CHANNEL_DECL

anaChannels (Channel_items cits) =

fmap Channel_items $ mapM (anaChannel) cits

anaChannel :: CHANNEL_ITEM -> State CSPSign CHANNEL_ITEM

anaChannel chdecl@(Channel_decl newnames s) = do

checkSorts [s]

sig <- get

let ext = extendedInfo sig

oldchn = channelNames ext

-- test for double declaration with different sorts should be added

let ins m n = Map.insert (mkId [n]) s m

put sig { extendedInfo = ext { channelNames = foldl ins oldchn newnames } }

return chdecl

anaProcesses :: PROCESS_DEFN -> State CSPSign PROCESS_DEFN

anaProcesses p = return p