Skip to content

Commit

Permalink
Formatted & reapplied copyright
Browse files Browse the repository at this point in the history
  • Loading branch information
@leventeBajczi
leventeBajczi committed Jul 24, 2023
1 parent fad785d commit c03432c
Show file tree
Hide file tree
Showing 13 changed files with 318 additions and 236 deletions.
40 changes: 20 additions & 20 deletions subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,21 +40,21 @@
* ArgBuilder.
*/
public final class ARG<S extends State, A extends Action> {
private final Collection<ArgNode<S, A>> initNodes;
public boolean initialized; // Set by ArgBuilder
private int nextId = 0;
private final PartialOrd<S> partialOrd;
private final Collection<ArgNode<S, A>> initNodes;
public boolean initialized; // Set by ArgBuilder
private int nextId = 0;
private final PartialOrd<S> partialOrd;

private final CexHashStorage<S, A> cexHashStorage;
private final ArgPrecHashStorage<S, A, Prec> argPrecHashStorage; // TODO not the best solution with Prec

private ARG(final PartialOrd<S> partialOrd) {
initNodes = Containers.createSet();
this.partialOrd = partialOrd;
this.initialized = false;
private ARG(final PartialOrd<S> partialOrd) {
initNodes = Containers.createSet();
this.partialOrd = partialOrd;
this.initialized = false;
this.cexHashStorage = new CexHashStorage<S, A>();
this.argPrecHashStorage = new ArgPrecHashStorage<S, A, Prec>();
}
}

public static <S extends State, A extends Action> ARG<S, A> create(final PartialOrd<S> partialOrd) {
return new ARG<>(partialOrd);
Expand Down Expand Up @@ -209,11 +209,11 @@ public Stream<ArgTrace<S, A>> getCexs() {
*/
public <P extends Prec> Stream<ArgTrace<S, A>> getNewCexs(P prec) {
return getUnsafeNodes().map(ArgTrace::to).filter(trace -> {
if(cexHashStorage.contains(trace)) {
if (cexHashStorage.contains(trace)) {
// isEmpty() below, because:
// if it is empty because we are in the first iteration - cexHashStorage is also empty, we can not be here
// if it is empty, because we do not track args and precs - cexHashStorage contains trace so it is not new - return false
if(argPrecHashStorage.isEmpty() || argPrecHashStorage.contains(Tuple2.of(this, prec))) {
if (argPrecHashStorage.isEmpty() || argPrecHashStorage.contains(Tuple2.of(this, prec))) {
return false;
}
}
Expand All @@ -222,11 +222,11 @@ public <P extends Prec> Stream<ArgTrace<S, A>> getNewCexs(P prec) {
}

/**
* Gets the size of the ARG, i.e., the number of nodes.
*/
public long size() {
return getNodes().count();
}
* Gets the size of the ARG, i.e., the number of nodes.
*/
public long size() {
return getNodes().count();
}

/**
* Gets the depth of the ARG, i.e., the maximal depth of its nodes. Depth
Expand Down Expand Up @@ -257,10 +257,10 @@ public boolean equals(Object o) {
initNodes.equals(arg.initNodes);
}

@Override
public int hashCode() {
return Objects.hash(initNodes, initialized, partialOrd);
}
@Override
public int hashCode() {
return Objects.hash(initNodes, initialized, partialOrd);
}

public CexHashStorage<S, A> getCexHashStorage() {
return cexHashStorage;
Expand Down
46 changes: 23 additions & 23 deletions subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -163,24 +163,24 @@ public boolean isCovered() {
return coveringNode.isPresent();
}

/**
* Checks if the node is not a bottom state.
*/
public boolean isFeasible() {
return !state.isBottom();
}
/**
* Checks if the node is not a bottom state.
*/
public boolean isFeasible() {
return !state.isBottom();
}

private boolean isTargetOfKnownInfeasibleTrace() {
return isTarget() && arg.getCexHashStorage().contains(ArgTrace.to(this)); // cex hash storage contains an infeasible trace to it
}

/**
* 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 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
Expand Down Expand Up @@ -212,19 +212,19 @@ public boolean isLeaf() {
return outEdges.isEmpty();
}

/**
* Checks if the node is safe, i.e., not target or excluded.
*/
public boolean isSafe() {
return !isTarget() || isExcluded() || isTargetOfKnownInfeasibleTrace();
}
/**
* Checks if the node is safe, i.e., not target or excluded.
*/
public boolean isSafe() {
return !isTarget() || isExcluded() || isTargetOfKnownInfeasibleTrace();
}

/**
* Checks if the node is complete, i.e., expanded or excluded.
*/
public boolean isComplete() {
return isExpanded() || isExcluded();
}
* Checks if the node is complete, i.e., expanded or excluded.
*/
public boolean isComplete() {
return isExpanded() || isExcluded();
}

////

Expand Down
24 changes: 12 additions & 12 deletions ...mon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,9 +93,9 @@ public AbstractorResult check(final ARG<S, A> arg, final P prec) {
reachedSet.addAll(arg.getNodes());
waitlist.addAll(arg.getIncompleteNodes());

if (!(stopCriterion.canStop(arg, prec))) {
while (!waitlist.isEmpty()) {
final ArgNode<S, A> node = waitlist.remove();
if (!(stopCriterion.canStop(arg, prec))) {
while (!waitlist.isEmpty()) {
final ArgNode<S, A> node = waitlist.remove();

Collection<ArgNode<S, A>> newNodes = Collections.emptyList();
close(node, reachedSet.get(node));
Expand All @@ -106,26 +106,26 @@ public AbstractorResult check(final ARG<S, A> arg, final P prec) {
}

if (stopCriterion.canStop(arg, newNodes, prec)) break;
}
}
}
}

logger.write(Level.SUBSTEP, "done%n");
logger.write(Level.INFO, "| | Finished ARG: %d nodes, %d incomplete, %d unsafe%n", arg.getNodes().count(),
arg.getIncompleteNodes().count(), arg.getUnsafeNodes().count());

waitlist.clear(); // Optimization

if(!arg.isComplete()) {
if (!arg.isComplete()) {
MonitorCheckpoint.Checkpoints.execute("CegarChecker.unsafeARG");
}

if (arg.isSafe() && arg.getNewCexs(prec).toList().isEmpty()) { // TODO the second half of the condition is a quick fix and the check ARG part should especially be refactored
checkState(arg.isComplete(), "Returning incomplete ARG as safe");
return AbstractorResult.safe();
} else {
return AbstractorResult.unsafe();
}
}
checkState(arg.isComplete(), "Returning incomplete ARG as safe");
return AbstractorResult.safe();
} else {
return AbstractorResult.unsafe();
}
}

private void close(final ArgNode<S, A> node, final Collection<ArgNode<S, A>> candidates) {
if (!node.isLeaf()) {
Expand Down
24 changes: 14 additions & 10 deletions ...common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@
import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter;
import hu.bme.mit.theta.common.visualization.writer.JSONWriter;
import hu.bme.mit.theta.common.visualization.writer.WebDebuggerLogger;

import java.io.FileWriter;
import java.io.IOException;
import java.util.concurrent.TimeUnit;
Expand Down Expand Up @@ -73,18 +74,21 @@ public static <S extends State, A extends Action, P extends Prec> CegarChecker<S
public ARG<S, A> getArg() {
return arg;
}
public Prec getCurrentPrec() { return prec; }

public Prec getCurrentPrec() {
return prec;
}

@Override
public SafetyResult<S, A> check(final P initPrec) {
logger.write(Level.INFO, "Configuration: %s%n", this);
final Stopwatch stopwatch = Stopwatch.createStarted();
long abstractorTime = 0;
long refinerTime = 0;
RefinerResult<S, A, P> refinerResult = null;
AbstractorResult abstractorResult = null;
prec = initPrec;
int iteration = 0;
public SafetyResult<S, A> check(final P initPrec) {
logger.write(Level.INFO, "Configuration: %s%n", this);
final Stopwatch stopwatch = Stopwatch.createStarted();
long abstractorTime = 0;
long refinerTime = 0;
RefinerResult<S, A, P> refinerResult = null;
AbstractorResult abstractorResult = null;
prec = initPrec;
int iteration = 0;
WebDebuggerLogger wdl = WebDebuggerLogger.getInstance();
do {
++iteration;
Expand Down
30 changes: 16 additions & 14 deletions ...sis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/abstractor/StopCriterion.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,19 +27,21 @@
* Interface for stopping criterions during abstraction.
*/
public interface StopCriterion<S extends State, A extends Action> {
/**
* Check if abstraction can stop based on the whole ARG.
* @param arg ARG
* @return True if abstraction can stop
*/
boolean canStop(ARG<S, A> arg, Prec prec);
/**
* Check if abstraction can stop based on the whole ARG.
*
* @param arg ARG
* @return True if abstraction can stop
*/
boolean canStop(ARG<S, A> arg, Prec prec);

/**
* Check if abstraction can stop based on the whole ARG or based on
* the new successor nodes (optimization: the whole ARG might not be needed).
* @param arg ARG
* @param newNodes New successor nodes
* @return True if abstraction can stop
*/
boolean canStop(ARG<S, A> arg, Collection<ArgNode<S, A>> newNodes, Prec prec);
/**
* Check if abstraction can stop based on the whole ARG or based on
* the new successor nodes (optimization: the whole ARG might not be needed).
*
* @param arg ARG
* @param newNodes New successor nodes
* @return True if abstraction can stop
*/
boolean canStop(ARG<S, A> arg, Collection<ArgNode<S, A>> newNodes, Prec prec);
}
78 changes: 39 additions & 39 deletions ...is/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/abstractor/StopCriterions.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,12 +51,12 @@ public static <S extends State, A extends Action> StopCriterion<S, A> firstCexWi
return new FirstCexWithMitigation<>();
}

/**
* @return Criterion that explores the whole state space
*/
public static <S extends State, A extends Action> StopCriterion<S, A> fullExploration() {
return new FullExploration<>();
}
/**
* @return Criterion that explores the whole state space
*/
public static <S extends State, A extends Action> StopCriterion<S, A> fullExploration() {
return new FullExploration<>();
}

/**
* @param n Number of counterexamples to collect
Expand All @@ -70,17 +70,17 @@ private static final class FirstCexWithMitigation<S extends State, A extends Act
@Override
public boolean canStop(final ARG<S, A> arg, Prec prec) {
boolean present = arg.getNewCexs(prec).findAny().isPresent();
if(!present) MonitorCheckpoint.Checkpoints.execute("StopCriterion.noNewCexFound");
if (!present) MonitorCheckpoint.Checkpoints.execute("StopCriterion.noNewCexFound");
return present;
// return arg.getUnsafeNodes().findAny().isPresent();
}

@Override
public boolean canStop(ARG<S, A> arg, Collection<ArgNode<S, A>> newNodes, Prec prec) {
Optional<ArgNode<S, A>> any = newNodes.stream()
.filter(n -> n.isTarget() && !n.isExcluded()).findFirst();
if(any.isPresent()) {
if(!arg.getNewCexs(prec).toList().contains(ArgTrace.to(any.get()))) {
.filter(n -> n.isTarget() && !n.isExcluded()).findFirst();
if (any.isPresent()) {
if (!arg.getNewCexs(prec).toList().contains(ArgTrace.to(any.get()))) {
// cex is not new, remove covers
MonitorCheckpoint.Checkpoints.execute("StopCriterion.noNewCexFound");
return false;
Expand All @@ -94,22 +94,22 @@ public boolean canStop(ARG<S, A> arg, Collection<ArgNode<S, A>> newNodes, Prec p
@Override
public String toString() {
return Utils.lispStringBuilder(StopCriterion.class.getSimpleName()).add(getClass().getSimpleName())
.toString();
.toString();
}
}

private static final class FirstCex<S extends State, A extends Action> implements StopCriterion<S, A> {
@Override
public boolean canStop(final ARG<S, A> arg, Prec prec) {
return arg.getCexs().findAny().isPresent();
@Override
public boolean canStop(final ARG<S, A> arg, Prec prec) {
return arg.getCexs().findAny().isPresent();
// return arg.getUnsafeNodes().findAny().isPresent();
}
}

@Override
public boolean canStop(ARG<S, A> arg, Collection<ArgNode<S, A>> newNodes, Prec prec) {
@Override
public boolean canStop(ARG<S, A> arg, Collection<ArgNode<S, A>> newNodes, Prec prec) {
return (newNodes.stream().anyMatch(n -> n.isTarget() && !n.isExcluded())) &&
arg.getCexs().findAny().isPresent();
}
arg.getCexs().findAny().isPresent();
}

@Override
public String toString() {
Expand All @@ -118,16 +118,16 @@ public String toString() {
}
}

private static final class FullExploration<S extends State, A extends Action, P extends Prec> implements StopCriterion<S, A> {
@Override
public boolean canStop(final ARG<S, A> arg, final Prec prec) {
return false;
}
private static final class FullExploration<S extends State, A extends Action, P extends Prec> implements StopCriterion<S, A> {
@Override
public boolean canStop(final ARG<S, A> arg, final Prec prec) {
return false;
}

@Override
public boolean canStop(ARG<S, A> arg, Collection<ArgNode<S, A>> newNodes, final Prec prec) {
return false;
}
@Override
public boolean canStop(ARG<S, A> arg, Collection<ArgNode<S, A>> newNodes, final Prec prec) {
return false;
}

@Override
public String toString() {
Expand All @@ -144,17 +144,17 @@ private AtLeastNCexs(final int n) {
this.n = n;
}

@Override
public boolean canStop(final ARG<S, A> arg, final Prec prec) {
// TODO: this could be optimized: we don't need to count it,
// we just need to know if there are >= n elements
return arg.getUnsafeNodes().count() >= n;
}

@Override
public boolean canStop(ARG<S, A> arg, Collection<ArgNode<S, A>> newNodes, final Prec prec) {
return canStop(arg, prec);
}
@Override
public boolean canStop(final ARG<S, A> arg, final Prec prec) {
// TODO: this could be optimized: we don't need to count it,
// we just need to know if there are >= n elements
return arg.getUnsafeNodes().count() >= n;
}

@Override
public boolean canStop(ARG<S, A> arg, Collection<ArgNode<S, A>> newNodes, final Prec prec) {
return canStop(arg, prec);
}

@Override
public String toString() {
Expand Down
Loading

0 comments on commit c03432c

Please sign in to comment.