Verites / verigraph

Software specification and verification system based on graph rewriting
https://verites.github.io/verigraph/
Apache License 2.0
37 stars 4 forks source link

Abnormal behaviour on GraphMorphism equality #24

Closed lm-rodrigues closed 7 years ago

lm-rodrigues commented 7 years ago

While writing some tests, I found an abnormal behaviour on the equality tests of Graph Morphisms, the problem seems to be w.r.t. Relations Equality Comparison.

Test

spec :: Spec
spec = describe "Graph Morphism API" $ do

  describe "removeNodeFromCodomain" $ do

  it "Should remove node without incident edges" $ do
      (nodeRelation $ removeNodeFromCodomain 3 g1) `shouldBe` (nodeRelation g4)

Output

Graph.GraphMorphism, Graph Morphism API, removeNodeFromCodomain, Should remove node without incident edges
       expected: Relation {domain = [1,2,4,3], codomain = [1,2,4], mapping = fromList [(1,[1]),(2,[2]),(4,[4])]}
        but got: Relation {domain = [1,2,3,4], codomain = [1,2,4], mapping = fromList [(1,[1]),(2,[2]),(3,[]),(4,[4])]}

Context

g1' :: Graph (Maybe a) (Maybe b)
g1' = build [1,2,3,4] [(1,1,2)]

g2' :: Graph (Maybe a) (Maybe b)
g2' = build [1,2,4] [(1,1,2)]

g1 :: GraphMorphism (Maybe a) (Maybe b)
g1 = buildGraphMorphism g1' g1' [(1,1),(2,2),(3,3),(4,4)] [(1,1)]

g4 :: GraphMorphism (Maybe a) (Maybe b)
g4 = buildGraphMorphism g1' g2' [(1,1),(2,2),(4,4)] [(1,1)]
ggazzi commented 7 years ago

Apparently the problem is that elements for which the mapping is undefined may be represented in two ways: being absent from the map, or being mapped to an empty list.

jsbezerra commented 7 years ago

Moreover, the function may alter ther order of elements in the domain (and possibly codomain?) list. Thus, the lists are different and the equality fails for this case.