Main.hs revision b87efd3db0d2dc41615ea28669faf80fc1b48d56
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceModule : $EmptyHeader$
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceDescription : <optional short description entry>
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceCopyright : (c) <Authors or Affiliations>
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceLicense : GPLv2 or higher
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceMaintainer : <email>
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceStability : unstable | experimental | provisional | stable | frozen
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancePortability : portable | non-portable (<reason>)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance<optional description>
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancemodule Main where
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport Data.List (intersperse)
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Manceimport System.Directory (doesFileExist)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport System.Exit (exitFailure)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport System.IO (getContents, hWaitForInput, stdin)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport Text.ParserCombinators.Parsec (parse)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport ModalCasl as Casl
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport ModalCaslToNuSmvLtl as CaslToLtl
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport NuSmv as NuSmv
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancemain = do args <- getArgs
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance file <- if length args == 1 then doesFileExist (args !! 0)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance else return False
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance formula <- if file then readFile (args !! 0)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance else return (concat (intersperse " " args))
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance let filename = if file then args !! 0
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance else "<<arguments>>"
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance case parse (Casl.parser CaslToLtl.expr) filename formula of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Left e1 -> do putStrLn (show e1)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Right cf -> case CaslToLtl.convert cf of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Nothing -> do putStrLn "Not a LTL formula."
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Just lf -> do i <- hWaitForInput stdin 0
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance when i $ do contents <- getContents
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance case parse NuSmv.program "<<input>>" contents of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Left e2 -> do putStrLn (show e2)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Right model -> do putStrLn (show model)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance putStrLn (show lf)