diff --git a/src/Compare/Compare.hs b/src/Compare/Compare.hs index 7efc2ae9cc1e8b19861dbe2881ec49cd74d0cb3b..410f3835ccd23896914f713acbc2d2e8fb510845 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 521bb1a8a40e943f857c621e952d712ab07fe335..ac6ca69d39dace5c2177ce8185d7bb906aa06051 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 a28dbdbf4eede06e30efba331d6f9746b25b6a43..4bc4794150666d08f6da7752c3fde972646b6e03 100644 --- a/stack.yaml +++ b/stack.yaml @@ -4,3 +4,5 @@ packages: - '.' extra-deps: resolver: lts-8.5 +ghc-options: + '*': -fno-ignore-asserts