From df1fc2fe7306d28c092427f6c13f9bd646b1f460 Mon Sep 17 00:00:00 2001 From: RipplB Date: Wed, 16 Oct 2024 22:31:29 +0200 Subject: [PATCH] Further generalize refiners Refiners and all their links don't need state and action generics specified anymore --- .../algorithm/cegar/ArgCegarChecker.java | 4 +-- .../analysis/algorithm/cegar/ArgRefiner.java | 2 +- .../algorithm/cegar/CegarChecker.java | 18 ++++++------ .../analysis/algorithm/cegar/Refiner.java | 6 ++-- .../algorithm/cegar/RefinerResult.java | 28 +++++++++---------- .../expr/refinement/AasporRefiner.java | 4 +-- .../refinement/MultiExprTraceRefiner.java | 2 +- .../refinement/SingleExprTraceRefiner.java | 2 +- .../analysis/XcfaSingeExprTraceRefiner.kt | 4 +-- 9 files changed, 32 insertions(+), 38 deletions(-) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgCegarChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgCegarChecker.java index 06260c732c..3492ab9091 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgCegarChecker.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgCegarChecker.java @@ -35,12 +35,12 @@ public final class ArgCegarChecker { private ArgCegarChecker() { } - public static CegarChecker, Trace> create( + public static CegarChecker, Trace> create( final ArgAbstractor abstractor, final ArgRefiner refiner) { return create(abstractor, refiner, NullLogger.getInstance()); } - public static CegarChecker, Trace> create( + public static CegarChecker, Trace> create( final ArgAbstractor abstractor, final ArgRefiner refiner, final Logger logger) { return CegarChecker.create(abstractor, refiner, logger, ArgVisualizer.getDefault()); } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgRefiner.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgRefiner.java index 2683a2fd0f..36ef2d3520 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgRefiner.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgRefiner.java @@ -25,5 +25,5 @@ * Common interface for refiners. It takes an ARG and a precision, checks if the counterexample in * the ARG is feasible and if not, it refines the precision and may also prune the ARG. */ -public interface ArgRefiner extends Refiner, Trace> { +public interface ArgRefiner extends Refiner, Trace> { } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java index 30da9a28e5..c84619981e 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java @@ -16,10 +16,8 @@ package hu.bme.mit.theta.analysis.algorithm.cegar; import com.google.common.base.Stopwatch; -import hu.bme.mit.theta.analysis.Action; import hu.bme.mit.theta.analysis.Cex; import hu.bme.mit.theta.analysis.Prec; -import hu.bme.mit.theta.analysis.State; import hu.bme.mit.theta.analysis.algorithm.Proof; import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; import hu.bme.mit.theta.analysis.algorithm.SafetyResult; @@ -42,15 +40,15 @@ * check counterexamples and refine them if needed. It also provides certain * statistics about its execution. */ -public final class CegarChecker implements SafetyChecker { +public final class CegarChecker

