Further generalize refiners

Refiners and all their links don't need state and action generics specified anymore
ftsrg · Oct 16, 2024 · df1fc2f · df1fc2f
1 parent a62fe2b
commit df1fc2f
Show file tree

Hide file tree

Showing 9 changed files with 32 additions and 38 deletions.
diff --git a/...mon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgCegarChecker.java b/...mon/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 <S extends State, A extends Action, P extends Prec> CegarChecker<S, A, P, ARG<S, A>, Trace<S, A>> create(
+    public static <S extends State, A extends Action, P extends Prec> CegarChecker<P, ARG<S, A>, Trace<S, A>> create(
             final ArgAbstractor<S, A, P> abstractor, final ArgRefiner<S, A, P> refiner) {
         return create(abstractor, refiner, NullLogger.getInstance());
     }
 
-    public static <S extends State, A extends Action, P extends Prec> CegarChecker<S, A, P, ARG<S, A>, Trace<S, A>> create(
+    public static <S extends State, A extends Action, P extends Prec> CegarChecker<P, ARG<S, A>, Trace<S, A>> create(
             final ArgAbstractor<S, A, P> abstractor, final ArgRefiner<S, A, P> refiner, final Logger logger) {
         return CegarChecker.create(abstractor, refiner, logger, ArgVisualizer.getDefault());
     }

diff --git a/...s/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgRefiner.java b/...s/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<S extends State, A extends Action, P extends Prec> extends Refiner<S, A, P, ARG<S, A>, Trace<S, A>> {
+public interface ArgRefiner<S extends State, A extends Action, P extends Prec> extends Refiner<P, ARG<S, A>, Trace<S, A>> {
 }
diff --git a/...common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java b/...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,29 +40,29 @@
  * check counterexamples and refine them if needed. It also provides certain
  * statistics about its execution.
  */
-public final class CegarChecker<S extends State, A extends Action, P extends Prec, Pr extends Proof, C extends Cex> implements SafetyChecker<Pr, C, P> {
+public final class CegarChecker<P extends Prec, Pr extends Proof, C extends Cex> implements SafetyChecker<Pr, C, P> {
 
     private final Abstractor<P, Pr> abstractor;
-    private final Refiner<S, A, P, Pr, C> refiner;
+    private final Refiner<P, Pr, C> refiner;
     private final Logger logger;
     private final Pr proof;
     private final ProofVisualizer<? super Pr> proofVisualizer;
 
-    private CegarChecker(final Abstractor<P, Pr> abstractor, final Refiner<S, A, P, Pr, C> refiner, final Logger logger, final ProofVisualizer<? super Pr> proofVisualizer) {
+    private CegarChecker(final Abstractor<P, Pr> abstractor, final Refiner<P, Pr, C> refiner, final Logger logger, final ProofVisualizer<? super Pr> proofVisualizer) {
         this.abstractor = checkNotNull(abstractor);
         this.refiner = checkNotNull(refiner);
         this.logger = checkNotNull(logger);
         proof = abstractor.createProof();
         this.proofVisualizer = checkNotNull(proofVisualizer);
     }
 
-    public static <S extends State, A extends Action, P extends Prec, Pr extends Proof, C extends Cex> CegarChecker<S, A, P, Pr, C> create(
-            final Abstractor<P, Pr> abstractor, final Refiner<S, A, P, Pr, C> refiner, final ProofVisualizer<Pr> proofVisualizer) {
+    public static <P extends Prec, Pr extends Proof, C extends Cex> CegarChecker<P, Pr, C> create(
+            final Abstractor<P, Pr> abstractor, final Refiner<P, Pr, C> refiner, final ProofVisualizer<Pr> proofVisualizer) {
         return create(abstractor, refiner, NullLogger.getInstance(), proofVisualizer);
     }
 
-    public static <S extends State, A extends Action, P extends Prec, Pr extends Proof, C extends Cex> CegarChecker<S, A, P, Pr, C> create(
-            final Abstractor<P, Pr> abstractor, final Refiner<S, A, P, Pr, C> refiner, final Logger logger, final ProofVisualizer<? super Pr> proofVisualizer) {
+    public static <P extends Prec, Pr extends Proof, C extends Cex> CegarChecker<P, Pr, C> create(
+            final Abstractor<P, Pr> abstractor, final Refiner<P, Pr, C> refiner, final Logger logger, final ProofVisualizer<? super Pr> proofVisualizer) {
         return new CegarChecker<>(abstractor, refiner, logger, proofVisualizer);
     }
 
@@ -78,7 +76,7 @@ public SafetyResult<Pr, C> check(final P initPrec) {
         final Stopwatch stopwatch = Stopwatch.createStarted();
         long abstractorTime = 0;
         long refinerTime = 0;
-        RefinerResult<S, A, P, C> refinerResult = null;
+        RefinerResult<P, C> refinerResult = null;
         AbstractorResult abstractorResult;
         P prec = initPrec;
         int iteration = 0;

diff --git a/...ects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Refiner.java b/...ects/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<S extends State, A extends Action, P extends Prec, Pr extends Proof, C extends Cex> {
+public interface Refiner<P extends Prec, Pr extends Proof, C extends Cex> {
 
     /**
      * Checks if the counterexample in the witness is feasible. If not, refines the precision
      */
-    RefinerResult<S, A, P, C> refine(Pr witness, P prec);
+    RefinerResult<P, C> refine(Pr witness, P prec);
 }
diff --git a/...ommon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/RefinerResult.java b/...ommon/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<S extends State, A extends Action, P extends Prec, C extends Cex> {
+public abstract class RefinerResult<P extends Prec, C extends Cex> {
 
     protected RefinerResult() {
     }
@@ -37,7 +35,7 @@ protected RefinerResult() {
      *
      * @param refinedPrec Refined precision
      */
-    public static <S extends State, A extends Action, P extends Prec, C extends Cex> Spurious<S, A, P, C> spurious(
+    public static <P extends Prec, C extends Cex> Spurious<P, C> spurious(
             final P refinedPrec) {
         return new Spurious<>(refinedPrec);
     }
@@ -47,7 +45,7 @@ public static <S extends State, A extends Action, P extends Prec, C extends Cex>
      *
      * @param cex Feasible counterexample
      */
-    public static <S extends State, A extends Action, P extends Prec, C extends Cex> Unsafe<S, A, P, C> unsafe(
+    public static <P extends Prec, C extends Cex> Unsafe<P, C> unsafe(
             final C cex) {
         return new Unsafe<>(cex);
     }
@@ -56,15 +54,15 @@ public static <S extends State, A extends Action, P extends Prec, C extends Cex>
 
     public abstract boolean isUnsafe();
 
-    public abstract Spurious<S, A, P, C> asSpurious();
+    public abstract Spurious<P, C> asSpurious();
 
-    public abstract Unsafe<S, A, P, C> asUnsafe();
+    public abstract Unsafe<P, C> asUnsafe();
 
     /**
      * Represents the spurious result with a refined precision.
      */
-    public static final class Spurious<S extends State, A extends Action, P extends Prec, C extends Cex>
-            extends RefinerResult<S, A, P, C> {
+    public static final class Spurious<P extends Prec, C extends Cex>
+            extends RefinerResult<P, C> {
 
         private final P refinedPrec;
 
@@ -87,12 +85,12 @@ public boolean isUnsafe() {
         }
 
         @Override
-        public Spurious<S, A, P, C> asSpurious() {
+        public Spurious<P, C> asSpurious() {
             return this;
         }
 
         @Override
-        public Unsafe<S, A, P, C> asUnsafe() {
+        public Unsafe<P, C> 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<S extends State, A extends Action, P extends Prec, C extends Cex> extends
-            RefinerResult<S, A, P, C> {
+    public static final class Unsafe<P extends Prec, C extends Cex> extends
+            RefinerResult<P, C> {
 
         private final C cex;
 
@@ -133,14 +131,14 @@ public boolean isUnsafe() {
         }
 
         @Override
-        public Spurious<S, A, P, C> asSpurious() {
+        public Spurious<P, C> asSpurious() {
             throw new ClassCastException(
                     "Cannot cast " + Unsafe.class.getSimpleName() + " to "
                             + Spurious.class.getSimpleName());
         }
 
         @Override
-        public Unsafe<S, A, P, C> asUnsafe() {
+        public Unsafe<P, C> asUnsafe() {
             return this;
         }
 

diff --git a/...ommon/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/AasporRefiner.java b/...ommon/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/AasporRefiner.java
@@ -53,8 +53,8 @@ public static <S extends ExprState, A extends ExprAction, P extends Prec> Aaspor
     }
 
     @Override
-    public RefinerResult<S, A, P, Trace<S, A>> refine(final ARG<S, A> arg, final P prec) {
-        final RefinerResult<S, A, P, Trace<S, A>> result = refiner.refine(arg, prec);
+    public RefinerResult<P, Trace<S, A>> refine(final ARG<S, A> arg, final P prec) {
+        final RefinerResult<P, Trace<S, A>> result = refiner.refine(arg, prec);
         if (result.isUnsafe() || pruneStrategy != PruneStrategy.LAZY) return result;
 
         final P newPrec = result.asSpurious().getRefinedPrec();

diff --git a/...alysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/MultiExprTraceRefiner.java b/...alysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/MultiExprTraceRefiner.java
@@ -76,7 +76,7 @@ public static <S extends ExprState, A extends ExprAction, P extends Prec, R exte
     }
 
     @Override
-    public RefinerResult<S, A, P, Trace<S, A>> refine(final ARG<S, A> arg, final P prec) {
+    public RefinerResult<P, Trace<S, A>> refine(final ARG<S, A> arg, final P prec) {
         checkNotNull(arg);
         checkNotNull(prec);
         assert !arg.isSafe() : "ARG must be unsafe";

diff --git a/...lysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java b/...lysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java
@@ -78,7 +78,7 @@ public static <S extends ExprState, A extends ExprAction, P extends Prec, R exte
     }
 
     @Override
-    public RefinerResult<S, A, P, Trace<S, A>> refine(final ARG<S, A> arg, final P prec) {
+    public RefinerResult<P, Trace<S, A>> refine(final ARG<S, A> arg, final P prec) {
         checkNotNull(arg);
         checkNotNull(prec);
         assert !arg.isSafe() : "ARG must be unsafe";

diff --git a/...a/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt b/...a/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt
@@ -64,7 +64,7 @@ class XcfaSingleExprTraceRefiner<S : ExprState, A : ExprAction, P : Prec, R : Re
         return null
     }
 
-    fun refineTemp(arg: ARG<S, A>, prec: P?): RefinerResult<S, A, P?, Trace<S, A>> {
+    fun refineTemp(arg: ARG<S, A>, prec: P?): RefinerResult<P?, Trace<S, A>> {
         Preconditions.checkNotNull(arg)
         Preconditions.checkNotNull(prec)
         assert(!arg.isSafe) { "ARG must be unsafe" }
@@ -118,7 +118,7 @@ class XcfaSingleExprTraceRefiner<S : ExprState, A : ExprAction, P : Prec, R : Re
         }
     }
 
-    override fun refine(arg: ARG<S, A>, prec: P?): RefinerResult<S, A, P?, Trace<S, A>> {
+    override fun refine(arg: ARG<S, A>, prec: P?): RefinerResult<P?, Trace<S, A>> {
         Preconditions.checkNotNull(arg)
         Preconditions.checkNotNull<P>(prec)
         assert(!arg.isSafe) { "ARG must be unsafe" }