Rename Witness to Proof

ftsrg · Oct 12, 2024 · 291e948 · 291e948
1 parent 6b0cbfb
commit 291e948
Show file tree

Hide file tree

Showing 43 changed files with 277 additions and 356 deletions.
diff --git a/...analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java b/...analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java
@@ -15,32 +15,31 @@
  */
 package hu.bme.mit.theta.cfa.analysis.impact;
 
-import static org.junit.Assert.assertTrue;
-
-import java.io.FileInputStream;
-import java.io.FileNotFoundException;
-import java.io.IOException;
-
 import hu.bme.mit.theta.analysis.Trace;
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
-import hu.bme.mit.theta.analysis.pred.PredState;
-import hu.bme.mit.theta.cfa.analysis.CfaAction;
-import hu.bme.mit.theta.cfa.analysis.CfaState;
-import hu.bme.mit.theta.solver.Solver;
-import org.junit.Test;
-
 import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgChecker;
 import hu.bme.mit.theta.analysis.expr.ExprAction;
 import hu.bme.mit.theta.analysis.expr.ExprState;
+import hu.bme.mit.theta.analysis.pred.PredState;
 import hu.bme.mit.theta.analysis.unit.UnitPrec;
 import hu.bme.mit.theta.analysis.utils.ArgVisualizer;
 import hu.bme.mit.theta.cfa.CFA;
+import hu.bme.mit.theta.cfa.analysis.CfaAction;
+import hu.bme.mit.theta.cfa.analysis.CfaState;
 import hu.bme.mit.theta.cfa.analysis.lts.CfaLbeLts;
 import hu.bme.mit.theta.cfa.dsl.CfaDslManager;
 import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter;
 import hu.bme.mit.theta.solver.ItpSolver;
+import hu.bme.mit.theta.solver.Solver;
 import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory;
