diff --git a/osek-verification.cabal b/osek-verification.cabal index 41c47077eea7a21630647f0de871ad79dfdfff0c..ffba188149df1d0abe646cf89459d1a253ecf96f 100644 --- a/osek-verification.cabal +++ b/osek-verification.cabal @@ -61,6 +61,7 @@ executable mockup_generator , osek-verification , optparse-applicative >= 0.12 && <0.14 , microlens >= 0.4 && < 0.5 + , aeson >= 1.0 && <1.1 hs-source-dirs: src/main default-language: Haskell2010 ghc-options: -Wall -fno-warn-name-shadowing diff --git a/src/main/Main.hs b/src/main/Main.hs index f9b5ec9aa3a5c3a57c3d34b8ce0fe9eecac6c868..441279b23b705ddd49471c37cc79de2f1445ed90 100644 --- a/src/main/Main.hs +++ b/src/main/Main.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE LambdaCase #-} module Main where @@ -12,6 +13,7 @@ import Data.Text (Text) import qualified Data.Text.IO as T import Lens.Micro import Options.Applicative +import Data.Aeson import CFG.Types import qualified CFG.Parser as P @@ -21,12 +23,18 @@ import CFG.C import CFG.Sanitize import Search.Search import Search.Dot +import qualified Search.EpsilonElimination as EE import qualified Compare.JSON as JSON import Compare.Compare import Compare.Types import Compare.Preprocess +import Compare.SSEGraph -data Command = Mockup MockupOpts | Search SearchOpts | JSON2DOT FilePath | Compare CompareOpts +data Command = Mockup MockupOpts + | Search SearchOpts + | JSON2DOT FilePath + | Compare CompareOpts + | EpsilonEliminate EpsilonOpts optParser :: Parser Command optParser = subparser @@ -37,6 +45,8 @@ optParser = subparser (progDesc "generate dot graph on stdout from json")) <> command "compare" (info (helper <*> (Compare <$> compareParser)) (progDesc "compare SSE and search graph")) + <> command "ee" (info (helper <*> (EpsilonEliminate <$> epsilonParser)) + (progDesc "epsilon eliminate graph and dump it to stdout")) ) data SearchOpts = SearchOpts @@ -78,11 +88,24 @@ compareParser = CompareOpts <$> argument str (metavar "SSE-JSON") <*> argument str (metavar "SEARCH-JSON") +data EpsilonOpts = EpsilonOpts FilePath + +epsilonParser :: Parser EpsilonOpts +epsilonParser = EpsilonOpts <$> argument str (metavar "JSON-GRAPH") + main :: IO () main = do cmd <- execParser $ info (helper <*> optParser) ( fullDesc <> progDesc "dOSEK verification tool" ) case cmd of + EpsilonEliminate (EpsilonOpts file) -> do + json <- BS.readFile file + case JSON.parseFile json of + Left err -> do + hPutStrLn stderr $ "Could not parse sse graph json: " <> err + exitFailure + Right (graph :: Graph NodeLabelMeta SSEEdgeLabel) -> do + BS.putStr (encode (EE.eliminateEpsilons graph)) (Search opts) -> do json <- traverse BS.readFile (sseGraphJsonFile opts) case JSON.parseFile <$> json of @@ -121,4 +144,3 @@ main = do NotIsomorphic reason -> do putStrLn "Graphs are not isomorphic :(" print reason -