diff --git a/launch/GROOVE - build maven artifact.launch b/launch/GROOVE - build local maven artefact.launch similarity index 100% rename from launch/GROOVE - build maven artifact.launch rename to launch/GROOVE - build local maven artefact.launch diff --git a/launch/GROOVE - build release (all).launch b/launch/GROOVE - build release (all).launch index 0fe48e324..73931c679 100644 --- a/launch/GROOVE - build release (all).launch +++ b/launch/GROOVE - build release (all).launch @@ -4,7 +4,7 @@ - + @@ -14,7 +14,7 @@ - + diff --git a/launch/GROOVE - zip up.launch b/launch/GROOVE - zip up local release.launch similarity index 100% rename from launch/GROOVE - zip up.launch rename to launch/GROOVE - zip up local release.launch diff --git a/src/main/java/nl/utwente/groove/grammar/Rule.java b/src/main/java/nl/utwente/groove/grammar/Rule.java index ab51ecfbc..2b610732e 100755 --- a/src/main/java/nl/utwente/groove/grammar/Rule.java +++ b/src/main/java/nl/utwente/groove/grammar/Rule.java @@ -737,7 +737,7 @@ public void addColorMap(Map colorMap) { this.colorMap.putAll(colorMap); } - /** Returns a mapping from RHS nodes to colours for those nodes. */ + /** Returns a mapping from RHS nodes on this rule level to colours for those nodes. */ public Map getColorMap() { return this.colorMap; } @@ -745,6 +745,19 @@ public Map getColorMap() { /** Mapping from rule nodes to explicitly declared colours. */ private final Map colorMap = new HashMap<>(); + /** Indicates if this rule (or any of its subrules) has any coloring instructions. */ + public boolean hasColors() { + return this.hasColors.get(); + } + + /** Computes the value of {@link #hasColors}. */ + private boolean createHasColors() { + return !getColorMap().isEmpty() || getSubRules().stream().anyMatch(Rule::hasColors); + } + + /** Flag indicating if this rule (or any of its subrules) has any coloring instructions. */ + private final Supplier hasColors = lazy(this::createHasColors); + /** Returns the anchor of the rule. */ public Anchor getAnchor() { return this.anchor.get(); @@ -861,7 +874,7 @@ private RuleNode[] computeIsolatedNodes() { private final Supplier isolatedNodes = lazy(this::computeIsolatedNodes); /** - * Indicates if application of this rule actually changes the host graph. If + * Indicates if application of this rule (or any of its subrules) actually changes the host graph. If * false, this means the rule is essentially a graph * condition. */ @@ -873,24 +886,37 @@ public boolean isModifying() { * Computes if the rule is modifying or not. */ private boolean computeIsModifying() { - boolean result = getEraserEdges().length > 0 || getEraserNodes().length > 0 || hasMergers() - || hasNodeCreators() || hasEdgeCreators() || !getColorMap().isEmpty(); - if (!result) { - for (Rule subRule : getSubRules()) { - result = subRule.isModifying(); - if (result) { - break; - } - } - } - return result; + return hasNodeErasers() || hasEdgeErasers() || hasMergers() || hasNodeCreators() + || hasEdgeCreators() || hasColors(); } /** - * Indicates if this rule makes changes to a graph at all. + * Indicates if this rule (or any of its subrules) makes changes to a graph at all. */ private final Supplier modifying = lazy(this::computeIsModifying); + /** + * Indicates if this rule level modifies a graph to which it is applied, + * irregardless of its subrules. + */ + public boolean isLocallyModifying() { + return this.locallyModifying.get(); + } + + /** + * Computes the value of {@link #locallyModifying}. + */ + private boolean computeLocallyModifying() { + return getCreatorNodes().length > 0 || getCreatorEdges().length > 0 + || getEraserNodes().length > 0 || getEraserEdges().length > 0 + || !getColorMap().isEmpty() || !getMergers().isEmpty(); + } + + /** + * Indicates if this rule level modifies a graph to which it is applied. + */ + private final Supplier locallyModifying = lazy(this::computeLocallyModifying); + /** * Returns an array of LHS nodes that are endpoints of eraser edges, creator * edges or mergers. @@ -972,39 +998,31 @@ private Set computeModifierVars() { private final Supplier> modifierVars = lazy(this::computeModifierVars); /** - * Indicates if the rule creates any nodes. + * Indicates if the rule (or one of its subrules) creates any nodes. */ public boolean hasNodeCreators() { return this.hasNodeCreators.get(); } private boolean computeHasNodeCreators() { - boolean result = getCreatorNodes().length > 0; - if (!result) { - for (Rule subRule : getSubRules()) { - result = subRule.hasNodeCreators(); - if (result) { - break; - } - } - } - return result; + return getCreatorNodes().length > 0 + || getSubRules().stream().anyMatch(Rule::hasNodeCreators); } /** - * Indicates if this rule has creator nodes. + * Indicates if this rule (or one of its subrules) has creator nodes. */ private final Supplier hasNodeCreators = lazy(this::computeHasNodeCreators); /** - * Returns the RHS nodes that are not images of an LHS node. + * Returns the RHS nodes on this rule level that are not images of an LHS node. */ final public RuleNode[] getCreatorNodes() { return this.creatorNodes.get(); } /** - * Computes the creator (i.e., RHS-only) nodes. + * Computes the creator (i.e., RHS-only) nodes of this rule (excluding its subrules). */ private RuleNode[] computeCreatorNodes() { Set result = new HashSet<>(rhs().nodeSet()); @@ -1017,29 +1035,20 @@ private RuleNode[] computeCreatorNodes() { } /** - * The rhs nodes that are not ruleMorph images - * @invariant creatorNodes \subseteq rhs.nodeSet() + * The RHS nodes on this rule level that are not images of an LHS node. */ private final Supplier creatorNodes = lazy(this::computeCreatorNodes); /** - * Indicates if the rule creates any edges. + * Indicates if the rule (or one of its subrules) creates any edges. */ public boolean hasEdgeCreators() { return this.hasEdgeCreators.get(); } private boolean computeHasEdgeCreators() { - boolean result = getCreatorEdges().length > 0; - if (!result) { - for (Rule subRule : getSubRules()) { - result = subRule.hasEdgeCreators(); - if (result) { - break; - } - } - } - return result; + return getCreatorEdges().length > 0 + || getSubRules().stream().anyMatch(Rule::hasEdgeCreators); } /** @@ -1048,7 +1057,7 @@ private boolean computeHasEdgeCreators() { private final Supplier hasEdgeCreators = lazy(this::computeHasEdgeCreators); /** - * Returns the RHS edges that are not images of an LHS edge. + * Returns the RHS edges on this rule level that are not images of an LHS edge. */ final public RuleEdge[] getCreatorEdges() { return this.creatorEdges.get(); @@ -1070,7 +1079,7 @@ private RuleEdge[] computeCreatorEdges() { } /** - * The rhs edges that are not ruleMorph images + * The RHS edges on this rule level that are not images of an LHS edge. */ private final Supplier creatorEdges = lazy(this::computeCreatorEdges); @@ -1099,8 +1108,7 @@ private RuleEdge[] computeSimpleCreatorEdges() { } /** - * The rhs edges that are not ruleMorph images but with all ends morphism - * images + * The creator edges between reader nodes. */ private final Supplier simpleCreatorEdges = lazy(this::computeSimpleCreatorEdges); @@ -1121,21 +1129,20 @@ private Set computeComplexCreatorEdges() { } /** - * The rhs edges with at least one end not a morphism image + * The creator edges that have at least one creator end. */ private final Supplier> complexCreatorEdges = lazy(this::computeComplexCreatorEdges); /** - * Returns the variables that occur in creator edges. - * @see #getCreatorEdges() + * Returns the variables that occur in creator nodes and edges. */ public final LabelVar[] getCreatorVars() { return this.creatorVars.get(); } /** - * Computes the variables occurring in RHS nodes and edges. + * Computes the variables that occur in creator nodes and edges. */ private LabelVar[] computeCreatorVars() { var result = new ArrayList(); @@ -1153,7 +1160,7 @@ private LabelVar[] computeCreatorVars() { } /** - * Variables occurring in the rhsOnlyEdges + * Variables that occur in creator nodes and edges. */ private final Supplier creatorVars = lazy(this::computeCreatorVars); @@ -1166,7 +1173,7 @@ final RuleGraph getCreatorGraph() { } /** - * Computes a creator graph, consisting of the creator nodes together with + * Computes the creator graph, consisting of the creator nodes together with * the creator edges and their endpoints. */ private RuleGraph computeCreatorGraph() { @@ -1179,8 +1186,8 @@ private RuleGraph computeCreatorGraph() { } /** - * A sub-graph of the production rule's right hand side, consisting only of - * the fresh nodes and edges. + * The creator graph, consisting of the creator nodes together with + * the creator edges and their endpoints. */ private final Supplier creatorGraph = lazy(this::computeCreatorGraph); @@ -1193,9 +1200,8 @@ public final Set getCreatorEnds() { } /** - * A map from the nodes of rhsOnlyGraph to lhs, which is - * the restriction of the inverse of ruleMorph to - * rhsOnlyGraph. + * The RHS nodes that are not themselves creator nodes but are + * the ends of creator edges. */ private final Supplier> creatorEnds = lazy(() -> { var result = new HashSet<>(getCreatorGraph().nodeSet()); @@ -1204,39 +1210,31 @@ public final Set getCreatorEnds() { }); /** - * Indicates if the rule creates any nodes. + * Indicates if the rule (or one of its subrules) erases any nodes. */ public boolean hasNodeErasers() { return this.hasNodeErasers.get(); } + /** Computes the value of {@link #hasNodeErasers}. */ private boolean computeHasNodeErasers() { - boolean result = getEraserNodes().length > 0; - if (!result) { - for (Rule subRule : getSubRules()) { - result = subRule.hasNodeErasers(); - if (result) { - break; - } - } - } - return result; + return getEraserNodes().length > 0 || getSubRules().stream().anyMatch(Rule::hasNodeErasers); } /** - * Indicates if this rule has eraser nodes. + * Indicates if this rule (or any of its subrules) has eraser nodes. */ private final Supplier hasNodeErasers = lazy(this::computeHasNodeErasers); /** - * Returns the LHS nodes that are not mapped to the RHS. + * Returns the LHS nodes on this rule level that are not mapped to the RHS. */ public final DefaultRuleNode[] getEraserNodes() { return this.eraserNodes.get(); } /** - * Computes the eraser (i.e., lhs-only) nodes. + * Computes the LHS nodes on this rule level that are not mapped to the RHS. */ private DefaultRuleNode[] computeEraserNodes() { //testFixed(true); @@ -1246,44 +1244,36 @@ private DefaultRuleNode[] computeEraserNodes() { } /** - * The lhs nodes that are not ruleMorph keys - * @invariant lhsOnlyNodes \subseteq lhs.nodeSet() + * The LHS nodes on this rule level that are not mapped to the RHS. */ private final Supplier eraserNodes = lazy(this::computeEraserNodes); /** - * Indicates if the rule creates any edges. + * Indicates if the rule (or any of its subrules) erases any edges. */ public boolean hasEdgeErasers() { return this.hasEdgeErasers.get(); } + /** Computes the value of {@link #hasEdgeErasers}. */ private boolean computeHasEdgeErasers() { - boolean result = getEraserEdges().length > 0; - if (!result) { - for (Rule subRule : getSubRules()) { - result = subRule.hasEdgeErasers(); - if (result) { - break; - } - } - } - return result; + return getEraserEdges().length > 0 || getSubRules().stream().anyMatch(Rule::hasEdgeErasers); } /** - * Indicates if this rule has eraser edges. + * Indicates if this rule (or any of its subrules) erases any edges. */ private final Supplier hasEdgeErasers = lazy(this::computeHasEdgeErasers); - /** Returns the eraser (i.e., LHS-only) edges. */ + /** Returns the LHS edges on this rule level that do not have an image in the RHS, + * minus the incident edges of the eraser nodes. + */ public final RuleEdge[] getEraserEdges() { return this.eraserEdges.get(); } /** - * Computes the eraser (i.e., LHS-only) edges. - * Note: this does not include the incident edges of the eraser nodes. + * Computes the value of {@link #eraserEdges}. */ private RuleEdge[] computeEraserEdges() { testFixed(true); @@ -1297,8 +1287,8 @@ private RuleEdge[] computeEraserEdges() { } /** - * The lhs edges that are not ruleMorph keys - * @invariant lhsOnlyEdges \subseteq lhs.edgeSet() + * The LHS edges on this rule level that do not have an image in the RHS, + * minus the incident edges of the eraser nodes. */ private final Supplier eraserEdges = lazy(this::computeEraserEdges); @@ -1308,7 +1298,7 @@ public final RuleEdge[] getEraserNonAnchorEdges() { } /** - * Computes the array of creator edges that are not themselves anchors. + * Computes the value of {@link #eraserNonAnchorEdges}. */ private RuleEdge[] computeEraserNonAnchorEdges() { Set result = new LinkedHashSet<>(Arrays.asList(getEraserEdges())); @@ -1317,36 +1307,27 @@ private RuleEdge[] computeEraserNonAnchorEdges() { } /** - * The lhs edges that are not ruleMorph keys and are not anchors + * The eraser edges that are not themselves anchors. */ private final Supplier eraserNonAnchorEdges = lazy(this::computeEraserNonAnchorEdges); /** - * Indicates if this rule has mergers. + * Indicates if this rule (or any of its subrules) has (node) mergers. */ final public boolean hasMergers() { return this.hasMergers.get(); } /** - * Computes if the rule has mergers or not. + * Computes the value of {@link #hasMergers}. */ private boolean computeHasMergers() { - boolean result = !getLhsMergeMap().isEmpty() || !getRhsMergeMap().isEmpty(); - if (!result) { - for (Rule subRule : getSubRules()) { - result = subRule.hasMergers(); - if (result) { - break; - } - } - } - return result; + return !getMergers().isEmpty() || getSubRules().stream().anyMatch(Rule::hasMergers); } /** - * Indicates if this rule has node mergers. + * Indicates if this rule (or any of its subrules) has node mergers. */ private final Supplier hasMergers = lazy(this::computeHasMergers); @@ -1356,7 +1337,7 @@ public final Set getLhsMergers() { } /** - * Returns the set of merger edges in the RHS of which at least one end + * Returns the set of merger edges in the RHS of this rule level which at least one end * is a creator node. */ public final Set getRhsMergers() { @@ -1364,7 +1345,7 @@ public final Set getRhsMergers() { } /** - * Returns a map from each LHS node that is merged with + * Returns a map from each LHS node of this rule level that is merged with * another to the LHS node it is merged with. */ public final Map getLhsMergeMap() { @@ -1372,20 +1353,21 @@ public final Map getLhsMergeMap() { } /** - * Returns a map from merged nodes to their merge targets, + * Returns a map from merged nodes of this rule level to their merge targets, * at least one of which is a creator node. */ public final Map getRhsMergeMap() { return getMergers().rhsMergeMap(); } + /** Computes the value of {@link #mergers}. */ private Mergers getMergers() { return this.mergers.get(); } private final Supplier mergers = lazy(() -> new Mergers(this)); - /** Merger information. + /** Merger information for this rule level. * @param lhsMergers he set of merger edges in the RHS of which both ends are in the LHS * @param rhsMergers the set of merger edges in the RHS of which at least one end * is a creator node. @@ -1400,6 +1382,11 @@ static private record Mergers(Set lhsMergers, Set rhsMergers init(rule); } + /** Indicates if the merge action represented by this object is empty. */ + public boolean isEmpty() { + return lhsMergers().isEmpty() && rhsMergers().isEmpty(); + } + private void init(Rule rule) { var lhs = rule.lhs(); var rhs = rule.rhs(); diff --git a/src/main/java/nl/utwente/groove/io/external/format/LTS2ControlExporter.java b/src/main/java/nl/utwente/groove/io/external/format/LTS2ControlExporter.java index d9db21172..77a784f15 100644 --- a/src/main/java/nl/utwente/groove/io/external/format/LTS2ControlExporter.java +++ b/src/main/java/nl/utwente/groove/io/external/format/LTS2ControlExporter.java @@ -88,9 +88,7 @@ private void emit(GraphState state) { .filter(t -> this.covered.add(t.target())) .toList(); if (outs.isEmpty()) { - emit(state.isFinal() - ? "// final state" - : "halt"); + emit("// final state"); } else if (outs.size() == 1 && !state.isFinal()) { var out = outs.get(0); emit(out.label() + ";"); diff --git a/src/main/java/nl/utwente/groove/lts/MatchApplier.java b/src/main/java/nl/utwente/groove/lts/MatchApplier.java index db23ab060..6f6c6ea9e 100644 --- a/src/main/java/nl/utwente/groove/lts/MatchApplier.java +++ b/src/main/java/nl/utwente/groove/lts/MatchApplier.java @@ -168,8 +168,8 @@ private RuleTransition createTransition(GraphState source, MatchResult match, Gr RuleTransition parentOut = match.getTransition(); addedNodes = parentOut.getAddedNodes(); } else if (match.getAction().hasNodeCreators()) { - RuleEffect effect - = new RuleEffect(source.getGraph(), Fragment.NODE_CREATION, this.gts.getOracle()); + RuleEffect effect = new RuleEffect(source.getGraph(), Fragment.NODE_CREATION, + this.gts.getOracle()); event.recordEffect(effect); effect.setFixed(); addedNodes = effect.getCreatedNodeArray(); diff --git a/src/main/java/nl/utwente/groove/transform/BasicEvent.java b/src/main/java/nl/utwente/groove/transform/BasicEvent.java index 720f30723..56431f9ce 100755 --- a/src/main/java/nl/utwente/groove/transform/BasicEvent.java +++ b/src/main/java/nl/utwente/groove/transform/BasicEvent.java @@ -487,7 +487,7 @@ private HostEdgeSet computeSimpleCreatedEdges() { /** Computes an array of created nodes that are fresh both * with respect to a given set of source graph nodes and with respect * to a set of nodes that were already created. - * @param record the source graph + * @param record object in which the effect of this {@link BasicEvent} (and possibly others) is recorded * @return array of fresh nodes, in the order of the node creators * @throws InterruptedException if an oracle input was cancelled */ @@ -557,7 +557,7 @@ private HostNode createNode(RuleEffect record, int creatorIndex, TypeNode type) int previousCount = previous.size(); for (int i = 0; !added && i < previousCount; i++) { result = previous.get(i); - added = !record.getSource().containsNode(result); + added = !record.containsNode(result); } } if (!added) { diff --git a/src/main/java/nl/utwente/groove/transform/Proof.java b/src/main/java/nl/utwente/groove/transform/Proof.java index 0dd20f1e7..2441848ac 100644 --- a/src/main/java/nl/utwente/groove/transform/Proof.java +++ b/src/main/java/nl/utwente/groove/transform/Proof.java @@ -143,7 +143,8 @@ public RuleEvent newEvent(@Nullable Record record) { Collection eventSet = new ArrayList<>(); collectEvents(eventSet, record); assert !eventSet.isEmpty(); - if (eventSet.size() == 1 && !getRule().hasSubRules()) { + if (!getRule().hasSubRules()) { + assert eventSet.size() == 1; return eventSet.iterator().next(); } else { return createCompositeEvent(record, eventSet); @@ -153,12 +154,13 @@ public RuleEvent newEvent(@Nullable Record record) { /** * Recursively collects the events of this proof and all sub-proofs into a * given collection. + * Events of locally non-modifying rules are skipped except for the top-level rule. * @param events the resulting set of events * @param record factory for events; may be null, in which case * events are not reused among transitions */ private void collectEvents(Collection events, @Nullable Record record) { - if (hasRule()) { + if (hasRule() && (getRule().isTop() || getRule().isLocallyModifying())) { BasicEvent myEvent = createSimpleEvent(record); events.add(myEvent); } diff --git a/src/main/java/nl/utwente/groove/transform/RuleEffect.java b/src/main/java/nl/utwente/groove/transform/RuleEffect.java index a8fd172be..e25877e15 100644 --- a/src/main/java/nl/utwente/groove/transform/RuleEffect.java +++ b/src/main/java/nl/utwente/groove/transform/RuleEffect.java @@ -20,6 +20,7 @@ import java.util.Arrays; import java.util.Collection; import java.util.HashMap; +import java.util.HashSet; import java.util.Iterator; import java.util.List; import java.util.Map; @@ -147,13 +148,21 @@ void addCreatorNodes(RuleNode[] creatorNodes) { this.createdNodeMap = createdNodeMap = new HashMap<>(); } int createdNodeStart = this.createdNodeIndex; - int creatorCount = creatorNodes.length; - for (int i = 0; i < creatorCount; i++) { + int count = creatorNodes.length; + for (int i = 0; i < count; i++) { createdNodeMap.put(creatorNodes[i], createdNodes.get(createdNodeStart + i)); } - this.createdNodeIndex = createdNodeStart + creatorCount; + this.createdNodeIndex = createdNodeStart + count; } + /** + * List of created nodes, either predefined or built up during construction + */ + private final List createdNodeList; + + /** Index of the first unused element in {@link #createdNodeList}. */ + private int createdNodeIndex; + /** * Adds information about created nodes to that already stored in the record. * Should only be used if {@link #isNodesPredefined()} is {@code false}. @@ -165,34 +174,50 @@ void addCreatedNodes(RuleNode[] creatorNodes, HostNode[] createdNodes) { assert !isNodesPredefined(); int createdNodeCount = createdNodes.length; if (createdNodeCount > 0) { - Map oldCreatedNodeMap = this.createdNodeMap; - if (oldCreatedNodeMap == null) { - this.createdNodeMap = oldCreatedNodeMap = new HashMap<>(); + var createdNodeMap = this.createdNodeMap; + var createdNodeList = this.createdNodeList; + if (createdNodeMap == null) { + this.createdNodeMap = createdNodeMap = new HashMap<>(); } - List oldCreatedNodes = this.createdNodeList; + var createdNodeSet = this.createdNodeSet; for (int i = 0; i < createdNodeCount; i++) { HostNode createdNode = createdNodes[i]; - oldCreatedNodes.add(createdNode); - oldCreatedNodeMap.put(creatorNodes[i], createdNode); + createdNodeMap.put(creatorNodes[i], createdNode); + createdNodeList.add(createdNode); + if (createdNodeSet != null) { + boolean fresh = createdNodeSet.add(createdNode); + assert fresh : "New node %s was already in created nodes list %s" + .formatted(createdNode, createdNodeSet); + } } } } + /** Mapping from rule node creators to the corresponding created nodes. */ + private Map createdNodeMap; + + /** Tests if either the source graph contains a given node or this effect record adds it. */ + boolean containsNode(HostNode node) { + if (getSource().containsNode(node)) { + return true; + } + var createdNodeSet = this.createdNodeSet; + if (createdNodeSet == null) { + this.createdNodeSet = createdNodeSet = new HashSet<>(this.createdNodeList); + assert createdNodeSet.size() == this.createdNodeList + .size() : "Duplicate node in list %s".formatted(this.createdNodeList); + } + return createdNodeSet.contains(node); + } + + private Set createdNodeSet; + /** Creates and adds an edge by invoking the source graph's factory. */ void addCreateEdge(HostNode source, TypeLabel label, HostNode target) { HostEdge edge = getSource().getFactory().createEdge(source, label, target); addCreatedEdge(edge); } - /** Mapping from rule node creators to the corresponding created nodes. */ - private Map createdNodeMap; - /** - * List of created nodes, either predefined or built up during construction - */ - private final List createdNodeList; - /** Index of the first unused element in {@link #createdNodeList}. */ - private int createdNodeIndex; - /** * Adds a collection of erased nodes to those already stored in this record. */ diff --git a/src/main/java/nl/utwente/groove/util/Factory.java b/src/main/java/nl/utwente/groove/util/Factory.java index 9fd59efe9..6481d5bea 100644 --- a/src/main/java/nl/utwente/groove/util/Factory.java +++ b/src/main/java/nl/utwente/groove/util/Factory.java @@ -17,8 +17,10 @@ package nl.utwente.groove.util; import java.util.ArrayList; +import java.util.Arrays; import java.util.Collections; import java.util.HashSet; +import java.util.Objects; import java.util.Set; import java.util.concurrent.locks.ReentrantLock; import java.util.function.Supplier; @@ -161,9 +163,9 @@ private void removeUsed(Factory used) { @Override public String toString() { var value = this.value; - return value == null - ? "null" - : value.toString(); + return value instanceof Object[] a + ? Arrays.toString(a) + : Objects.toString(value); } /** Creates an instance of this factory from a given supplier. */