From 15c1a5bc26046e8d54a7444de8a448d2d402189e Mon Sep 17 00:00:00 2001
From: Hans-Peter Deifel <hpd@hpdeifel.de>
Date: Wed, 15 Feb 2017 09:43:39 +0100
Subject: [PATCH] Add module to prepare search graph for comparison
---
osek-verification.cabal | 1 +
src/Search/Prepare.hs | 21 +++++++++++++++++++++
src/Search/Search.hs | 39 +++++++++++++++++++++------------------
src/Search/Types.hs | 5 +----
src/main/Main.hs | 4 +++-
5 files changed, 47 insertions(+), 23 deletions(-)
create mode 100644 src/Search/Prepare.hs
diff --git a/osek-verification.cabal b/osek-verification.cabal
index db8ad3a..1d57383 100644
--- a/osek-verification.cabal
+++ b/osek-verification.cabal
@@ -25,6 +25,7 @@ library
, Search.Types
, Search.EpsilonElimination
, Search.Dot
+ , Search.Prepare
, Protocol
, Compare.JSON
, Compare.Types
diff --git a/src/Search/Prepare.hs b/src/Search/Prepare.hs
new file mode 100644
index 0000000..e76e20e
--- /dev/null
+++ b/src/Search/Prepare.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Search.Prepare (prepareForCompare) where
+
+import Data.Monoid
+
+import qualified Data.Graph.Inductive as G
+import Data.Text (Text)
+import Lens.Micro
+
+import Search.Types
+
+prepareForCompare :: Graph VertexLabel EdgeLabel -> Graph Text Text
+prepareForCompare = over _graph (G.nemap formatNode formatEdge)
+
+formatNode :: VertexLabel -> Text
+formatNode vert = vertState vert <> "@" <> vertABB vert
+
+formatEdge :: EdgeLabel -> Text
+formatEdge (EdgeLabel Nothing) = "" -- should not happen after EpsilonElimination
+formatEdge (EdgeLabel (Just x)) = x
diff --git a/src/Search/Search.hs b/src/Search/Search.hs
index b725f91..4622e84 100644
--- a/src/Search/Search.hs
+++ b/src/Search/Search.hs
@@ -4,7 +4,6 @@
module Search.Search (driver) where
-import Control.Monad
import Data.IORef
import Data.Map (Map)
import qualified Data.Map as M
@@ -28,6 +27,7 @@ import Protocol
import Search.Types
import Search.EpsilonElimination
import Search.Dot
+import Search.Prepare
type DecisionNumber = Int
type Decision = (G.Node, DecisionNumber)
@@ -90,10 +90,10 @@ findOpenDecision = listToMaybe . mapMaybe isHalf . M.elems . view decisions
type EliminateEpsilons = Bool
-driver :: EliminateEpsilons -> FilePath -> IO ()
+driver :: EliminateEpsilons -> FilePath -> IO (Graph Text Text)
driver ee prog = driver' ee prog (VertexLabel "start" "" "")
-driver' :: EliminateEpsilons -> FilePath -> VertexLabel -> IO ()
+driver' :: EliminateEpsilons -> FilePath -> VertexLabel -> IO (Graph Text Text)
driver' elimEpsis prog startVertex = do
let startOS = Just "startOS" -- first edge
state <- newIORef $ State
@@ -106,21 +106,24 @@ driver' elimEpsis prog startVertex = do
}
oneProgRun prog state Nothing
- forever $ do
- modifyIORef state $ \s -> (s & curTrace .~ []
- & currentVertex .~ 0
- & currentSyscall .~ startOS)
-
- findOpenDecision <$> readIORef state >>= \case
- Nothing -> do
- s <- readIORef state
- let graph' = if elimEpsis
- then eliminateEpsilons (s^.foundGraph)
- else s^.foundGraph
- T.putStrLn (dottify graph')
- exitSuccess
- Just trace ->
- oneProgRun prog state (Just $ reverse trace)
+ let loop = do
+ modifyIORef state $ \s -> (s & curTrace .~ []
+ & currentVertex .~ 0
+ & currentSyscall .~ startOS)
+
+ findOpenDecision <$> readIORef state >>= \case
+ Nothing -> do
+ s <- readIORef state
+ let graph' = if elimEpsis
+ then eliminateEpsilons (s^.foundGraph)
+ else s^.foundGraph
+ T.putStrLn (dottify graph')
+ return $ prepareForCompare graph'
+ Just trace -> do
+ oneProgRun prog state (Just $ reverse trace)
+ loop
+
+ loop
oneProgRun :: FilePath -> IORef State -> Maybe [Bool] -> IO ()
oneProgRun prog state trace = do
diff --git a/src/Search/Types.hs b/src/Search/Types.hs
index 8e213b3..ccbd402 100644
--- a/src/Search/Types.hs
+++ b/src/Search/Types.hs
@@ -26,10 +26,7 @@ instance Eq VertexLabel where
instance Ord VertexLabel where
compare v1 v2 = compare (vertState v1, vertABB v1) (vertState v2, vertABB v2)
-data EdgeLabel = EdgeLabel
- {
- edgeSyscall :: Maybe Text -- ^ Nothing if transition wasn't a syscall
- }
+data EdgeLabel = EdgeLabel { edgeSyscall :: Maybe Text } -- ^ Nothing if transition wasn't a syscall
deriving (Eq, Ord, Show)
-- TODO Document
diff --git a/src/main/Main.hs b/src/main/Main.hs
index 9e18d42..9245342 100644
--- a/src/main/Main.hs
+++ b/src/main/Main.hs
@@ -2,6 +2,8 @@
module Main where
+import Control.Monad
+
import qualified Data.ByteString.Lazy as BS
import qualified Data.Text.IO as T
import Options.Applicative
@@ -51,7 +53,7 @@ main = do
( fullDesc <> progDesc "dOSEK verification tool" )
case cmd of
(Search opts) -> do
- driver (eliminateEpsilons opts) (mockupExecutable opts)
+ void (driver (eliminateEpsilons opts) (mockupExecutable opts))
Mockup opts -> do
cntnt <- BS.getContents
case P.parseFile cntnt of
--
GitLab