Hets - the Heterogeneous Tool Set

Copyright(c) Dominik Luecke, Uni Bremen 2007
LicenseGPLv2 or higher, see LICENSE.txt
Portabilityportable Definition of morphisms for temporal logic copied from "Propositional.Morphism" Ref. Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki. What is a Logic?. In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser. 2005.
Safe HaskellSafe-Inferred






data Morphism

The datatype for morphisms in temporal logic as maps of sets




source :: Sign
target :: Sign
propMap :: Map Id Id


Eq Morphism 
Ord Morphism 
Show Morphism 
ShATermConvertible Morphism 
Pretty Morphism 
Typeable * Morphism 
Category Sign Morphism

Instance of Category for temporal logic

Sentences Temporal FORMULA Sign Morphism Symbol

Instance of Sentences for temporal logic

StaticAnalysis Temporal BASIC_SPEC FORMULA () () Sign Morphism Symbol Symbol

Static Analysis for propositional logic

Logic Temporal () BASIC_SPEC FORMULA () () Sign Morphism Symbol Symbol ()

Instance of Logic for propositional logc

pretty :: Pretty a => a -> Doc

idMor :: Sign -> Morphism

Constructs an id-morphism

isLegalMorphism :: Morphism -> Result ()

Determines whether a morphism is valid

composeMor :: Morphism -> Morphism -> Result Morphism

Composition of morphisms in temporal Logic

inclusionMap :: Sign -> Sign -> Morphism

Inclusion map of a subsig into a supersig

mapSentence :: Morphism -> FORMULA -> Result FORMULA

sentence translation along signature morphism here just the renaming of formulae

applyMap :: Map Id Id -> Id -> Id

Application function for propMaps

applyMorphism :: Morphism -> Id -> Id

Application funtion for morphisms