implements SafetyChecker { private final Abstractor abstractor; - private final Refiner refiner; + private final Refiner refiner; private final Logger logger; private final Pr proof; private final ProofVisualizer proofVisualizer; - private CegarChecker(final Abstractor abstractor, final Refiner refiner, final Logger logger, final ProofVisualizer proofVisualizer) { + private CegarChecker(final Abstractor abstractor, final Refiner refiner, final Logger logger, final ProofVisualizer proofVisualizer) { this.abstractor = checkNotNull(abstractor); this.refiner = checkNotNull(refiner); this.logger = checkNotNull(logger); @@ -58,13 +56,13 @@ private CegarChecker(final Abstractor abstractor, final Refiner CegarChecker create( - final Abstractor abstractor, final Refiner refiner, final ProofVisualizer proofVisualizer) { + public static

CegarChecker create( + final Abstractor abstractor, final Refiner refiner, final ProofVisualizer proofVisualizer) { return create(abstractor, refiner, NullLogger.getInstance(), proofVisualizer); } - public static CegarChecker create( - final Abstractor abstractor, final Refiner refiner, final Logger logger, final ProofVisualizer proofVisualizer) { + public static

CegarChecker create( + final Abstractor abstractor, final Refiner refiner, final Logger logger, final ProofVisualizer proofVisualizer) { return new CegarChecker<>(abstractor, refiner, logger, proofVisualizer); } @@ -78,7 +76,7 @@ public SafetyResult check(final P initPrec) { final Stopwatch stopwatch = Stopwatch.createStarted(); long abstractorTime = 0; long refinerTime = 0; - RefinerResult refinerResult = null; + RefinerResult refinerResult = null; AbstractorResult abstractorResult; P prec = initPrec; int iteration = 0; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Refiner.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Refiner.java index abd645f3cf..f59c368766 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Refiner.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Refiner.java @@ -15,20 +15,18 @@ */ package hu.bme.mit.theta.analysis.algorithm.cegar; -import hu.bme.mit.theta.analysis.Action; import hu.bme.mit.theta.analysis.Cex; import hu.bme.mit.theta.analysis.Prec; -import hu.bme.mit.theta.analysis.State; import hu.bme.mit.theta.analysis.algorithm.Proof; /** * Common interface for refiners. It takes a witness and a precision, checks if the counterexample in * the witness is feasible and if not, it refines the precision */ -public interface Refiner { +public interface Refiner

{ /** * Checks if the counterexample in the witness is feasible. If not, refines the precision */ - RefinerResult refine(Pr witness, P prec); + RefinerResult refine(Pr witness, P prec); } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/RefinerResult.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/RefinerResult.java index a4be30781e..544b3185a1 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/RefinerResult.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/RefinerResult.java @@ -15,10 +15,8 @@ */ package hu.bme.mit.theta.analysis.algorithm.cegar; -import hu.bme.mit.theta.analysis.Action; import hu.bme.mit.theta.analysis.Cex; import hu.bme.mit.theta.analysis.Prec; -import hu.bme.mit.theta.analysis.State; import hu.bme.mit.theta.common.Utils; import static com.google.common.base.Preconditions.checkNotNull; @@ -27,7 +25,7 @@ * Represents the result of the Refiner class that can be either spurious or unsafe. In the former * case it also contains the refined precision and in the latter case the feasible counterexample. */ -public abstract class RefinerResult { +public abstract class RefinerResult

{ protected RefinerResult() { } @@ -37,7 +35,7 @@ protected RefinerResult() { * * @param refinedPrec Refined precision */ - public static Spurious spurious( + public static

Spurious spurious( final P refinedPrec) { return new Spurious<>(refinedPrec); } @@ -47,7 +45,7 @@ public static * * @param cex Feasible counterexample */ - public static Unsafe unsafe( + public static

Unsafe unsafe( final C cex) { return new Unsafe<>(cex); } @@ -56,15 +54,15 @@ public static public abstract boolean isUnsafe(); - public abstract Spurious asSpurious(); + public abstract Spurious asSpurious(); - public abstract Unsafe asUnsafe(); + public abstract Unsafe asUnsafe(); /** * Represents the spurious result with a refined precision. */ - public static final class Spurious - extends RefinerResult { + public static final class Spurious

+ extends RefinerResult { private final P refinedPrec; @@ -87,12 +85,12 @@ public boolean isUnsafe() { } @Override - public Spurious asSpurious() { + public Spurious asSpurious() { return this; } @Override - public Unsafe asUnsafe() { + public Unsafe asUnsafe() { throw new ClassCastException( "Cannot cast " + Spurious.class.getSimpleName() + " to " + Unsafe.class.getSimpleName()); @@ -109,8 +107,8 @@ public String toString() { /** * Represents the unsafe result with a feasible counterexample. */ - public static final class Unsafe extends - RefinerResult { + public static final class Unsafe

extends + RefinerResult { private final C cex; @@ -133,14 +131,14 @@ public boolean isUnsafe() { } @Override - public Spurious asSpurious() { + public Spurious asSpurious() { throw new ClassCastException( "Cannot cast " + Unsafe.class.getSimpleName() + " to " + Spurious.class.getSimpleName()); } @Override - public Unsafe asUnsafe() { + public Unsafe asUnsafe() { return this; } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/AasporRefiner.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/AasporRefiner.java index f1f7430241..b5b1c7e8b3 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/AasporRefiner.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/AasporRefiner.java @@ -53,8 +53,8 @@ public static Aaspor } @Override - public RefinerResult> refine(final ARG arg, final P prec) { - final RefinerResult> result = refiner.refine(arg, prec); + public RefinerResult> refine(final ARG arg, final P prec) { + final RefinerResult> result = refiner.refine(arg, prec); if (result.isUnsafe() || pruneStrategy != PruneStrategy.LAZY) return result; final P newPrec = result.asSpurious().getRefinedPrec(); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/MultiExprTraceRefiner.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/MultiExprTraceRefiner.java index b2cee796d0..6f9118b70b 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/MultiExprTraceRefiner.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/MultiExprTraceRefiner.java @@ -76,7 +76,7 @@ public static > refine(final ARG arg, final P prec) { + public RefinerResult> refine(final ARG arg, final P prec) { checkNotNull(arg); checkNotNull(prec); assert !arg.isSafe() : "ARG must be unsafe"; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java index 126f4212f4..27dd153e59 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java @@ -78,7 +78,7 @@ public static > refine(final ARG arg, final P prec) { + public RefinerResult> refine(final ARG arg, final P prec) { checkNotNull(arg); checkNotNull(prec); assert !arg.isSafe() : "ARG must be unsafe"; diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt index 93410e0641..e1301810d3 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt @@ -64,7 +64,7 @@ class XcfaSingleExprTraceRefiner, prec: P?): RefinerResult> { + fun refineTemp(arg: ARG, prec: P?): RefinerResult> { Preconditions.checkNotNull(arg) Preconditions.checkNotNull(prec) assert(!arg.isSafe) { "ARG must be unsafe" } @@ -118,7 +118,7 @@ class XcfaSingleExprTraceRefiner, prec: P?): RefinerResult> { + override fun refine(arg: ARG, prec: P?): RefinerResult> { Preconditions.checkNotNull(arg) Preconditions.checkNotNull

(prec) assert(!arg.isSafe) { "ARG must be unsafe" }