diff --git a/osek-verification.cabal b/osek-verification.cabal
index 0330434eda7a8951124bf2dae4a98e9382264ce3..243f54745d1e1cd79ad8fd912c0cc983b5d42794 100644
--- a/osek-verification.cabal
+++ b/osek-verification.cabal
@@ -24,6 +24,7 @@ library
, Search.States2Dot
, Search.Search2
, Search.Types
+ , Search.EpsilonElimination
, Protocol
hs-source-dirs: src
build-depends: base >=4.9 && <4.10
@@ -60,6 +61,7 @@ test-suite spec
, CFG.CSpec
, CFG.SanitizeSpec
, ProtocolSpec
+ , Search.EpsilonEliminationSpec
build-depends: base >= 4.8 && <4.10
, osek-verification
, hspec >= 2.2.3 && <2.3
diff --git a/src/Search/EpsilonElimination.hs b/src/Search/EpsilonElimination.hs
new file mode 100644
index 0000000000000000000000000000000000000000..84ef7c6ebcdfb1d0925fd4a0daff967483f0cf95
--- /dev/null
+++ b/src/Search/EpsilonElimination.hs
@@ -0,0 +1,97 @@
+module Search.EpsilonElimination
+ ( eliminateEpsilons
+ -- * Internal functions exported for easier testing
+ , epsilonClosure
+ , addTransitiveEdges
+ , removeEpsilonEdges
+ , removeUnreachableNodes
+ ) where
+
+import Data.Map (Map)
+import qualified Data.Map as M
+import Data.Maybe
+import Data.Set (Set)
+import qualified Data.Set as S
+
+import Search.Types
+
+eliminateEpsilons :: Vertex -> Graph -> Graph
+eliminateEpsilons start graph =
+ let
+ closureMap = epsilonClosure graph
+ transitiveClosure = addTransitiveEdges graph closureMap
+ withoutEpsilons = removeEpsilonEdges transitiveClosure
+ finalGraph = removeUnreachableNodes start withoutEpsilons
+ in
+ finalGraph
+
+type Closure = Set Vertex
+
+-- | Compute the epsilon closure for all vertices.
+--
+-- The epsilon closure for a vertex v is defined as the set of vertices that are
+-- reachable from v by following only ɛ transitions.
+epsilonClosure :: Graph -> Map Vertex Closure
+epsilonClosure graph = fixEq (epsilonClosureStep graph) identityMap
+ where
+ identityMap = foldr (\x m -> M.insert x (S.singleton x) m) M.empty (M.keys graph)
+
+-- | One step to compute the epsilon closure.
+--
+-- This has to be iterated until the result doesn't change (in respect to '==')
+epsilonClosureStep :: Graph -> Map Vertex Closure -> Map Vertex Closure
+epsilonClosureStep graph closureMap =
+ foldr reduceVertex closureMap (M.keys graph)
+
+ where
+ -- Add the closures of all epsilon successors to our own closure
+ reduceVertex vert cloMap = S.foldr (addClosure vert) cloMap (epsilonSuccessors graph vert)
+ -- Add the closure from the second vertex to the closure of the first
+ addClosure from to cloMap = M.insertWith S.union from (cloMap M.! to) cloMap
+
+-- | Return all direct successors of the vertex reachable over an ɛ edge.
+epsilonSuccessors :: Graph -> Vertex -> Set Vertex
+epsilonSuccessors graph vert =
+ let
+ edges = graph M.! vert
+ epsilonEdges = S.filter isEpsilon edges
+ in
+ S.map edgeTo epsilonEdges
+
+
+-- | For each vertex, add all outgoing vertices from it's ɛ-closure to the
+-- vertex itself.
+addTransitiveEdges :: Graph -> Map Vertex Closure -> Graph
+addTransitiveEdges graph closureMap = M.mapWithKey addEdges graph
+ where
+ addEdges vertex edges = S.unions (edges : closureEdges vertex)
+ closureEdges vertex = map (\w -> graph M.! w) $ S.toList (closureMap M.! vertex)
+
+-- | Delete all epsilon transitions from the graph
+removeEpsilonEdges :: Graph -> Graph
+removeEpsilonEdges = M.map (S.filter (not . isEpsilon))
+
+removeUnreachableNodes :: Vertex -> Graph -> Graph
+removeUnreachableNodes start graph =
+ let
+ reachable = getReachable S.empty start
+ unreachable = M.keysSet graph S.\\ reachable
+ in
+ S.foldr M.delete graph unreachable
+
+ where
+ getReachable visited node =
+ S.foldr (\succ visited' -> getReachable visited' succ) (S.insert node visited) (successors node)
+ successors node = S.map edgeTo $ graph M.! node
+
+-- | Return true iff the edge is an ɛ-transition
+isEpsilon :: Edge -> Bool
+isEpsilon = isNothing . edgeSyscall
+
+fixEq :: Eq a => (a -> a) -> a -> a
+fixEq f a =
+ let result = f a
+ in
+ if result == a
+ then result
+ else fixEq f result
diff --git a/test/Search/EpsilonEliminationSpec.hs b/test/Search/EpsilonEliminationSpec.hs
new file mode 100644
index 0000000000000000000000000000000000000000..25f7b324dec5b8956988ba84bffbc3f71c4d0d09
--- /dev/null
+++ b/test/Search/EpsilonEliminationSpec.hs
@@ -0,0 +1,162 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Search.EpsilonEliminationSpec (spec) where
+
+import Test.Hspec
+
+import Control.Arrow
+
+import Data.Map (Map)
+import qualified Data.Map as M
+import Data.Set (Set)
+import qualified Data.Set as S
+import Data.Text (Text)
+
+import Search.EpsilonElimination
+import Search.Types
+
+spec :: Spec
+spec = do
+ describe "epsilonClosure" epsilonClosureSpec
+ describe "eliminateEpsilons" eliminateEpsilonsSpec
+ describe "addTransitiveEdges" addTransitiveEdgesSpec
+ describe "removeEpsilonEdges" removeEpsilonEdgesSpec
+ describe "removeUnreachableNodes" removeUnreachableNodesSpec
+
+epsilonClosureSpec :: Spec
+epsilonClosureSpec = do
+ it "Returns the identity map for a graph without epsilons" $
+ let
+ graph = mkGraph [ ("A", edges [(Just "a", "B"), (Just "c", "C")])
+ , ("B", edges [(Just "b", "C")])
+ , ("C", [])
+ ]
+ closureMap = mkClosure [ ("A", ["A"])
+ , ("B", ["B"])
+ , ("C", ["C"])
+ ]
+ in epsilonClosure graph `shouldBe` closureMap
+
+ it "returns the correct closure in the presence of epsilons transitions" $
+ let
+ graph = mkGraph [ ("A", edges [(Nothing, "B"), (Just "c", "C")])
+ , ("B", edges [(Nothing, "C")])
+ , ("C", [])
+ ]
+ closureMap = mkClosure [ ("A", ["A", "B", "C"])
+ , ("B", ["B", "C"])
+ , ("C", ["C"])
+ ]
+ in epsilonClosure graph `shouldBe` closureMap
+
+
+eliminateEpsilonsSpec :: Spec
+eliminateEpsilonsSpec = do
+ it "Does nothing without epsilon transitions" $
+ let graph = mkGraph [ ("A", edges [(Just "a", "B"), (Just "c", "C")])
+ , ("B", edges [(Just "b", "C")])
+ , ("C", [])
+ ]
+ in eliminateEpsilons (mkVertex "A") graph `shouldBe` graph
+
+ it "Correctly transforms a graph in the presence of epsilon transitions" $
+ let
+ graph1 = mkGraph [ ("A", edges [(Nothing, "B"), (Just "c", "C")])
+ , ("B", edges [(Just "b", "C")])
+ , ("C", [])
+ ]
+ graph2 = mkGraph [ ("A", edges [(Just "b", "C"), (Just "c", "C")])
+ , ("C", [])
+ ]
+ in eliminateEpsilons (mkVertex "A") graph1 `shouldBe` graph2
+
+addTransitiveEdgesSpec :: Spec
+addTransitiveEdgesSpec = do
+ it "Does nothing without epsilon transitions" $
+ let
+ graph = mkGraph [ ("A", edges [(Just "a", "B"), (Just "c", "C")])
+ , ("B", edges [(Just "b", "C")])
+ , ("C", [])
+ ]
+ closureMap = mkClosure [ ("A", ["A"])
+ , ("B", ["B"])
+ , ("C", ["C"])
+ ]
+ in addTransitiveEdges graph closureMap `shouldBe` graph
+
+ it "Works in the presence of epsilons" $
+ let
+ graph1 = mkGraph [ ("A", edges [(Nothing, "B"), (Just "c", "C")])
+ , ("B", edges [(Just "b", "C")])
+ , ("C", [])
+ ]
+ graph2 = mkGraph [ ("A", edges [(Nothing, "B"), (Just "b", "C"), (Just "c", "C")])
+ , ("B", edges [(Just "b", "C")])
+ , ("C", [])
+ ]
+ closureMap = mkClosure [ ("A", ["A", "B"])
+ , ("B", ["B"])
+ , ("C", ["C"])
+ ]
+ in
+ addTransitiveEdges graph1 closureMap `shouldBe` graph2
+
+removeEpsilonEdgesSpec :: Spec
+removeEpsilonEdgesSpec = do
+ it "does nothing without epsilon transitions" $
+ let
+ graph = mkGraph [ ("A", edges [(Just "a", "B"), (Just "c", "C")])
+ , ("B", edges [(Just "b", "C")])
+ , ("C", [])
+ ]
+ in
+ removeEpsilonEdges graph `shouldBe` graph
+
+ it "removes present epsilon edges" $
+ let
+ graph1 = mkGraph [ ("A", edges [(Nothing, "B"), (Just "c", "C")])
+ , ("B", edges [(Nothing, "C")])
+ , ("C", [])
+ ]
+ graph2 = mkGraph [ ("A", edges [(Just "c", "C")])
+ , ("B", edges [])
+ , ("C", [])
+ ]
+ in
+ removeEpsilonEdges graph1 `shouldBe` graph2
+
+
+removeUnreachableNodesSpec :: Spec
+removeUnreachableNodesSpec = do
+ it "does nothing without unreachable nodes" $
+ let
+ graph = mkGraph [ ("A", edges [(Just "a", "B"), (Just "c", "C")])
+ , ("B", edges [(Just "b", "C")])
+ , ("C", [])
+ ]
+ in
+ removeUnreachableNodes (mkVertex "A") graph `shouldBe` graph
+
+ it "removes unreachable nodes" $
+ let
+ graph1 = mkGraph [ ("A", edges [(Just "c", "C")])
+ , ("B", edges [(Just "b", "C")])
+ , ("C", [])
+ ]
+ graph2 = mkGraph [ ("A", edges [(Just "c", "C")])
+ , ("C", [])
+ ]
+ in
+ removeUnreachableNodes (mkVertex "A") graph1 `shouldBe` graph2
+
+mkGraph :: [(Text, [Edge])] -> Graph
+mkGraph = M.fromList . map (\(v, es) -> (mkVertex v, S.fromList es))
+
+edges :: [(Maybe Text, Text)] -> [Edge]
+edges = map (\(e, v) -> Edge (mkVertex v) e)
+
+mkVertex :: Text -> Vertex
+mkVertex v = Vertex v "" ""
+
+mkClosure :: [(Text, [Text])] -> Map Vertex (Set Vertex)
+mkClosure = M.fromList . map (mkVertex *** (S.fromList . map mkVertex))