Merge pull request #292 from RipplB/xsts-cli-clikt

Xsts cli clikt

build.gradle.kts

@@ -28,7 +28,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.4.0"
+    version = "6.5.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }
@@ -38,8 +38,10 @@ sonar {
         property("sonar.projectKey", "ftsrg_theta")
         property("sonar.organization", "ftsrg-github")
         property("sonar.host.url", "https://sonarcloud.io")
-        property("sonar.coverage.jacoco.xmlReportPaths",
-            "${project.layout.buildDirectory.asFile.get()}/reports/jacoco/jacocoRootReport/jacocoRootReport.xml")
+        property(
+            "sonar.coverage.jacoco.xmlReportPaths",
+            "${project.layout.buildDirectory.asFile.get()}/reports/jacoco/jacocoRootReport/jacocoRootReport.xml"
+        )
     }
 }
 

buildSrc/gradle.properties

@@ -38,4 +38,5 @@ deltaVersion=0.0.1
 deltaCollectionsVersion=0.0.1
 gsonVersion=2.9.1
 javasmtVersion=4.1.1
-sosylabVersion=0.3000-569-g89796f98
+sosylabVersion=0.3000-569-g89796f98
+cliktVersion=4.4.0

buildSrc/src/main/kotlin/Deps.kt

@@ -77,4 +77,6 @@ object Deps {
         val stdlib = "org.jetbrains.kotlin:kotlin-stdlib-jdk8:${Versions.kotlin}"
         val reflect = "org.jetbrains.kotlin:kotlin-reflect:${Versions.kotlin}"
     }
+
+    val clikt = "com.github.ajalt.clikt:clikt:${Versions.clikt}"
 }

buildSrc/src/main/kotlin/cli-tool.gradle.kts

@@ -19,4 +19,5 @@ dependencies {
     val implementation: Configuration by configurations
 
     implementation(Deps.jcommander)
+    implementation(Deps.clikt)
 }

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

@@ -15,9 +15,7 @@
  */
 package hu.bme.mit.theta.analysis.algorithm;
 
-import hu.bme.mit.theta.analysis.Action;
 import hu.bme.mit.theta.analysis.Cex;
-import hu.bme.mit.theta.analysis.State;
 import hu.bme.mit.theta.common.Utils;
 
 import java.util.Optional;
@@ -56,6 +54,10 @@ public static <W extends Witness, C extends Cex> Unsafe<W, C> unsafe(final C cex
         return new Unsafe<>(cex, witness, Optional.empty());
     }
 
+    public static <W extends Witness, C extends Cex> Unknown<W, C> unknown() {
+        return new Unknown<>();
+    }
+
     public static <W extends Witness, C extends Cex> Safe<W, C> safe(final W witness, final Statistics stats) {
         return new Safe<>(witness, Optional.of(stats));
     }
@@ -65,8 +67,8 @@ public static <W extends Witness, C extends Cex> Unsafe<W, C> unsafe(final C cex
         return new Unsafe<>(cex, witness, Optional.of(stats));
     }
 
-    public static <W extends Witness, C extends Cex> Unknown<W, C> unknown() {
-        return new Unknown<>();
+    public static <W extends Witness, C extends Cex> Unknown<W, C> unknown(final Statistics stats) {
+        return new Unknown<>(Optional.of(stats));
     }
 
     public abstract boolean isSafe();
@@ -154,6 +156,14 @@ public String toString() {
 
     public static final class Unknown<W extends Witness, C extends Cex> extends SafetyResult<W, C> {
 
+        public Unknown() {
+            super();
+        }
+
+        public Unknown(final Optional<Statistics> stats) {
+            super(null, stats);
+        }
+
         @Override
         public boolean isSafe() {
             return false;

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt

@@ -79,6 +79,7 @@ class BoundedChecker<S : ExprState, A : ExprAction> @JvmOverloads constructor(
     private val indices = mutableListOf(monolithicExpr.initOffsetIndex)
     private val exprs = mutableListOf<Expr<BoolType>>()
     private var kindLastIterLookup = 0
+    private var iteration = 0
 
     init {
         check(bmcSolver != itpSolver || bmcSolver == null) { "Use distinct solvers for BMC and IMC!" }
@@ -87,7 +88,8 @@ class BoundedChecker<S : ExprState, A : ExprAction> @JvmOverloads constructor(
     }
 
     override fun check(prec: UnitPrec?): SafetyResult<EmptyWitness, Trace<S, A>> {
-        var iteration = 0
+
+        iteration = 0
 
         val isBmcEnabled = bmcEnabled() // we don't allow per-iteration setting of bmc enabledness
         bmcSolver?.add(unfoldedInitExpr)
@@ -116,7 +118,7 @@ class BoundedChecker<S : ExprState, A : ExprAction> @JvmOverloads constructor(
                 itp()?.let { return it }
             }
         }
-        return SafetyResult.unknown()
+        return SafetyResult.unknown(BoundedStatistics(iteration))
     }
 
     private fun bmc(): SafetyResult<EmptyWitness, Trace<S, A>>? {
@@ -137,7 +139,7 @@ class BoundedChecker<S : ExprState, A : ExprAction> @JvmOverloads constructor(
 
             if (bmcSolver.check().isUnsat) {
                 logger.write(Logger.Level.MAINSTEP, "Safety proven in BMC step\n")
-                return SafetyResult.safe(EmptyWitness.getInstance())
+                return SafetyResult.safe(EmptyWitness.getInstance(), BoundedStatistics(iteration))
             }
         }
 
@@ -147,7 +149,7 @@ class BoundedChecker<S : ExprState, A : ExprAction> @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())
+                SafetyResult.unsafe(trace, EmptyWitness.getInstance(), BoundedStatistics(iteration))
             } else null
         }
     }
@@ -165,7 +167,7 @@ class BoundedChecker<S : ExprState, A : ExprAction> @JvmOverloads constructor(
 
             if (indSolver.check().isUnsat) {
                 logger.write(Logger.Level.MAINSTEP, "Safety proven in k-induction step\n")
-                SafetyResult.safe(EmptyWitness.getInstance())
+                SafetyResult.safe(EmptyWitness.getInstance(), BoundedStatistics(iteration))
             } else null
         }
     }
@@ -201,7 +203,7 @@ class BoundedChecker<S : ExprState, A : ExprAction> @JvmOverloads constructor(
                 itpSolver.pop()
                 itpSolver.pop()
                 logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC/BMC step\n")
-                return SafetyResult.safe(EmptyWitness.getInstance())
+                return SafetyResult.safe(EmptyWitness.getInstance(), BoundedStatistics(iteration))
             }
             itpSolver.pop()
         }
