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