| Copyright | (c) Andy Gimblett, Liam O'Reilly, Markus Roggenbach, Swansea University 2008, C. Maeder, DFKI 2011 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
CspCASL.StatAnaCSP
Description
Static analysis of CSP-CASL specifications, following "Tool Support for CSP-CASL", MPhil thesis by Andy Gimblett, 2008. http://www.cs.swan.ac.uk/~csandy/mphil/
- type CspBasicSpec = BASIC_SPEC CspBasicExt () CspSen
- basicAnalysisCspCASL :: (CspBasicSpec, CspCASLSign, GlobalAnnos) -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen])
- basicAnaAux :: (CspBasicSpec, CspCASLSign, GlobalAnnos) -> Result (CspBasicSpec, ExtSign CspCASLSign Symbol, [Named CspCASLSen])
- ana_BASIC_CSP :: Ana CspBasicExt CspBasicExt () CspSen CspSign
- anaChanDecl :: CHANNEL_DECL -> State CspCASLSign ()
- anaChannelName :: SORT -> ChanNameMap -> CHANNEL_NAME -> State CspCASLSign ChanNameMap
- anaProcItem :: Mix b s () () -> Annoted PROC_ITEM -> State CspCASLSign ()
- anaProcDecl :: PROCESS_NAME -> PROC_ARGS -> PROC_ALPHABET -> State CspCASLSign ()
- findProfileForProcName :: FQ_PROCESS_NAME -> Int -> ProcNameMap -> State CspCASLSign (Maybe ProcProfile)
- anaProcName :: FQ_PROCESS_NAME -> Int -> State CspCASLSign (Maybe FQ_PROCESS_NAME)
- anaProcEq :: Mix b s () () -> Annoted a -> PARM_PROCNAME -> PROCESS -> State CspCASLSign ()
- anaProcVars :: FQ_PROCESS_NAME -> [SORT] -> [VAR] -> State CspCASLSign ProcVarList
- anaProcVar :: ProcVarList -> (VAR, SORT) -> State CspCASLSign ProcVarList
- anaProcTerm :: Mix b s () () -> PROCESS -> ProcVarMap -> ProcVarMap -> State CspCASLSign (CommAlpha, PROCESS)
- anaNamedProc :: Mix b s () () -> PROCESS -> FQ_PROCESS_NAME -> [TERM ()] -> ProcVarMap -> State CspCASLSign (FQ_PROCESS_NAME, CommAlpha, [TERM ()])
- anaNamedProcTerm :: Mix b s () () -> ProcVarMap -> (TERM (), SORT) -> State CspCASLSign (TERM ())
- anaEventSet :: EVENT_SET -> State CspCASLSign (CommAlpha, EVENT_SET)
- anaProcAlphabet :: PROC_ARGS -> PROC_ALPHABET -> State CspCASLSign ProcProfile
- anaCommType :: CspCASLSign -> (CommAlpha, [CommType]) -> CommType -> State CspCASLSign (CommAlpha, [CommType])
- anaEvent :: Mix b s () () -> EVENT -> ProcVarMap -> State CspCASLSign (CommAlpha, ProcVarMap, EVENT)
- anaTermEvent :: Mix b s () () -> TERM () -> ProcVarMap -> State CspCASLSign (CommAlpha, ProcVarMap, TERM ())
- anaPrefixChoice :: VAR -> SORT -> State CspCASLSign (CommAlpha, ProcVarMap, TERM ())
- anaChanSend :: Mix b s () () -> CHANNEL_NAME -> TERM () -> ProcVarMap -> State CspCASLSign (CommAlpha, ProcVarMap, (CHANNEL_NAME, SORT), TERM ())
- getDeclaredChanSort :: (CHANNEL_NAME, SORT) -> CspCASLSign -> Result SORT
- anaChanBinding :: CHANNEL_NAME -> VAR -> SORT -> State CspCASLSign (CommAlpha, ProcVarMap, (CHANNEL_NAME, SORT), TERM ())
- anaRenaming :: RENAMING -> State CspCASLSign (CommAlpha, RENAMING)
- alphaOfRename :: Rename -> Set SORT
- anaRenamingItem :: Rename -> State CspCASLSign [Rename]
- getUnaryOpsById :: Id -> State CspCASLSign [(OpKind, (SORT, SORT))]
- getBinPredsById :: Id -> State CspCASLSign [(SORT, SORT)]
- checkCommAlphaSub :: CommAlpha -> CommAlpha -> PROCESS -> String -> State CspCASLSign ()
- anaTermCspCASL :: Mix b s () () -> ProcVarMap -> TERM () -> State CspCASLSign (Maybe (TERM ()))
- idSetOfSig :: CspCASLSign -> IdSets
- anaTermCspCASL' :: Mix b s () () -> CspCASLSign -> TERM () -> Result (TERM ())
- ccTermCast :: TERM () -> SORT -> CspCASLSign -> Result (TERM ())
- anaFormulaCspCASL :: Mix b s () () -> ProcVarMap -> FORMULA () -> State CspCASLSign (Maybe (FORMULA ()))
- anaFormulaCspCASL' :: Mix b s () () -> CspCASLSign -> FORMULA () -> Result (FORMULA ())
- formulaComms :: FORMULA () -> CommAlpha
Documentation
type CspBasicSpec = BASIC_SPEC CspBasicExt () CspSen
basicAnalysisCspCASL :: (CspBasicSpec, CspCASLSign, GlobalAnnos) -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen])
The first element of the returned pair (CspBasicSpec) is the same as the inputted version just with some very minor optimisations - none in our case, but for CASL - brackets are otimized. This all that happens, the mixfixed terms are still mixed fixed terms in the returned version.
basicAnaAux :: (CspBasicSpec, CspCASLSign, GlobalAnnos) -> Result (CspBasicSpec, ExtSign CspCASLSign Symbol, [Named CspCASLSen])
anaChanDecl :: CHANNEL_DECL -> State CspCASLSign ()
Statically analyse a CspCASL channel declaration.
anaChannelName :: SORT -> ChanNameMap -> CHANNEL_NAME -> State CspCASLSign ChanNameMap
Statically analyse a CspCASL channel name.
anaProcItem :: Mix b s () () -> Annoted PROC_ITEM -> State CspCASLSign ()
Statically analyse a CspCASL process item.
anaProcDecl :: PROCESS_NAME -> PROC_ARGS -> PROC_ALPHABET -> State CspCASLSign ()
Statically analyse a CspCASL process declaration.
findProfileForProcName :: FQ_PROCESS_NAME -> Int -> ProcNameMap -> State CspCASLSign (Maybe ProcProfile)
Find a profile for a process name. Either the profile is given via a parsed fully qualified process name, in which case we check everything is valid and the process name with the profile is known. Or its a plain process name where we must deduce a unique profile if possible. We also know how many variables / parameters the process name has.
anaProcName :: FQ_PROCESS_NAME -> Int -> State CspCASLSign (Maybe FQ_PROCESS_NAME)
Analyse a process name an return a fully qualified one if possible. We also know how many variables / parameters the process name has.
anaProcEq :: Mix b s () () -> Annoted a -> PARM_PROCNAME -> PROCESS -> State CspCASLSign ()
Statically analyse a CspCASL process equation.
anaProcVars :: FQ_PROCESS_NAME -> [SORT] -> [VAR] -> State CspCASLSign ProcVarList
Statically analyse a CspCASL process equation's global variable names.
anaProcVar :: ProcVarList -> (VAR, SORT) -> State CspCASLSign ProcVarList
Statically analyse a CspCASL process-global variable name.
anaProcTerm :: Mix b s () () -> PROCESS -> ProcVarMap -> ProcVarMap -> State CspCASLSign (CommAlpha, PROCESS)
anaNamedProc :: Mix b s () () -> PROCESS -> FQ_PROCESS_NAME -> [TERM ()] -> ProcVarMap -> State CspCASLSign (FQ_PROCESS_NAME, CommAlpha, [TERM ()])
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
anaNamedProcTerm :: Mix b s () () -> ProcVarMap -> (TERM (), SORT) -> State CspCASLSign (TERM ())
Statically analysis a CASL term occurring in a CspCASL "named process" term.
anaEventSet :: EVENT_SET -> State CspCASLSign (CommAlpha, EVENT_SET)
Statically analyse a CspCASL event set. Returns the alphabet of the event set and a fully qualified version of the event set.
anaProcAlphabet :: PROC_ARGS -> PROC_ALPHABET -> State CspCASLSign ProcProfile
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.
anaCommType :: CspCASLSign -> (CommAlpha, [CommType]) -> CommType -> State CspCASLSign (CommAlpha, [CommType])
Statically analyse a CspCASL communication type. Returns the extended alphabet and the extended list of fully qualified event set elements - [CommType].
anaEvent :: Mix b s () () -> EVENT -> ProcVarMap -> State CspCASLSign (CommAlpha, ProcVarMap, EVENT)
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.
anaTermEvent :: Mix b s () () -> TERM () -> ProcVarMap -> State CspCASLSign (CommAlpha, ProcVarMap, TERM ())
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.
anaPrefixChoice :: VAR -> SORT -> State CspCASLSign (CommAlpha, ProcVarMap, TERM ())
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.
anaChanSend :: Mix b s () () -> CHANNEL_NAME -> TERM () -> ProcVarMap -> State CspCASLSign (CommAlpha, ProcVarMap, (CHANNEL_NAME, SORT), TERM ())
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.
getDeclaredChanSort :: (CHANNEL_NAME, SORT) -> CspCASLSign -> Result SORT
anaChanBinding :: CHANNEL_NAME -> VAR -> SORT -> State CspCASLSign (CommAlpha, ProcVarMap, (CHANNEL_NAME, SORT), TERM ())
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 and the fully qualified version of the variable.
anaRenaming :: RENAMING -> State CspCASLSign (CommAlpha, RENAMING)
Statically analyse a CspCASL renaming. Returns the alphabet and the fully qualified renaming.
alphaOfRename :: Rename -> Set SORT
anaRenamingItem :: Rename -> State CspCASLSign [Rename]
Statically analyse a CspCASL renaming item. Return the alphabet and the fully qualified list of renaming functions and predicates.
getUnaryOpsById :: Id -> State CspCASLSign [(OpKind, (SORT, SORT))]
Given a CASL identifier, find all unary operations with that name in the CASL signature, and return a list of corresponding profiles, i.e. kind, argument sort and result sort.
getBinPredsById :: Id -> State CspCASLSign [(SORT, SORT)]
Given a CASL identifier find all binary predicates with that name in the CASL signature, and return a list of corresponding profiles.
checkCommAlphaSub :: CommAlpha -> CommAlpha -> PROCESS -> String -> State CspCASLSign ()
Given two CspCASL communication alphabets, check that the first's subsort closure is a subset of the second's subsort closure.
anaTermCspCASL :: Mix b s () () -> ProcVarMap -> TERM () -> State CspCASLSign (Maybe (TERM ()))
Statically analyse a CASL term appearing in a CspCASL process; any in-scope process variables are added to the signature before performing the analysis.
idSetOfSig :: CspCASLSign -> IdSets
anaTermCspCASL' :: Mix b s () () -> CspCASLSign -> TERM () -> Result (TERM ())
Statically analyse a CASL term in the context of a CspCASL signature. If successful, returns a fully-qualified term.
ccTermCast :: TERM () -> SORT -> CspCASLSign -> Result (TERM ())
Attempt to cast a CASL term to a particular CASL sort.
anaFormulaCspCASL :: Mix b s () () -> ProcVarMap -> FORMULA () -> State CspCASLSign (Maybe (FORMULA ()))
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' :: Mix b s () () -> CspCASLSign -> FORMULA () -> Result (FORMULA ())
Statically analyse a CASL formula in the context of a CspCASL signature. If successful, returns a fully-qualified formula.
formulaComms :: FORMULA () -> CommAlpha
Compute the communication alphabet arising from a formula occurring in a CspCASL process term.