Copyright	(c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
License	GPLv2 or higher, see LICENSE.txt
Maintainer	M.Roggenbach@swansea.ac.uk
Stability	provisional
Portability	portable
Safe Haskell	None

CspCASL.SignCSP

Description

signatures for CSP-CASL

Synopsis

addProcNameToProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap -> ProcNameMap
ccSig2CASLSign :: CspCASLSign -> CASLSign
ccSig2CspSign :: CspCASLSign -> CspSign
type ChanNameMap = MapSet CHANNEL_NAME SORT
closeCspCommAlpha :: Rel SORT -> CommAlpha -> CommAlpha
type CspCASLSign = Sign CspSen CspSign
type CspCASLSen = FORMULA CspSen
data CspSen = ProcessEq FQ_PROCESS_NAME FQProcVarList CommAlpha PROCESS
data CspSign = CspSign {
- chans :: ChanNameMap
- procSet :: ProcNameMap
}
cspSignUnion :: CspSign -> CspSign -> CspSign
diffCspSig :: CspSign -> CspSign -> CspSign
emptyCspCASLSign :: CspCASLSign
emptyCspSign :: CspSign
type FQProcVarList = [TERM ()]
getUniqueProfileInProcNameMap :: PROCESS_NAME -> Int -> ProcNameMap -> Result ProcProfile
isCspCASLSubSig :: CspCASLSign -> CspCASLSign -> Bool
isCspSubSign :: CspSign -> CspSign -> Bool
isNameInProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap -> Bool
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
commType2Sort :: CommType -> SORT
relatedSorts :: CspCASLSign -> SORT -> SORT -> Bool
relatedProcs :: CspCASLSign -> ProcProfile -> ProcProfile -> Bool
unionCspCASLSign :: CspCASLSign -> CspCASLSign -> Result CspCASLSign

Documentation

addProcNameToProcNameMap :: PROCESS_NAME -> ProcProfile -> ProcNameMap -> ProcNameMap Source #

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

ccSig2CASLSign :: CspCASLSign -> CASLSign Source #

ccSig2CspSign :: CspCASLSign -> CspSign Source #

Projection from CspCASL signature to Csp signature

type ChanNameMap = MapSet CHANNEL_NAME SORT Source #

closeCspCommAlpha :: Rel SORT -> CommAlpha -> CommAlpha Source #

type CspCASLSign = Sign CspSen CspSign Source #

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

type CspCASLSen = FORMULA CspSen Source #

data CspSen Source #

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

Instances details

Eq CspSen Source #
Instance details Defined in CspCASL.SignCSP Methods (==) :: CspSen -> CspSen -> Bool (/=) :: CspSen -> CspSen -> Bool
Data CspSen Source #
Instance details Defined in CspCASL.SignCSP Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CspSen -> c CspSen gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CspSen toConstr :: CspSen -> Constr dataTypeOf :: CspSen -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CspSen) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CspSen) gmapT :: (forall b. Data b => b -> b) -> CspSen -> CspSen gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CspSen -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CspSen -> r gmapQ :: (forall d. Data d => d -> u) -> CspSen -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> CspSen -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> CspSen -> m CspSen gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CspSen -> m CspSen gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CspSen -> m CspSen
Ord CspSen Source #
Instance details Defined in CspCASL.SignCSP Methods compare :: CspSen -> CspSen -> Ordering (<) :: CspSen -> CspSen -> Bool (<=) :: CspSen -> CspSen -> Bool (>) :: CspSen -> CspSen -> Bool (>=) :: CspSen -> CspSen -> Bool max :: CspSen -> CspSen -> CspSen min :: CspSen -> CspSen -> CspSen
Show CspSen Source #
Instance details Defined in CspCASL.SignCSP Methods showsPrec :: Int -> CspSen -> ShowS show :: CspSen -> String showList :: [CspSen] -> ShowS
Generic CspSen
Instance details Defined in CspCASL.ATC_CspCASL Associated Types type Rep CspSen :: Type -> Type Methods from :: CspSen -> Rep CspSen x to :: Rep CspSen x -> CspSen
GetRange CspSen Source #
Instance details Defined in CspCASL.SignCSP Methods getRange :: CspSen -> Range Source # rangeSpan :: CspSen -> [Pos] Source #
FromJSON CspSen
Instance details Defined in CspCASL.ATC_CspCASL Methods parseJSON :: Value -> Parser CspSen parseJSONList :: Value -> Parser [CspSen]
ToJSON CspSen
Instance details Defined in CspCASL.ATC_CspCASL Methods toJSON :: CspSen -> Value toEncoding :: CspSen -> Encoding toJSONList :: [CspSen] -> Value toEncodingList :: [CspSen] -> Encoding
ShATermConvertible CspSen
Instance details Defined in CspCASL.ATC_CspCASL Methods toShATermAux :: ATermTable -> CspSen -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [CspSen] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, CspSen) fromShATermList' :: Int -> ATermTable -> (ATermTable, [CspSen])
Pretty CspSen Source #
Instance details Defined in CspCASL.SignCSP Methods pretty :: CspSen -> Doc Source # pretties :: [CspSen] -> Doc Source #
FormExtension CspSen Source #
Instance details Defined in CspCASL.SignCSP Methods isQuantifierLike :: CspSen -> Bool Source # prefixExt :: CspSen -> Doc -> Doc Source #
TermExtension CspSen Source #
Instance details Defined in CspCASL.SignCSP Methods freeVarsOfExt :: Sign CspSen e -> CspSen -> VarSet Source # optTermSort :: CspSen -> Maybe SORT Source # sortOfTerm :: CspSen -> SORT Source # termToFormula :: TERM CspSen -> Result (FORMULA CspSen) Source #
TermParser CspSen Source #
Instance details Defined in CspCASL.SignCSP Methods termParser :: Bool -> AParser st CspSen Source #
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 () Source #
Instance details Defined in Comorphisms.CspCASL2Modal Methods sourceLogic :: CspCASL2Modal -> CspCASL Source # sourceSublogic :: CspCASL2Modal -> () Source # sourceSublogicLossy :: CspCASL2Modal -> () Source # minSourceTheory :: CspCASL2Modal -> Maybe (LibName, String) Source # targetLogic :: CspCASL2Modal -> Modal Source # mapSublogic :: CspCASL2Modal -> () -> Maybe () Source # map_theory :: CspCASL2Modal -> (CspCASLSign, [Named CspCASLSen]) -> Result (MSign, [Named ModalFORMULA]) Source # mapMarkedTheory :: CspCASL2Modal -> (CspCASLSign, [Named CspCASLSen]) -> Result (MSign, [Named ModalFORMULA]) Source # map_morphism :: CspCASL2Modal -> CspCASLMorphism -> Result ModalMor Source # map_sentence :: CspCASL2Modal -> CspCASLSign -> CspCASLSen -> Result ModalFORMULA Source # map_symbol :: CspCASL2Modal -> CspCASLSign -> CspSymbol -> Set Symbol Source # extractModel :: CspCASL2Modal -> CspCASLSign -> () -> Result (CspCASLSign, [Named CspCASLSen]) Source # is_model_transportable :: CspCASL2Modal -> Bool Source # has_model_expansion :: CspCASL2Modal -> Bool Source # is_weakly_amalgamable :: CspCASL2Modal -> Bool Source # constituents :: CspCASL2Modal -> [String] Source # isInclusionComorphism :: CspCASL2Modal -> Bool Source # rps :: CspCASL2Modal -> Bool Source # eps :: CspCASL2Modal -> Bool Source # isGTC :: CspCASL2Modal -> Bool Source #
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 () Source #
Instance details Defined in Comorphisms.CASL2CspCASL Methods sourceLogic :: CASL2CspCASL -> CASL Source # sourceSublogic :: CASL2CspCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2CspCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2CspCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2CspCASL -> CspCASL Source # mapSublogic :: CASL2CspCASL -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2CspCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # mapMarkedTheory :: CASL2CspCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # map_morphism :: CASL2CspCASL -> CASLMor -> Result CspCASLMorphism Source # map_sentence :: CASL2CspCASL -> CASLSign -> CASLFORMULA -> Result CspCASLSen Source # map_symbol :: CASL2CspCASL -> CASLSign -> Symbol -> Set CspSymbol Source # extractModel :: CASL2CspCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2CspCASL -> Bool Source # has_model_expansion :: CASL2CspCASL -> Bool Source # is_weakly_amalgamable :: CASL2CspCASL -> Bool Source # constituents :: CASL2CspCASL -> [String] Source # isInclusionComorphism :: CASL2CspCASL -> Bool Source # rps :: CASL2CspCASL -> Bool Source # eps :: CASL2CspCASL -> Bool Source # isGTC :: CASL2CspCASL -> Bool Source #
Show a => Sentences (GenCspCASL a) CspCASLSen CspCASLSign CspCASLMorphism CspSymbol Source #	Instance of Sentences for CspCASL
Instance details Defined in CspCASL.Logic_CspCASL Methods map_sen :: GenCspCASL a -> CspCASLMorphism -> CspCASLSen -> Result CspCASLSen Source # simplify_sen :: GenCspCASL a -> CspCASLSign -> CspCASLSen -> CspCASLSen Source # negation :: GenCspCASL a -> CspCASLSen -> Maybe CspCASLSen Source # print_sign :: GenCspCASL a -> CspCASLSign -> Doc Source # print_named :: GenCspCASL a -> Named CspCASLSen -> Doc Source # sym_of :: GenCspCASL a -> CspCASLSign -> [Set CspSymbol] Source # mostSymsOf :: GenCspCASL a -> CspCASLSign -> [CspSymbol] Source # symmap_of :: GenCspCASL a -> CspCASLMorphism -> EndoMap CspSymbol Source # sym_name :: GenCspCASL a -> CspSymbol -> Id Source # sym_label :: GenCspCASL a -> CspSymbol -> Maybe String Source # fullSymName :: GenCspCASL a -> CspSymbol -> String Source # symKind :: GenCspCASL a -> CspSymbol -> String Source # symsOfSen :: GenCspCASL a -> CspCASLSign -> CspCASLSen -> [CspSymbol] Source # pair_symbols :: GenCspCASL a -> CspSymbol -> CspSymbol -> Result CspSymbol Source #
Show a => Syntax (GenCspCASL a) CspBasicSpec CspSymbol CspSymbItems CspSymbMapItems Source #	Syntax of CspCASL
Instance details Defined in CspCASL.Logic_CspCASL Methods parsersAndPrinters :: GenCspCASL a -> Map String (PrefixMap -> AParser st CspBasicSpec, CspBasicSpec -> Doc) Source # parse_basic_spec :: GenCspCASL a -> Maybe (PrefixMap -> AParser st CspBasicSpec) Source # parseSingleSymbItem :: GenCspCASL a -> Maybe (PrefixMap -> AParser st CspSymbItems) Source # parse_symb_items :: GenCspCASL a -> Maybe (PrefixMap -> AParser st CspSymbItems) Source # parse_symb_map_items :: GenCspCASL a -> Maybe (PrefixMap -> AParser st CspSymbMapItems) Source # toItem :: GenCspCASL a -> CspBasicSpec -> Item Source # symb_items_name :: GenCspCASL a -> CspSymbItems -> [String] Source #
Show a => StaticAnalysis (GenCspCASL a) CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol Source #	Static Analysis for CspCASL
Instance details Defined in CspCASL.Logic_CspCASL Methods basic_analysis :: GenCspCASL a -> Maybe ((CspBasicSpec, CspCASLSign, GlobalAnnos) -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen])) Source # sen_analysis :: GenCspCASL a -> Maybe ((CspBasicSpec, CspCASLSign, CspCASLSen) -> Result CspCASLSen) Source # extBasicAnalysis :: GenCspCASL a -> IRI -> LibName -> CspBasicSpec -> CspCASLSign -> GlobalAnnos -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen]) Source # stat_symb_map_items :: GenCspCASL a -> CspCASLSign -> Maybe CspCASLSign -> [CspSymbMapItems] -> Result (EndoMap CspRawSymbol) Source # stat_symb_items :: GenCspCASL a -> CspCASLSign -> [CspSymbItems] -> Result [CspRawSymbol] Source # convertTheory :: GenCspCASL a -> Maybe ((CspCASLSign, [Named CspCASLSen]) -> CspBasicSpec) Source # ensures_amalgamability :: GenCspCASL a -> ([CASLAmalgOpt], Gr CspCASLSign (Int, CspCASLMorphism), [(Int, CspCASLMorphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: GenCspCASL a -> CspCASLMorphism -> [Named CspCASLSen] -> Result (CspCASLSign, [Named CspCASLSen]) Source # signature_colimit :: GenCspCASL a -> Gr CspCASLSign (Int, CspCASLMorphism) -> Result (CspCASLSign, Map Int CspCASLMorphism) Source # qualify :: GenCspCASL a -> SIMPLE_ID -> LibName -> CspCASLMorphism -> CspCASLSign -> Result (CspCASLMorphism, [Named CspCASLSen]) Source # symbol_to_raw :: GenCspCASL a -> CspSymbol -> CspRawSymbol Source # id_to_raw :: GenCspCASL a -> Id -> CspRawSymbol Source # matches :: GenCspCASL a -> CspSymbol -> CspRawSymbol -> Bool Source # empty_signature :: GenCspCASL a -> CspCASLSign Source # add_symb_to_sign :: GenCspCASL a -> CspCASLSign -> CspSymbol -> Result CspCASLSign Source # signature_union :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source # signatureDiff :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source # intersection :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source # final_union :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source # morphism_union :: GenCspCASL a -> CspCASLMorphism -> CspCASLMorphism -> Result CspCASLMorphism Source # is_subsig :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Bool Source # subsig_inclusion :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLMorphism Source # generated_sign :: GenCspCASL a -> Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism Source # cogenerated_sign :: GenCspCASL a -> Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism Source # induced_from_morphism :: GenCspCASL a -> EndoMap CspRawSymbol -> CspCASLSign -> Result CspCASLMorphism Source # induced_from_to_morphism :: GenCspCASL a -> EndoMap CspRawSymbol -> ExtSign CspCASLSign CspSymbol -> ExtSign CspCASLSign CspSymbol -> Result CspCASLMorphism Source # is_transportable :: GenCspCASL a -> CspCASLMorphism -> Bool Source # is_injective :: GenCspCASL a -> CspCASLMorphism -> Bool Source # theory_to_taxonomy :: GenCspCASL a -> TaxoGraphKind -> MMiSSOntology -> CspCASLSign -> [Named CspCASLSen] -> Result MMiSSOntology Source # corresp2th :: GenCspCASL a -> String -> Bool -> CspCASLSign -> CspCASLSign -> [CspSymbItems] -> [CspSymbItems] -> EndoMap CspSymbol -> EndoMap CspSymbol -> REL_REF -> Result (CspCASLSign, [Named CspCASLSen], CspCASLSign, CspCASLSign, EndoMap CspSymbol, EndoMap CspSymbol) Source # equiv2cospan :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> [CspSymbItems] -> [CspSymbItems] -> Result (CspCASLSign, CspCASLSign, CspCASLSign, EndoMap CspSymbol, EndoMap CspSymbol) Source # extract_module :: GenCspCASL a -> [IRI] -> (CspCASLSign, [Named CspCASLSen]) -> Result (CspCASLSign, [Named CspCASLSen]) Source #
CspCASLSemantics a => Logic (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source #	Instance of Logic for CspCASL
Instance details Defined in CspCASL.Logic_CspCASL Methods parse_basic_sen :: GenCspCASL a -> Maybe (CspBasicSpec -> AParser st CspCASLSen) Source # stability :: GenCspCASL a -> Stability Source # data_logic :: GenCspCASL a -> Maybe AnyLogic Source # top_sublogic :: GenCspCASL a -> () Source # all_sublogics :: GenCspCASL a -> [()] Source # bottomSublogic :: GenCspCASL a -> Maybe () Source # sublogicDimensions :: GenCspCASL a -> [[()]] Source # parseSublogic :: GenCspCASL a -> String -> Maybe () Source # proj_sublogic_epsilon :: GenCspCASL a -> () -> CspCASLSign -> CspCASLMorphism Source # provers :: GenCspCASL a -> [Prover CspCASLSign CspCASLSen CspCASLMorphism () ()] Source # default_prover :: GenCspCASL a -> String Source # cons_checkers :: GenCspCASL a -> [ConsChecker CspCASLSign CspCASLSen () CspCASLMorphism ()] Source # conservativityCheck :: GenCspCASL a -> [ConservativityChecker CspCASLSign CspCASLSen CspCASLMorphism] Source # empty_proof_tree :: GenCspCASL a -> () Source # syntaxTable :: GenCspCASL a -> CspCASLSign -> Maybe SyntaxTable Source # omdoc_metatheory :: GenCspCASL a -> Maybe OMCD Source # export_symToOmdoc :: GenCspCASL a -> NameMap CspSymbol -> CspSymbol -> String -> Result TCElement Source # export_senToOmdoc :: GenCspCASL a -> NameMap CspSymbol -> CspCASLSen -> Result TCorOMElement Source # export_theoryToOmdoc :: GenCspCASL a -> SigMap CspSymbol -> CspCASLSign -> [Named CspCASLSen] -> Result [TCElement] Source # omdocToSym :: GenCspCASL a -> SigMapI CspSymbol -> TCElement -> String -> Result CspSymbol Source # omdocToSen :: GenCspCASL a -> SigMapI CspSymbol -> TCElement -> String -> Result (Maybe (Named CspCASLSen)) Source # addOMadtToTheory :: GenCspCASL a -> SigMapI CspSymbol -> (CspCASLSign, [Named CspCASLSen]) -> [[OmdADT]] -> Result (CspCASLSign, [Named CspCASLSen]) Source # addOmdocToTheory :: GenCspCASL a -> SigMapI CspSymbol -> (CspCASLSign, [Named CspCASLSen]) -> [TCElement] -> Result (CspCASLSign, [Named CspCASLSen]) Source # sublogicOfTheo :: GenCspCASL a -> (CspCASLSign, [CspCASLSen]) -> () Source #
(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 () Source #
Instance details Defined in CspCASL.Comorphisms Methods sourceLogic :: CspCASL2CspCASL a b -> GenCspCASL a Source # sourceSublogic :: CspCASL2CspCASL a b -> () Source # sourceSublogicLossy :: CspCASL2CspCASL a b -> () Source # minSourceTheory :: CspCASL2CspCASL a b -> Maybe (LibName, String) Source # targetLogic :: CspCASL2CspCASL a b -> GenCspCASL b Source # mapSublogic :: CspCASL2CspCASL a b -> () -> Maybe () Source # map_theory :: CspCASL2CspCASL a b -> (CspCASLSign, [Named CspCASLSen]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # mapMarkedTheory :: CspCASL2CspCASL a b -> (CspCASLSign, [Named CspCASLSen]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # map_morphism :: CspCASL2CspCASL a b -> CspCASLMorphism -> Result CspCASLMorphism Source # map_sentence :: CspCASL2CspCASL a b -> CspCASLSign -> CspCASLSen -> Result CspCASLSen Source # map_symbol :: CspCASL2CspCASL a b -> CspCASLSign -> CspSymbol -> Set CspSymbol Source # extractModel :: CspCASL2CspCASL a b -> CspCASLSign -> () -> Result (CspCASLSign, [Named CspCASLSen]) Source # is_model_transportable :: CspCASL2CspCASL a b -> Bool Source # has_model_expansion :: CspCASL2CspCASL a b -> Bool Source # is_weakly_amalgamable :: CspCASL2CspCASL a b -> Bool Source # constituents :: CspCASL2CspCASL a b -> [String] Source # isInclusionComorphism :: CspCASL2CspCASL a b -> Bool Source # rps :: CspCASL2CspCASL a b -> Bool Source # eps :: CspCASL2CspCASL a b -> Bool Source # isGTC :: CspCASL2CspCASL a b -> Bool Source #
type Rep CspSen
Instance details Defined in CspCASL.ATC_CspCASL type Rep CspSen = D1 ('MetaData "CspSen" "CspCASL.SignCSP" "main" 'False) (C1 ('MetaCons "ProcessEq" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FQ_PROCESS_NAME) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FQProcVarList)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CommAlpha) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PROCESS))))

data CspSign Source #

CSP process signature.

Constructors

CspSign
Fields chans :: ChanNameMap procSet :: ProcNameMap

Instances

Instances details

Eq CspSign Source #
Instance details Defined in CspCASL.SignCSP Methods (==) :: CspSign -> CspSign -> Bool (/=) :: CspSign -> CspSign -> Bool
Data CspSign Source #
Instance details Defined in CspCASL.SignCSP Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CspSign -> c CspSign gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CspSign toConstr :: CspSign -> Constr dataTypeOf :: CspSign -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CspSign) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CspSign) gmapT :: (forall b. Data b => b -> b) -> CspSign -> CspSign gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CspSign -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CspSign -> r gmapQ :: (forall d. Data d => d -> u) -> CspSign -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> CspSign -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> CspSign -> m CspSign gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CspSign -> m CspSign gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CspSign -> m CspSign
Ord CspSign Source #
Instance details Defined in CspCASL.SignCSP Methods compare :: CspSign -> CspSign -> Ordering (<) :: CspSign -> CspSign -> Bool (<=) :: CspSign -> CspSign -> Bool (>) :: CspSign -> CspSign -> Bool (>=) :: CspSign -> CspSign -> Bool max :: CspSign -> CspSign -> CspSign min :: CspSign -> CspSign -> CspSign
Show CspSign Source #
Instance details Defined in CspCASL.SignCSP Methods showsPrec :: Int -> CspSign -> ShowS show :: CspSign -> String showList :: [CspSign] -> ShowS
Generic CspSign
Instance details Defined in CspCASL.ATC_CspCASL Associated Types type Rep CspSign :: Type -> Type Methods from :: CspSign -> Rep CspSign x to :: Rep CspSign x -> CspSign
FromJSON CspSign
Instance details Defined in CspCASL.ATC_CspCASL Methods parseJSON :: Value -> Parser CspSign parseJSONList :: Value -> Parser [CspSign]
ToJSON CspSign
Instance details Defined in CspCASL.ATC_CspCASL Methods toJSON :: CspSign -> Value toEncoding :: CspSign -> Encoding toJSONList :: [CspSign] -> Value toEncodingList :: [CspSign] -> Encoding
ShATermConvertible CspSign
Instance details Defined in CspCASL.ATC_CspCASL Methods toShATermAux :: ATermTable -> CspSign -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [CspSign] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, CspSign) fromShATermList' :: Int -> ATermTable -> (ATermTable, [CspSign])
Pretty CspSign Source #	Pretty printing for CspCASL signatures
Instance details Defined in CspCASL.SignCSP Methods pretty :: CspSign -> Doc Source # pretties :: [CspSign] -> Doc Source #
SignExtension CspSign Source #	Instance for CspCASL signature extension
Instance details Defined in CspCASL.Morphism Methods isSubSignExtension :: CspSign -> CspSign -> Bool Source #
MorphismExtension CspSign CspAddMorphism Source #	Instance for CspCASL morphism extension (used for Category)
Instance details Defined in CspCASL.Morphism Methods ideMorphismExtension :: CspSign -> CspAddMorphism Source # composeMorphismExtension :: Morphism f CspSign CspAddMorphism -> Morphism f CspSign CspAddMorphism -> Result CspAddMorphism Source # inverseMorphismExtension :: Morphism f CspSign CspAddMorphism -> Result CspAddMorphism Source # isInclusionMorphismExtension :: CspAddMorphism -> Bool Source # prettyMorphismExtension :: Morphism f CspSign CspAddMorphism -> Doc Source # legalMorphismExtension :: Morphism f CspSign CspAddMorphism -> Result () Source #
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 () Source #
Instance details Defined in Comorphisms.CspCASL2Modal Methods sourceLogic :: CspCASL2Modal -> CspCASL Source # sourceSublogic :: CspCASL2Modal -> () Source # sourceSublogicLossy :: CspCASL2Modal -> () Source # minSourceTheory :: CspCASL2Modal -> Maybe (LibName, String) Source # targetLogic :: CspCASL2Modal -> Modal Source # mapSublogic :: CspCASL2Modal -> () -> Maybe () Source # map_theory :: CspCASL2Modal -> (CspCASLSign, [Named CspCASLSen]) -> Result (MSign, [Named ModalFORMULA]) Source # mapMarkedTheory :: CspCASL2Modal -> (CspCASLSign, [Named CspCASLSen]) -> Result (MSign, [Named ModalFORMULA]) Source # map_morphism :: CspCASL2Modal -> CspCASLMorphism -> Result ModalMor Source # map_sentence :: CspCASL2Modal -> CspCASLSign -> CspCASLSen -> Result ModalFORMULA Source # map_symbol :: CspCASL2Modal -> CspCASLSign -> CspSymbol -> Set Symbol Source # extractModel :: CspCASL2Modal -> CspCASLSign -> () -> Result (CspCASLSign, [Named CspCASLSen]) Source # is_model_transportable :: CspCASL2Modal -> Bool Source # has_model_expansion :: CspCASL2Modal -> Bool Source # is_weakly_amalgamable :: CspCASL2Modal -> Bool Source # constituents :: CspCASL2Modal -> [String] Source # isInclusionComorphism :: CspCASL2Modal -> Bool Source # rps :: CspCASL2Modal -> Bool Source # eps :: CspCASL2Modal -> Bool Source # isGTC :: CspCASL2Modal -> Bool Source #
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 () Source #
Instance details Defined in Comorphisms.CASL2CspCASL Methods sourceLogic :: CASL2CspCASL -> CASL Source # sourceSublogic :: CASL2CspCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2CspCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2CspCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2CspCASL -> CspCASL Source # mapSublogic :: CASL2CspCASL -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2CspCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # mapMarkedTheory :: CASL2CspCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # map_morphism :: CASL2CspCASL -> CASLMor -> Result CspCASLMorphism Source # map_sentence :: CASL2CspCASL -> CASLSign -> CASLFORMULA -> Result CspCASLSen Source # map_symbol :: CASL2CspCASL -> CASLSign -> Symbol -> Set CspSymbol Source # extractModel :: CASL2CspCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2CspCASL -> Bool Source # has_model_expansion :: CASL2CspCASL -> Bool Source # is_weakly_amalgamable :: CASL2CspCASL -> Bool Source # constituents :: CASL2CspCASL -> [String] Source # isInclusionComorphism :: CASL2CspCASL -> Bool Source # rps :: CASL2CspCASL -> Bool Source # eps :: CASL2CspCASL -> Bool Source # isGTC :: CASL2CspCASL -> Bool Source #
Show a => Sentences (GenCspCASL a) CspCASLSen CspCASLSign CspCASLMorphism CspSymbol Source #	Instance of Sentences for CspCASL
Instance details Defined in CspCASL.Logic_CspCASL Methods map_sen :: GenCspCASL a -> CspCASLMorphism -> CspCASLSen -> Result CspCASLSen Source # simplify_sen :: GenCspCASL a -> CspCASLSign -> CspCASLSen -> CspCASLSen Source # negation :: GenCspCASL a -> CspCASLSen -> Maybe CspCASLSen Source # print_sign :: GenCspCASL a -> CspCASLSign -> Doc Source # print_named :: GenCspCASL a -> Named CspCASLSen -> Doc Source # sym_of :: GenCspCASL a -> CspCASLSign -> [Set CspSymbol] Source # mostSymsOf :: GenCspCASL a -> CspCASLSign -> [CspSymbol] Source # symmap_of :: GenCspCASL a -> CspCASLMorphism -> EndoMap CspSymbol Source # sym_name :: GenCspCASL a -> CspSymbol -> Id Source # sym_label :: GenCspCASL a -> CspSymbol -> Maybe String Source # fullSymName :: GenCspCASL a -> CspSymbol -> String Source # symKind :: GenCspCASL a -> CspSymbol -> String Source # symsOfSen :: GenCspCASL a -> CspCASLSign -> CspCASLSen -> [CspSymbol] Source # pair_symbols :: GenCspCASL a -> CspSymbol -> CspSymbol -> Result CspSymbol Source #
Show a => StaticAnalysis (GenCspCASL a) CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol Source #	Static Analysis for CspCASL
Instance details Defined in CspCASL.Logic_CspCASL Methods basic_analysis :: GenCspCASL a -> Maybe ((CspBasicSpec, CspCASLSign, GlobalAnnos) -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen])) Source # sen_analysis :: GenCspCASL a -> Maybe ((CspBasicSpec, CspCASLSign, CspCASLSen) -> Result CspCASLSen) Source # extBasicAnalysis :: GenCspCASL a -> IRI -> LibName -> CspBasicSpec -> CspCASLSign -> GlobalAnnos -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen]) Source # stat_symb_map_items :: GenCspCASL a -> CspCASLSign -> Maybe CspCASLSign -> [CspSymbMapItems] -> Result (EndoMap CspRawSymbol) Source # stat_symb_items :: GenCspCASL a -> CspCASLSign -> [CspSymbItems] -> Result [CspRawSymbol] Source # convertTheory :: GenCspCASL a -> Maybe ((CspCASLSign, [Named CspCASLSen]) -> CspBasicSpec) Source # ensures_amalgamability :: GenCspCASL a -> ([CASLAmalgOpt], Gr CspCASLSign (Int, CspCASLMorphism), [(Int, CspCASLMorphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: GenCspCASL a -> CspCASLMorphism -> [Named CspCASLSen] -> Result (CspCASLSign, [Named CspCASLSen]) Source # signature_colimit :: GenCspCASL a -> Gr CspCASLSign (Int, CspCASLMorphism) -> Result (CspCASLSign, Map Int CspCASLMorphism) Source # qualify :: GenCspCASL a -> SIMPLE_ID -> LibName -> CspCASLMorphism -> CspCASLSign -> Result (CspCASLMorphism, [Named CspCASLSen]) Source # symbol_to_raw :: GenCspCASL a -> CspSymbol -> CspRawSymbol Source # id_to_raw :: GenCspCASL a -> Id -> CspRawSymbol Source # matches :: GenCspCASL a -> CspSymbol -> CspRawSymbol -> Bool Source # empty_signature :: GenCspCASL a -> CspCASLSign Source # add_symb_to_sign :: GenCspCASL a -> CspCASLSign -> CspSymbol -> Result CspCASLSign Source # signature_union :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source # signatureDiff :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source # intersection :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source # final_union :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source # morphism_union :: GenCspCASL a -> CspCASLMorphism -> CspCASLMorphism -> Result CspCASLMorphism Source # is_subsig :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Bool Source # subsig_inclusion :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLMorphism Source # generated_sign :: GenCspCASL a -> Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism Source # cogenerated_sign :: GenCspCASL a -> Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism Source # induced_from_morphism :: GenCspCASL a -> EndoMap CspRawSymbol -> CspCASLSign -> Result CspCASLMorphism Source # induced_from_to_morphism :: GenCspCASL a -> EndoMap CspRawSymbol -> ExtSign CspCASLSign CspSymbol -> ExtSign CspCASLSign CspSymbol -> Result CspCASLMorphism Source # is_transportable :: GenCspCASL a -> CspCASLMorphism -> Bool Source # is_injective :: GenCspCASL a -> CspCASLMorphism -> Bool Source # theory_to_taxonomy :: GenCspCASL a -> TaxoGraphKind -> MMiSSOntology -> CspCASLSign -> [Named CspCASLSen] -> Result MMiSSOntology Source # corresp2th :: GenCspCASL a -> String -> Bool -> CspCASLSign -> CspCASLSign -> [CspSymbItems] -> [CspSymbItems] -> EndoMap CspSymbol -> EndoMap CspSymbol -> REL_REF -> Result (CspCASLSign, [Named CspCASLSen], CspCASLSign, CspCASLSign, EndoMap CspSymbol, EndoMap CspSymbol) Source # equiv2cospan :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> [CspSymbItems] -> [CspSymbItems] -> Result (CspCASLSign, CspCASLSign, CspCASLSign, EndoMap CspSymbol, EndoMap CspSymbol) Source # extract_module :: GenCspCASL a -> [IRI] -> (CspCASLSign, [Named CspCASLSen]) -> Result (CspCASLSign, [Named CspCASLSen]) Source #
CspCASLSemantics a => Logic (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source #	Instance of Logic for CspCASL
Instance details Defined in CspCASL.Logic_CspCASL Methods parse_basic_sen :: GenCspCASL a -> Maybe (CspBasicSpec -> AParser st CspCASLSen) Source # stability :: GenCspCASL a -> Stability Source # data_logic :: GenCspCASL a -> Maybe AnyLogic Source # top_sublogic :: GenCspCASL a -> () Source # all_sublogics :: GenCspCASL a -> [()] Source # bottomSublogic :: GenCspCASL a -> Maybe () Source # sublogicDimensions :: GenCspCASL a -> [[()]] Source # parseSublogic :: GenCspCASL a -> String -> Maybe () Source # proj_sublogic_epsilon :: GenCspCASL a -> () -> CspCASLSign -> CspCASLMorphism Source # provers :: GenCspCASL a -> [Prover CspCASLSign CspCASLSen CspCASLMorphism () ()] Source # default_prover :: GenCspCASL a -> String Source # cons_checkers :: GenCspCASL a -> [ConsChecker CspCASLSign CspCASLSen () CspCASLMorphism ()] Source # conservativityCheck :: GenCspCASL a -> [ConservativityChecker CspCASLSign CspCASLSen CspCASLMorphism] Source # empty_proof_tree :: GenCspCASL a -> () Source # syntaxTable :: GenCspCASL a -> CspCASLSign -> Maybe SyntaxTable Source # omdoc_metatheory :: GenCspCASL a -> Maybe OMCD Source # export_symToOmdoc :: GenCspCASL a -> NameMap CspSymbol -> CspSymbol -> String -> Result TCElement Source # export_senToOmdoc :: GenCspCASL a -> NameMap CspSymbol -> CspCASLSen -> Result TCorOMElement Source # export_theoryToOmdoc :: GenCspCASL a -> SigMap CspSymbol -> CspCASLSign -> [Named CspCASLSen] -> Result [TCElement] Source # omdocToSym :: GenCspCASL a -> SigMapI CspSymbol -> TCElement -> String -> Result CspSymbol Source # omdocToSen :: GenCspCASL a -> SigMapI CspSymbol -> TCElement -> String -> Result (Maybe (Named CspCASLSen)) Source # addOMadtToTheory :: GenCspCASL a -> SigMapI CspSymbol -> (CspCASLSign, [Named CspCASLSen]) -> [[OmdADT]] -> Result (CspCASLSign, [Named CspCASLSen]) Source # addOmdocToTheory :: GenCspCASL a -> SigMapI CspSymbol -> (CspCASLSign, [Named CspCASLSen]) -> [TCElement] -> Result (CspCASLSign, [Named CspCASLSen]) Source # sublogicOfTheo :: GenCspCASL a -> (CspCASLSign, [CspCASLSen]) -> () Source #
(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 () Source #
Instance details Defined in CspCASL.Comorphisms Methods sourceLogic :: CspCASL2CspCASL a b -> GenCspCASL a Source # sourceSublogic :: CspCASL2CspCASL a b -> () Source # sourceSublogicLossy :: CspCASL2CspCASL a b -> () Source # minSourceTheory :: CspCASL2CspCASL a b -> Maybe (LibName, String) Source # targetLogic :: CspCASL2CspCASL a b -> GenCspCASL b Source # mapSublogic :: CspCASL2CspCASL a b -> () -> Maybe () Source # map_theory :: CspCASL2CspCASL a b -> (CspCASLSign, [Named CspCASLSen]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # mapMarkedTheory :: CspCASL2CspCASL a b -> (CspCASLSign, [Named CspCASLSen]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # map_morphism :: CspCASL2CspCASL a b -> CspCASLMorphism -> Result CspCASLMorphism Source # map_sentence :: CspCASL2CspCASL a b -> CspCASLSign -> CspCASLSen -> Result CspCASLSen Source # map_symbol :: CspCASL2CspCASL a b -> CspCASLSign -> CspSymbol -> Set CspSymbol Source # extractModel :: CspCASL2CspCASL a b -> CspCASLSign -> () -> Result (CspCASLSign, [Named CspCASLSen]) Source # is_model_transportable :: CspCASL2CspCASL a b -> Bool Source # has_model_expansion :: CspCASL2CspCASL a b -> Bool Source # is_weakly_amalgamable :: CspCASL2CspCASL a b -> Bool Source # constituents :: CspCASL2CspCASL a b -> [String] Source # isInclusionComorphism :: CspCASL2CspCASL a b -> Bool Source # rps :: CspCASL2CspCASL a b -> Bool Source # eps :: CspCASL2CspCASL a b -> Bool Source # isGTC :: CspCASL2CspCASL a b -> Bool Source #
type Rep CspSign
Instance details Defined in CspCASL.ATC_CspCASL type Rep CspSign = D1 ('MetaData "CspSign" "CspCASL.SignCSP" "main" 'False) (C1 ('MetaCons "CspSign" 'PrefixI 'True) (S1 ('MetaSel ('Just "chans") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ChanNameMap) :*: S1 ('MetaSel ('Just "procSet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProcNameMap)))

cspSignUnion :: CspSign -> CspSign -> CspSign Source #

plain union

diffCspSig :: CspSign -> CspSign -> CspSign Source #

Compute difference of two CSP process signatures.

emptyCspCASLSign :: CspCASLSign Source #

Empty CspCASL signature.

emptyCspSign :: CspSign Source #

Empty CSP process signature.

type FQProcVarList = [TERM ()] Source #

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

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

Is one CspCASL Signature a sub signature of another

isCspSubSign :: CspSign -> CspSign -> Bool Source #

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

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

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

isProcessEq :: CspCASLSen -> Bool Source #

type ProcNameMap = MapSet PROCESS_NAME ProcProfile Source #

type ProcVarList = [(SIMPLE_ID, SORT)] Source #

type ProcVarMap = Map SIMPLE_ID SORT Source #

reduceProcProfile :: Rel SORT -> ProcProfile -> ProcProfile Source #

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

relatedSorts :: CspCASLSign -> SORT -> SORT -> Bool Source #

unionCspCASLSign :: CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

Compute union of two CSP CASL signatures.