Fix FindCospanCommuter

src/library/Graph/Graph.hs

@@ -385,7 +385,7 @@ removeNode n g@(Graph ns es)
     | Prelude.null $ getIncidentEdges g n = Graph (delFromAL ns n) es
     | otherwise = g
 
--- | Removes the given node from the graph, unless it has any incident edges. /O(v + e²)/.
+-- | Removes the given node from the graph, even if it has any incident edges.
 -- It does not verify if the node has incident edges, thus it may generate invalid graphs.
 removeNodeForced :: NodeId -> Graph n e -> Graph n e
 removeNodeForced n (Graph ns es) = Graph (delFromAL ns n) es

src/library/TypedGraph/Morphism/FindMorphism.hs

@@ -19,58 +19,95 @@ instance FindMorphism (TypedGraphMorphism a b) where
   partialInjectiveMatches = partialInjectiveMatches'
   findCospanCommuter      = findCospanCommuter'
 
+
+type ExpandedEdge = (EdgeId, NodeId, NodeId)
+
 data CospanBuilderState =
   State {
-    unmappedDomainNodes    :: [NodeId]
+    expandedDomainEdges    :: [ExpandedEdge]
+  , expandedCodomainEdges  :: [ExpandedEdge]
+  , unmappedDomainNodes    :: [NodeId]
   , unmappedDomainEdges    :: [EdgeId]
   , availableCodomainNodes :: [NodeId]
   , availableCodomainEdges :: [EdgeId]
   , nodeRelation           :: R.Relation NodeId
   , edgeRelation           :: R.Relation EdgeId
   , finalNodeRelation      :: R.Relation NodeId
   , finalEdgeRelation      :: R.Relation EdgeId
-  } deriving (Show)
+  }
 
 -- | Given two TypedGraphMorphism @f : B -> A@ and @g : C -> A@ it finds a list of Morphisms
--- @hi : B -> C@ shuch that @f . ¬g  = hi@ for all @i@.
+-- @hi : B -> C@ shuch that @¬g . f = hi@ for all @i@.
 findCospanCommuter' :: MorphismType -> TypedGraphMorphism a b -> TypedGraphMorphism a b -> [TypedGraphMorphism a b]
 findCospanCommuter' conf morphismF morphismG
   | codomain morphismF /= codomain morphismG = []
-  | otherwise = findCospanCommuterMorphisms conf initialState morphismF morphismG
-    where
-      nodesFromF = nodeIdsFromDomain morphismF
-      edgesFromF = edgeIdsFromDomain morphismF
-      nodesFromG = nodeIdsFromDomain morphismG
-      edgesFromG = edgeIdsFromDomain morphismG
+  | otherwise =
+  let
+    typedDomainFromF   = domain morphismF
+    untypedDomainFromF = domain typedDomainFromF
+    mappingFromF       = mapping morphismF
 
-      nodeRelationF = GM.nodeRelation $ mapping morphismF
-      edgeRelationF = GM.edgeRelation $ mapping morphismF
-      nodeRelationInvertedG = R.inverseRelation $ GM.nodeRelation $ mapping morphismG
-      edgeRelationInvertedG = R.inverseRelation $ GM.edgeRelation $ mapping morphismG
+    typedDomainFromG   = domain morphismG
+    untypedDomainFromG = domain typedDomainFromG
+    mappingFromG       = mapping morphismG
 
-      composedNodeRelation = R.compose nodeRelationF nodeRelationInvertedG
-      composedEdgeRelation = R.compose edgeRelationF edgeRelationInvertedG
+    nodesIdsFromF = nodeIds untypedDomainFromF
+    edgesIdsFromF = edgeIds untypedDomainFromF
+    nodesIdsFromG = nodeIds untypedDomainFromG
+    edgesIdsFromG = edgeIds untypedDomainFromG
 
