diff --git a/osek-verification.cabal b/osek-verification.cabal index db8ad3a9ed5df97226334c011ce7eaf1447bb905..1d573839733aa811750fe3816a882a8c1c3e2780 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 0000000000000000000000000000000000000000..e76e20e4e6a8c5e4569c557927591cd4feada291 --- /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 b725f913948fa38488bc70e1c3cddfdb5a7c5a64..4622e8490a6ec63368f0eb1988340ef139c247f6 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 8e213b3cb39ad6b413cf969fa36976e3bf68e6ce..ccbd40264a8b9e65e9d2c19df5ec843df4e91ee3 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 9e18d42dd85d0d6492849a457f93b871dc756116..9245342908416fdb06e6c9d78005f6543bd55f52 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