Copyright	(c) Till Mossakowski and Uni Bremen 2004
License	GPLv2 or higher, see LICENSE.txt
Maintainer	till@informatik.uni-bremen.de
Stability	provisional
Portability	non-portable (imports Logic.Logic)
Safe Haskell	None

Comorphisms.CspCASL2Modal

Description

The embedding comorphism from CspCASL to ModalCASL. It keeps the CASL part and interprets the CspCASL LTS semantics as Kripke structure

Synopsis

data CspCASL2Modal = CspCASL2Modal
mapSen :: CspCASLSen -> ModalFORMULA

Documentation

data CspCASL2Modal Source #

The identity of the comorphism

Constructors

CspCASL2Modal

Instances

Instances details

Show CspCASL2Modal Source #
Instance details Defined in Comorphisms.CspCASL2Modal Methods showsPrec :: Int -> CspCASL2Modal -> ShowS show :: CspCASL2Modal -> String showList :: [CspCASL2Modal] -> ShowS
Language CspCASL2Modal Source #
Instance details Defined in Comorphisms.CspCASL2Modal Methods language_name :: CspCASL2Modal -> String Source # description :: CspCASL2Modal -> String 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 #

mapSen :: CspCASLSen -> ModalFORMULA Source #