b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescu{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./Temporal/Main.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-}

f1edf379717f0ddb7607585a027cf6f03a6fce68Christian Maeder

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskimodule Main where

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport Control.Monad (when)

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport Data.List (intersperse)

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport System.Directory (doesFileExist)

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport System.Environment (getArgs)

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport System.Exit (exitFailure)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport System.IO (getContents, hReady, stdin)

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport Text.ParserCombinators.Parsec (parse)

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport ModalCasl as Casl

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport ModalCaslToNuSmvLtl as CaslToLtl

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport NuSmv

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskimain :: IO ()

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskimain = do args <- getArgs

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder file <- if length args == 1 then doesFileExist (head args)

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski else return False

9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder formula <- if file then readFile (head args)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else return (unwords args)

9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let filename = if file then head args

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski else "<<arguments>>"

9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski case parse (Casl.parser CaslToLtl.expr) filename formula of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Left e1 -> do print e1

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder exitFailure

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski Right cf -> case CaslToLtl.convert cf of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Nothing -> do putStrLn "Not a LTL formula."

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder exitFailure

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Just lf -> do i <- hReady stdin

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder when i $

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder do contents <- getContents

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder case parse NuSmv.program "<<input>>"

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder contents of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Left e2 -> do print e2

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder exitFailure

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Right model -> print model

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder print lf