5ffb0c9b03b5149ff4f5821a62be4a52408ada2aToomas Soome{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

5ffb0c9b03b5149ff4f5821a62be4a52408ada2aToomas Soome{- |

5ffb0c9b03b5149ff4f5821a62be4a52408ada2aToomas SoomeModule : $Header$

5ffb0c9b03b5149ff4f5821a62be4a52408ada2aToomas SoomeCopyright : (c) Till Mossakowski and Uni Bremen 2004

5ffb0c9b03b5149ff4f5821a62be4a52408ada2aToomas SoomeLicense : GPLv2 or higher, see LICENSE.txt

5ffb0c9b03b5149ff4f5821a62be4a52408ada2aToomas Soome

5ffb0c9b03b5149ff4f5821a62be4a52408ada2aToomas SoomeMaintainer : till@informatik.uni-bremen.de

5ffb0c9b03b5149ff4f5821a62be4a52408ada2aToomas SoomeStability : provisional

5ffb0c9b03b5149ff4f5821a62be4a52408ada2aToomas SoomePortability : non-portable (imports Logic.Logic)

5ffb0c9b03b5149ff4f5821a62be4a52408ada2aToomas Soome

5ffb0c9b03b5149ff4f5821a62be4a52408ada2aToomas SoomeThe embedding comorphism from CspCASL to ModalCASL.

5ffb0c9b03b5149ff4f5821a62be4a52408ada2aToomas Soome It keeps the CASL part and interprets the CspCASL LTS semantics as

5ffb0c9b03b5149ff4f5821a62be4a52408ada2aToomas Soome Kripke structure

5ffb0c9b03b5149ff4f5821a62be4a52408ada2aToomas Soome-}

5ffb0c9b03b5149ff4f5821a62be4a52408ada2aToomas Soome

5ffb0c9b03b5149ff4f5821a62be4a52408ada2aToomas Soomemodule Comorphisms.CspCASL2Modal where

5ffb0c9b03b5149ff4f5821a62be4a52408ada2aToomas Soome

5ffb0c9b03b5149ff4f5821a62be4a52408ada2aToomas Soomeimport Logic.Logic

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveashimport Logic.Comorphism

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash-- CASL

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveashimport CASL.Sign

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveashimport CASL.AS_Basic_CASL

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveashimport CASL.Morphism

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash-- CspCASL

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveashimport CspCASL.Logic_CspCASL

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveashimport CspCASL.SignCSP

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveashimport CspCASL.StatAnaCSP (CspBasicSpec)

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveashimport CspCASL.Morphism (CspCASLMorphism)

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveashimport CspCASL.SymbItems

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveashimport CspCASL.Symbol

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash-- ModalCASL

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveashimport Modal.Logic_Modal

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveashimport Modal.AS_Modal

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveashimport Modal.ModalSign

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash-- | The identity of the comorphism

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveashdata CspCASL2Modal = CspCASL2Modal deriving (Show)

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveashinstance Language CspCASL2Modal -- default definition is okay

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveashinstance Comorphism CspCASL2Modal

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol ()

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash MSign ModalMor Symbol RawSymbol () where

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash sourceLogic CspCASL2Modal = cspCASL

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash sourceSublogic CspCASL2Modal = ()

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash targetLogic CspCASL2Modal = Modal

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash mapSublogic CspCASL2Modal _ = Just ()

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash map_theory CspCASL2Modal = return . embedTheory mapSen emptyModalSign

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash map_morphism CspCASL2Modal = return . mapCASLMor emptyModalSign emptyMorExt

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash map_sentence CspCASL2Modal _ = return . mapSen

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash

4890a7493fa5781f7cd15fa207cbcb58cc418882Will FiveashmapSen :: CspCASLSen -> ModalFORMULA

4890a7493fa5781f7cd15fa207cbcb58cc418882Will FiveashmapSen _ = trueForm

4890a7493fa5781f7cd15fa207cbcb58cc418882Will Fiveash