{- |
Module      :  ./Temporal/ModalCaslToNuSmvLtl.hs
Copyright   :  (c) Klaus Hartke, Uni Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

-}

module ModalCaslToNuSmvLtl where

import Control.Monad as Monad
import Data.Maybe as Maybe
import Text.ParserCombinators.Parsec hiding (State)

import ModalCasl as Casl
import NuSmvLtl as Ltl


{- ----------------------------------------------------------------------------
Convert Modal CASL formulas to LTL formulas recognized by NuSMV
---------------------------------------------------------------------------- -}


convert :: Casl.StateFormula a -> Maybe (Ltl.Formula a)

convert (Casl.Var x) = Just (Ltl.Var x)
convert (Casl.A phi) = convert' phi
convert _ = Nothing


convert' :: Casl.PathFormula a -> Maybe (Ltl.Formula a)

convert' (Casl.Por (Casl.Pnot phi) psi) = liftM2 Ltl.Impl (convert' phi)
                                                          (convert' psi)

convert' (Casl.State (Casl.Var x)) = Just (Ltl.Var x)

convert' (Casl.Pnot phi) = liftM Ltl.Not (convert' phi)
convert' (Casl.Pand phi psi) = liftM2 Ltl.And (convert' phi) (convert' psi)
convert' (Casl.Por phi psi) = liftM2 Ltl.Or (convert' phi) (convert' psi)

convert' (Casl.X phi) = liftM Ltl.X (convert' phi)
convert' (Casl.G phi) = liftM Ltl.G (convert' phi)
convert' (Casl.F phi) = liftM Ltl.F (convert' phi)

convert' (Casl.W phi psi) = convert' ((phi `Casl.Pand` psi) `Casl.B`
                                          (Casl.Pnot phi `Casl.Pand` psi))
convert' (Casl.U phi psi) = convert' (psi `Casl.B` (Casl.Pnot phi `Casl.Pand`
                                                        Casl.Pnot psi))
convert' (Casl.B phi psi) = liftM2 Ltl.V (convert' phi) (convert' psi)

convert' (Casl.W' phi psi) = convert' (Casl.Pnot psi `Casl.U'`
                                           (phi `Casl.Pand` psi))
convert' (Casl.U' phi psi) = liftM2 Ltl.U (convert' phi) (convert' psi)
convert' (Casl.B' phi psi) = convert' (Casl.Pnot psi `Casl.U'`
                                           (phi `Casl.Pand` Casl.Pnot psi))

convert' (Casl.XPast phi) = liftM Ltl.Y (convert' phi)
convert' (Casl.GPast phi) = liftM Ltl.H (convert' phi)
convert' (Casl.FPast phi) = liftM Ltl.O (convert' phi)

convert' (Casl.WPast phi psi) = convert' ((phi `Casl.Pand` psi) `Casl.BPast`
                                              (Casl.Pnot phi `Casl.Pand` psi))
convert' (Casl.UPast phi psi) = convert' (psi `Casl.BPast`
                                     (Casl.Pnot phi `Casl.Pand` Casl.Pnot psi))
convert' (Casl.BPast phi psi) = liftM2 Ltl.T (convert' phi) (convert' psi)

convert' (Casl.WPast' phi psi) = convert' (Casl.Pnot psi `Casl.UPast'`
                                               (phi `Casl.Pand` psi))
convert' (Casl.UPast' phi psi) = liftM2 Ltl.S (convert' phi) (convert' psi)
convert' (Casl.BPast' phi psi) = convert' (Casl.Pnot psi `Casl.UPast'`
                                      (phi `Casl.Pand` Casl.Pnot psi))

convert' (Casl.XPast' phi) = liftM Ltl.Z (convert' phi)

convert' _ = Nothing


-- ----------------------------------------------------------------------------


data Expr = Expr String

instance Show Expr where show (Expr x) = x

expr = liftM Expr (many1 (lower <|> char '=' <|> char '_' <|> char '.' <|>
                              digit))

parseAndConvert :: String -> Formula Expr
parseAndConvert text = let Right x = parse (Casl.parser expr) "<<input>>" text
                           Just y = convert x in y


-- ----------------------------------------------------------------------------
