ModalCaslToMu.hs revision f1edf379717f0ddb7607585a027cf6f03a6fce68
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{- |
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederCopyright : (c) Klaus Hartke, Uni Bremen 2008
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiLicense : GPLv2 or higher, see LICENSE.txt
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : Christian.Maeder@dfki.de
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiStability : experimental
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder-}
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskimodule ModalCaslToMu where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskiimport Control.Monad as Monad
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskiimport Data.Maybe as Maybe
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskiimport ModalCasl as Casl
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Mu as Mu
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder{------------------------------------------------------------------------------}
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{- -}
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{- Convert Modal CASL formulas to formulas of the �-Calculus -}
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{- -}
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder{------------------------------------------------------------------------------}
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederconvert :: Casl.StateFormula a -> Maybe (Mu.StateFormula a)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiconvert (Casl.Var x) = Just (Mu.Var x)
0c2a90cbfb63865ff485c3fbe20a14589a5914beTill Mossakowski
9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowskiconvert (Casl.Snot phi) = liftM Mu.Snot (convert phi)
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maederconvert (Casl.Sand phi psi) = liftM2 Mu.Sand (convert phi) (convert psi)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederconvert (Casl.Sor phi psi) = liftM2 Mu.Sor (convert phi) (convert psi)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiconvert (Casl.E phi) = liftM Mu.E (convert' phi)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiconvert (Casl.A phi) = liftM Mu.A (convert' phi)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maederconvert (Casl.Diamond phi) = liftM Mu.Diamond (convert phi)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maederconvert (Casl.Box phi) = liftM Mu.Box (convert phi)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiconvert (Casl.DiamondPast phi) = liftM Mu.DiamondPast (convert phi)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiconvert (Casl.BoxPast phi) = liftM Mu.BoxPast (convert phi)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiconvert (Casl.Mu x phi) = liftM (Mu.Mu x) (convert phi)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiconvert (Casl.Nu x phi) = liftM (Mu.Nu x) (convert phi)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiconvert' :: Casl.PathFormula a -> Maybe (Mu.PathFormula a)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiconvert' (Casl.State phi) = liftM Mu.SF (convert phi)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiconvert' (Casl.Pnot phi) = liftM Mu.Pnot (convert' phi)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiconvert' (Casl.Pand phi psi) = liftM2 Mu.Pand (convert' phi) (convert' psi)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederconvert' (Casl.Por phi psi) = liftM2 Mu.Por (convert' phi) (convert' psi)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maederconvert' (Casl.X phi) = liftM Mu.X (convert' phi)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiconvert' _ = Nothing
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{------------------------------------------------------------------------------}
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder