Hets - the Heterogeneous Tool Set

Copyright(c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerM.Roggenbach@swansea.ac.uk
Stabilityprovisional
Portabilityportable
Safe HaskellNone

CspCASL.SignCSP

Description

signatures for CSP-CASL

Synopsis

Documentation

addProcNameToProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap -> ProcNameMap

Add a process name and its profile to a process name map. exist.

ccSig2CASLSign :: CspCASLSign -> CASLSign

ccSig2CspSign :: CspCASLSign -> CspSign

Projection from CspCASL signature to Csp signature

type ChanNameMap = MapSet CHANNEL_NAME SORT

closeCspCommAlpha :: Rel SORT -> CommAlpha -> CommAlpha

type CspCASLSign = Sign CspSen CspSign

A CspCASL signature is a CASL signature with a CSP process signature in the extendedInfo part.

type CspCASLSen = FORMULA CspSen

data CspSen

A CspCASl senetence is either a CASL formula or a Procsses equation. A process equation has on the LHS a process name, a list of parameters which are qualified variables (which are terms), a constituent( or is it permitted ?) communication alphabet and finally on the RHS a fully qualified process.

Constructors

ProcessEq FQ_PROCESS_NAME FQProcVarList CommAlpha PROCESS 

Instances

Eq CspSen 
Data CspSen 
Ord CspSen 
Show CspSen 
ShATermConvertible CspSen 
GetRange CspSen 
Pretty CspSen 
TermParser CspSen 
FormExtension CspSen 
TermExtension CspSen 
Typeable * CspSen 
Comorphism CASL2CspCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () 
Comorphism CspCASL2Modal CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () 
Show a => Sentences (GenCspCASL a) CspCASLSen CspCASLSign CspCASLMorphism CspSymbol

Instance of Sentences for CspCASL

Show a => Syntax (GenCspCASL a) CspBasicSpec CspSymbol CspSymbItems CspSymbMapItems

Syntax of CspCASL

Show a => StaticAnalysis (GenCspCASL a) CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol

Static Analysis for CspCASL

CspCASLSemantics a => Logic (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol ()

Instance of Logic for CspCASL

(CspCASLSemantics a, CspCASLSemantics b) => Comorphism (CspCASL2CspCASL a b) (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () (GenCspCASL b) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () 

data CspSign

CSP process signature.

Constructors

CspSign 

Fields

chans :: ChanNameMap
 
procSet :: ProcNameMap
 

Instances

Eq CspSign 
Data CspSign 
Ord CspSign 
Show CspSign 
ShATermConvertible CspSign 
Pretty CspSign

Pretty printing for CspCASL signatures

SignExtension CspSign

Instance for CspCASL signature extension

Typeable * CspSign 
MorphismExtension CspSign CspAddMorphism

Instance for CspCASL morphism extension (used for Category)

Comorphism CASL2CspCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () 
Comorphism CspCASL2Modal CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () 
Show a => Sentences (GenCspCASL a) CspCASLSen CspCASLSign CspCASLMorphism CspSymbol

Instance of Sentences for CspCASL

Show a => StaticAnalysis (GenCspCASL a) CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol

Static Analysis for CspCASL

CspCASLSemantics a => Logic (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol ()

Instance of Logic for CspCASL

(CspCASLSemantics a, CspCASLSemantics b) => Comorphism (CspCASL2CspCASL a b) (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () (GenCspCASL b) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () 

cspSignUnion :: CspSign -> CspSign -> CspSign

plain union

diffCspSig :: CspSign -> CspSign -> CspSign

Compute difference of two CSP process signatures.

emptyCspCASLSign :: CspCASLSign

Empty CspCASL signature.

emptyCspSign :: CspSign

Empty CSP process signature.

type FQProcVarList = [TERM ()]

FQProcVarList should only contain fully qualified CASL variables which are TERMs i.e. constructed via the TERM constructor Qual_var.

getUniqueProfileInProcNameMap :: PROCESS_NAME -> Int -> ProcNameMap -> Result ProcProfile

Given a simple process name and a required number of parameters, find a unqiue profile with that many parameters if possible. If this is not possible (i.e., name does not exist, or no profile with the required number of arguments or not unique profile for the required number of arguments), then the functions returns a failed result with a helpful error message. failure.

isCspCASLSubSig :: CspCASLSign -> CspCASLSign -> Bool

Is one CspCASL Signature a sub signature of another

isCspSubSign :: CspSign -> CspSign -> Bool

Is one Csp Signature a sub signature of another assuming the same data signature for now.

isNameInProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap -> Bool

Test if a simple process name with a profile is in the process name map.

isProcessEq :: CspCASLSen -> Bool

type ProcNameMap = MapSet PROCESS_NAME ProcProfile

type ProcVarList = [(SIMPLE_ID, SORT)]

type ProcVarMap = Map SIMPLE_ID SORT

reduceProcProfile :: Rel SORT -> ProcProfile -> ProcProfile

Remove the implicit sorts from a profile under a sub-sort relation. Assumes all the proc profile's comms are in the sub sort relation and simply makes the comms contain only the minimal super sorts under the sub-sort relation.

commType2Sort :: CommType -> SORT

relatedSorts :: CspCASLSign -> SORT -> SORT -> Bool

relatedProcs :: CspCASLSign -> ProcProfile -> ProcProfile -> Bool

unionCspCASLSign :: CspCASLSign -> CspCASLSign -> Result CspCASLSign

Compute union of two CSP CASL signatures.