b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescu{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./Temporal/ModalCaslToMu.hs

f1edf379717f0ddb7607585a027cf6f03a6fce68Christian MaederCopyright : (c) Klaus Hartke, Uni Bremen 2008

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescu

f1edf379717f0ddb7607585a027cf6f03a6fce68Christian MaederMaintainer : Christian.Maeder@dfki.de

f1edf379717f0ddb7607585a027cf6f03a6fce68Christian MaederStability : experimental

f1edf379717f0ddb7607585a027cf6f03a6fce68Christian MaederPortability : portable

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescu

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescu-}

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskimodule ModalCaslToMu where

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport Control.Monad as Monad

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport Data.Maybe as Maybe

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport ModalCasl as Casl

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Mu

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------------------------------------------------

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederConvert Modal CASL formulas to formulas of the µ-Calculus

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------------------------------------------------- -}

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiconvert :: Casl.StateFormula a -> Maybe (Mu.StateFormula a)

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconvert (Casl.Var x) = Just (Mu.Var x)

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconvert (Casl.Snot phi) = liftM Mu.Snot (convert phi)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconvert (Casl.Sand phi psi) = liftM2 Mu.Sand (convert phi) (convert psi)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconvert (Casl.Sor phi psi) = liftM2 Mu.Sor (convert phi) (convert psi)

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconvert (Casl.E phi) = liftM Mu.E (convert' phi)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconvert (Casl.A phi) = liftM Mu.A (convert' phi)

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconvert (Casl.Diamond phi) = liftM Mu.Diamond (convert phi)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconvert (Casl.Box phi) = liftM Mu.Box (convert phi)

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconvert (Casl.DiamondPast phi) = liftM Mu.DiamondPast (convert phi)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconvert (Casl.BoxPast phi) = liftM Mu.BoxPast (convert phi)

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconvert (Casl.Mu x phi) = liftM (Mu.Mu x) (convert phi)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconvert (Casl.Nu x phi) = liftM (Mu.Nu x) (convert phi)

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiconvert' :: Casl.PathFormula a -> Maybe (Mu.PathFormula a)

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconvert' (Casl.State phi) = liftM Mu.SF (convert phi)

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconvert' (Casl.Pnot phi) = liftM Mu.Pnot (convert' phi)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconvert' (Casl.Pand phi psi) = liftM2 Mu.Pand (convert' phi) (convert' psi)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconvert' (Casl.Por phi psi) = liftM2 Mu.Por (convert' phi) (convert' psi)

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconvert' (Casl.X phi) = liftM Mu.X (convert' phi)

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconvert' _ = Nothing

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ----------------------------------------------------------------------------