-      initialState = State
-                     nodesFromF edgesFromF
-                     nodesFromG edgesFromG
-                     composedNodeRelation composedEdgeRelation
-                     (R.empty nodesFromF nodesFromG) (R.empty edgesFromF edgesFromG)
+    nodeRelationF = GM.nodeRelation mappingFromF
+    edgeRelationF = GM.edgeRelation mappingFromF
+    nodeRelationInvertedG = R.inverseRelation $ GM.nodeRelation mappingFromG
+    edgeRelationInvertedG = R.inverseRelation $ GM.edgeRelation mappingFromG
+
+    composedNodeRelation = R.compose nodeRelationF nodeRelationInvertedG
+    composedEdgeRelation = R.compose edgeRelationF edgeRelationInvertedG
+
+    expandedEdgesFromDomain   = map (\e -> (edgeId e, sourceId e, targetId e)) $ edges untypedDomainFromF
+    expandedEdgesFromCodomain = map (\e -> (edgeId e, sourceId e, targetId e)) $ edges untypedDomainFromG
+
+    initialState = State
+                   expandedEdgesFromDomain expandedEdgesFromCodomain
+                   nodesIdsFromF edgesIdsFromF
+                   nodesIdsFromG edgesIdsFromG
+                   composedNodeRelation composedEdgeRelation
+                   (R.empty nodesIdsFromF nodesIdsFromG) (R.empty edgesIdsFromF edgesIdsFromG)
+
+    edgesMapped = findCospanCommuterEdgeRelations conf initialState
+    finalStates = concatMap (findCospanCommuterNodeRelations conf) edgesMapped
+
+    buildTGMFromState state = buildTypedGraphMorphism typedDomainFromF typedDomainFromG $
+      GM.fromGraphsAndRelations untypedDomainFromF untypedDomainFromG
+      (finalNodeRelation state) (finalEdgeRelation state)
 
--- | Given a MorphismType and a initial @CospanBuilderState@ with empty final Relations,
--- finds relations @B -> C@ between nodes and edges of @B@ and @C@. (Auxiliary function)
-findCospanCommuterMorphisms :: MorphismType -> CospanBuilderState -> TypedGraphMorphism a b -> TypedGraphMorphism a b -> [TypedGraphMorphism a b]
-findCospanCommuterMorphisms conf state morphismF morphismG =
-  let nodesUpdated = findCospanCommuterNodeRelations conf state
-      edgesUpdated = concatMap (findCospanCommuterEdgeRelations conf) nodesUpdated
-
-      typedDomain = domain morphismF
-      typedCodomain = domain morphismG
-      untypedDomain = domain typedDomain
-      untypedCodomain = domain typedCodomain
   in
-  map (\x ->  buildTypedGraphMorphism typedDomain typedCodomain
-             $ GM.fromGraphsAndRelations untypedDomain untypedCodomain (finalNodeRelation x) (finalEdgeRelation x)) edgesUpdated
+    map buildTGMFromState finalStates
+
+-- | Given a MorphismType and a initial @CospanBuilderState@ with final Node Relations complete,
+-- finds a Relation @B -> C@ between edges of @B@ and @C@. (Auxiliary function)
+findCospanCommuterEdgeRelations :: MorphismType -> CospanBuilderState -> [CospanBuilderState]
+findCospanCommuterEdgeRelations conf state
+  | L.null $ unmappedDomainEdges state =
+    let isoCondition = L.null $ availableCodomainEdges state
+        epiCondition = L.null . R.orphans $ finalEdgeRelation state
+    in case conf of
+         Isomorphism ->
+           if isoCondition then return state else []
+
+         Epimorphism ->
+           if epiCondition then return state else []
+
+         _ -> return state
+
+  | otherwise =
+    do
+      let (edgeOnDomain:_) = unmappedDomainEdges state
+
+      edgeOnCodomain <- R.apply (edgeRelation state) edgeOnDomain
+      updatedState <- updateEdgeState conf edgeOnDomain edgeOnCodomain state
+
+      findCospanCommuterEdgeRelations conf updatedState
 
 -- | Given a MorphismType and a initial @CospanBuilderState@ with empty final Relations,
 -- finds a Relation @B -> C@ between nodes of @B@ and @C@. (Auxiliary function)
@@ -101,16 +138,27 @@ findCospanCommuterNodeRelations conf state
 updateNodeState :: MorphismType -> NodeId -> NodeId -> CospanBuilderState -> [CospanBuilderState]
 updateNodeState conf nodeOnDomain nodeOnCodomain state =
   let
