Main.hs revision 26db4a742376d513cdba128780ee8ca60eeb927e
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskimodule Main where
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport Data.List (intersperse)
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport System.Directory (doesFileExist)
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport System.Exit (exitFailure)
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport System.IO (getContents, hWaitForInput, stdin)
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport Text.ParserCombinators.Parsec (parse)
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport ModalCasl as Casl
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport ModalCaslToNuSmvLtl as CaslToLtl
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport NuSmv as NuSmv
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskimain = do args <- getArgs
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski file <- if length args == 1 then doesFileExist (args !! 0)
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski else return False
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski formula <- if file then readFile (args !! 0)
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski else return (concat (intersperse " " args))
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski let filename = if file then args !! 0
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski else "<<arguments>>"
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski case parse (Casl.parser CaslToLtl.expr) filename formula of
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski Left e1 -> do putStrLn (show e1)
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski Right cf -> case CaslToLtl.convert cf of
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski Nothing -> do putStrLn "Not a LTL formula."
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski Just lf -> do i <- hWaitForInput stdin 0
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski when i $ do contents <- getContents
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski case parse NuSmv.program "<<input>>" contents of
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski Left e2 -> do putStrLn (show e2)
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski Right model -> do putStrLn (show model)
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski putStrLn (show lf)