From c49c65d04f5d23809f49e81e64f23ae72ae2eecb Mon Sep 17 00:00:00 2001
From: Hans-Peter Deifel <hpd@hpdeifel.de>
Date: Wed, 15 Feb 2017 10:35:21 +0100
Subject: [PATCH] Make graph comparison available in CLI
---
osek-verification.cabal | 1 +
src/main/Main.hs | 23 ++++++++++++++++++++++-
2 files changed, 23 insertions(+), 1 deletion(-)
diff --git a/osek-verification.cabal b/osek-verification.cabal
index 1d57383..041b826 100644
--- a/osek-verification.cabal
+++ b/osek-verification.cabal
@@ -55,6 +55,7 @@ executable mockup_generator
, bytestring >= 0.10 && <0.11
, osek-verification
, optparse-applicative >= 0.12 && <0.13
+ , microlens >= 0.4 && < 0.5
hs-source-dirs: src/main
default-language: Haskell2010
ghc-options: -Wall -fdefer-typed-holes -fno-warn-name-shadowing
diff --git a/src/main/Main.hs b/src/main/Main.hs
index 9245342..6b3eddc 100644
--- a/src/main/Main.hs
+++ b/src/main/Main.hs
@@ -3,10 +3,13 @@
module Main where
import Control.Monad
+import System.IO
+import System.Exit
import qualified Data.ByteString.Lazy as BS
import qualified Data.Text.IO as T
import Options.Applicative
+import Lens.Micro
import CFG.Types
import qualified CFG.Parser as P
@@ -15,6 +18,9 @@ import CFG.IR
import CFG.C
import CFG.Sanitize
import Search.Search
+import qualified Compare.JSON as JSON
+import Compare.Compare
+import Compare.Types
data Command = Mockup MockupOpts | Search SearchOpts
@@ -27,12 +33,14 @@ optParser = subparser
data SearchOpts = SearchOpts
{ mockupExecutable :: FilePath
+ , sseGraphJsonFile :: Maybe FilePath
, eliminateEpsilons :: Bool
}
searchOptParser :: Parser SearchOpts
searchOptParser = SearchOpts
<$> argument str (metavar "EXECUTABLE")
+ <*> optional (argument str (metavar "SSE-JSON"))
<*> (not <$> switch ( long "no-epsilon-elimination"
<> help "Don't do epsilon elimination on the search graph"
))
@@ -53,7 +61,20 @@ main = do
( fullDesc <> progDesc "dOSEK verification tool" )
case cmd of
(Search opts) -> do
- void (driver (eliminateEpsilons opts) (mockupExecutable opts))
+ json <- traverse BS.readFile (sseGraphJsonFile opts)
+ case JSON.parseFile <$> json of
+ -- Don't do any comparision between graphs
+ Nothing -> void (driver (eliminateEpsilons opts) (mockupExecutable opts))
+ Just (Left e) -> do
+ hPutStrLn stderr $ "Could not parse sse graph json: " <> e
+ exitFailure
+ Just (Right graph1) -> do
+ graph2 <- driver (eliminateEpsilons opts) (mockupExecutable opts)
+ if (not (isDeterministic (graph1^._graph)) || not (isDeterministic (graph2^._graph))) then do
+ hPutStrLn stderr $ "One of the graphs is not deterministic"
+ exitFailure
+ else
+ hPrint stderr (isIsomorphic graph1 graph2)
Mockup opts -> do
cntnt <- BS.getContents
case P.parseFile cntnt of
--
GitLab