-    monoCondition = nodeOnCodomain`elem` availableCodomainNodes state
-
-    updatedGenericState = state { unmappedDomainNodes = delete nodeOnDomain $ unmappedDomainNodes state
-                                , finalNodeRelation   = R.updateRelation nodeOnDomain nodeOnCodomain (finalNodeRelation state) }
-
-    updatedMonoState = updatedGenericState { availableCodomainNodes = delete nodeOnCodomain $ availableCodomainNodes updatedGenericState }
+    nodeDomainApplied = R.apply (finalNodeRelation state) nodeOnDomain
+
+    monoCondition =
+      nodeOnCodomain `elem` availableCodomainNodes state ||
+      ( not (L.null nodeDomainApplied) &&
+        head (R.apply (finalNodeRelation state) nodeOnDomain) == nodeOnCodomain)
+
+    updatedGenericState =
+      state { unmappedDomainNodes = delete nodeOnDomain $ unmappedDomainNodes state
+            , finalNodeRelation   =
+                R.updateRelation nodeOnDomain nodeOnCodomain $ finalNodeRelation state
+            }
+
+    updatedMonoState =
+      updatedGenericState { availableCodomainNodes =
+                              delete nodeOnCodomain $ availableCodomainNodes updatedGenericState
+                          }
   in
     case (conf, monoCondition) of
       (Monomorphism, False) ->
-       []
+        []
 
       (Isomorphism, False) ->
         []
@@ -124,43 +172,38 @@ updateNodeState conf nodeOnDomain nodeOnCodomain state =
       _ ->
         return updatedGenericState
 
--- | Given a MorphismType and a initial @CospanBuilderState@ with final Node Relations complete,
--- finds a Relation @B -> C@ between edges of @B@ and @C@. (Auxiliary function)
-findCospanCommuterEdgeRelations :: MorphismType -> CospanBuilderState -> [CospanBuilderState]
-findCospanCommuterEdgeRelations conf state
-  | L.null $ unmappedDomainEdges state =
-    let isoCondition = L.null $ availableCodomainEdges state
-        epiCondition = L.null . R.orphans $ finalEdgeRelation state
-    in case conf of
-         Isomorphism ->
-           if isoCondition then return state else []
-
-         Epimorphism ->
-           if epiCondition then return state else []
-
-         _ -> return state
+-- | Verify if a edge of @B@ can be mapped to a node of @C@, if possible, updates the given @CospanBuilderState@. (Auxiliary function)
+updateEdgeState :: MorphismType -> EdgeId -> EdgeId -> CospanBuilderState -> [CospanBuilderState]
+updateEdgeState conf edgeOnDomain edgeOnCodomain state =
+  do
+    let monoCondition = edgeOnCodomain`elem` availableCodomainEdges state
 
-  | otherwise =
-    do
-      let (edgeOnDomain:_) = unmappedDomainEdges state
+        (_, sourceOnDomain, targetOnDomain) =
+          fromJust $ lookupExpandedEdge (expandedDomainEdges state) edgeOnDomain
 
-      edgeOnCodomain <- R.apply (edgeRelation state) edgeOnDomain
-      updatedState <- updateEdgeState conf edgeOnDomain edgeOnCodomain state
+        (_, sourceOnCodomain, targetOnCodomain) =
+          fromJust $ lookupExpandedEdge (expandedCodomainEdges state) edgeOnCodomain
 
-      findCospanCommuterEdgeRelations conf updatedState
+        lookupExpandedEdge :: [(EdgeId, NodeId, NodeId)] -> EdgeId -> Maybe ExpandedEdge
+        lookupExpandedEdge [] _ = Nothing
+        lookupExpandedEdge ((e,s,t):tl) edgeid = if edgeid == e
+                                                 then Just (e,s,t)
+                                                 else lookupExpandedEdge tl edgeid
 
--- | Verify if a edge of @B@ can be mapped to a node of @C@, if possible, updates the given @CospanBuilderState@. (Auxiliary function)
-updateEdgeState :: MorphismType -> EdgeId -> EdgeId -> CospanBuilderState -> [CospanBuilderState]
-updateEdgeState conf edgeOnDomain edgeOnCodomain state =
-  let
-    monoCondition = edgeOnCodomain`elem` availableCodomainEdges state
+    sourceNodeUpdate <- updateNodeState conf sourceOnDomain sourceOnCodomain state
+    targetNodeUpdate <- updateNodeState conf targetOnDomain targetOnCodomain sourceNodeUpdate
 
-    updatedGenericState = state { unmappedDomainEdges = delete edgeOnDomain $ unmappedDomainEdges state
-                                , finalEdgeRelation   = R.updateRelation edgeOnDomain edgeOnCodomain (finalEdgeRelation state) }
+    let updatedGenericState =
+          targetNodeUpdate { unmappedDomainEdges = delete edgeOnDomain $ unmappedDomainEdges state
+                , finalEdgeRelation   =
+                    R.updateRelation edgeOnDomain edgeOnCodomain (finalEdgeRelation state)
+                }
 
