Trace generation

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/arg/ArgNode.java

@@ -15,19 +15,18 @@
  */
 package hu.bme.mit.theta.analysis.algorithm.arg;
 
+import static com.google.common.base.Preconditions.checkArgument;
+import static com.google.common.base.Preconditions.checkNotNull;
+
 import hu.bme.mit.theta.analysis.Action;
 import hu.bme.mit.theta.analysis.State;
 import hu.bme.mit.theta.common.Utils;
 import hu.bme.mit.theta.common.container.Containers;
-
 import java.util.ArrayList;
 import java.util.Collection;
 import java.util.Optional;
 import java.util.stream.Stream;
 
-import static com.google.common.base.Preconditions.checkArgument;
-import static com.google.common.base.Preconditions.checkNotNull;
-
 public final class ArgNode<S extends State, A extends Action> {
 
     final ARG<S, A> arg;
@@ -47,7 +46,12 @@ public final class ArgNode<S extends State, A extends Action> {
 
     public boolean expanded; // Set by ArgBuilder
 
-    ArgNode(final ARG<S, A> arg, final S state, final int id, final int depth, final boolean target) {
+    ArgNode(
+            final ARG<S, A> arg,
+            final S state,
+            final int id,
+            final int depth,
+            final boolean target) {
         this.arg = arg;
         this.state = state;
         this.id = id;
@@ -67,8 +71,8 @@ public int getId() {
     }
 
     /**
-     * Gets the depth of the node, which is 0 if the node has no parent, and
-     * depth(parent) + 1 otherwise.
+     * Gets the depth of the node, which is 0 if the node has no parent, and depth(parent) + 1
+     * otherwise.
      */
     public int getDepth() {
         return depth;
@@ -83,6 +87,10 @@ public void setState(final S state) {
         this.state = state;
     }
 
+    public boolean inPartialOrder(final ArgNode<S, A> node) {
+        return arg.getPartialOrd().isLeq(node.getState(), this.getState());
+    }
+
     public boolean mayCover(final ArgNode<S, A> node) {
         if (arg.getPartialOrd().isLeq(node.getState(), this.getState())) {
             return ancestors().noneMatch(n -> n.equals(node) || n.isSubsumed());
@@ -162,77 +170,59 @@ public Stream<S> getSuccStates() {
 
     ////
 
-    /**
-     * Checks if the node is covered, i.e., there is a covering edge for the
-     * node.
-     */
+    /** Checks if the node is covered, i.e., there is a covering edge for the node. */
     public boolean isCovered() {
         return coveringNode.isPresent();
     }
 
-    /**
-     * Checks if the node is not a bottom state.
-     */
+    /** Checks if the node is not a bottom state. */
     public boolean isFeasible() {
         return !state.isBottom();
     }
 
-    /**
-     * Checks if the node is subsumed, i.e., the node is covered or not
-     * feasible.
-     */
+    /** Checks if the node is subsumed, i.e., the node is covered or not feasible. */
     public boolean isSubsumed() {
         return isCovered() || !isFeasible();
     }
 
-    /**
-     * Checks if the node is excluded, i.e., the node is subsumed or has an
-     * excluded parent.
-     */
+    /** Checks if the node is excluded, i.e., the node is subsumed or has an excluded parent. */
     public boolean isExcluded() {
         return ancestors().anyMatch(ArgNode::isSubsumed);
     }
 
     /**
-     * Checks if the node is target, i.e., the target predicate holds (e.g., it
-     * is an error state).
+     * Checks if the node is target, i.e., the target predicate holds (e.g., it is an error state).
      */
     public boolean isTarget() {
         return target;
     }
 
-    /**
-     * Checks if the node is expanded, i.e., all of its successors are present.
-     */
+    /** Checks if the node is expanded, i.e., all of its successors are present. */
     public boolean isExpanded() {
         return expanded;
     }
 
-    /**
-     * Checks if the node is leaf, i.e., it has no successors.
-     */
+    /** Checks if the node is leaf, i.e., it has no successors. */
     public boolean isLeaf() {
         return outEdges.isEmpty();
     }
 
-    /**
-     * Checks if the node is safe, i.e., not target or excluded.
-     */
+    /** Checks if the node is safe, i.e., not target or excluded. */
     public boolean isSafe() {
         return !isTarget() || isExcluded();
     }
 
-    /**
-     * Checks if the node is complete, i.e., expanded or excluded.
-     */
+    /** Checks if the node is complete, i.e., expanded or excluded. */
     public boolean isComplete() {
         return isExpanded() || isExcluded();
     }
 
     ////
 
     public Stream<ArgNode<S, A>> properAncestors() {
-        return getParent().map(p -> Stream.concat(Stream.of(p), p.properAncestors())).orElse(Stream.empty());
+        return getParent()
+                .map(p -> Stream.concat(Stream.of(p), p.properAncestors()))
+                .orElse(Stream.empty());
     }
 
     public Stream<ArgNode<S, A>> ancestors() {
@@ -263,7 +253,8 @@ private Stream<ArgNode<S, A>> unexcludedDescendantsOfNode() {
         if (this.isSubsumed()) {
             return Stream.empty();
         } else {
-            return Stream.concat(Stream.of(this), this.children().flatMap(ArgNode::unexcludedDescendantsOfNode));
+            return Stream.concat(
+                    Stream.of(this), this.children().flatMap(ArgNode::unexcludedDescendantsOfNode));
         }
     }
 

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java

@@ -91,7 +91,6 @@ public SafetyResult<Pr, C> check(final P initPrec) {
         WebDebuggerLogger wdl = WebDebuggerLogger.getInstance();
         do {
             ++iteration;
-
             logger.write(Level.MAINSTEP, "Iteration %d%n", iteration);
             logger.write(Level.MAINSTEP, "| Checking abstraction...%n");
             final long abstractorStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS);

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/AdvancedArgTrace.java

@@ -0,0 +1,166 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.algorithm.tracegeneration;
+
+import static com.google.common.base.Preconditions.checkNotNull;
+import static java.util.stream.Collectors.toList;
+
+import hu.bme.mit.theta.analysis.Action;
+import hu.bme.mit.theta.analysis.State;
+import hu.bme.mit.theta.analysis.Trace;
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgEdge;
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode;
+import java.util.*;
+import java.util.stream.Collectors;
+
+class AdvancedArgTrace<S extends State, A extends Action> implements Iterable<ArgNode<S, A>> {
+    private static final int HASH_SEED = 7453;
+    private volatile int hashCode = 0;
+
+    private final List<ArgNode<S, A>> nodes;
+    private final List<ArgEdge<S, A>> edges;
+    private final Collection<State> states;
+
+    private AdvancedArgTrace(final ArgNode<S, A> node) {
+        // adding items to first index will lead to O(N^2) performance
+        final List<ArgNode<S, A>> nodeList = new ArrayList<>();
+        final List<ArgEdge<S, A>> edgeList = new ArrayList<>();
+
+        ArgNode<S, A> running = node;
+        nodeList.add(running);
+
+        while (running.getInEdge().isPresent()) {
+            final ArgEdge<S, A> inEdge = running.getInEdge().get();
+            running = inEdge.getSource();
+            edgeList.add(inEdge);
+            nodeList.add(running);
+        }
+
+        // create the correct order by reversing O(N)
+        Collections.reverse(nodeList);
+        Collections.reverse(edgeList);
+
+        this.nodes = Collections.unmodifiableList(nodeList);
+        this.edges = Collections.unmodifiableList(edgeList);
+        states = nodes.stream().map(ArgNode::getState).collect(Collectors.toList());
+    }
+
+    private AdvancedArgTrace(List<ArgNode<S, A>> nodeList, List<ArgEdge<S, A>> edgeList) {
+        this.nodes = Collections.unmodifiableList(nodeList);
+        this.edges = Collections.unmodifiableList(edgeList);
+        states = nodes.stream().map(ArgNode::getState).collect(Collectors.toList());
+    }
+
+    ////
+
+    public static <S extends State, A extends Action> AdvancedArgTrace<S, A> to(
+            final ArgNode<S, A> node) {
+        checkNotNull(node);
+        return new AdvancedArgTrace<>(node);
+    }
+
+    public static <S extends State, A extends Action> AdvancedArgTrace<S, A> fromTo(
+            final ArgNode<S, A> fromNode, final ArgNode<S, A> toNode) {
+        checkNotNull(fromNode);
+        checkNotNull(toNode);
+        AdvancedArgTrace<S, A> differenceTrace = new AdvancedArgTrace<>(fromNode);
+        AdvancedArgTrace<S, A> fullTrace = new AdvancedArgTrace<>(toNode);
+        return substituteTrace(fullTrace, differenceTrace);
+    }
+
+    /**
+     * Substitutes the differenceTrace from the fullTrace, where the differenceTrace should be the
+     * beginning of the full trace
+     */
+    private static <A extends Action, S extends State> AdvancedArgTrace<S, A> substituteTrace(
+            AdvancedArgTrace<S, A> fullTrace, AdvancedArgTrace<S, A> differenceTrace) {
+        List<ArgNode<S, A>> differenceNodes = differenceTrace.nodes;
+
+        List<ArgNode<S, A>> remainingNodes = new ArrayList<>(fullTrace.nodes);
+        remainingNodes.removeIf(
+                saArgNode ->
+                        !(saArgNode.equals(differenceNodes.get(differenceNodes.size() - 1)))
+                                && differenceNodes.contains(saArgNode));
+
+        List<ArgEdge<S, A>> remainingEdges = new ArrayList<>(fullTrace.edges);
+        remainingEdges.removeIf(differenceTrace.edges::contains);
+
+        return new AdvancedArgTrace<>(remainingNodes, remainingEdges);
+    }
+
+    ////
+
+    /** Gets the length of the trace, i.e., the number of edges. */
+    public int length() {
+        return edges.size();
+    }
+
+    public ArgNode<S, A> node(final int index) {
+        return nodes.get(index);
+    }
+
+    public ArgEdge<S, A> edge(final int index) {
+        return edges.get(index);
+    }
+
+    public List<ArgNode<S, A>> nodes() {
+        return nodes;
+    }
+
+    public List<ArgEdge<S, A>> edges() {
+        return edges;
+    }
+
+    ////
+
+    /**
+     * Converts the ArgTrace to a Trace by extracting states and actions from nodes and edges
+     * respectively.
+     */
+    public Trace<S, A> toTrace() {
+        final List<S> states = nodes.stream().map(ArgNode::getState).collect(toList());
+        final List<A> actions = edges.stream().map(ArgEdge::getAction).collect(toList());
+        return Trace.of(states, actions);
+    }
+
+    ////
+
+    @Override
+    public Iterator<ArgNode<S, A>> iterator() {
+        return nodes.iterator();
+    }
+
+    @Override
+    public boolean equals(Object o) {
+        if (this == o) return true;
+        if (o == null || getClass() != o.getClass()) return false;
+        AdvancedArgTrace<?, ?> argTrace = (AdvancedArgTrace<?, ?>) o;
+        return states.equals(argTrace.states); // && edges.equals(argTrace.edges);
+    }
+
+    @Override
+    public int hashCode() {
+        int result = hashCode;
+        if (result == 0) {
+            result = HASH_SEED;
+            result = 31 * result + states.hashCode();
+            result = 31 * result + edges.hashCode();
+            hashCode = result;
+        }
+        return result;
+        // return Objects.hash(states, edges);
+    }
+}