From c077adf54fa2b25d7de41061681f8bb521622aaa Mon Sep 17 00:00:00 2001
From: Hans-Peter Deifel <hpd@hpdeifel.de>
Date: Wed, 10 May 2017 12:11:25 +0200
Subject: [PATCH] Actually check determinism before comparision
---
src/Compare/Compare.hs | 11 ++++++-----
src/main/Main.hs | 9 ++++++++-
stack.yaml | 2 ++
3 files changed, 16 insertions(+), 6 deletions(-)
diff --git a/src/Compare/Compare.hs b/src/Compare/Compare.hs
index 7efc2ae..410f383 100644
--- a/src/Compare/Compare.hs
+++ b/src/Compare/Compare.hs
@@ -53,7 +53,7 @@ isIsomorphic g1 g2 =
initQueue = Seq.singleton (point g1, point g2)
initMatching = M.empty
in
- assert True $
+ assert (isDeterministic g1 && isDeterministic g2) $
isomorphicWorker g1 g2 initQueue initMatching
@@ -106,7 +106,8 @@ isBisimilar g1 g2 =
initQueue = Seq.singleton (point g1, point g2)
initMatching = S.empty
in
- bisimilarWorker g1 g2 initQueue initMatching
+ assert (isDeterministic g1 && isDeterministic g2) $
+ bisimilarWorker g1 g2 initQueue initMatching
type Bisimulation = S.Set (Int, Int)
@@ -144,10 +145,10 @@ nodesBisimilar g1 g2 matching node1 node2 = case (node1,node2) `S.member` matchi
Right (Seq.fromList newPairs, newMatching)
-- | Return true if all outgoing edge labels of a node are different.
-isDeterministic :: Ord e => G.Gr n e -> Bool
-isDeterministic g = all differentEdgeLabels (G.nodes g)
+isDeterministic :: Ord e => Graph n e -> Bool
+isDeterministic g = all differentEdgeLabels (G.nodes (g^._graph))
where
differentEdgeLabels :: G.Node -> Bool
differentEdgeLabels node =
- let outEdges = G.out g node
+ let outEdges = G.out (g^._graph) node
in length outEdges == length (S.fromList (map G.edgeLabel outEdges))
diff --git a/src/main/Main.hs b/src/main/Main.hs
index 521bb1a..ac6ca69 100644
--- a/src/main/Main.hs
+++ b/src/main/Main.hs
@@ -137,9 +137,16 @@ main = do
hPutStrLn stderr $ "Could not parse sse graph json: " <> e
exitFailure
Just (Right graph1) -> do
+ let graph1' = preprocess graph1
graph2 <- driver (eliminateEpsilons opts) (dumpJSON opts) (debugOutput opts) (mockupExecutable opts)
+ when (not (isDeterministic graph1')) $ do
+ hPutStrLn stderr "JSON graph is not deterministic!!!"
+ exitFailure
+ when (not (isDeterministic graph2)) $ do
+ hPutStrLn stderr "Explored graph is not deterministic!!!"
+ exitFailure
hPutStr stderr $ "GRAPH COMPARISION FOR " ++ (mockupExecutable opts) ++ ": "
- hPrint stderr (compareGraphs (preprocess graph1) graph2)
+ hPrint stderr (compareGraphs graph1' graph2)
Mockup opts -> do
cntnt <- BS.getContents
case P.parseFile cntnt of
diff --git a/stack.yaml b/stack.yaml
index a28dbdb..4bc4794 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -4,3 +4,5 @@ packages:
- '.'
extra-deps:
resolver: lts-8.5
+ghc-options:
+ '*': -fno-ignore-asserts
--
GitLab