From a62fe2b754691cba131b707537037f722a53d9c9 Mon Sep 17 00:00:00 2001 From: RipplB Date: Sat, 12 Oct 2024 08:33:57 +0200 Subject: [PATCH] Rename Witness to Proof --- .../impact/CfaPredImpactCheckerTest.java | 25 ++++----- .../java/hu/bme/mit/theta/cfa/cli/CfaCli.java | 20 +------ .../mit/theta/analysis/algorithm/Checker.java | 4 +- .../{EmptyWitness.java => EmptyProof.java} | 8 +-- .../algorithm/{Witness.java => Proof.java} | 2 +- .../mit/theta/analysis/algorithm/Result.java | 4 +- .../analysis/algorithm/SafetyChecker.java | 11 ++-- .../analysis/algorithm/SafetyResult.java | 56 +++++++++---------- .../mit/theta/analysis/algorithm/arg/ARG.java | 8 +-- .../algorithm/bounded/BoundedChecker.kt | 24 ++++---- .../analysis/algorithm/cegar/Abstractor.java | 8 +-- .../algorithm/cegar/BasicArgAbstractor.java | 2 +- .../algorithm/cegar/CegarChecker.java | 50 ++++++++--------- .../analysis/algorithm/cegar/Refiner.java | 6 +- .../analysis/algorithm/chc/HornChecker.kt | 5 +- .../mcm/analysis/FiniteStateChecker.kt | 8 +-- .../analysis/algorithm/mdd/MddChecker.java | 37 ++++++------ .../mdd/{MddWitness.java => MddProof.java} | 10 ++-- .../theta/analysis/utils/ArgVisualizer.java | 22 ++++---- ...ssVisualizer.java => ProofVisualizer.java} | 6 +- .../algorithm/mdd/MddCheckerTest.java | 5 +- .../theta/grammar/gson/SafetyResultAdapter.kt | 4 +- .../mit/theta/sts/analysis/StsExplTest.java | 23 ++------ .../theta/sts/analysis/StsMddCheckerTest.java | 5 +- .../mit/theta/sts/analysis/StsPredTest.java | 52 +++++++---------- .../java/hu/bme/mit/theta/sts/cli/StsCli.java | 15 +---- .../theta/xcfa/analysis/oc/XcfaOcChecker.kt | 16 +++--- .../bme/mit/theta/xcfa/cli/ExecuteConfig.kt | 13 +++-- .../cli/checkers/ConfigToBoundedChecker.kt | 6 +- .../xcfa/cli/checkers/ConfigToCegarChecker.kt | 4 +- .../xcfa/cli/checkers/ConfigToHornChecker.kt | 10 ++-- .../xcfa/cli/checkers/ConfigToOcChecker.kt | 10 ++-- .../xcfa/cli/checkers/InProcessChecker.kt | 16 +++--- ...aCliWitnessTest.kt => XcfaCliProofTest.kt} | 2 +- .../xsts/analysis/mdd/XstsMddChecker.java | 36 ++++++------ .../xsts/analysis/XstsMddCheckerTest.java | 8 +-- .../bme/mit/theta/xsts/cli/XstsCliBounded.kt | 4 +- .../hu/bme/mit/theta/xsts/cli/XstsCliCegar.kt | 8 +-- .../hu/bme/mit/theta/xsts/cli/XstsCliMdd.kt | 16 +----- .../xta/analysis/LazyXtaCheckerTest.java | 4 +- .../theta/xta/analysis/XtaAnalysisTest.java | 25 ++++----- .../xta/analysis/XtaZoneAnalysisTest.java | 27 +++++---- .../java/hu/bme/mit/theta/xta/cli/XtaCli.java | 7 +-- 43 files changed, 276 insertions(+), 356 deletions(-) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/{EmptyWitness.java => EmptyProof.java} (79%) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/{Witness.java => Proof.java} (96%) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/{MddWitness.java => MddProof.java} (81%) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/{WitnessVisualizer.java => ProofVisualizer.java} (84%) rename subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/{XcfaCliWitnessTest.kt => XcfaCliProofTest.kt} (99%) diff --git a/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java b/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java index 4204a3785d..6e9e92186b 100644 --- a/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java +++ b/subprojects/cfa/cfa-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 arg = status.getWitness(); + final ARG 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 index 024911743e..9756f1be64 100644 --- 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> 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 index e1a86bee69..90b85d5a06 100644 --- 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 { +public interface Checker { - Result check(I input); + Result check(I input); } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/EmptyWitness.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/EmptyProof.java similarity index 79% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/EmptyWitness.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/EmptyProof.java index 49794dd84e..d0220b0d64 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/EmptyWitness.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/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/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Witness.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Proof.java similarity index 96% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Witness.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Proof.java index ff6157e1e3..4cf21da2f4 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Witness.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/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 index 0c81bf5836..2e47333d23 100644 --- 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 { +public interface Result { - W getWitness(); + Pr getProof(); Optional getStats(); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyChecker.java index 4f13fac64c..8d24556feb 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyChecker.java +++ b/subprojects/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 extends Checker { +public interface SafetyChecker extends Checker { @Override - SafetyResult check(final I input); + SafetyResult check(final I input); - default SafetyResult check() { + default SafetyResult check() { return check(null); } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java index dfd812ebea..e2f3d74b32 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java @@ -22,23 +22,23 @@ import static com.google.common.base.Preconditions.checkNotNull; -public abstract class SafetyResult implements Result { - private final W witness; +public abstract class SafetyResult implements Result { + private final Pr proof; private final Optional stats; - private SafetyResult(final W witness, final Optional stats) { - this.witness = checkNotNull(witness); + private SafetyResult(final Pr proof, final Optional 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 @@ -46,28 +46,28 @@ public Optional getStats() { return stats; } - public static Safe safe(final W witness) { + public static Safe safe(final Pr witness) { return new Safe<>(witness, Optional.empty()); } - public static Unsafe unsafe(final C cex, final W witness) { + public static Unsafe unsafe(final C cex, final Pr witness) { return new Unsafe<>(cex, witness, Optional.empty()); } - public static Unknown unknown() { + public static Unknown unknown() { return new Unknown<>(); } - public static Safe safe(final W witness, final Statistics stats) { + public static Safe safe(final Pr witness, final Statistics stats) { return new Safe<>(witness, Optional.of(stats)); } - public static Unsafe unsafe(final C cex, final W witness, + public static Unsafe unsafe(final C cex, final Pr witness, final Statistics stats) { return new Unsafe<>(cex, witness, Optional.of(stats)); } - public static Unknown unknown(final Statistics stats) { + public static Unknown unknown(final Statistics stats) { return new Unknown<>(Optional.of(stats)); } @@ -75,15 +75,15 @@ public static Unknown unknown(final Sta public abstract boolean isUnsafe(); - public abstract Safe asSafe(); + public abstract Safe asSafe(); - public abstract Unsafe asUnsafe(); + public abstract Unsafe asUnsafe(); //// - public static final class Safe extends SafetyResult { - private Safe(final W witness, final Optional stats) { - super(witness, stats); + public static final class Safe extends SafetyResult { + private Safe(final Pr proof, final Optional stats) { + super(proof, stats); } @Override @@ -97,12 +97,12 @@ public boolean isUnsafe() { } @Override - public Safe asSafe() { + public Safe asSafe() { return this; } @Override - public Unsafe asUnsafe() { + public Unsafe 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 extends SafetyResult { + public static final class Unsafe extends SafetyResult { private final C cex; - private Unsafe(final C cex, final W witness, final Optional stats) { - super(witness, stats); + private Unsafe(final C cex, final Pr proof, final Optional stats) { + super(proof, stats); this.cex = checkNotNull(cex); } @@ -137,13 +137,13 @@ public boolean isUnsafe() { } @Override - public Safe asSafe() { + public Safe asSafe() { throw new ClassCastException( "Cannot cast " + Unsafe.class.getSimpleName() + " to " + Safe.class.getSimpleName()); } @Override - public Unsafe asUnsafe() { + public Unsafe asUnsafe() { return this; } @@ -154,7 +154,7 @@ public String toString() { } } - public static final class Unknown extends SafetyResult { + public static final class Unknown extends SafetyResult { public Unknown() { super(); @@ -175,12 +175,12 @@ public boolean isUnsafe() { } @Override - public Safe asSafe() { + public Safe asSafe() { return null; } @Override - public Unsafe asUnsafe() { + public Unsafe 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 index b43fb37e35..893f745770 100644 --- 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 implements Witness { +public final class ARG implements Proof { private final Collection> initNodes; public boolean initialized; // Set by ArgBuilder diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt index 72b90fe53f..8a4de2c6e0 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt @@ -17,7 +17,7 @@ package hu.bme.mit.theta.analysis.algorithm.bounded import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness +import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.expr.ExprAction @@ -71,7 +71,7 @@ class BoundedChecker @JvmOverloads constructor( private val valToState: (Valuation) -> S, private val biValToAction: (Valuation, Valuation) -> A, private val logger: Logger, -) : SafetyChecker, UnitPrec> { +) : SafetyChecker, UnitPrec> { private val vars = monolithicExpr.vars() private val unfoldedInitExpr = PathUtils.unfold(monolithicExpr.initExpr, VarIndexingFactory.indexing(0)) @@ -87,7 +87,7 @@ class BoundedChecker @JvmOverloads constructor( check(itpSolver != indSolver || itpSolver == null) { "Use distinct solvers for IMC and KInd!" } } - override fun check(prec: UnitPrec?): SafetyResult> { + override fun check(prec: UnitPrec?): SafetyResult> { iteration = 0 @@ -121,7 +121,7 @@ class BoundedChecker @JvmOverloads constructor( return SafetyResult.unknown(BoundedStatistics(iteration)) } - private fun bmc(): SafetyResult>? { + private fun bmc(): SafetyResult>? { val bmcSolver = this.bmcSolver!! logger.write(Logger.Level.MAINSTEP, "\tStarting BMC\n") @@ -139,7 +139,7 @@ class BoundedChecker @JvmOverloads constructor( if (bmcSolver.check().isUnsat) { logger.write(Logger.Level.MAINSTEP, "Safety proven in BMC step\n") - return SafetyResult.safe(EmptyWitness.getInstance(), BoundedStatistics(iteration)) + return SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration)) } } @@ -149,12 +149,12 @@ class BoundedChecker @JvmOverloads constructor( if (bmcSolver.check().isSat) { val trace = getTrace(bmcSolver.model) logger.write(Logger.Level.MAINSTEP, "CeX found in BMC step (length ${trace.length()})\n") - SafetyResult.unsafe(trace, EmptyWitness.getInstance(), BoundedStatistics(iteration)) + SafetyResult.unsafe(trace, EmptyProof.getInstance(), BoundedStatistics(iteration)) } else null } } - private fun kind(): SafetyResult>? { + private fun kind(): SafetyResult>? { val indSolver = this.indSolver!! logger.write(Logger.Level.MAINSTEP, "\tStarting k-induction\n") @@ -167,12 +167,12 @@ class BoundedChecker @JvmOverloads constructor( if (indSolver.check().isUnsat) { logger.write(Logger.Level.MAINSTEP, "Safety proven in k-induction step\n") - SafetyResult.safe(EmptyWitness.getInstance(), BoundedStatistics(iteration)) + SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration)) } else null } } - private fun itp(): SafetyResult>? { + private fun itp(): SafetyResult>? { val itpSolver = this.itpSolver!! logger.write(Logger.Level.MAINSTEP, "\tStarting IMC\n") @@ -203,7 +203,7 @@ class BoundedChecker @JvmOverloads constructor( itpSolver.pop() itpSolver.pop() logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC/BMC step\n") - return SafetyResult.safe(EmptyWitness.getInstance(), BoundedStatistics(iteration)) + return SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration)) } itpSolver.pop() } @@ -217,7 +217,7 @@ class BoundedChecker @JvmOverloads constructor( logger.write(Logger.Level.MAINSTEP, "CeX found in IMC/BMC step (length ${trace.length()})\n") itpSolver.pop() itpSolver.pop() - return SafetyResult.unsafe(trace, EmptyWitness.getInstance(), BoundedStatistics(iteration)) + return SafetyResult.unsafe(trace, EmptyProof.getInstance(), BoundedStatistics(iteration)) } var img = unfoldedInitExpr @@ -234,7 +234,7 @@ class BoundedChecker @JvmOverloads constructor( logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC step\n") itpSolver.pop() itpSolver.pop() - return SafetyResult.safe(EmptyWitness.getInstance(), BoundedStatistics(iteration)) + return SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration)) } itpSolver.pop() img = Or(img, itpFormula) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Abstractor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Abstractor.java index a6cb49bb43..05e275a95e 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Abstractor.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Abstractor.java @@ -16,22 +16,22 @@ package hu.bme.mit.theta.analysis.algorithm.cegar; import hu.bme.mit.theta.analysis.Prec; -import hu.bme.mit.theta.analysis.algorithm.Witness; +import hu.bme.mit.theta.analysis.algorithm.Proof; /** * Common interface for the abstractor component. It can create an initial witness and check a witness with * a given precision. */ -public interface Abstractor

{ +public interface Abstractor

{ /** * Create initial witness */ - W createWitness(); + Pr createProof(); /** * Check witness with given precision */ - AbstractorResult check(W witness, P prec); + AbstractorResult check(Pr witness, P prec); } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicArgAbstractor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicArgAbstractor.java index 050ae32ce3..8a05b8c801 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicArgAbstractor.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicArgAbstractor.java @@ -64,7 +64,7 @@ public static Builder createWitness() { + public ARG createProof() { return argBuilder.createArg(); } 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 fa811afc42..30da9a28e5 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 @@ -20,11 +20,11 @@ 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; -import hu.bme.mit.theta.analysis.algorithm.Witness; import hu.bme.mit.theta.analysis.runtimemonitor.MonitorCheckpoint; -import hu.bme.mit.theta.analysis.utils.WitnessVisualizer; +import hu.bme.mit.theta.analysis.utils.ProofVisualizer; import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.common.logging.Logger.Level; @@ -42,38 +42,38 @@ * 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 Abstractor abstractor; + private final Refiner refiner; private final Logger logger; - private final W witness; - private final WitnessVisualizer witnessVisualizer; + private final Pr proof; + private final ProofVisualizer proofVisualizer; - private CegarChecker(final Abstractor abstractor, final Refiner refiner, final Logger logger, final WitnessVisualizer witnessVisualizer) { + 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); - witness = abstractor.createWitness(); - this.witnessVisualizer = checkNotNull(witnessVisualizer); + proof = abstractor.createProof(); + this.proofVisualizer = checkNotNull(proofVisualizer); } - public static CegarChecker create( - final Abstractor abstractor, final Refiner refiner, final WitnessVisualizer witnessVisualizer) { - return create(abstractor, refiner, NullLogger.getInstance(), witnessVisualizer); + 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 WitnessVisualizer witnessVisualizer) { - return new CegarChecker<>(abstractor, refiner, logger, witnessVisualizer); + public static CegarChecker create( + final Abstractor abstractor, final Refiner refiner, final Logger logger, final ProofVisualizer proofVisualizer) { + return new CegarChecker<>(abstractor, refiner, logger, proofVisualizer); } - public W getWitness() { - return witness; + public Pr getProof() { + return proof; } @Override - public SafetyResult check(final P initPrec) { + public SafetyResult check(final P initPrec) { logger.write(Level.INFO, "Configuration: %s%n", this); final Stopwatch stopwatch = Stopwatch.createStarted(); long abstractorTime = 0; @@ -89,12 +89,12 @@ public SafetyResult check(final P initPrec) { logger.write(Level.MAINSTEP, "Iteration %d%n", iteration); logger.write(Level.MAINSTEP, "| Checking abstraction...%n"); final long abstractorStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS); - abstractorResult = abstractor.check(witness, prec); + abstractorResult = abstractor.check(proof, prec); abstractorTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - abstractorStartTime; logger.write(Level.MAINSTEP, "| Checking abstraction done, result: %s%n", abstractorResult); if (WebDebuggerLogger.enabled()) { - String argGraph = JSONWriter.getInstance().writeString(witnessVisualizer.visualize(witness)); + String argGraph = JSONWriter.getInstance().writeString(proofVisualizer.visualize(proof)); String precString = prec.toString(); wdl.addIteration(iteration, argGraph, precString); } @@ -105,7 +105,7 @@ public SafetyResult check(final P initPrec) { P lastPrec = prec; logger.write(Level.MAINSTEP, "| Refining abstraction...%n"); final long refinerStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS); - refinerResult = refiner.refine(witness, prec); + refinerResult = refiner.refine(proof, prec); refinerTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - refinerStartTime; logger.write(Level.MAINSTEP, "Refining abstraction done, result: %s%n", refinerResult); @@ -124,16 +124,16 @@ public SafetyResult check(final P initPrec) { } while (!abstractorResult.isSafe() && !refinerResult.isUnsafe()); stopwatch.stop(); - SafetyResult cegarResult = null; + SafetyResult cegarResult = null; final CegarStatistics stats = new CegarStatistics(stopwatch.elapsed(TimeUnit.MILLISECONDS), abstractorTime, refinerTime, iteration); assert abstractorResult.isSafe() || refinerResult.isUnsafe(); if (abstractorResult.isSafe()) { - cegarResult = SafetyResult.safe(witness, stats); + cegarResult = SafetyResult.safe(proof, stats); } else if (refinerResult.isUnsafe()) { - cegarResult = SafetyResult.unsafe(refinerResult.asUnsafe().getCex(), witness, stats); + cegarResult = SafetyResult.unsafe(refinerResult.asUnsafe().getCex(), proof, stats); } assert cegarResult != null; 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 6eca5d7c21..abd645f3cf 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 @@ -19,16 +19,16 @@ 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.Witness; +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(W witness, P prec); + RefinerResult refine(Pr witness, P prec); } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/chc/HornChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/chc/HornChecker.kt index 0c083b7cd0..98ce4ecb75 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/chc/HornChecker.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/chc/HornChecker.kt @@ -17,9 +17,9 @@ package hu.bme.mit.theta.analysis.algorithm.chc import hu.bme.mit.theta.analysis.Cex +import hu.bme.mit.theta.analysis.algorithm.Proof import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult -import hu.bme.mit.theta.analysis.algorithm.Witness import hu.bme.mit.theta.analysis.unit.UnitPrec import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.core.Relation @@ -30,7 +30,8 @@ import hu.bme.mit.theta.solver.ProofNode import hu.bme.mit.theta.solver.SolverFactory import hu.bme.mit.theta.solver.SolverStatus -data class Invariant(val lookup: Map>) : Witness +data class Invariant(val lookup: Map>) : + Proof data class CexTree(val proofNode: ProofNode) : Cex { diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/FiniteStateChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/FiniteStateChecker.kt index 05c02303c3..41c1a600b8 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/FiniteStateChecker.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/FiniteStateChecker.kt @@ -20,7 +20,7 @@ import hu.bme.mit.theta.analysis.EmptyCex import hu.bme.mit.theta.analysis.InitFunc import hu.bme.mit.theta.analysis.LTS import hu.bme.mit.theta.analysis.TransFunc -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness +import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.mcm.interpreter.MemoryEventProvider @@ -46,9 +46,9 @@ class FiniteStateChecker( private val memoryEventProvider: MemoryEventProvider, private val graphPatternCompiler: GraphPatternCompiler, private val graphPatternSolver: GraphSolver -) : SafetyChecker { +) : SafetyChecker { - override fun check(prec: ExplPrec): SafetyResult { + override fun check(prec: ExplPrec): SafetyResult { val eventIds = LinkedList() val rels = LinkedList>() val lastIds = LinkedHashMap() @@ -74,7 +74,7 @@ class FiniteStateChecker( initStates.addAll(nextStates) } // PartialSolver(mcm, CandidateExecutionGraph(eventIds, rels)) - return SafetyResult.unsafe(EmptyCex.getInstance(), EmptyWitness.getInstance()) + return SafetyResult.unsafe(EmptyCex.getInstance(), EmptyProof.getInstance()) } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java index df1feb4743..e9dba956d7 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java @@ -15,28 +15,26 @@ */ package hu.bme.mit.theta.analysis.algorithm.mdd; -import hu.bme.mit.delta.collections.impl.RecursiveIntObjMapViews; -import hu.bme.mit.delta.java.mdd.*; +import hu.bme.mit.delta.java.mdd.JavaMddFactory; +import hu.bme.mit.delta.java.mdd.MddGraph; +import hu.bme.mit.delta.java.mdd.MddHandle; +import hu.bme.mit.delta.java.mdd.MddVariableOrder; import hu.bme.mit.delta.mdd.MddInterpreter; import hu.bme.mit.delta.mdd.MddVariableDescriptor; -import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; +import hu.bme.mit.theta.analysis.algorithm.SafetyResult; +import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.AbstractNextStateDescriptor; +import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.MddNodeInitializer; +import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.MddNodeNextStateDescriptor; +import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.ExprLatticeDefinition; +import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.MddExpressionTemplate; import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.BfsProvider; import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.GeneralizedSaturationProvider; -import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.AbstractNextStateDescriptor; import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.SimpleSaturationProvider; import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.StateSpaceEnumerationProvider; -import hu.bme.mit.theta.common.logging.Logger.Level; -import hu.bme.mit.theta.solver.SolverPool; -import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.ExprLatticeDefinition; -import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.MddExpressionTemplate; -import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.MddNodeInitializer; -import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.MddNodeNextStateDescriptor; import hu.bme.mit.theta.analysis.expr.ExprAction; -import hu.bme.mit.theta.analysis.utils.MddNodeVisualizer; import hu.bme.mit.theta.common.logging.Logger; -import hu.bme.mit.theta.common.visualization.Graph; -import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter; +import hu.bme.mit.theta.common.logging.Logger.Level; import hu.bme.mit.theta.core.decl.Decl; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.Expr; @@ -45,15 +43,14 @@ import hu.bme.mit.theta.core.utils.PathUtils; import hu.bme.mit.theta.core.utils.indexings.VarIndexing; import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; -import hu.bme.mit.theta.solver.SolverFactory; +import hu.bme.mit.theta.solver.SolverPool; -import java.io.FileNotFoundException; import java.util.List; import java.util.Set; import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not; -public class MddChecker implements SafetyChecker { +public class MddChecker implements SafetyChecker { private final Expr initRel; private final VarIndexing initIndexing; @@ -103,7 +100,7 @@ public static MddChecker create(Expr initRel } @Override - public SafetyResult check(Void input) { + public SafetyResult check(Void input) { final MddGraph mddGraph = JavaMddFactory.getDefault().createMddGraph(ExprLatticeDefinition.forExpr()); @@ -166,11 +163,11 @@ public SafetyResult check(Void input) { final MddAnalysisStatistics statistics = new MddAnalysisStatistics(violatingSize, stateSpaceSize, stateSpaceProvider.getHitCount(), stateSpaceProvider.getQueryCount(), stateSpaceProvider.getCacheSize()); - final SafetyResult result; + final SafetyResult result; if (violatingSize != 0) { - result = SafetyResult.unsafe(MddCex.of(propViolating), MddWitness.of(stateSpace), statistics); + result = SafetyResult.unsafe(MddCex.of(propViolating), MddProof.of(stateSpace), statistics); } else { - result = SafetyResult.safe(MddWitness.of(stateSpace), statistics); + result = SafetyResult.safe(MddProof.of(stateSpace), statistics); } logger.write(Level.RESULT, "%s%n", result); return result; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddWitness.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddProof.java similarity index 81% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddWitness.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddProof.java index 300dc6579f..805a138399 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddWitness.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddProof.java @@ -17,18 +17,18 @@ import hu.bme.mit.delta.java.mdd.MddHandle; import hu.bme.mit.delta.mdd.MddInterpreter; -import hu.bme.mit.theta.analysis.algorithm.Witness; +import hu.bme.mit.theta.analysis.algorithm.Proof; -public class MddWitness implements Witness { +public class MddProof implements Proof { private final MddHandle stateSpace; - private MddWitness(MddHandle stateSpace) { + private MddProof(MddHandle stateSpace) { this.stateSpace = stateSpace; } - public static MddWitness of(MddHandle stateSpace) { - return new MddWitness(stateSpace); + public static MddProof of(MddHandle stateSpace) { + return new MddProof(stateSpace); } public Long size() { diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ArgVisualizer.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ArgVisualizer.java index c4c82eeb74..eda1f709a9 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ArgVisualizer.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ArgVisualizer.java @@ -15,28 +15,26 @@ */ package hu.bme.mit.theta.analysis.utils; -import static hu.bme.mit.theta.common.visualization.Alignment.LEFT; -import static hu.bme.mit.theta.common.visualization.Shape.RECTANGLE; - -import java.awt.Color; - -import hu.bme.mit.theta.common.container.Containers; - -import java.util.Set; -import java.util.function.Function; -import java.util.stream.Collectors; - import hu.bme.mit.theta.analysis.Action; import hu.bme.mit.theta.analysis.State; import hu.bme.mit.theta.analysis.algorithm.arg.ARG; import hu.bme.mit.theta.analysis.algorithm.arg.ArgEdge; import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode; +import hu.bme.mit.theta.common.container.Containers; import hu.bme.mit.theta.common.visualization.EdgeAttributes; import hu.bme.mit.theta.common.visualization.Graph; import hu.bme.mit.theta.common.visualization.LineStyle; import hu.bme.mit.theta.common.visualization.NodeAttributes; -public final class ArgVisualizer implements WitnessVisualizer> { +import java.awt.*; +import java.util.Set; +import java.util.function.Function; +import java.util.stream.Collectors; + +import static hu.bme.mit.theta.common.visualization.Alignment.LEFT; +import static hu.bme.mit.theta.common.visualization.Shape.RECTANGLE; + +public final class ArgVisualizer implements ProofVisualizer> { private static final LineStyle COVER_EDGE_STYLE = LineStyle.DASHED; private static final LineStyle SUCC_EDGE_STYLE = LineStyle.NORMAL; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/WitnessVisualizer.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ProofVisualizer.java similarity index 84% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/WitnessVisualizer.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ProofVisualizer.java index bd1a9d8234..8c91ded53c 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/WitnessVisualizer.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ProofVisualizer.java @@ -16,11 +16,11 @@ package hu.bme.mit.theta.analysis.utils; -import hu.bme.mit.theta.analysis.algorithm.Witness; +import hu.bme.mit.theta.analysis.algorithm.Proof; import hu.bme.mit.theta.common.visualization.Graph; -public interface WitnessVisualizer { +public interface ProofVisualizer { - Graph visualize(W witness); + Graph visualize(Pr proof); } diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddCheckerTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddCheckerTest.java index 070daeb91f..8f901e59dc 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddCheckerTest.java +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddCheckerTest.java @@ -33,7 +33,6 @@ import org.junit.runner.RunWith; import org.junit.runners.Parameterized; -import java.io.IOException; import java.util.Arrays; import java.util.Collection; @@ -143,7 +142,7 @@ public void testWithIterationStrategy(MddChecker.IterationStrategy iterationStra final Logger logger = new ConsoleLogger(Logger.Level.SUBSTEP); - final SafetyResult status; + final SafetyResult status; try (var solverPool = new SolverPool(Z3LegacySolverFactory.getInstance())) { final MddChecker checker = MddChecker.create(initExpr, VarIndexingFactory.indexing(0), new ExprAction() { @Override @@ -164,7 +163,7 @@ public VarIndexing nextIndexing() { } else { assertTrue(status.isUnsafe()); } - assertEquals(stateSpaceSize, status.getWitness().size()); + assertEquals(stateSpaceSize, status.getProof().size()); } diff --git a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/SafetyResultAdapter.kt b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/SafetyResultAdapter.kt index 6829d577c0..f9c091be92 100644 --- a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/SafetyResultAdapter.kt +++ b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/gson/SafetyResultAdapter.kt @@ -24,9 +24,9 @@ import com.google.gson.stream.JsonWriter import hu.bme.mit.theta.analysis.Action import hu.bme.mit.theta.analysis.State import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.arg.ARG import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.Statistics +import hu.bme.mit.theta.analysis.algorithm.arg.ARG import java.lang.reflect.Type import java.util.* @@ -45,7 +45,7 @@ class SafetyResultAdapter( initGson() writer.beginObject() writer.name("arg") - gson.toJson(gson.toJsonTree(value.witness), writer) + gson.toJson(gson.toJsonTree(value.proof), writer) writer.name("stats") // gson.toJson(gson.toJsonTree(value.stats), writer) gson.toJson(gson.toJsonTree(Optional.empty()), writer) diff --git a/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java b/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java index 4f2f998af5..658bcae573 100644 --- a/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java +++ b/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java @@ -19,14 +19,14 @@ import hu.bme.mit.theta.analysis.LTS; import hu.bme.mit.theta.analysis.State; import hu.bme.mit.theta.analysis.Trace; +import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.arg.ARG; import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder; import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators; -import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor; -import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor; import hu.bme.mit.theta.analysis.algorithm.cegar.ArgCegarChecker; +import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor; import hu.bme.mit.theta.analysis.expl.ExplAnalysis; import hu.bme.mit.theta.analysis.expl.ExplPrec; import hu.bme.mit.theta.analysis.expl.ExplState; @@ -34,12 +34,7 @@ import hu.bme.mit.theta.analysis.expr.ExprAction; import hu.bme.mit.theta.analysis.expr.ExprState; import hu.bme.mit.theta.analysis.expr.ExprStatePredicate; -import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceChecker; -import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceUnsatCoreChecker; -import hu.bme.mit.theta.analysis.expr.refinement.JoiningPrecRefiner; -import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy; -import hu.bme.mit.theta.analysis.expr.refinement.SingleExprTraceRefiner; -import hu.bme.mit.theta.analysis.expr.refinement.VarsRefutation; +import hu.bme.mit.theta.analysis.expr.refinement.*; import hu.bme.mit.theta.analysis.waitlist.PriorityWaitlist; import hu.bme.mit.theta.common.logging.ConsoleLogger; import hu.bme.mit.theta.common.logging.Logger; @@ -60,14 +55,8 @@ import static hu.bme.mit.theta.analysis.algorithm.arg.ArgUtils.isWellLabeled; import static hu.bme.mit.theta.core.decl.Decls.Var; import static hu.bme.mit.theta.core.type.anytype.Exprs.Prime; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Imply; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Add; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Eq; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Geq; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Lt; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.*; import static org.junit.Assert.assertTrue; public class StsExplTest { @@ -127,7 +116,7 @@ public void test() { final SafetyResult, Trace> safetyStatus = checker.check(prec); - final ARG arg = safetyStatus.getWitness(); + final ARG arg = safetyStatus.getProof(); assertTrue(isWellLabeled(arg, abstractionSolver)); // System.out.println(new diff --git a/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsMddCheckerTest.java b/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsMddCheckerTest.java index e9f88faaad..25847b9e0a 100644 --- a/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsMddCheckerTest.java +++ b/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsMddCheckerTest.java @@ -19,7 +19,7 @@ import hu.bme.mit.theta.analysis.algorithm.mdd.MddCex; import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker; import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker.IterationStrategy; -import hu.bme.mit.theta.analysis.algorithm.mdd.MddWitness; +import hu.bme.mit.theta.analysis.algorithm.mdd.MddProof; import hu.bme.mit.theta.analysis.expr.ExprAction; import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.common.logging.ConsoleLogger; @@ -40,7 +40,6 @@ import org.junit.runners.Parameterized; import java.io.FileInputStream; -import java.io.IOException; import java.util.Arrays; import java.util.Collection; @@ -100,7 +99,7 @@ public void test() throws Exception { sts = Utils.singleElementOf(spec.getAllSts()); } - final SafetyResult status; + final SafetyResult status; try (var solverPool = new SolverPool(Z3LegacySolverFactory.getInstance())) { final MddChecker checker = MddChecker.create(sts.getInit(), VarIndexingFactory.indexing(0), new ExprAction() { @Override diff --git a/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java b/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java index bed9497f54..793dc580c9 100644 --- a/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java +++ b/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java @@ -15,56 +15,44 @@ */ package hu.bme.mit.theta.sts.analysis; -import static hu.bme.mit.theta.analysis.algorithm.arg.ArgUtils.isWellLabeled; -import static hu.bme.mit.theta.core.decl.Decls.Var; -import static hu.bme.mit.theta.core.type.anytype.Exprs.Prime; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Imply; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Add; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Eq; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Geq; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Lt; -import static org.junit.Assert.assertTrue; - -import java.util.function.Predicate; - -import hu.bme.mit.theta.analysis.Trace; -import hu.bme.mit.theta.analysis.algorithm.SafetyResult; -import hu.bme.mit.theta.analysis.expr.refinement.*; -import hu.bme.mit.theta.solver.ItpSolver; -import hu.bme.mit.theta.solver.Solver; -import org.junit.Before; -import org.junit.Test; - import hu.bme.mit.theta.analysis.Analysis; import hu.bme.mit.theta.analysis.LTS; import hu.bme.mit.theta.analysis.State; +import hu.bme.mit.theta.analysis.Trace; +import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; +import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.arg.ARG; import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder; -import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor; -import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor; import hu.bme.mit.theta.analysis.algorithm.cegar.ArgCegarChecker; +import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor; import hu.bme.mit.theta.analysis.expr.ExprAction; import hu.bme.mit.theta.analysis.expr.ExprState; import hu.bme.mit.theta.analysis.expr.ExprStatePredicate; -import hu.bme.mit.theta.analysis.pred.ExprSplitters; -import hu.bme.mit.theta.analysis.pred.ItpRefToPredPrec; -import hu.bme.mit.theta.analysis.pred.PredAbstractors; -import hu.bme.mit.theta.analysis.pred.PredAnalysis; -import hu.bme.mit.theta.analysis.pred.PredPrec; -import hu.bme.mit.theta.analysis.pred.PredState; +import hu.bme.mit.theta.analysis.expr.refinement.*; +import hu.bme.mit.theta.analysis.pred.*; import hu.bme.mit.theta.common.logging.ConsoleLogger; import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.common.logging.Logger.Level; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.inttype.IntType; +import hu.bme.mit.theta.solver.ItpSolver; +import hu.bme.mit.theta.solver.Solver; import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; import hu.bme.mit.theta.sts.STS; import hu.bme.mit.theta.sts.STS.Builder; +import org.junit.Before; +import org.junit.Test; + +import java.util.function.Predicate; + +import static hu.bme.mit.theta.analysis.algorithm.arg.ArgUtils.isWellLabeled; +import static hu.bme.mit.theta.core.decl.Decls.Var; +import static hu.bme.mit.theta.core.type.anytype.Exprs.Prime; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.*; +import static org.junit.Assert.assertTrue; public class StsPredTest { @@ -123,7 +111,7 @@ public void testPredPrec() { final SafetyResult, Trace> safetyStatus = checker.check(prec); System.out.println(safetyStatus); - final ARG arg = safetyStatus.getWitness(); + final ARG arg = safetyStatus.getProof(); assertTrue(isWellLabeled(arg, abstractionSolver)); // System.out.println(new diff --git a/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java b/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java index ddb48470eb..53822ff7e6 100644 --- a/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java +++ b/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java @@ -52,20 +52,11 @@ import hu.bme.mit.theta.sts.analysis.StsTraceConcretizer; import hu.bme.mit.theta.sts.analysis.config.StsConfig; import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder; -import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder.Domain; -import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder.InitPrec; -import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder.PredSplit; -import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder.Refinement; -import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder.Search; +import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder.*; import hu.bme.mit.theta.sts.dsl.StsDslManager; import hu.bme.mit.theta.sts.dsl.StsSpec; -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.util.concurrent.TimeUnit; import java.util.stream.Stream; @@ -278,7 +269,7 @@ private void printResult(final SafetyResult> 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/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt index 6ffa9bc1fb..c42552c2dd 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt @@ -16,12 +16,10 @@ package hu.bme.mit.theta.xcfa.analysis.oc -import hu.bme.mit.theta.analysis.EmptyCex import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness +import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult -import hu.bme.mit.theta.analysis.algorithm.arg.ARG import hu.bme.mit.theta.analysis.algorithm.oc.EventType import hu.bme.mit.theta.analysis.algorithm.oc.OcChecker import hu.bme.mit.theta.analysis.algorithm.oc.Relation @@ -55,7 +53,7 @@ import hu.bme.mit.theta.xcfa.passes.MutexToVarPass private val Expr<*>.vars get() = ExprUtils.getVars(this) class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, private val logger: Logger) : - SafetyChecker>, XcfaAction>, XcfaPrec> { + SafetyChecker>, XcfaAction>, XcfaPrec> { private val ocChecker: OcChecker = decisionProcedure.checker() private val solver = ocChecker.solver @@ -74,22 +72,22 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv private val rfs = mutableMapOf, MutableSet>() override fun check( - prec: XcfaPrec?): SafetyResult>, XcfaAction>> = let { + prec: XcfaPrec?): SafetyResult>, XcfaAction>> = let { if (xcfa.initProcedures.size > 1) error("Multiple entry points are not supported by OC checker.") logger.write(Logger.Level.MAINSTEP, "Adding constraints...\n") xcfa.initProcedures.forEach { processThread(Thread(it.first)) } addCrossThreadRelations() - if (!addToSolver()) return@let SafetyResult.safe>, XcfaAction>>( - EmptyWitness.getInstance()) // no violations in the model + if (!addToSolver()) return@let SafetyResult.safe>, XcfaAction>>( + EmptyProof.getInstance()) // no violations in the model logger.write(Logger.Level.MAINSTEP, "Start checking...\n") val status = ocChecker.check(events, pos, rfs) when { - status?.isUnsat == true -> SafetyResult.safe(EmptyWitness.getInstance()) + status?.isUnsat == true -> SafetyResult.safe(EmptyProof.getInstance()) status?.isSat == true -> SafetyResult.unsafe( XcfaOcTraceExtractor(xcfa, ocChecker, threads, events, violations, pos).trace, - EmptyWitness.getInstance() + EmptyProof.getInstance() ) else -> SafetyResult.unknown() diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt index 9469c2eca3..1ce4f218b9 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt @@ -23,7 +23,7 @@ import hu.bme.mit.theta.analysis.Action import hu.bme.mit.theta.analysis.EmptyCex import hu.bme.mit.theta.analysis.State import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness +import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.arg.ARG import hu.bme.mit.theta.analysis.algorithm.arg.debug.ARGWebDebugger @@ -194,10 +194,11 @@ private fun backend( throwDontExit: Boolean ): SafetyResult<*, *> = if (config.backendConfig.backend == Backend.NONE) { - SafetyResult.unknown() + SafetyResult.unknown() } else { if (xcfa.procedures.all { it.errorLoc.isEmpty && config.inputConfig.property == ErrorDetection.ERROR_LOCATION }) { - val result = SafetyResult.safe(EmptyWitness.getInstance()) + val result = SafetyResult.safe( + EmptyProof.getInstance()) logger.write(Logger.Level.INFO, "Input is trivially safe\n") logger.write(RESULT, result.toString() + "\n") @@ -217,7 +218,7 @@ private fun backend( when { result.isSafe && LoopUnrollPass.FORCE_UNROLL_USED -> { // cannot report safe if force unroll was used logger.write(RESULT, "Incomplete loop unroll used: safe result is unreliable.\n") - SafetyResult.unknown() + SafetyResult.unknown() } else -> result @@ -309,9 +310,9 @@ private fun postVerificationLogging( ) // TODO eliminate the need for the instanceof check - if (!config.outputConfig.argConfig.disable && safetyResult.witness is ARG?) { + if (!config.outputConfig.argConfig.disable && safetyResult.proof is ARG?) { val argFile = File(resultFolder, "arg-${safetyResult.isSafe}.dot") - val g: Graph = ArgVisualizer.getDefault().visualize(safetyResult.witness as ARG?) + val g: Graph = ArgVisualizer.getDefault().visualize(safetyResult.proof as ARG?) argFile.writeText(GraphvizWriter.getInstance().writeString(g)) } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt index 18e0bd82ca..e354104f6d 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt @@ -17,7 +17,7 @@ package hu.bme.mit.theta.xcfa.cli.checkers import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness +import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.bounded.BoundedChecker import hu.bme.mit.theta.analysis.ptr.PtrState @@ -32,7 +32,7 @@ import hu.bme.mit.theta.xcfa.model.XCFA fun getBoundedChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, - logger: Logger): SafetyChecker>, XcfaAction>, XcfaPrec<*>> { + logger: Logger): SafetyChecker>, XcfaAction>, XcfaPrec<*>> { val boundedConfig = config.backendConfig.specConfig as BoundedConfig @@ -51,7 +51,7 @@ fun getBoundedChecker(xcfa: XCFA, mcm: MCM, valToState = { xcfa.valToState(it) }, biValToAction = { val1, val2 -> xcfa.valToAction(val1, val2) }, logger = logger - ) as SafetyChecker>, XcfaAction>, XcfaPrec<*>> + ) as SafetyChecker>, XcfaAction>, XcfaPrec<*>> } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt index f8bf86f8d2..cf625c3351 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt @@ -19,10 +19,10 @@ package hu.bme.mit.theta.xcfa.cli.checkers import hu.bme.mit.theta.analysis.PartialOrd import hu.bme.mit.theta.analysis.Prec import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.arg.ARG +import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor import hu.bme.mit.theta.analysis.algorithm.cegar.ArgCegarChecker import hu.bme.mit.theta.analysis.algorithm.cegar.ArgRefiner @@ -131,7 +131,7 @@ fun getCegarChecker( // initialize monitors MonitorCheckpoint.reset() if (cegarConfig.cexMonitor == CexMonitorOptions.CHECK) { - val cm = CexMonitor(logger, cegarChecker.witness) + val cm = CexMonitor(logger, cegarChecker.proof) MonitorCheckpoint.register(cm, "CegarChecker.unsafeARG") } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt index dd63b5eb48..22366bfaed 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt @@ -17,7 +17,7 @@ package hu.bme.mit.theta.xcfa.cli.checkers import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness +import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.chc.HornChecker @@ -37,7 +37,7 @@ import hu.bme.mit.theta.xcfa2chc.toCHC import org.abego.treelayout.internal.util.Contract.checkState fun getHornChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, logger: Logger): - SafetyChecker>, XcfaAction>, XcfaPrec<*>> { + SafetyChecker>, XcfaAction>, XcfaPrec<*>> { checkState(xcfa.isInlined, "Only inlined XCFAs work right now") checkState(xcfa.initProcedures.size == 1, "Only one-procedure XCFAs work right now") @@ -50,15 +50,15 @@ fun getHornChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, logger: Logge logger = logger, ) - return SafetyChecker>, XcfaAction>, XcfaPrec<*>> { + return SafetyChecker>, XcfaAction>, XcfaPrec<*>> { val result = checker.check(null) if (result.isSafe) { - SafetyResult.safe(EmptyWitness.getInstance()) + SafetyResult.safe(EmptyProof.getInstance()) } else if (result.isUnsafe) { val proof = result.asUnsafe().cex val state = XcfaState>(xcfa, mapOf(), PtrState(PredState.of(proof.proofNode.expr))) - SafetyResult.unsafe(Trace.of(listOf(state), listOf()), EmptyWitness.getInstance()) + SafetyResult.unsafe(Trace.of(listOf(state), listOf()), EmptyProof.getInstance()) } else { SafetyResult.unknown() } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt index df14f6ee8f..f9f6bec692 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt @@ -17,7 +17,7 @@ package hu.bme.mit.theta.xcfa.cli.checkers import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness +import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.ptr.PtrState @@ -33,12 +33,12 @@ import hu.bme.mit.theta.xcfa.model.XCFA fun getOcChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, - logger: Logger): SafetyChecker>, XcfaAction>, XcfaPrec<*>> { + logger: Logger): SafetyChecker>, XcfaAction>, XcfaPrec<*>> { val ocChecker = XcfaOcChecker(xcfa, (config.backendConfig.specConfig as OcConfig).decisionProcedure, logger) - return object : SafetyChecker>, XcfaAction>, XcfaPrec<*>> { + return object : SafetyChecker>, XcfaAction>, XcfaPrec<*>> { override fun check( - prec: XcfaPrec<*>?): SafetyResult>, XcfaAction>> = check() + prec: XcfaPrec<*>?): SafetyResult>, XcfaAction>> = check() - override fun check(): SafetyResult>, XcfaAction>> = ocChecker.check() + override fun check(): SafetyResult>, XcfaAction>> = ocChecker.check() } } \ No newline at end of file diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt index a20d9a5aaf..9d97f6b85e 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt @@ -20,10 +20,9 @@ import com.zaxxer.nuprocess.NuAbstractProcessHandler import com.zaxxer.nuprocess.NuProcess import com.zaxxer.nuprocess.NuProcessBuilder import hu.bme.mit.theta.analysis.EmptyCex -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness +import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult -import hu.bme.mit.theta.analysis.ptr.PtrState import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.xcfa.analysis.XcfaPrec @@ -44,14 +43,14 @@ class InProcessChecker( val config: XcfaConfig, val parseContext: ParseContext, val logger: Logger, -) : SafetyChecker> { +) : SafetyChecker> { override fun check( - prec: XcfaPrec<*>?): SafetyResult { + prec: XcfaPrec<*>?): SafetyResult { return check() } - override fun check(): SafetyResult { + override fun check(): SafetyResult { val tempDir = createTempDirectory(config.outputConfig.resultFolder.toPath()) val xcfaJson = CachingFileSerializer.serialize("xcfa.json", xcfa) { getGson(xcfa).toJson(xcfa) } @@ -122,7 +121,7 @@ class InProcessChecker( } tempDir.toFile().deleteRecursively() - return booleanSafetyResult as SafetyResult + return booleanSafetyResult as SafetyResult } private class ProcessHandler : NuAbstractProcessHandler() { @@ -142,10 +141,11 @@ class InProcessChecker( stdoutRemainder += str if (stdoutRemainder.contains("SafetyResult Safe")) { - safetyResult = SafetyResult.safe(EmptyWitness.getInstance()) + safetyResult = SafetyResult.safe( + EmptyProof.getInstance()) } if (stdoutRemainder.contains("SafetyResult Unsafe")) { - safetyResult = SafetyResult.unsafe(EmptyCex.getInstance(), EmptyWitness.getInstance()) + safetyResult = SafetyResult.unsafe(EmptyCex.getInstance(), EmptyProof.getInstance()) } val newLines = stdoutRemainder.split("\n") // if ends with \n, last element will be "" diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliWitnessTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliProofTest.kt similarity index 99% rename from subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliWitnessTest.kt rename to subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliProofTest.kt index bc5657f5ba..82e64bf2b6 100644 --- a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliWitnessTest.kt +++ b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliProofTest.kt @@ -33,7 +33,7 @@ data class WitnessEdge( val assumption: Regex?, ) -class XcfaCliWitnessTest { +class XcfaCliProofTest { companion object { @JvmStatic diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/mdd/XstsMddChecker.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/mdd/XstsMddChecker.java index ae9262e03f..cd363b3237 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/mdd/XstsMddChecker.java +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/mdd/XstsMddChecker.java @@ -16,29 +16,27 @@ package hu.bme.mit.theta.xsts.analysis.mdd; import com.google.common.base.Preconditions; -import hu.bme.mit.delta.collections.impl.RecursiveIntObjMapViews; -import hu.bme.mit.delta.java.mdd.*; +import hu.bme.mit.delta.java.mdd.JavaMddFactory; +import hu.bme.mit.delta.java.mdd.MddGraph; +import hu.bme.mit.delta.java.mdd.MddHandle; +import hu.bme.mit.delta.java.mdd.MddVariableOrder; import hu.bme.mit.delta.mdd.MddInterpreter; import hu.bme.mit.delta.mdd.MddVariableDescriptor; -import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; +import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.mdd.MddAnalysisStatistics; import hu.bme.mit.theta.analysis.algorithm.mdd.MddCex; import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker.IterationStrategy; -import hu.bme.mit.theta.analysis.algorithm.mdd.MddWitness; -import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.*; +import hu.bme.mit.theta.analysis.algorithm.mdd.MddProof; import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.AbstractNextStateDescriptor; +import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.MddNodeInitializer; +import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.MddNodeNextStateDescriptor; import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.OrNextStateDescriptor; -import hu.bme.mit.theta.common.logging.Logger; -import hu.bme.mit.theta.common.logging.Logger.Level; -import hu.bme.mit.theta.solver.SolverPool; import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.ExprLatticeDefinition; import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.MddExpressionTemplate; -import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.MddNodeInitializer; -import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.MddNodeNextStateDescriptor; -import hu.bme.mit.theta.analysis.utils.MddNodeVisualizer; -import hu.bme.mit.theta.common.visualization.Graph; -import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter; +import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.*; +import hu.bme.mit.theta.common.logging.Logger; +import hu.bme.mit.theta.common.logging.Logger.Level; import hu.bme.mit.theta.core.decl.Decl; import hu.bme.mit.theta.core.stmt.NonDetStmt; import hu.bme.mit.theta.core.stmt.SequenceStmt; @@ -48,9 +46,9 @@ import hu.bme.mit.theta.core.utils.PathUtils; import hu.bme.mit.theta.core.utils.StmtUtils; import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; +import hu.bme.mit.theta.solver.SolverPool; import hu.bme.mit.theta.xsts.XSTS; -import java.io.FileNotFoundException; import java.util.ArrayList; import java.util.List; @@ -58,7 +56,7 @@ import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not; -public class XstsMddChecker implements SafetyChecker { +public class XstsMddChecker implements SafetyChecker { private final SolverPool solverPool; private final XSTS xsts; @@ -82,7 +80,7 @@ public static XstsMddChecker create(XSTS xsts, SolverPool solverPool, Logger log } @Override - public SafetyResult check(Void input) { + public SafetyResult check(Void input) { final MddGraph mddGraph = JavaMddFactory.getDefault().createMddGraph(ExprLatticeDefinition.forExpr()); @@ -183,11 +181,11 @@ public SafetyResult check(Void input) { final MddAnalysisStatistics statistics = new MddAnalysisStatistics(violatingSize, stateSpaceSize, stateSpaceProvider.getHitCount(), stateSpaceProvider.getQueryCount(), stateSpaceProvider.getCacheSize()); - final SafetyResult result; + final SafetyResult result; if (violatingSize != 0) { - result = SafetyResult.unsafe(MddCex.of(propViolating), MddWitness.of(stateSpace), statistics); + result = SafetyResult.unsafe(MddCex.of(propViolating), MddProof.of(stateSpace), statistics); } else { - result = SafetyResult.safe(MddWitness.of(stateSpace), statistics); + result = SafetyResult.safe(MddProof.of(stateSpace), statistics); } logger.write(Level.RESULT, "%s%n", result); return result; diff --git a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsMddCheckerTest.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsMddCheckerTest.java index bda3053ed6..54d62303b1 100644 --- a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsMddCheckerTest.java +++ b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsMddCheckerTest.java @@ -18,7 +18,7 @@ import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.mdd.MddCex; import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker.IterationStrategy; -import hu.bme.mit.theta.analysis.algorithm.mdd.MddWitness; +import hu.bme.mit.theta.analysis.algorithm.mdd.MddProof; import hu.bme.mit.theta.common.logging.ConsoleLogger; import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.solver.SolverPool; @@ -26,12 +26,8 @@ import hu.bme.mit.theta.xsts.XSTS; import hu.bme.mit.theta.xsts.analysis.mdd.XstsMddChecker; import hu.bme.mit.theta.xsts.dsl.XstsDslManager; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; import java.io.FileInputStream; -import java.io.IOException; import java.io.InputStream; import java.io.SequenceInputStream; import java.util.Arrays; @@ -116,7 +112,7 @@ public static void runTestWithIterationStrategy(String filePath, String propPath xsts = XstsDslManager.createXsts(inputStream); } - final SafetyResult status; + final SafetyResult status; try (var solverPool = new SolverPool(Z3LegacySolverFactory.getInstance())) { final XstsMddChecker checker = XstsMddChecker.create(xsts, solverPool, logger, iterationStrategy); status = checker.check(null); diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBounded.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBounded.kt index b0582bf87f..6bb8a39ed2 100644 --- a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBounded.kt +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBounded.kt @@ -21,7 +21,7 @@ import com.github.ajalt.clikt.parameters.options.option import com.github.ajalt.clikt.parameters.types.enum import com.google.common.base.Stopwatch import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness +import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.bounded.* import hu.bme.mit.theta.analysis.expl.ExplState @@ -85,7 +85,7 @@ class XstsCliBounded : XstsCliBaseCommand( private val variant by option().enum().default(Variant.BMC) - private fun printResult(status: SafetyResult>, xsts: XSTS, totalTimeMs: Long) { + private fun printResult(status: SafetyResult>, xsts: XSTS, totalTimeMs: Long) { if (!outputOptions.benchmarkMode) return printCommonResult(status, xsts, totalTimeMs) val stats = status.stats.orElse(BoundedStatistics(0)) as BoundedStatistics diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliCegar.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliCegar.kt index ee455f86dc..5c1feb8857 100644 --- a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliCegar.kt +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliCegar.kt @@ -65,9 +65,9 @@ class XstsCliCegar : XstsCliBaseCommand( stats.abstractorTimeMs, stats.refinerTimeMs, stats.iterations, - status.witness!!.size(), - status.witness!!.depth, - status.witness!!.meanBranchingFactor, + status.proof!!.size(), + status.proof!!.depth, + status.proof!!.meanBranchingFactor, ).forEach(writer::cell) writer.newRow() } @@ -76,7 +76,7 @@ class XstsCliCegar : XstsCliBaseCommand( status: SafetyResult?, out Trace?> ) { if (outputOptions.visualize == null) return - val graph = if (status.isSafe) ArgVisualizer.getDefault().visualize(status.asSafe().witness) + val graph = if (status.isSafe) ArgVisualizer.getDefault().visualize(status.asSafe().proof) else TraceVisualizer.getDefault().visualize(status.asUnsafe().cex) GraphvizWriter.getInstance().writeFile(graph, outputOptions.visualize!!) } diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMdd.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMdd.kt index cc74818770..31058b9c28 100644 --- a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMdd.kt +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMdd.kt @@ -18,28 +18,16 @@ package hu.bme.mit.theta.xsts.cli import com.github.ajalt.clikt.parameters.options.default import com.github.ajalt.clikt.parameters.options.option -import com.github.ajalt.clikt.parameters.options.required import com.github.ajalt.clikt.parameters.types.enum import com.google.common.base.Stopwatch -import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.EmptyWitness import hu.bme.mit.theta.analysis.algorithm.SafetyResult -import hu.bme.mit.theta.analysis.algorithm.bounded.* -import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics import hu.bme.mit.theta.analysis.algorithm.mdd.MddAnalysisStatistics import hu.bme.mit.theta.analysis.algorithm.mdd.MddCex import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker -import hu.bme.mit.theta.analysis.algorithm.mdd.MddWitness -import hu.bme.mit.theta.common.logging.Logger -import hu.bme.mit.theta.core.model.Valuation -import hu.bme.mit.theta.solver.SolverFactory +import hu.bme.mit.theta.analysis.algorithm.mdd.MddProof import hu.bme.mit.theta.solver.SolverManager import hu.bme.mit.theta.solver.SolverPool import hu.bme.mit.theta.xsts.XSTS -import hu.bme.mit.theta.xsts.analysis.XstsAction -import hu.bme.mit.theta.xsts.analysis.hu.bme.mit.theta.xsts.analysis.toMonolithicExpr -import hu.bme.mit.theta.xsts.analysis.hu.bme.mit.theta.xsts.analysis.valToAction -import hu.bme.mit.theta.xsts.analysis.hu.bme.mit.theta.xsts.analysis.valToState import hu.bme.mit.theta.xsts.analysis.mdd.XstsMddChecker import java.util.concurrent.TimeUnit import kotlin.system.exitProcess @@ -53,7 +41,7 @@ class XstsCliMdd : XstsCliBaseCommand( help = "The state space enumeration algorithm to use" ).enum().default(MddChecker.IterationStrategy.GSAT) - private fun printResult(status: SafetyResult, xsts: XSTS, totalTimeMs: Long) { + private fun printResult(status: SafetyResult, xsts: XSTS, totalTimeMs: Long) { if (!outputOptions.benchmarkMode) return printCommonResult(status, xsts, totalTimeMs) val stats = status.stats.orElse(MddAnalysisStatistics(0, 0, 0, 0, 0)) as MddAnalysisStatistics diff --git a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/LazyXtaCheckerTest.java b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/LazyXtaCheckerTest.java index be1fc4afe0..a45b9b912c 100644 --- a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/LazyXtaCheckerTest.java +++ b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/LazyXtaCheckerTest.java @@ -18,10 +18,10 @@ import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; import hu.bme.mit.theta.analysis.Trace; +import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.arg.ARG; import hu.bme.mit.theta.analysis.algorithm.arg.ArgChecker; -import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; import hu.bme.mit.theta.analysis.unit.UnitPrec; import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; import hu.bme.mit.theta.xta.XtaSystem; @@ -106,7 +106,7 @@ public void test() { // Assert final ArgChecker argChecker = ArgChecker.create( Z3LegacySolverFactory.getInstance().createSolver()); - final boolean argCheckResult = argChecker.isWellLabeled(status.getWitness()); + final boolean argCheckResult = argChecker.isWellLabeled(status.getProof()); assertTrue(argCheckResult); } diff --git a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaAnalysisTest.java b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaAnalysisTest.java index 6bbc845a97..3e09a28404 100644 --- a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaAnalysisTest.java +++ b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaAnalysisTest.java @@ -15,18 +15,6 @@ */ package hu.bme.mit.theta.xta.analysis; -import java.io.FileNotFoundException; -import java.io.IOException; -import java.io.InputStream; -import java.util.Arrays; -import java.util.Collection; - -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; -import org.junit.runners.Parameterized.Parameter; -import org.junit.runners.Parameterized.Parameters; - import hu.bme.mit.theta.analysis.Analysis; import hu.bme.mit.theta.analysis.LTS; import hu.bme.mit.theta.analysis.algorithm.arg.ARG; @@ -40,6 +28,17 @@ import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter; import hu.bme.mit.theta.xta.XtaSystem; import hu.bme.mit.theta.xta.dsl.XtaDslManager; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.junit.runners.Parameterized.Parameter; +import org.junit.runners.Parameterized.Parameters; + +import java.io.FileNotFoundException; +import java.io.IOException; +import java.io.InputStream; +import java.util.Arrays; +import java.util.Collection; @RunWith(Parameterized.class) public final class XtaAnalysisTest { @@ -83,7 +82,7 @@ public void test() throws FileNotFoundException, IOException { argBuilder) .projection(s -> s.getLocs()).build(); - final ARG, XtaAction> arg = abstractor.createWitness(); + final ARG, XtaAction> arg = abstractor.createProof(); abstractor.check(arg, UnitPrec.getInstance()); System.out.println( diff --git a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaZoneAnalysisTest.java b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaZoneAnalysisTest.java index 111e451934..d02dba7ba7 100644 --- a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaZoneAnalysisTest.java +++ b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaZoneAnalysisTest.java @@ -15,19 +15,6 @@ */ package hu.bme.mit.theta.xta.analysis; -import java.io.FileNotFoundException; -import java.io.IOException; -import java.io.InputStream; -import java.util.Arrays; -import java.util.Collection; -import java.util.stream.Collectors; - -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; -import org.junit.runners.Parameterized.Parameter; -import org.junit.runners.Parameterized.Parameters; - import hu.bme.mit.theta.analysis.Analysis; import hu.bme.mit.theta.analysis.LTS; import hu.bme.mit.theta.analysis.algorithm.arg.ARG; @@ -46,6 +33,18 @@ import hu.bme.mit.theta.xta.analysis.expl.XtaExplAnalysis; import hu.bme.mit.theta.xta.analysis.zone.XtaZoneAnalysis; import hu.bme.mit.theta.xta.dsl.XtaDslManager; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.junit.runners.Parameterized.Parameter; +import org.junit.runners.Parameterized.Parameters; + +import java.io.FileNotFoundException; +import java.io.IOException; +import java.io.InputStream; +import java.util.Arrays; +import java.util.Collection; +import java.util.stream.Collectors; @RunWith(Parameterized.class) public final class XtaZoneAnalysisTest { @@ -94,7 +93,7 @@ public void test() throws FileNotFoundException, IOException { final ArgAbstractor>, XtaAction, ZonePrec> abstractor = BasicArgAbstractor .builder(argBuilder).projection(s -> s.getLocs()).build(); - final ARG>, XtaAction> arg = abstractor.createWitness(); + final ARG>, XtaAction> arg = abstractor.createProof(); abstractor.check(arg, prec); System.out.println(arg.getNodes().collect(Collectors.toSet())); diff --git a/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java b/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java index 4bf1694ff4..958386eac9 100644 --- a/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java +++ b/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java @@ -15,12 +15,9 @@ */ package hu.bme.mit.theta.xta.cli; -import java.io.*; - import com.beust.jcommander.JCommander; import com.beust.jcommander.Parameter; import com.beust.jcommander.ParameterException; - import hu.bme.mit.theta.analysis.Action; import hu.bme.mit.theta.analysis.State; import hu.bme.mit.theta.analysis.Trace; @@ -43,6 +40,8 @@ import hu.bme.mit.theta.xta.analysis.lazy.LazyXtaStatistics; import hu.bme.mit.theta.xta.dsl.XtaDslManager; +import java.io.*; + public final class XtaCli { private static final String JAR_NAME = "theta-xta.jar"; @@ -176,7 +175,7 @@ private void printError(final Throwable ex) { private void writeVisualStatus(final SafetyResult, ? extends Trace> status, final String filename) throws FileNotFoundException { final Graph graph = - status.isSafe() ? ArgVisualizer.getDefault().visualize(status.asSafe().getWitness()) + status.isSafe() ? ArgVisualizer.getDefault().visualize(status.asSafe().getProof()) : TraceVisualizer.getDefault().visualize(status.asUnsafe().getCex()); GraphvizWriter.getInstance().writeFile(graph, filename); }