> ancestors() {
@@ -256,32 +263,18 @@ private Stream> 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));
}
}
////
- @Override
- public int hashCode() {
- int result = hashCode;
- if (result == 0) {
- result = HASH_SEED;
- result = 31 * result + id;
- hashCode = result;
- }
- return result;
- }
-
- @Override
- public boolean equals(final Object obj) {
- return super.equals(obj);
- }
-
@Override
public String toString() {
return Utils.lispStringBuilder("ArgNode").add(id).body().add(state).toString();
}
+ public void disableCoveringAbility() {
+ canCover = false;
+ }
}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNodeComparators.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNodeComparators.java
index c990cdb893..fde6fb2f56 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNodeComparators.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNodeComparators.java
@@ -1,5 +1,5 @@
/*
- * Copyright 2023 Budapest University of Technology and Economics
+ * 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.
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgStructuralEquality.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgStructuralEquality.java
new file mode 100644
index 0000000000..8003232ff9
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgStructuralEquality.java
@@ -0,0 +1,192 @@
+/*
+ * 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;
+
+import hu.bme.mit.theta.analysis.Action;
+import hu.bme.mit.theta.analysis.State;
+
+import java.util.LinkedHashMap;
+import java.util.Map;
+import java.util.Set;
+import java.util.stream.Collectors;
+
+import static com.google.common.base.Objects.equal;
+
+/**
+ * Structural comparisons using equal() and hashCode() for ARG-related classes.
+ * Each node is uniquely identifiable using its incoming edge (or its absence), and wrapped state.
+ * Each edge is uniquely identifiable using its source node, and wrapped action.
+ * An ARG is uniquely identifiable using its leaf nodes.
+ * An ArgTrace is uniquely identifiable using its last node.
+ *
+ * We perform caching for the hash codes, but equals() checks will always traverse the ancestors of
+ * a node (and edge). However, this traversal only goes towards the root, rather than in all
+ * directions.
+ */
+public final class ArgStructuralEquality {
+ private static final Map hashCodeCache = new LinkedHashMap<>();
+
+ private ArgStructuralEquality() {
+ }
+
+ public static boolean equals(final ArgNode n1,
+ final ArgNode n2) {
+
+ // if references are the same, the two nodes are equal
+ if (n1 == n2) {
+ return true;
+ }
+
+ // if one is null, the two nodes are not equal
+ if (n1 == null || n2 == null) {
+ return false;
+ }
+
+ // if wrapped state is not same, nodes are not equal
+ if (!n1.getState().equals(n2.getState())) {
+ return false;
+ }
+
+ // if one node has a parent but the other one does not, nodes are not equal
+ if (n1.inEdge.isPresent() != n2.inEdge.isPresent()) {
+ return false;
+ }
+
+ // if in edge is not same, nodes are not equal
+ if (n1.inEdge.isPresent() && !equals(n1.inEdge.get(), n2.inEdge.get())) {
+ return false;
+ }
+
+ return true;
+ }
+
+ public static boolean equals(final ArgEdge e1,
+ final ArgEdge e2) {
+
+ // if references are the same, the two edges are equal
+ if (e1 == e2) {
+ return true;
+ }
+
+ // if one is null, the two edges are not equal
+ if (e1 == null || e2 == null) {
+ return false;
+ }
+
+
+ // if wrapped action is not same, edges are not equal
+ if (!e1.getAction().equals(e2.getAction())) {
+ return false;
+ }
+
+ // if source node is not same, edges are not equal
+ if (!equals(e1.getSource(), e2.getSource())) {
+ return false;
+ }
+
+ return true;
+ }
+
+ public static boolean equals(final ARG a1,
+ final ARG a2) {
+
+ // if references are the same, the two edges are equal
+ if (a1 == a2) {
+ return true;
+ }
+
+ // if one is null, the two args are not equal
+ if (a1 == null || a2 == null) {
+ return false;
+ }
+
+ Set> leaves1 = a1.getNodes().filter(ArgNode::isLeaf).collect(Collectors.toUnmodifiableSet());
+ Set> leaves2 = a2.getNodes().filter(ArgNode::isLeaf).collect(Collectors.toUnmodifiableSet());
+
+ // if the two ARGs contain a different number of leaf nodes, they are not equal
+ if (leaves1.size() != leaves2.size()) {
+ return false;
+ }
+
+ leaves1loop:
+ for (ArgNode n1 : leaves1) {
+ for (ArgNode n2 : leaves2) {
+ if (equals(n1, n2)) {
+ continue leaves1loop;
+ }
+ }
+ // a leaf node did not have a corresponding leaf node in the other arg
+ return false;
+ }
+ return true;
+ }
+
+ public static boolean equals(final ArgTrace t1,
+ final ArgTrace t2) {
+
+ return equal(t1.node(t1.length()), t2.node(t2.length()));
+ }
+
+
+ public static int hashCode(final ArgNode n) {
+ if (!hashCodeCache.containsKey(n)) {
+ int hashcode = 0;
+
+ if (n.inEdge.isPresent()) {
+ hashcode += hashCode(n.inEdge.get());
+ }
+
+ hashcode += n.getState().hashCode();
+ hashCodeCache.put(n, hashcode);
+ }
+ return hashCodeCache.get(n);
+ }
+
+ public static int hashCode(final ArgEdge e) {
+ if (!hashCodeCache.containsKey(e)) {
+ int hashcode = 0;
+
+ hashcode += hashCode(e.getSource());
+
+ hashcode += e.getAction().hashCode();
+
+ hashCodeCache.put(e, hashcode);
+ }
+ return hashCodeCache.get(e);
+ }
+
+ // ARG is not immutable, so we don't cache
+ public static int hashCode(final ARG a) {
+ int hashcode = 0;
+
+ Set> leaves = a.getNodes().filter(ArgNode::isLeaf).collect(Collectors.toUnmodifiableSet());
+ for (ArgNode leaf : leaves) {
+ hashcode += hashCode(leaf);
+ }
+
+ return hashcode;
+ }
+
+ public static int hashCode(final ArgTrace t) {
+ if (!hashCodeCache.containsKey(t)) {
+ int hashcode = hashCode(t.node(t.length()));
+ hashCodeCache.put(t, hashcode);
+ }
+ return hashCodeCache.get(t);
+ }
+
+}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgTrace.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgTrace.java
index a786f29df8..8595ed5893 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgTrace.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgTrace.java
@@ -1,5 +1,5 @@
/*
- * Copyright 2023 Budapest University of Technology and Economics
+ * 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.
@@ -34,9 +34,6 @@
*/
public final class ArgTrace implements Iterable> {
- private static final int HASH_SEED = 7653;
- private volatile int hashCode = 0;
-
private final List> nodes;
private final List> edges;
private final Collection states;
@@ -116,30 +113,4 @@ public Iterator> iterator() {
return nodes.iterator();
}
- @Override
- public boolean equals(Object o) {
- if (this == o) {
- return true;
- }
- if (o == null || getClass() != o.getClass()) {
- return false;
- }
- ArgTrace argTrace = (ArgTrace) 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);
- }
- ////
-
}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgUtils.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgUtils.java
index c67d63daa1..e9c1ffab5b 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgUtils.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgUtils.java
@@ -1,5 +1,5 @@
/*
- * Copyright 2023 Budapest University of Technology and Economics
+ * 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.
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/MonolithicTransFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/MonolithicTransFunc.java
new file mode 100644
index 0000000000..883058e1d2
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/MonolithicTransFunc.java
@@ -0,0 +1,36 @@
+/*
+ * 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;
+
+import com.google.errorprone.annotations.Var;
+import hu.bme.mit.theta.core.type.Expr;
+import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.core.utils.indexings.VarIndexing;
+import hu.bme.mit.theta.solver.SolverFactory;
+
+public interface MonolithicTransFunc {
+ Expr getTransExpr();
+
+ Expr getInitExpr();
+
+ Expr getPropExpr();
+
+ VarIndexing getInitIndexing();
+
+ VarIndexing getOffsetIndexing();
+
+
+}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/PorLts.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/PorLts.java
deleted file mode 100644
index f8cb7b5f35..0000000000
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/PorLts.java
+++ /dev/null
@@ -1,278 +0,0 @@
-/*
- * Copyright 2023 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;
-
-import hu.bme.mit.theta.analysis.Action;
-import hu.bme.mit.theta.analysis.LTS;
-import hu.bme.mit.theta.analysis.State;
-import hu.bme.mit.theta.core.decl.Decl;
-import hu.bme.mit.theta.core.type.Type;
-
-import java.util.*;
-import java.util.function.Predicate;
-
-/**
- * LTS with a POR (Partial Order Reduction) algorithm applied as a filter when returning enabled
- * actions.
- *
- * @param the type of the state
- * @param the type of the action (transition in the state space)
- * @param the type of the transition in the original formalism
- */
-public abstract class PorLts implements LTS {
-
- /* CACHE COLLECTIONS */
-
- /**
- * Shared objects (~global variables) used by a transition.
- */
- private final HashMap>> usedSharedObjects = new HashMap<>();
-
- /**
- * Shared objects (~global variables) that are used by the key transition or by transitions
- * reachable from the current state via a given transition.
- */
- private final HashMap>> influencedSharedObjects = new HashMap<>();
-
- /**
- * Backward transitions in the transition system (a transition of a loop).
- */
- protected final Set backwardTransitions = new HashSet<>();
-
-
- /**
- * Returns the enabled actions in the ARG from the given state filtered with a POR algorithm.
- *
- * @param state the state whose enabled actions we would like to know
- * @return the enabled actions
- */
- @Override
- public Collection getEnabledActionsFor(S state) {
- // Collecting enabled actions
- Collection allEnabledActions = getAllEnabledActionsFor(state);
-
- // Calculating the persistent set starting from every (or some of the) enabled transition; the minimal persistent set is stored
- Collection minimalPersistentSet = new HashSet<>();
- Collection persistentSetFirstActions = getPersistentSetFirstActions(allEnabledActions);
- for (A firstAction : persistentSetFirstActions) {
- Collection persistentSet = calculatePersistentSet(allEnabledActions, firstAction);
- if (minimalPersistentSet.size() == 0
- || persistentSet.size() < minimalPersistentSet.size()) {
- minimalPersistentSet = persistentSet;
- }
- }
-
- return minimalPersistentSet;
- }
-
- /**
- * Calculates a persistent set of enabled actions starting from a particular action.
- *
- * @param enabledActions the enabled actions in the present state
- * @param firstAction the action who will be added to the persistent set as the first action
- * @return the persistent set of enabled actions
- */
- protected Collection calculatePersistentSet(Collection enabledActions, A firstAction) {
- if (isBackwardAction(firstAction)) {
- return new HashSet<>(enabledActions);
- }
-
- Set persistentSet = new HashSet<>();
- Set otherActions = new HashSet<>(enabledActions); // actions not in the persistent set
- persistentSet.add(firstAction);
- otherActions.remove(firstAction);
-
- boolean addedNewAction = true;
- while (addedNewAction) {
- addedNewAction = false;
- Set actionsToRemove = new HashSet<>();
- for (A action : otherActions) {
- // for every action that is not in the persistent set it is checked whether it should be added to the persistent set
- // (because it is dependent with an action already in the persistent set)
- if (persistentSet.stream()
- .anyMatch(persistentSetAction -> areDependents(persistentSetAction, action))) {
- if (isBackwardAction(action)) {
- return new HashSet<>(
- enabledActions); // see POR algorithm for the reason of removing backward transitions
- }
-
- persistentSet.add(action);
- actionsToRemove.add(action);
- addedNewAction = true;
- }
- }
- actionsToRemove.forEach(otherActions::remove);
- }
-
- return persistentSet;
- }
-
- /**
- * Returns all the enabled actions in a state.
- *
- * @param state the state whose enabled actions are to be returned
- * @return the enabled actions in the state
- */
- protected abstract Collection getAllEnabledActionsFor(S state);
-
- /**
- * Returns the actions from where persistent sets will be calculated (a subset of the given
- * enabled actions). The default implementation returns all enabled actions.
- *
- * @param allEnabledActions all the enabled actions in the present state
- * @return the actions from where persistent sets will be calculated
- */
- protected Collection getPersistentSetFirstActions(Collection allEnabledActions) {
- return allEnabledActions;
- }
-
- /**
- * Determines whether an action is dependent with another one (based on the notions introduced
- * for the POR algorithm) already in the persistent set.
- *
- * @param persistentSetAction the action in the persistent set
- * @param action the other action (not in the persistent set)
- * @return true, if the two actions are dependent in the context of persistent sets
- */
- protected boolean areDependents(A persistentSetAction, A action) {
- return canEnOrDisableEachOther(persistentSetAction, action) ||
- getInfluencedSharedObjects(getTransitionOf(action)).stream().anyMatch(varDecl ->
- getCachedUsedSharedObjects(getTransitionOf(persistentSetAction)).contains(varDecl));
- }
-
- /**
- * Determines whether two actions can enable or disable each other (if true, the two actions are
- * dependent).
- *
- * @param action1 action 1
- * @param action2 action 2
- * @return true, if the two actions can enable or disable each other
- */
- protected abstract boolean canEnOrDisableEachOther(A action1, A action2);
-
- /**
- * Determines whether the given action is a backward action.
- *
- * @param action the action to be classified as backward action or non-backward action
- * @return true, if the action is a backward action
- */
- protected boolean isBackwardAction(A action) {
- return backwardTransitions.contains(getTransitionOf(action));
- }
-
- /**
- * Get the original transition of an action (from which the action has been created).
- *
- * @param action whose original transition is to be returned
- * @return the original transition
- */
- protected abstract T getTransitionOf(A action);
-
- /**
- * Returns the successive transitions of a transition (transitions whose source is the target of
- * the given parameter).
- *
- * @param transition whose successive transitions is to be returned
- * @return the successive transitions of the transition given as the parameter
- */
- protected abstract Set getSuccessiveTransitions(T transition);
-
-
- /**
- * Returns the shared objects (~global variables) that an action uses (it is present in one of
- * its labels).
- *
- * @param transition whose shared objects are to be returned
- * @return the set of used shared objects
- */
- protected abstract Set> getDirectlyUsedSharedObjects(
- T transition);
-
- /**
- * Returns the shared objects (~global variables) that an action uses.
- *
- * @param transition whose shared objects are to be returned
- * @return the set of directly or indirectly used shared objects
- */
- protected Set> getUsedSharedObjects(T transition) {
- return getDirectlyUsedSharedObjects(transition);
- }
-
- /**
- * Same as {@link PorLts#getUsedSharedObjects(T transition)} with an additional cache layer.
- *
- * @param transition whose shared objects are to be returned
- * @return the set of directly or indirectly used shared objects
- */
- private Set> getCachedUsedSharedObjects(T transition) {
- if (!usedSharedObjects.containsKey(transition)) {
- Set> vars = getUsedSharedObjects(transition);
- usedSharedObjects.put(transition, vars);
- }
- return usedSharedObjects.get(transition);
- }
-
- /**
- * Returns the shared objects (~global variables) used by the given transition or by transitions
- * that are reachable via the given transition ("influenced shared objects").
- *
- * @param transition whose successor transitions' shared objects are to be returned.
- * @return the set of influenced shared objects
- */
- protected Set> getInfluencedSharedObjects(T transition) {
- if (!influencedSharedObjects.containsKey(transition)) {
- influencedSharedObjects.put(transition, getSharedObjectsWithBFS(transition, t -> true));
- }
- return influencedSharedObjects.get(transition);
- }
-
- /**
- * Returns shared objects (~global variables) encountered in a search starting from a given
- * transition.
- *
- * @param startTransition the start point (transition) of the search
- * @param visitTransition the predicate that tells whether a transition has to be explored
- * @return the set of encountered shared objects
- */
- protected Set> getSharedObjectsWithBFS(T startTransition,
- Predicate visitTransition) {
- Set> vars = new HashSet<>();
- List exploredTransitions = new ArrayList<>();
- List transitionsToExplore = new ArrayList<>();
- transitionsToExplore.add(startTransition);
-
- while (!transitionsToExplore.isEmpty()) {
- T exploring = transitionsToExplore.remove(0);
- vars.addAll(getDirectlyUsedSharedObjects(exploring));
- Set successiveTransitions = getSuccessiveTransitions(exploring);
-
- for (var newTransition : successiveTransitions) {
- if (!exploredTransitions.contains(newTransition) && visitTransition.test(
- newTransition)) {
- transitionsToExplore.add(newTransition);
- }
- }
- exploredTransitions.add(exploring);
- }
- return vars;
- }
-
- /**
- * Collects backward transitions of the transition system.
- */
- protected abstract void collectBackwardTransitions();
-}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyChecker.java
index 64359f6eda..8ef5560d14 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyChecker.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyChecker.java
@@ -1,5 +1,5 @@
/*
- * Copyright 2023 Budapest University of Technology and Economics
+ * 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.
@@ -19,8 +19,13 @@
import hu.bme.mit.theta.analysis.Prec;
import hu.bme.mit.theta.analysis.State;
+@FunctionalInterface
public interface SafetyChecker {
SafetyResult check(final P prec);
+ default SafetyResult check() {
+ return check(null);
+ }
+
}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java
index 0bb37cdfbf..ebc215711c 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java
@@ -1,5 +1,5 @@
/*
- * Copyright 2023 Budapest University of Technology and Economics
+ * 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.
@@ -15,51 +15,79 @@
*/
package hu.bme.mit.theta.analysis.algorithm;
-import static com.google.common.base.Preconditions.checkNotNull;
-
-import java.util.Optional;
-
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.common.Utils;
+import java.util.Optional;
+
+import static com.google.common.base.Preconditions.checkNotNull;
+
public abstract class SafetyResult {
- private final ARG arg;
+ private final Optional> arg;
private final Optional stats;
private SafetyResult(final ARG arg, final Optional stats) {
- this.arg = checkNotNull(arg);
+ this.arg = Optional.of(arg);
this.stats = checkNotNull(stats);
}
+ private SafetyResult() {
+ this.arg = Optional.empty();
+ this.stats = Optional.empty();
+ }
+
+
+ public boolean hasArg() {
+ return arg.isPresent();
+ }
+
public ARG getArg() {
- return arg;
+ return arg.orElseThrow();
}
public Optional getStats() {
return stats;
}
+ // Factory methods
+
+ public static Safe safe(final ARG arg,
+ final Statistics stats) {
+ return new Safe<>(arg, Optional.of(stats));
+ }
+
public static Safe safe(final ARG arg) {
return new Safe<>(arg, Optional.empty());
}
+ public static Safe safe() {
+ return new Safe<>();
+ }
+
+ public static Unsafe unsafe(final Trace cex,
+ final ARG arg,
+ final Statistics stats) {
+ return new Unsafe<>(cex, arg, Optional.of(stats));
+ }
+
public static Unsafe unsafe(final Trace cex,
final ARG arg) {
return new Unsafe<>(cex, arg, Optional.empty());
}
- public static Safe safe(final ARG arg,
- final Statistics stats) {
- return new Safe<>(arg, Optional.of(stats));
+ public static Unsafe unsafe(final Trace cex) {
+ return new Unsafe<>(cex);
}
- public static Unsafe unsafe(final Trace cex,
- final ARG arg,
- final Statistics stats) {
- return new Unsafe<>(cex, arg, Optional.of(stats));
+ public static Unsafe unsafe() {
+ return new Unsafe<>();
+ }
+
+ public static Unknown unknown() {
+ return new Unknown<>();
}
public abstract boolean isSafe();
@@ -78,6 +106,9 @@ private Safe(final ARG arg, final Optional stats) {
super(arg, stats);
}
+ private Safe() {
+ }
+
@Override
public boolean isSafe() {
return true;
@@ -110,16 +141,28 @@ public String toString() {
public static final class Unsafe extends SafetyResult {
- private final Trace cex;
+ private final Optional> cex;
private Unsafe(final Trace cex, final ARG arg,
final Optional stats) {
super(arg, stats);
- this.cex = checkNotNull(cex);
+ this.cex = Optional.of(cex);
+ }
+
+ private Unsafe(final Trace cex) {
+ this.cex = Optional.of(cex);
+ }
+
+ private Unsafe() {
+ this.cex = Optional.empty();
+ }
+
+ public boolean hasTrace() {
+ return cex.isPresent();
}
public Trace getTrace() {
- return cex;
+ return cex.orElseThrow();
}
@Override
@@ -148,7 +191,36 @@ public Unsafe asUnsafe() {
public String toString() {
return Utils.lispStringBuilder(SafetyResult.class.getSimpleName())
.add(Unsafe.class.getSimpleName())
- .add("Trace length: " + cex.length()).toString();
+ .add("Trace length: " + cex.map(Trace::length).orElse(-1)).toString();
+ }
+ }
+
+ public static final class Unknown extends SafetyResult {
+ @Override
+ public boolean isSafe() {
+ return false;
+ }
+
+ @Override
+ public boolean isUnsafe() {
+ return false;
+ }
+
+ @Override
+ public Safe asSafe() {
+ return null;
+ }
+
+ @Override
+ public Unsafe asUnsafe() {
+ return null;
+ }
+
+ @Override
+ public String toString() {
+ return Utils.lispStringBuilder(SafetyResult.class.getSimpleName())
+ .add(Unknown.class.getSimpleName())
+ .toString();
}
}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SearchStrategy.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SearchStrategy.java
index 309e46c1bb..92016c78de 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SearchStrategy.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SearchStrategy.java
@@ -1,5 +1,5 @@
/*
- * Copyright 2023 Budapest University of Technology and Economics
+ * 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.
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Statistics.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Statistics.java
index 9de218da80..e7fcc7f9fe 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Statistics.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Statistics.java
@@ -1,5 +1,5 @@
/*
- * Copyright 2023 Budapest University of Technology and Economics
+ * 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.
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bmc/BmcChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bmc/BmcChecker.java
deleted file mode 100644
index 7c061dadcb..0000000000
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bmc/BmcChecker.java
+++ /dev/null
@@ -1,189 +0,0 @@
-/*
- * Copyright 2023 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.bmc;
-
-import com.google.common.collect.Lists;
-import hu.bme.mit.theta.analysis.InitFunc;
-import hu.bme.mit.theta.analysis.LTS;
-import hu.bme.mit.theta.analysis.Prec;
-import hu.bme.mit.theta.analysis.TransFunc;
-import hu.bme.mit.theta.analysis.algorithm.ARG;
-import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
-import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
-import hu.bme.mit.theta.analysis.expr.ExprState;
-import hu.bme.mit.theta.analysis.expr.StmtAction;
-import hu.bme.mit.theta.common.Utils;
-import hu.bme.mit.theta.common.logging.Logger;
-import hu.bme.mit.theta.solver.Solver;
-
-import java.util.ArrayList;
-import java.util.Collection;
-import java.util.LinkedList;
-import java.util.List;
-import java.util.function.Predicate;
-import java.util.stream.Collectors;
-
-import static com.google.common.base.Preconditions.checkState;
-
-public class BmcChecker implements
- SafetyChecker {
-
- private final LTS lts;
- private final InitFunc initFunc;
- private final TransFunc transFunc;
- private final Predicate unsafePredicate;
- private final Solver solver;
- private final int upperBound;
- private final Logger logger;
- private final boolean onlyFeasible; // only keep feasible traces (i.e. test in each iteration)
-
- private BmcChecker(final LTS lts,
- final InitFunc initFunc,
- final TransFunc transFunc,
- final Predicate unsafePredicate,
- final Solver solver,
- final Logger logger,
- final int upperBound, boolean onlyFeasible) {
- this.lts = lts;
- this.initFunc = initFunc;
- this.transFunc = transFunc;
- this.unsafePredicate = unsafePredicate;
- this.solver = solver;
- this.upperBound = upperBound;
- this.logger = logger;
- this.onlyFeasible = onlyFeasible;
- }
-
- public static BmcChecker create(
- final LTS lts,
- final InitFunc initFunc,
- final TransFunc transFunc,
- final Predicate unsafePredicate,
- final Solver solver,
- final Logger logger,
- final int upperBound,
- final boolean onlyFeasible) {
- return new BmcChecker(lts, initFunc, transFunc, unsafePredicate, solver, logger,
- upperBound, onlyFeasible);
- }
-
- public static BmcChecker create(
- final LTS lts,
- final InitFunc initFunc,
- final TransFunc transFunc,
- final Predicate unsafePredicate,
- final Solver solver,
- final Logger logger,
- final boolean onlyFeasible) {
- return new BmcChecker(lts, initFunc, transFunc, unsafePredicate, solver, logger,
- -1, onlyFeasible);
- }
-
- @Override
- public SafetyResult check(P prec) {
- logger.write(Logger.Level.INFO, "Configuration: %s%n", this);
- final Collection initStates = initFunc.getInitStates(prec);
- final List> traces = initStates.stream()
- .map(s -> BmcTrace.of(List.of(s), List.of()))
- .collect(Collectors.toCollection(LinkedList::new));
- int currentBound = 0;
- SafetyResult bmcresult = null;
- outerloop:
- while ((upperBound < 0 || currentBound < upperBound) && traces.size() > 0) {
- currentBound++;
- logger.write(Logger.Level.MAINSTEP, "Iteration %d%n", currentBound);
- logger.write(Logger.Level.MAINSTEP, "| Current traces: %d%n", traces.size());
- logger.write(Logger.Level.MAINSTEP, "| Expanding traces...%n");
- int size = traces.size();
- final List toRemove = new ArrayList<>();
- for (int i = 0; i < size; i++) {
- BmcTrace t = traces.get(i);
- checkState(t.length() == currentBound - 1, "Trace " + t + " not well formatted");
- final S lastState = t.getLastState();
- final Collection actions = lts.getEnabledActionsFor(lastState);
- int actionCnt = 0;
- int addCount = 0;
- for (A a : actions) {
- actionCnt++;
- final Collection states = transFunc.getSuccStates(lastState, a,
- prec);
- int stateCnt = 0;
- for (S succState : states) {
- stateCnt++;
- final BmcTrace trace;
- final int idx;
- addCount++;
- if (actions.size() == actionCnt && states.size() == stateCnt) {
- trace = t.addState(succState, a);
- idx = i;
- } else {
- trace = t.copy().addState(succState, a);
- idx = traces.size();
- traces.add(trace);
- }
- if (onlyFeasible) {
- final boolean feasible = trace.isFeasible(solver);
- if (feasible) {
- final boolean unsafe = unsafePredicate.test(succState);
- if (unsafe) {
- bmcresult = SafetyResult.unsafe(trace.toImmutableTrace(),
- ARG.create(
- (state1, state2) -> false)); // TODO: this is only a placeholder, we don't give back an ARG
- break outerloop;
- }
- } else {
- addCount--;
- traces.remove(idx);
- if (idx <= i) {
- size--;
- i--;
- }
- }
- } else {
- if (unsafePredicate.test(succState) && trace.isFeasible(solver)) {
- bmcresult = SafetyResult.unsafe(trace.toImmutableTrace(),
- ARG.create(
- (state1, state2) -> false)); // TODO: this is only a placeholder, we don't give back an ARG
- break outerloop;
- }
- }
- }
- }
- if (addCount == 0) {
- traces.remove(i);
- size--;
- i--;
- }
- }
- for (int idx : Lists.reverse(toRemove)) {
- traces.remove(idx);
- }
- }
- if (bmcresult == null) {
- bmcresult = SafetyResult.safe(ARG.create(
- (state1, state2) -> false)); // TODO: this is only a placeholder, we don't give back an ARG
- }
- logger.write(Logger.Level.RESULT, "%s%n", bmcresult);
- return bmcresult;
- }
-
- @Override
- public String toString() {
- return Utils.lispStringBuilder(getClass().getSimpleName()).add(upperBound).add(lts)
- .add(initFunc).toString();
- }
-}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bmc/BmcTrace.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bmc/BmcTrace.java
deleted file mode 100644
index d001868433..0000000000
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bmc/BmcTrace.java
+++ /dev/null
@@ -1,197 +0,0 @@
-/*
- * Copyright 2023 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.bmc;
-
-import com.google.common.collect.ImmutableList;
-import com.google.common.collect.Lists;
-import com.google.common.collect.Streams;
-import hu.bme.mit.theta.analysis.Trace;
-import hu.bme.mit.theta.analysis.expr.ExprState;
-import hu.bme.mit.theta.analysis.expr.StmtAction;
-import hu.bme.mit.theta.common.LispStringBuilder;
-import hu.bme.mit.theta.common.Utils;
-import hu.bme.mit.theta.core.stmt.Stmt;
-import hu.bme.mit.theta.core.utils.PathUtils;
-import hu.bme.mit.theta.solver.Solver;
-
-import java.util.LinkedList;
-import java.util.List;
-import java.util.stream.Collectors;
-
-import static com.google.common.base.Preconditions.checkArgument;
-import static com.google.common.base.Preconditions.checkElementIndex;
-import static com.google.common.base.Preconditions.checkNotNull;
-import static hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory.indexing;
-
-/**
- * Represents a mutable, alternating trace in the form of a (State, Action, State, ..., State,
- * Action, State) sequence. A trace always contains at least one state and the number of actions is
- * one less than the number of states.
- */
-public final class BmcTrace {
-
- private final List states;
- private final List actions;
- private final List statements;
-
- private BmcTrace(final List states, final List actions,
- final List statements) {
- checkNotNull(states);
- checkNotNull(actions);
- checkArgument(!states.isEmpty(), "A trace must contain at least one state.");
- checkArgument(states.size() == actions.size() + 1, "#states = #actions + 1 must hold.");
- this.states = new LinkedList<>(states);
- this.actions = new LinkedList<>(actions);
- this.statements = new LinkedList<>(statements);
- }
-
- private BmcTrace(final List states, final List actions) {
- this(states,
- actions,
- actions.stream().map(a -> a.getStmts().stream()).reduce(Streams::concat)
- .map(s -> s.collect(Collectors.toList())).orElse(List.of()));
- }
-
- /**
- * Create a trace. The size of states must be at least one, and the size of the actions must be
- * one less than the number of states.
- */
- public static BmcTrace of(
- final List states, final List actions) {
- return new BmcTrace<>(states, actions);
- }
-
- /**
- * Gets the length of the trace, which is the number of actions.
- */
- public int length() {
- return actions.size();
- }
-
- /**
- * Gets a state at a given index.
- *
- * @param i Index
- * @return State
- */
- public S getState(final int i) {
- checkElementIndex(0, states.size());
- return states.get(i);
- }
-
- /**
- * Gets an action at a given index
- *
- * @param i Index
- * @return Action
- */
- public A getAction(final int i) {
- checkElementIndex(0, actions.size());
- return actions.get(i);
- }
-
- /**
- * Gets all states.
- *
- * @return
- */
- public List getStates() {
- return ImmutableList.copyOf(states);
- }
-
- /**
- * Gets all actions.
- *
- * @return
- */
- public List getActions() {
- return ImmutableList.copyOf(actions);
- }
-
- /**
- * Creates a reversed trace by reversing both the states and the actions. The original trace is
- * not modified.
- *
- * @return Reversed trace
- */
- public BmcTrace reverse() {
- return BmcTrace.of(Lists.reverse(states), Lists.reverse(actions));
- }
-
- public BmcTrace copy() {
- return new BmcTrace<>(states, actions);
- }
-
- @Override
- public int hashCode() {
- return 31 * states.hashCode() + actions.hashCode();
- }
-
- @Override
- public boolean equals(final Object obj) {
- if (this == obj) {
- return true;
- } else if (obj instanceof BmcTrace) {
- final BmcTrace that = (BmcTrace) obj;
- return this.states.equals(that.states) && this.actions.equals(that.actions);
- } else {
- return false;
- }
- }
-
- @Override
- public String toString() {
- final LispStringBuilder sb = Utils.lispStringBuilder(getClass().getSimpleName()).body();
- for (int i = 0; i < length(); i++) {
- sb.add(states.get(i));
- sb.add(actions.get(i));
- }
- sb.add(states.get(length()));
- return sb.toString();
- }
-
- public BmcTrace addState(final S state, final A action) {
- states.add(state);
- actions.add(action);
- statements.addAll(action.getStmts());
- return this;
- }
-
- public S getLastState() {
- return states.get(states.size() - 1);
- }
-
- public boolean isFeasible(final Solver solver) {
- solver.push();
- StmtAction stmtAction = new StmtAction() {
- @Override
- public List getStmts() {
- return statements;
- }
- };
- solver.add(PathUtils.unfold(stmtAction.toExpr(), indexing(0)));
- if (solver.check().isUnsat()) {
- solver.pop();
- return false;
- }
- solver.pop();
- return true;
- }
-
- public Trace toImmutableTrace() {
- return Trace.of(states, actions);
- }
-}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bmc/IterativeBmcChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bmc/IterativeBmcChecker.java
deleted file mode 100644
index 0b5287b67f..0000000000
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bmc/IterativeBmcChecker.java
+++ /dev/null
@@ -1,211 +0,0 @@
-/*
- * Copyright 2023 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.bmc;
-
-import com.google.common.collect.Streams;
-import hu.bme.mit.theta.analysis.InitFunc;
-import hu.bme.mit.theta.analysis.LTS;
-import hu.bme.mit.theta.analysis.Prec;
-import hu.bme.mit.theta.analysis.Trace;
-import hu.bme.mit.theta.analysis.TransFunc;
-import hu.bme.mit.theta.analysis.algorithm.ARG;
-import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
-import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
-import hu.bme.mit.theta.analysis.expr.ExprState;
-import hu.bme.mit.theta.analysis.expr.StmtAction;
-import hu.bme.mit.theta.common.Tuple5;
-import hu.bme.mit.theta.common.Utils;
-import hu.bme.mit.theta.common.logging.Logger;
-import hu.bme.mit.theta.core.type.Expr;
-import hu.bme.mit.theta.core.type.booltype.BoolType;
-import hu.bme.mit.theta.core.utils.PathUtils;
-import hu.bme.mit.theta.core.utils.indexings.VarIndexing;
-import hu.bme.mit.theta.solver.Solver;
-
-import java.util.ArrayList;
-import java.util.Collection;
-import java.util.LinkedHashSet;
-import java.util.List;
-import java.util.function.Predicate;
-import java.util.stream.Collectors;
-import java.util.stream.Stream;
-
-import static hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory.indexing;
-
-public class IterativeBmcChecker implements
- SafetyChecker {
-
- private final LTS lts;
- private final InitFunc initFunc;
- private final TransFunc transFunc;
- private final Predicate unsafePredicate;
- private final Solver solver;
- private final int upperBound;
- private final int stepSize;
- private final Logger logger;
-
- private IterativeBmcChecker(final LTS lts,
- final InitFunc