-    updatedMonoState = updatedGenericState { availableCodomainEdges = delete edgeOnCodomain $ availableCodomainEdges updatedGenericState }
+        updatedMonoState =
+          updatedGenericState { availableCodomainEdges =
+                                  delete edgeOnCodomain $ availableCodomainEdges updatedGenericState
+                              }
 
-  in
     case (conf, monoCondition) of
       (Monomorphism, False) ->
         []
@@ -177,6 +220,7 @@ updateEdgeState conf edgeOnDomain edgeOnCodomain state =
       _ ->
         return updatedGenericState
 
+
 -- | Given two lists of TypedGraphMorphism @fi : Ai -> B@ and @gi : Ai -> C@ it induces a Morphism
 -- @h : B -> C@ shuch that @h . fi = gi@ for all @i@. The lists must have the same length and must
 -- not be empty.

tests/TypedGraph/Morphism/FindMorphismSpec/FindCospanCommuterTest.hs

@@ -39,6 +39,10 @@ findCospanCommuterTest =
   genericTest tgm9 tgm8
   genericTest tgm8 tgm9
 
+  -- | Tests with loops
+  genericTest tgm10 tgm11
+  genericTest tgm11 tgm10
+
 
 -- | TypedGraphMorphism instances. Digraphs with only nodes
 
@@ -57,6 +61,7 @@ tgm4 = TGM.buildTypedGraphMorphism g1 g2 $ GM.buildGraphMorphism g1' g2' [(1,1)]
 tgm5 :: TGM a b
 tgm5 = TGM.buildTypedGraphMorphism g3 g2 $ GM.buildGraphMorphism g3' g2' [(1,1),(2,2),(3,2)] []
 
+
 -- | TypedGraphMorphism instances. Digraphs with only nodes
 
 tgm6 :: TGM a b
@@ -71,6 +76,16 @@ tgm8 = TGM.buildTypedGraphMorphism g5 g5 $ GM.buildGraphMorphism g5' g5' [(1,1),
 tgm9 :: TGM a b
 tgm9 = TGM.buildTypedGraphMorphism g6 g5 $ GM.buildGraphMorphism g6' g5' [(1,1),(2,2)][(1,1),(2,2),(3,1)]
 
+
+-- | TypedGraphMorphism instances. Digraphs with loops
+
+tgm10 :: TGM a b
+tgm10 = TGM.buildTypedGraphMorphism g7 g7 $ GM.buildGraphMorphism g7' g7' [(1,1)] [(1,1)]
+
+tgm11 :: TGM a b
+tgm11 = TGM.buildTypedGraphMorphism g8 g7 $ GM.buildGraphMorphism g8' g7' [(1,1),(2,1)][(1,1),(2,1)]
+
+
 -- | Graphs instances for tests
 
 typegraph :: Graph (Maybe a) (Maybe b)
@@ -155,6 +170,35 @@ g6' :: G a b
 g6' = build [1,2] [(1,1,2),(2,1,2),(3,1,2)]
 
 
+-- | Digraphs with loops for validity tests
+
+-- | digraph G7 {
+--    1 [shape = circle];
+--
+--    1 -> 1;
+--
+--   }
+g7 :: GM a b
+g7 = GM.buildGraphMorphism g7' typegraph [(1,1)] [(1,1)]
+
+g7' :: G a b
+g7' = build [1] [(1,1,1)]
+
+-- | digraph G8 {
+--    1 [shape = circle];
+--    2 [shape = circle];
+--
+--    1 -> 1;
+--    2 -> 2;
+--
+--   }
+g8 :: GM a b
+g8 = GM.buildGraphMorphism g8' typegraph [(1,1),(2,1)] [(1,1),(2,1)]
+
+g8' :: G a b
+g8' = build [1,2] [(1,1,1),(2,2,2)]
+
+
 -- | Auxiliary functions to tests
 
 genericTest :: TGM a b -> TGM a b -> Expectation

verigraph.cabal

@@ -1,5 +1,5 @@
 name:                verigraph
-version:             1.1.0
+version:             1.1.1
 synopsis:            Software specification and verification tool based on graph rewriting.
 -- description:
 license:             Apache-2.0