content: {- |
  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
  
  
  -- ----------------------------------------------------------------------------
  