diff --git a/osek-verification.cabal b/osek-verification.cabal index a49f997c3c1762dc2285f272d760b00706078c9a..d091c7e94157e30bfe3b7be1cfe7f8939143aa6f 100644 --- a/osek-verification.cabal +++ b/osek-verification.cabal @@ -34,6 +34,7 @@ library , Compare.Matching , Compare.Preprocess , Compare.SSEGraph + , Compare.GraphDebugger hs-source-dirs: src build-depends: base >=4.9 && <4.10 , megaparsec >= 5 && <5.3 @@ -52,6 +53,7 @@ library , hashable >= 1.2 && < 1.3 , unix >= 2.7 && <2.8 , attoparsec >= 0.13 && <0.14 + , haskeline >= 0.7 && <0.8 default-language: Haskell2010 ghc-options: -Wall -fno-warn-name-shadowing diff --git a/src/Compare/GraphDebugger.hs b/src/Compare/GraphDebugger.hs new file mode 100644 index 0000000000000000000000000000000000000000..02cf0a5eb88073e24b8473bfe720041b9a0e097b --- /dev/null +++ b/src/Compare/GraphDebugger.hs @@ -0,0 +1,85 @@ +module Compare.GraphDebugger (debugGraph) where + +import Data.Semigroup +import Data.Tuple + +import Control.Monad.Reader +import qualified Data.Graph.Inductive.Graph as G +import Data.Text (Text) +import qualified Data.Text as T +import Lens.Micro +import System.Console.Haskeline +import Data.HashMap.Strict (HashMap) +import qualified Data.HashMap.Strict as HM + +import Compare.Types +import Compare.Types.Lenses + +data State = State + { stGraph :: Graph Text Text + , stNodes :: HashMap Text G.Node + } + +type M = InputT (ReaderT State IO) + +debugGraph :: Graph Text Text -> IO () +debugGraph g = + let + nodeMap = HM.fromList $ map swap (g^. _graph . to G.labNodes) + state = State g nodeMap + in + runReaderT (runInputT defaultSettings loop) state + where + loop :: M () + loop = do + input <- fmap words <$> getInputLine "> " + case input of + Nothing -> return () + Just [] -> loop + Just ("help":_) -> help >> loop + Just ("stat":args) -> stat args >> loop + Just ("entry":args) -> entry args >> loop + Just ("out":args) -> outEdges args >> loop + Just ("in":args) -> inEdges args >> loop + Just (cmd:_) -> outputStrLn ("Unknown command " <> cmd) >> loop + +help :: M () +help = outputStr $ unlines $ + [ "Available commands: " + , " help" + ] + +type Command = [String] -> M () + +stat :: Command +stat [] = do + g <- lift $ asks stGraph + outputStrLn ("Node count: " <> show (g ^. _graph . to G.noNodes)) + outputStrLn ("Edge count: " <> show (g ^. _graph . to G.size)) +stat _ = outputStrLn "Invalid arguments for \"stat\"" + +entry :: Command +entry [] = do + g <- lift $ asks stGraph + outputStrLn ("Entry node " <> T.unpack (g ^. node (g ^. _point))) +entry _ = outputStrLn "Invalid arguments for \"entry\"" + +outEdges :: Command +outEdges [n] = do + State g nodes <- lift ask + case HM.lookup (T.pack n) nodes of + Nothing -> outputStrLn "Node not found" + Just n' -> do + forM_ (g^..out n') $ \(_,to,l) -> + outputStrLn ("--" <> T.unpack l <> "-> " <> T.unpack (g^?!node to)) +outEdges _ = outputStrLn "Invalid arguments for \"out\"" + +inEdges :: Command +inEdges [n] = do + State g nodes <- lift ask + case HM.lookup (T.pack n) nodes of + Nothing -> outputStrLn "Node not found" + Just n' -> do + forM_ (g^..inn n') $ \(_,to,l) -> + outputStrLn ("--" <> T.unpack l <> "-> " <> T.unpack (g^?!node to)) +inEdges _ = outputStrLn "Invalid arguments for \"in\"" diff --git a/src/main/Main.hs b/src/main/Main.hs index 00db6a64328bc265de74f76b39cd236038e876cb..b9a7def99777aa9cb700639e2949b441760b6541 100644 --- a/src/main/Main.hs +++ b/src/main/Main.hs @@ -31,6 +31,7 @@ import Compare.Preprocess import Compare.SSEGraph import Compare.Types import Compare.Types.Lenses +import Compare.GraphDebugger import Search.Dot import qualified Search.EpsilonElimination as EE import Search.Search @@ -41,6 +42,7 @@ data Command = Mockup MockupOpts | JSON2DOT (Maybe FilePath) | Compare CompareOpts | EpsilonEliminate EpsilonOpts + | DebugGraph (Maybe FilePath) optParser :: Parser Command optParser = subparser @@ -53,6 +55,8 @@ optParser = subparser (progDesc "compare SSE and search graph")) <> command "ee" (info (helper <*> (EpsilonEliminate <$> epsilonParser)) (progDesc "epsilon eliminate graph and dump it to stdout")) + <> command "debug" (info (helper <*> (DebugGraph <$> json2DotParser)) + (progDesc "Start graph debugger")) ) data SearchOpts = SearchOpts @@ -161,6 +165,11 @@ main = do let Right x = (JSON.parseFile json) <> (JSON.parseFile json & _Right . nodes %~ T.pack . show @Int) LT.putStrLn (graph2dot x) + DebugGraph file -> do + json <- maybe BS.getContents BS.readFile file + let Right x = (JSON.parseFile json) + <> (JSON.parseFile json & _Right . nodes %~ T.pack . show @Int) + debugGraph x Compare opts -> do sseJSON <- BS.readFile (sseGraphFile opts) searchJSON <- BS.readFile (searchGraphFile opts)