kore-repl: In the graph visualizer add no. of nodes on dotted edges (#2944)

* kore-repl: In the graph visualizer add no. of nodes on dotted edges

* Use data EdgeLabel

Co-authored-by: rv-jenkins <[email protected]>

Author: andreiburdusa

kore/src/Kore/Repl/Interpreter.hs

@@ -490,7 +490,7 @@ showGraph view mfile out = do
     processedGraph <-
         case view of
             Just Expanded ->
-                return $ Graph.emap Just graph
+                return $ Graph.emap IndividualLabel graph
             _ ->
                 maybe (showOriginalGraph graph) return (smoothOutGraph graph)
     installed <- liftIO Graph.isGraphvizInstalled
@@ -507,7 +507,7 @@ showGraph view mfile out = do
         putStrLn'
             "Could not process execution graph for visualization.\
             \ Will default to showing the full graph."
-        return $ Graph.emap Just graph
+        return $ Graph.emap IndividualLabel graph
 
 -- | Executes 'n' prove steps, or until branching occurs.
 proveSteps ::
@@ -1448,7 +1448,7 @@ printNotFound = putStrLn' "Variable or index not found"
 showDotGraph ::
     From axiom AttrLabel.Label =>
     From axiom RuleIndex =>
-    Gr CommonClaimState (Maybe (Seq axiom)) ->
+    Gr CommonClaimState (EdgeLabel (Seq axiom)) ->
     IO ()
 showDotGraph gr =
     flip Graph.runGraphvizCanvas' Graph.Xlib
@@ -1459,7 +1459,7 @@ showDotGraph gr =
 showDotGraphCatchException ::
     From axiom AttrLabel.Label =>
     From axiom RuleIndex =>
-    Gr CommonClaimState (Maybe (Seq axiom)) ->
+    Gr CommonClaimState (EdgeLabel (Seq axiom)) ->
     IO ()
 showDotGraphCatchException gr =
     catch (showDotGraph gr) $ \(e :: GraphvizException) ->
@@ -1479,7 +1479,7 @@ showDotGraphCatchException gr =
 saveDotGraph ::
     From axiom AttrLabel.Label =>
     From axiom RuleIndex =>
-    Gr CommonClaimState (Maybe (Seq axiom)) ->
+    Gr CommonClaimState (EdgeLabel (Seq axiom)) ->
     Graph.GraphvizOutput ->
     FilePath ->
     IO ()
@@ -1499,17 +1499,17 @@ saveDotGraph gr format file =
 graphParams ::
     From axiom AttrLabel.Label =>
     From axiom RuleIndex =>
-    Gr CommonClaimState (Maybe (Seq axiom)) ->
+    Gr CommonClaimState (EdgeLabel (Seq axiom)) ->
     Graph.GraphvizParams
         Graph.Node
         CommonClaimState
-        (Maybe (Seq axiom))
+        (EdgeLabel (Seq axiom))
         ()
         CommonClaimState
 graphParams gr =
     Graph.nonClusteredParams
         { Graph.fmtEdge = \(_, resN, l) ->
-            [ Graph.textLabel (maybe "" (ruleIndex resN) l)
+            [ Graph.textLabel (eitherEdgeLabel nrOfNodes (ruleIndex resN) l)
             , Graph.Attr.Style [dottedOrSolidEdge l]
             ]
         , Graph.fmtNode = \(_, ps) ->
@@ -1521,9 +1521,13 @@ graphParams gr =
             ]
         }
   where
+    nrOfNodes :: Natural -> Text.Lazy.Text
+    nrOfNodes quantity
+        | quantity < 1 = ""
+        | otherwise = "(" <> Text.Lazy.pack (show quantity) <> " nodes omitted)"
     dottedOrSolidEdge lbl =
-        maybe
-            (Graph.Attr.SItem Graph.Attr.Dotted mempty)
+        eitherEdgeLabel
+            (const $ Graph.Attr.SItem Graph.Attr.Dotted mempty)
             (const $ Graph.Attr.SItem Graph.Attr.Solid mempty)
             lbl
     ruleIndex resultNode lbl =

kore/src/Kore/Repl/State.hs

@@ -6,6 +6,10 @@ License     : BSD-3-Clause
 Maintainer  : [email protected]
 -}
 module Kore.Repl.State (
+    EdgeLabel (..),
+    eitherEdgeLabel,
+    ommitedNodes,
+    individualLabel,
     emptyExecutionGraph,
     getClaimByIndex,
     getAxiomByIndex,
@@ -80,6 +84,7 @@ import Data.Graph.Inductive.PatriciaTree (
 import qualified Data.Graph.Inductive.Query.DFS as Graph
 import Data.List.Extra (
     findIndex,
+    genericLength,
     groupSort,
  )
 import Data.Map.Strict (
@@ -340,13 +345,13 @@ updateExecutionGraph gph = do
  with its edges pointed "downwards" (from the root)
  and is partially ordered (parent(node) < node).
 -}
-smoothOutGraph :: Gr node edge -> Maybe (Gr node (Maybe edge))
+smoothOutGraph :: Gr node edgeLabel -> Maybe (Gr node (EdgeLabel edgeLabel))
 smoothOutGraph graph = do
     let subGraph = Graph.nfilter inOutDegreeOne graph
     edgesToAdd <-
         traverse (componentToEdge subGraph) (Graph.components subGraph)
     let nodesToRemove = Graph.nodes subGraph
-        liftedSubGraph = Graph.emap Just (Graph.delNodes nodesToRemove graph)
+        liftedSubGraph = Graph.emap IndividualLabel (Graph.delNodes nodesToRemove graph)
         liftedGraph = Graph.insEdges edgesToAdd liftedSubGraph
     return liftedGraph
   where
@@ -356,32 +361,54 @@ smoothOutGraph graph = do
             && Graph.indeg graph node == 1
             && not (all isBranchingNode $ Graph.pre graph node)
     componentToEdge ::
-        Gr node edge ->
+        Gr node edgeLabel ->
         [Graph.Node] ->
-        Maybe (Graph.LEdge (Maybe edge))
+        Maybe (Graph.LEdge (EdgeLabel edgeLabel))
     componentToEdge subGraph nodes =
         case filter (isTerminalNode subGraph) nodes of
-            [node] -> makeNewEdge node node
+            [node] -> makeNewEdge node 1 node
             [node1, node2] ->
                 if node1 < node2
-                    then makeNewEdge node1 node2
-                    else makeNewEdge node2 node1
+                    then makeNewEdge node1 (genericLength nodes) node2
+                    else makeNewEdge node2 (genericLength nodes) node1
             _ -> Nothing
     makeNewEdge ::
         Graph.Node ->
+        Natural ->
         Graph.Node ->
-        Maybe (Graph.LEdge (Maybe edge))
-    makeNewEdge node1 node2 = do
+        Maybe (Graph.LEdge (EdgeLabel edgeLabel))
+    makeNewEdge node1 nrOfNodes node2 = do
         nodePre <- headMay (Graph.pre graph node1)
         nodeSuc <- headMay (Graph.suc graph node2)
-        return (nodePre, nodeSuc, Nothing)
+        return (nodePre, nodeSuc, OmmitedNodes nrOfNodes)
     isBranchingNode :: Graph.Node -> Bool
     isBranchingNode node =
         Graph.outdeg graph node > 1
-    isTerminalNode :: Gr node edge -> Graph.Node -> Bool
+    isTerminalNode :: Gr node edgeLabel -> Graph.Node -> Bool
     isTerminalNode graph' node =
         Graph.indeg graph' node == 0 || Graph.outdeg graph' node == 0
 
+data EdgeLabel individualLabel
+    = OmmitedNodes Natural
+    | IndividualLabel individualLabel
+    deriving stock (Eq, Ord)
+
+eitherEdgeLabel ::
+    (Natural -> a) ->
+    (individualLabel -> a) ->
+    EdgeLabel individualLabel ->
+    a
+eitherEdgeLabel f _ (OmmitedNodes quantity) = f quantity
+eitherEdgeLabel _ g (IndividualLabel label) = g label
+
+ommitedNodes :: EdgeLabel individualLabel -> Natural
+ommitedNodes (OmmitedNodes quantity) = quantity
+ommitedNodes _ = error "EdgeLabel.ommitedNodes: IndividualLabel"
+
+individualLabel :: EdgeLabel individualLabel -> individualLabel
+individualLabel (IndividualLabel label) = label
+individualLabel _ = error "EdgeLabel.individualLabel: OmmitedNodes"
+
 {- | Returns the first interesting branching node encountered by
 exploring the proof graph for 'n' steps over all branches, starting
 from 'node'. If no such node exists, it tries to return the only existing

kore/test/Test/Kore/Repl/Graph.hs

@@ -15,6 +15,7 @@ import Data.Set (
  )
 import qualified Data.Set as Set
 import Kore.Repl.State (
+    EdgeLabel (..),
     smoothOutGraph,
  )
 import Prelude.Kore
@@ -159,7 +160,7 @@ tree2 =
         , (4, 11)
         ]
 
-g1', g2', chain', tree1', tree2' :: Gr () (Maybe ())
+g1', g2', chain', tree1', tree2' :: Gr () (EdgeLabel ())
 g1' = fromJust $ smoothOutGraph g1
 g2' = fromJust $ smoothOutGraph g2
 chain' = fromJust $ smoothOutGraph chain
@@ -171,16 +172,16 @@ expectedG1'
     , expectedChain'
     , expectedTree1'
     , expectedTree2' ::
-        Gr () (Maybe ())
+        Gr () (EdgeLabel ())
 expectedG1' = Graph.mkGraph [(1, ())] []
 expectedG2' =
     Graph.mkGraph
         [(1, ()), (2, ())]
-        [(1, 2, Just ())]
+        [(1, 2, IndividualLabel ())]
 expectedChain' =
     Graph.mkGraph
         [(0, ()), (100, ())]
-        [(0, 100, Nothing)]
+        [(0, 100, OmmitedNodes 99)]
 expectedTree1' =
     Graph.mkGraph
         [ (0, ())
@@ -195,16 +196,16 @@ expectedTree1' =
         , (10, ())
         , (13, ())
         ]
-        [ (0, 1, Just ())
-        , (1, 2, Just ())
-        , (1, 3, Just ())
-        , (2, 5, Nothing)
-        , (5, 6, Just ())
-        , (5, 7, Just ())
-        , (5, 8, Just ())
-        , (6, 9, Just ())
-        , (8, 10, Just ())
-        , (3, 13, Nothing)
+        [ (0, 1, IndividualLabel ())
+        , (1, 2, IndividualLabel ())
+        , (1, 3, IndividualLabel ())
+        , (2, 5, OmmitedNodes 1)
+        , (5, 6, IndividualLabel ())
+        , (5, 7, IndividualLabel ())
+        , (5, 8, IndividualLabel ())
+        , (6, 9, IndividualLabel ())
+        , (8, 10, IndividualLabel ())
+        , (3, 13, OmmitedNodes 2)
         ]
 expectedTree2' =
     Graph.mkGraph
@@ -217,11 +218,11 @@ expectedTree2' =
         , (10, ())
         , (9, ())
         ]
-        [ (0, 1, Just ())
-        , (0, 2, Just ())
-        , (0, 3, Just ())
-        , (0, 4, Just ())
-        , (2, 10, Nothing)
-        , (3, 9, Nothing)
-        , (4, 11, Just ())
+        [ (0, 1, IndividualLabel ())
+        , (0, 2, IndividualLabel ())
+        , (0, 3, IndividualLabel ())
+        , (0, 4, IndividualLabel ())
+        , (2, 10, OmmitedNodes 3)
+        , (3, 9, OmmitedNodes 1)
+        , (4, 11, IndividualLabel ())
         ]