+import org.junit.Test;
+
+import java.io.FileInputStream;
+import java.io.FileNotFoundException;
+import java.io.IOException;
+
+import static org.junit.Assert.assertTrue;
 
 public final class CfaPredImpactCheckerTest {
 
@@ -64,7 +63,7 @@ public void test() throws FileNotFoundException, IOException {
         // Assert
         assertTrue(status.isSafe());
 
-        final ARG<? extends ExprState, ? extends ExprAction> arg = status.getWitness();
+        final ARG<? extends ExprState, ? extends ExprAction> arg = status.getProof();
         arg.minimize();
 
         final ArgChecker argChecker = ArgChecker.create(abstractionSolver);

diff --git a/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java b/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java
@@ -27,8 +27,6 @@
 import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr;
 import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics;
 import hu.bme.mit.theta.analysis.expl.ExplState;
-import hu.bme.mit.theta.analysis.expr.ExprAction;
-import hu.bme.mit.theta.analysis.expr.ExprState;
 import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy;
 import hu.bme.mit.theta.cfa.CFA;
 import hu.bme.mit.theta.cfa.analysis.CfaAction;
@@ -37,14 +35,7 @@
 import hu.bme.mit.theta.cfa.analysis.CfaTraceConcretizer;
 import hu.bme.mit.theta.cfa.analysis.config.CfaConfig;
 import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder;
-import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Algorithm;
-import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Domain;
-import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Encoding;
-import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.InitPrec;
-import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.PrecGranularity;
-import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.PredSplit;
-import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Refinement;
-import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Search;
+import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.*;
 import hu.bme.mit.theta.cfa.analysis.utils.CfaVisualizer;
 import hu.bme.mit.theta.cfa.dsl.CfaDslManager;
 import hu.bme.mit.theta.common.CliUtils;
@@ -63,12 +54,7 @@
 import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory;
 import hu.bme.mit.theta.solver.z3legacy.Z3SolverManager;
 
-import java.io.File;
-import java.io.FileInputStream;
-import java.io.FileNotFoundException;
-import java.io.InputStream;
-import java.io.PrintWriter;
-import java.io.StringWriter;
+import java.io.*;
 import java.nio.file.Path;
 import java.util.concurrent.TimeUnit;
 import java.util.stream.Stream;
@@ -345,7 +331,7 @@ private void printResult(final SafetyResult<?, ? extends Trace<?, ?>> status, fi
             writer.cell(stats.getAbstractorTimeMs());
             writer.cell(stats.getRefinerTimeMs());
             writer.cell(stats.getIterations());
-            if (status.getWitness() instanceof ARG<?, ?> arg) {
+            if (status.getProof() instanceof ARG<?, ?> arg) {
                 writer.cell(arg.size());
                 writer.cell(arg.getDepth());
                 writer.cell(arg.getMeanBranchingFactor());

diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Checker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Checker.java
@@ -15,8 +15,8 @@
  */
 package hu.bme.mit.theta.analysis.algorithm;
 
-public interface Checker<W extends Witness, I> {
+public interface Checker<Pr extends Proof, I> {
 
-    Result<W> check(I input);
+    Result<Pr> check(I input);
 
 }
diff --git a/...heta/analysis/algorithm/EmptyWitness.java → .../theta/analysis/algorithm/EmptyProof.java b/...heta/analysis/algorithm/EmptyWitness.java → .../theta/analysis/algorithm/EmptyProof.java
@@ -15,14 +15,14 @@
  */
 package hu.bme.mit.theta.analysis.algorithm;
 
-public class EmptyWitness implements Witness {
+public class EmptyProof implements Proof {
 
-    private final static EmptyWitness empty = new EmptyWitness();
+    private final static EmptyProof empty = new EmptyProof();
 
-    private EmptyWitness() {
+    private EmptyProof() {
     }
 
-    public static EmptyWitness getInstance() {
+    public static EmptyProof getInstance() {
         return empty;
     }
 

diff --git a/...mit/theta/analysis/algorithm/Witness.java → ...e/mit/theta/analysis/algorithm/Proof.java b/...mit/theta/analysis/algorithm/Witness.java → ...e/mit/theta/analysis/algorithm/Proof.java
@@ -15,5 +15,5 @@
  */
 package hu.bme.mit.theta.analysis.algorithm;
 
-public interface Witness {
+public interface Proof {
 }
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Result.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Result.java
@@ -17,9 +17,9 @@
 
 import java.util.Optional;
 
-public interface Result<W extends Witness> {
+public interface Result<Pr extends Proof> {
 
-    W getWitness();
+    Pr getProof();
 
     Optional<Statistics> getStats();
 

diff --git a/...ects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyChecker.java b/...ects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyChecker.java
@@ -15,18 +15,15 @@
  */
 package hu.bme.mit.theta.analysis.algorithm;
 
-import hu.bme.mit.theta.analysis.*;
-import hu.bme.mit.theta.analysis.algorithm.Checker;
-import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
-import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
+import hu.bme.mit.theta.analysis.Cex;
 
 @FunctionalInterface
-public interface SafetyChecker<W extends Witness, C extends Cex, I> extends Checker<W, I> {
+public interface SafetyChecker<Pr extends Proof, C extends Cex, I> extends Checker<Pr, I> {
 
     @Override
-    SafetyResult<W, C> check(final I input);
+    SafetyResult<Pr, C> check(final I input);
 
-    default SafetyResult<W, C> check() {
+    default SafetyResult<Pr, C> check() {
         return check(null);
     }
 

diff --git a/...jects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java b/...jects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java
@@ -22,68 +22,68 @@
 
 import static com.google.common.base.Preconditions.checkNotNull;
 
-public abstract class SafetyResult<W extends Witness, C extends Cex> implements Result<W> {
-    private final W witness;
+public abstract class SafetyResult<Pr extends Proof, C extends Cex> implements Result<Pr> {
+    private final Pr proof;
     private final Optional<Statistics> stats;
 
-    private SafetyResult(final W witness, final Optional<Statistics> stats) {
-        this.witness = checkNotNull(witness);
+    private SafetyResult(final Pr proof, final Optional<Statistics> stats) {
+        this.proof = checkNotNull(proof);
         this.stats = checkNotNull(stats);
     }
 
     private SafetyResult() {
-        this.witness = null;
+        this.proof = null;
         this.stats = Optional.empty();
     }
 
     @Override
-    public W getWitness() {
-        return witness;
+    public Pr getProof() {
+        return proof;
     }
 
     @Override
     public Optional<Statistics> getStats() {
         return stats;
     }
 
-    public static <W extends Witness, C extends Cex> Safe<W, C> safe(final W witness) {
+    public static <Pr extends Proof, C extends Cex> Safe<Pr, C> safe(final Pr witness) {
         return new Safe<>(witness, Optional.empty());
     }
 
-    public static <W extends Witness, C extends Cex> Unsafe<W, C> unsafe(final C cex, final W witness) {
+    public static <Pr extends Proof, C extends Cex> Unsafe<Pr, C> unsafe(final C cex, final Pr witness) {
         return new Unsafe<>(cex, witness, Optional.empty());
     }
 
-    public static <W extends Witness, C extends Cex> Unknown<W, C> unknown() {
+    public static <Pr extends Proof, C extends Cex> Unknown<Pr, C> unknown() {
         return new Unknown<>();
     }
 
-    public static <W extends Witness, C extends Cex> Safe<W, C> safe(final W witness, final Statistics stats) {
+    public static <Pr extends Proof, C extends Cex> Safe<Pr, C> safe(final Pr witness, final Statistics stats) {
         return new Safe<>(witness, Optional.of(stats));
     }
 
-    public static <W extends Witness, C extends Cex> Unsafe<W, C> unsafe(final C cex, final W witness,
+    public static <Pr extends Proof, C extends Cex> Unsafe<Pr, C> unsafe(final C cex, final Pr witness,
                                                                          final Statistics stats) {
         return new Unsafe<>(cex, witness, Optional.of(stats));
     }
 
-    public static <W extends Witness, C extends Cex> Unknown<W, C> unknown(final Statistics stats) {
+    public static <Pr extends Proof, C extends Cex> Unknown<Pr, C> unknown(final Statistics stats) {
         return new Unknown<>(Optional.of(stats));
     }
 
     public abstract boolean isSafe();
 
     public abstract boolean isUnsafe();
 
-    public abstract Safe<W, C> asSafe();
+    public abstract Safe<Pr, C> asSafe();
 
-    public abstract Unsafe<W, C> asUnsafe();
+    public abstract Unsafe<Pr, C> asUnsafe();
 
     ////
 
-    public static final class Safe<W extends Witness, C extends Cex> extends SafetyResult<W, C> {
-        private Safe(final W witness, final Optional<Statistics> stats) {
-            super(witness, stats);
+    public static final class Safe<Pr extends Proof, C extends Cex> extends SafetyResult<Pr, C> {
+        private Safe(final Pr proof, final Optional<Statistics> stats) {
+            super(proof, stats);
         }
 
         @Override
@@ -97,12 +97,12 @@ public boolean isUnsafe() {
         }
 
         @Override
-        public Safe<W, C> asSafe() {
+        public Safe<Pr, C> asSafe() {
             return this;
         }
 
         @Override
-        public Unsafe<W, C> asUnsafe() {
+        public Unsafe<Pr, C> asUnsafe() {
             throw new ClassCastException(
                     "Cannot cast " + Safe.class.getSimpleName() + " to " + Unsafe.class.getSimpleName());
         }
@@ -114,11 +114,11 @@ public String toString() {
         }
     }
 
-    public static final class Unsafe<W extends Witness, C extends Cex> extends SafetyResult<W, C> {
+    public static final class Unsafe<Pr extends Proof, C extends Cex> extends SafetyResult<Pr, C> {
         private final C cex;
 
-        private Unsafe(final C cex, final W witness, final Optional<Statistics> stats) {
-            super(witness, stats);
+        private Unsafe(final C cex, final Pr proof, final Optional<Statistics> stats) {
+            super(proof, stats);
             this.cex = checkNotNull(cex);
         }
 
@@ -137,13 +137,13 @@ public boolean isUnsafe() {
         }
 
         @Override
-        public Safe<W, C> asSafe() {
+        public Safe<Pr, C> asSafe() {
             throw new ClassCastException(
                     "Cannot cast " + Unsafe.class.getSimpleName() + " to " + Safe.class.getSimpleName());
         }
 
         @Override
-        public Unsafe<W, C> asUnsafe() {
+        public Unsafe<Pr, C> asUnsafe() {
             return this;
         }
 
@@ -154,7 +154,7 @@ public String toString() {
         }
     }
 
-    public static final class Unknown<W extends Witness, C extends Cex> extends SafetyResult<W, C> {
+    public static final class Unknown<Pr extends Proof, C extends Cex> extends SafetyResult<Pr, C> {
 
         public Unknown() {
             super();
@@ -175,12 +175,12 @@ public boolean isUnsafe() {
         }
 
         @Override
-        public Safe<W, C> asSafe() {
+        public Safe<Pr, C> asSafe() {
             return null;
         }
 
         @Override
-        public Unsafe<W, C> asUnsafe() {
+        public Unsafe<Pr, C> asUnsafe() {
             return null;
         }
 

diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/arg/ARG.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/arg/ARG.java
@@ -18,7 +18,7 @@
 import hu.bme.mit.theta.analysis.Action;
 import hu.bme.mit.theta.analysis.PartialOrd;
 import hu.bme.mit.theta.analysis.State;
-import hu.bme.mit.theta.analysis.algorithm.Witness;
+import hu.bme.mit.theta.analysis.algorithm.Proof;
 import hu.bme.mit.theta.analysis.algorithm.arg.debug.ARGWebDebugger;
 import hu.bme.mit.theta.common.container.Containers;
 
@@ -27,16 +27,14 @@
 import java.util.OptionalInt;
 import java.util.stream.Stream;
 
-import static com.google.common.base.Preconditions.checkArgument;
-import static com.google.common.base.Preconditions.checkNotNull;
-import static com.google.common.base.Preconditions.checkState;
+import static com.google.common.base.Preconditions.*;
 import static java.util.stream.Collectors.toList;
 
 /**
  * Represents an abstract reachability graph (ARG). See the related class
  * ArgBuilder.
  */
-public final class ARG<S extends State, A extends Action> implements Witness {
+public final class ARG<S extends State, A extends Action> implements Proof {
 
     private final Collection<ArgNode<S, A>> initNodes;
     public boolean initialized; // Set by ArgBuilder