Hets - the Heterogeneous Tool Set

Copyright(c) Andy Gimblett Liam O'Reilly Markus Roggenbach
Swansea University 2008 C. Maeder DFKI 2011
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

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/

Synopsis

Documentation

basicAnalysisCspCASL :: (CspBasicSpec, CspCASLSign, GlobalAnnos) -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen]) Source #

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.

anaChanDecl :: CHANNEL_DECL -> State CspCASLSign () Source #

Statically analyse a CspCASL channel declaration.

anaChannelName :: SORT -> ChanNameMap -> CHANNEL_NAME -> State CspCASLSign ChanNameMap Source #

Statically analyse a CspCASL channel name.

anaProcItem :: Mix b s () () -> Annoted PROC_ITEM -> State CspCASLSign () Source #

Statically analyse a CspCASL process item.

anaProcDecl :: PROCESS_NAME -> PROC_ARGS -> PROC_ALPHABET -> State CspCASLSign () Source #

Statically analyse a CspCASL process declaration.

findProfileForProcName :: FQ_PROCESS_NAME -> Int -> ProcNameMap -> State CspCASLSign (Maybe ProcProfile) Source #

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) Source #

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 () Source #

Statically analyse a CspCASL process equation.

anaProcVars :: FQ_PROCESS_NAME -> [SORT] -> [VAR] -> State CspCASLSign ProcVarList Source #

Statically analyse a CspCASL process equation's global variable names.

anaProcVar :: ProcVarList -> (VAR, SORT) -> State CspCASLSign ProcVarList Source #

Statically analyse a CspCASL process-global variable name.

anaNamedProc :: Mix b s () () -> PROCESS -> FQ_PROCESS_NAME -> [TERM ()] -> ProcVarMap -> State CspCASLSign (FQ_PROCESS_NAME, CommAlpha, [TERM ()]) Source #

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 ()) Source #

Statically analysis a CASL term occurring in a CspCASL "named process" term.

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

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 Source #

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]) Source #

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) Source #

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 ()) Source #

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 ()) Source #

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 ()) Source #

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.

anaChanBinding :: CHANNEL_NAME -> VAR -> SORT -> State CspCASLSign (CommAlpha, ProcVarMap, (CHANNEL_NAME, SORT), TERM ()) Source #

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) Source #

Statically analyse a CspCASL renaming. Returns the alphabet and the fully qualified renaming.

anaRenamingItem :: Rename -> State CspCASLSign [Rename] Source #

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))] Source #

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)] Source #

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 () Source #

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 ())) Source #

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' :: Mix b s () () -> CspCASLSign -> TERM () -> Result (TERM ()) Source #

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 ()) Source #

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

anaFormulaCspCASL :: Mix b s () () -> ProcVarMap -> FORMULA () -> State CspCASLSign (Maybe (FORMULA ())) Source #

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 ()) Source #

Statically analyse a CASL formula in the context of a CspCASL signature. If successful, returns a fully-qualified formula.

formulaComms :: FORMULA () -> CommAlpha Source #

Compute the communication alphabet arising from a formula occurring in a CspCASL process term.