@@ -215,7 +217,7 @@ class BoundedChecker<S : ExprState, A : ExprAction> @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())
+            return SafetyResult.unsafe(trace, EmptyWitness.getInstance(), BoundedStatistics(iteration))
         }
 
         var img = unfoldedInitExpr
@@ -232,7 +234,7 @@ class BoundedChecker<S : ExprState, A : ExprAction> @JvmOverloads constructor(
                 logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC step\n")
                 itpSolver.pop()
                 itpSolver.pop()
-                return SafetyResult.safe(EmptyWitness.getInstance())
+                return SafetyResult.safe(EmptyWitness.getInstance(), BoundedStatistics(iteration))
             }
             itpSolver.pop()
             img = Or(img, itpFormula)

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedStatistics.kt

@@ -0,0 +1,27 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
+package hu.bme.mit.theta.analysis.algorithm.bounded
+
+import hu.bme.mit.theta.analysis.algorithm.Statistics
+
+class BoundedStatistics(val iterations: Int) : Statistics() {
+
+    init {
+        addStat("iterations", this::iterations)
+    }
+
+}

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java

@@ -25,6 +25,7 @@
 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;
@@ -133,27 +134,20 @@ public SafetyResult<MddWitness, MddCex> check(Void input) {
 
         logger.write(Level.INFO, "Created next-state node, starting fixed point calculation");
 
-        final MddHandle stateSpace;
-        final Cache cache;
+        final StateSpaceEnumerationProvider stateSpaceProvider;
         switch (iterationStrategy) {
             case BFS -> {
-                final var bfs = new BfsProvider(stateSig.getVariableOrder());
-                stateSpace = bfs.compute(MddNodeInitializer.of(initNode), nextStates, stateSig.getTopVariableHandle());
-                cache = bfs.getRelProdCache();
+                stateSpaceProvider = new BfsProvider(stateSig.getVariableOrder());
             }
             case SAT -> {
-                final var sat = new SimpleSaturationProvider(stateSig.getVariableOrder());
-                stateSpace = sat.compute(MddNodeInitializer.of(initNode), nextStates, stateSig.getTopVariableHandle());
-                cache = sat.getSaturateCache();
+                stateSpaceProvider = new SimpleSaturationProvider(stateSig.getVariableOrder());
             }
             case GSAT -> {
-                final var gsat = new GeneralizedSaturationProvider(stateSig.getVariableOrder());
-                stateSpace = gsat.compute(MddNodeInitializer.of(initNode), nextStates, stateSig.getTopVariableHandle());
-                cache = gsat.getSaturateCache();
-
+                stateSpaceProvider = new GeneralizedSaturationProvider(stateSig.getVariableOrder());
             }
             default -> throw new IllegalStateException("Unexpected value: " + iterationStrategy);
         }
+        final MddHandle stateSpace = stateSpaceProvider.compute(MddNodeInitializer.of(initNode), nextStates, stateSig.getTopVariableHandle());
 
         logger.write(Level.INFO, "Enumerated state-space");
 
@@ -170,7 +164,7 @@ public SafetyResult<MddWitness, MddCex> check(Void input) {
         final Long stateSpaceSize = MddInterpreter.calculateNonzeroCount(stateSpace);
         logger.write(Level.DETAIL, "State space size: " + stateSpaceSize);
 
-        final MddAnalysisStatistics statistics = new MddAnalysisStatistics(violatingSize, stateSpaceSize, cache.getHitCount(), cache.getQueryCount(), cache.getCacheSize());
+        final MddAnalysisStatistics statistics = new MddAnalysisStatistics(violatingSize, stateSpaceSize, stateSpaceProvider.getHitCount(), stateSpaceProvider.getQueryCount(), stateSpaceProvider.getCacheSize());
 
         final SafetyResult<MddWitness, MddCex> result;
         if (violatingSize != 0) {

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/BfsProvider.java

@@ -20,7 +20,7 @@
 
 import java.util.Optional;
 
-public final class BfsProvider implements MddTransformationProvider<AbstractNextStateDescriptor> {
+public final class BfsProvider implements StateSpaceEnumerationProvider {
     public static boolean verbose = false;
 
     private final CacheManager<BinaryOperationCache<MddNode, AbstractNextStateDescriptor, MddNode>> cacheManager = new CacheManager<>(
@@ -135,4 +135,19 @@ public void cleanup() {
     public Cache getRelProdCache() {
         return relProdProvider.getRelProdCache();
     }
+
+    @Override
+    public long getCacheSize() {
+        return getRelProdCache().getCacheSize();
+    }
+
+    @Override
+    public long getQueryCount() {
+        return getRelProdCache().getQueryCount();
+    }
+
+    @Override
+    public long getHitCount() {
+        return getRelProdCache().getHitCount();
+    }
 }

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/GeneralizedSaturationProvider.java

@@ -27,7 +27,7 @@
 import java.util.function.Consumer;
 import java.util.function.ToLongFunction;
 
-public final class GeneralizedSaturationProvider implements MddTransformationProvider<AbstractNextStateDescriptor> {
+public final class GeneralizedSaturationProvider implements StateSpaceEnumerationProvider {
     public static boolean verbose = false;
 
     private MddVariableOrder variableOrder;
@@ -48,6 +48,7 @@ public GeneralizedSaturationProvider(
         this.terminalZeroNode = variableOrder.getMddGraph().getTerminalZeroNode();
     }
 
+    @Override
     public MddHandle compute(
             AbstractNextStateDescriptor.Postcondition initializer,
             AbstractNextStateDescriptor nextStateRelation,
@@ -443,6 +444,7 @@ public void cleanup() {
     }
 
     private class Aggregator implements Consumer<SaturationCache> {
+
         public long result = 0;
         private final ToLongFunction<SaturationCache> extractor;
 
@@ -454,6 +456,7 @@ private Aggregator(final ToLongFunction<SaturationCache> extractor) {
         public void accept(final SaturationCache cache) {
             result += extractor.applyAsLong(cache);
         }
+
     }
 
     public Cache getSaturateCache() {
@@ -495,6 +498,7 @@ public long getHitCount() {
     }
 
     // TODO: HAXXXX DON'T DO THIS EVER AGAIN
+
     public Set<MddNode> getSaturatedNodes() {
         final Set<MddNode> ret = HashObjSets.newUpdatableSet();
         cacheManager.forEachCache((c) -> c.getSaturateCache().clearSelectively((source, ns, result) -> {
@@ -541,4 +545,19 @@ public long getHitCount() {
 
         return new RelProdCache(cacheManager);
     }
+
+    @Override
+    public long getCacheSize() {
+        return getSaturateCache().getCacheSize();
+    }
+
+    @Override
+    public long getQueryCount() {
+        return getSaturateCache().getQueryCount();
+    }
+
+    @Override
+    public long getHitCount() {
+        return getSaturateCache().getHitCount();
+    }
 }

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/SimpleSaturationProvider.java

@@ -28,7 +28,7 @@
 import java.util.function.Consumer;
 import java.util.function.ToLongFunction;
 
-public final class SimpleSaturationProvider implements MddTransformationProvider<AbstractNextStateDescriptor> {
+public final class SimpleSaturationProvider implements StateSpaceEnumerationProvider {
     public static boolean verbose = false;
 
     private MddVariableOrder variableOrder;
@@ -546,4 +546,19 @@ public long getHitCount() {
 
         return new RelProdCache(cacheManager);
     }
+
+    @Override
+    public long getCacheSize() {
+        return getSaturateCache().getCacheSize();
+    }
+
+    @Override
+    public long getQueryCount() {
+        return getSaturateCache().getQueryCount();
+    }
+
+    @Override
+    public long getHitCount() {
+        return getSaturateCache().getHitCount();
+    }
 }

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/StateSpaceEnumerationProvider.java

@@ -0,0 +1,23 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
+package hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint;
+
+import hu.bme.mit.delta.java.mdd.MddTransformationProvider;
+import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.AbstractNextStateDescriptor;
+
+public interface StateSpaceEnumerationProvider extends MddTransformationProvider.Cached<AbstractNextStateDescriptor>, MddTransformationProvider.Initializable<AbstractNextStateDescriptor, AbstractNextStateDescriptor.Postcondition> {
+}