content: {- |
  Module      :  ./Temporal/Main.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 Main where
  
  import Control.Monad (when)
  import Data.List (intersperse)
  import System.Directory (doesFileExist)
  import System.Environment (getArgs)
  import System.Exit (exitFailure)
  import System.IO (getContents, hReady, stdin)
  import Text.ParserCombinators.Parsec (parse)
  
  import ModalCasl as Casl
  import ModalCaslToNuSmvLtl as CaslToLtl
  import NuSmv
  
  main :: IO ()
  
  main = do args <- getArgs
            file <- if length args == 1 then doesFileExist (head args)
                                        else return False
  
            formula <- if file then readFile (head args)
                               else return (unwords args)
  
            let filename = if file then head args
                                   else "<<arguments>>"
  
            case parse (Casl.parser CaslToLtl.expr) filename formula of
                 Left e1 -> do print e1
                               exitFailure
                 Right cf -> case CaslToLtl.convert cf of
                  Nothing -> do putStrLn "Not a LTL formula."
                                exitFailure
                  Just lf -> do i <- hReady stdin
                                when i $
                                   do contents <- getContents
                                      case parse NuSmv.program "<<input>>"
                                                 contents of
                                       Left e2 -> do print e2
                                                     exitFailure
                                       Right model -> print model
                                print lf
  