Further generalize refiners

Refiners and all their links don't need state and action generics specified anymore

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

@@ -25,24 +25,25 @@
 import hu.bme.mit.theta.common.logging.NullLogger;
 
 /**
- * Counterexample-Guided Abstraction Refinement (CEGAR) loop implementation,
- * that uses an Abstractor to explore the abstract state space and a Refiner to
- * check counterexamples and refine them if needed. It also provides certain
- * statistics about its execution.
+ * Counterexample-Guided Abstraction Refinement (CEGAR) loop implementation, that uses an Abstractor
+ * to explore the abstract state space and a Refiner to check counterexamples and refine them if
+ * needed. It also provides certain statistics about its execution.
  */
 public final class ArgCegarChecker {
 
-    private 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(
-            final ArgAbstractor<S, A, P> abstractor, final ArgRefiner<S, A, P> refiner) {
+    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(
-            final ArgAbstractor<S, A, P> abstractor, final ArgRefiner<S, A, P> refiner, final Logger logger) {
+    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());
     }
-
 }

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<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>> {}

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

@@ -15,11 +15,11 @@
  */
 package hu.bme.mit.theta.analysis.algorithm.cegar;
 
+import static com.google.common.base.Preconditions.checkNotNull;
+
 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;
@@ -31,40 +31,46 @@
 import hu.bme.mit.theta.common.logging.NullLogger;
 import hu.bme.mit.theta.common.visualization.writer.JSONWriter;
 import hu.bme.mit.theta.common.visualization.writer.WebDebuggerLogger;
-
 import java.util.concurrent.TimeUnit;
 
-import static com.google.common.base.Preconditions.checkNotNull;
-
 /**
- * Counterexample-Guided Abstraction Refinement (CEGAR) loop implementation,
- * that uses an Abstractor to explore the abstract state space and a Refiner to
- * check counterexamples and refine them if needed. It also provides certain
- * statistics about its execution.
+ * Counterexample-Guided Abstraction Refinement (CEGAR) loop implementation, that uses an Abstractor
+ * to explore the abstract state space and a Refiner to 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 +84,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;
@@ -91,10 +97,12 @@ public SafetyResult<Pr, C> check(final P initPrec) {
             final long abstractorStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS);
             abstractorResult = abstractor.check(proof, prec);
             abstractorTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - abstractorStartTime;
-            logger.write(Level.MAINSTEP, "| Checking abstraction done, result: %s%n", abstractorResult);
+            logger.write(
+                    Level.MAINSTEP, "| Checking abstraction done, result: %s%n", abstractorResult);
 
             if (WebDebuggerLogger.enabled()) {
-                String argGraph = JSONWriter.getInstance().writeString(proofVisualizer.visualize(proof));
+                String argGraph =
+                        JSONWriter.getInstance().writeString(proofVisualizer.visualize(proof));
                 String precString = prec.toString();
                 wdl.addIteration(iteration, argGraph, precString);
             }
@@ -107,26 +115,35 @@ public SafetyResult<Pr, C> check(final P initPrec) {
                 final long refinerStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS);
                 refinerResult = refiner.refine(proof, prec);
                 refinerTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - refinerStartTime;
-                logger.write(Level.MAINSTEP, "Refining abstraction done, result: %s%n", refinerResult);
+                logger.write(
+                        Level.MAINSTEP, "Refining abstraction done, result: %s%n", refinerResult);
 
                 if (refinerResult.isSpurious()) {
                     prec = refinerResult.asSpurious().getRefinedPrec();
                 }
 
                 if (lastPrec.equals(prec)) {
-                    logger.write(Level.MAINSTEP, "! Precision did NOT change in this iteration" + System.lineSeparator());
+                    logger.write(
+                            Level.MAINSTEP,
+                            "! Precision did NOT change in this iteration"
+                                    + System.lineSeparator());
                 } else {
-                    logger.write(Level.MAINSTEP, "! Precision DID change in this iteration" + System.lineSeparator());
+                    logger.write(
+                            Level.MAINSTEP,
+                            "! Precision DID change in this iteration" + System.lineSeparator());
                 }
-
             }
 
         } while (!abstractorResult.isSafe() && !refinerResult.isUnsafe());
 
         stopwatch.stop();
         SafetyResult<Pr, C> cegarResult = null;
-        final CegarStatistics stats = new CegarStatistics(stopwatch.elapsed(TimeUnit.MILLISECONDS), abstractorTime,
-                refinerTime, iteration);
+        final CegarStatistics stats =
+                new CegarStatistics(
+                        stopwatch.elapsed(TimeUnit.MILLISECONDS),
+                        abstractorTime,
+                        refinerTime,
+                        iteration);
 
         assert abstractorResult.isSafe() || refinerResult.isUnsafe();
 
@@ -144,6 +161,9 @@ public SafetyResult<Pr, C> check(final P initPrec) {
 
     @Override
     public String toString() {
-        return Utils.lispStringBuilder(getClass().getSimpleName()).add(abstractor).add(refiner).toString();
+        return Utils.lispStringBuilder(getClass().getSimpleName())
+                .add(abstractor)
+                .add(refiner)
+                .toString();
     }
 }

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

@@ -15,20 +15,16 @@
  */
 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
+ * 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);
+    /** Checks if the counterexample in the witness is feasible. If not, refines the precision */
+    RefinerResult<P, C> refine(Pr witness, P prec);
 }

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

@@ -15,30 +15,26 @@
  */
 package hu.bme.mit.theta.analysis.algorithm.cegar;
 
-import hu.bme.mit.theta.analysis.Action;
+import static com.google.common.base.Preconditions.checkNotNull;
+
 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;
-
 /**
  * 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() {
-    }
+    protected RefinerResult() {}
 
     /**
      * Create a new spurious result.
      *
      * @param refinedPrec Refined precision
      */
-    public static <S extends State, A extends Action, P extends Prec, C extends Cex> Spurious<S, A, P, C> spurious(
-            final P refinedPrec) {
+    public static <P extends Prec, C extends Cex> Spurious<P, C> spurious(final P refinedPrec) {
         return new Spurious<>(refinedPrec);
     }
 
@@ -47,24 +43,20 @@ 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(
-            final C cex) {
+    public static <P extends Prec, C extends Cex> Unsafe<P, C> unsafe(final C cex) {
         return new Unsafe<>(cex);
     }
 
     public abstract boolean isSpurious();
 
     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> {
+    /** Represents the spurious result with a refined precision. */
+    public static final class Spurious<P extends Prec, C extends Cex> extends RefinerResult<P, C> {
 
         private final P refinedPrec;
 
@@ -87,14 +79,16 @@ 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 "
+                    "Cannot cast "
+                            + Spurious.class.getSimpleName()
+                            + " to "
                             + Unsafe.class.getSimpleName());
         }
 
@@ -106,11 +100,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> {
+    /** Represents the unsafe result with a feasible counterexample. */
+    public static final class Unsafe<P extends Prec, C extends Cex> extends RefinerResult<P, C> {
 
         private final C cex;
 
@@ -133,14 +124,16 @@ 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 "
+                    "Cannot cast "
+                            + Unsafe.class.getSimpleName()
+                            + " to "
                             + Spurious.class.getSimpleName());
         }
 
         @Override
-        public Unsafe<S, A, P, C> asUnsafe() {
+        public Unsafe<P, C> asUnsafe() {
             return this;
         }