Migrate XstsCli to Clikt

RipplB · Aug 2, 2024 · 94a5b12 · 94a5b12
1 parent 942d3ec
commit 94a5b12
Show file tree

Hide file tree

Showing 23 changed files with 962 additions and 54 deletions.
diff --git a/...nalysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/BfsProvider.java b/...nalysis/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 FixedPointEnumerationProvider {
     public static boolean verbose = false;
 
     private final CacheManager<BinaryOperationCache<MddNode, AbstractNextStateDescriptor, MddNode>> cacheManager = new CacheManager<>(
@@ -135,4 +135,14 @@ public void cleanup() {
     public Cache getRelProdCache() {
         return relProdProvider.getRelProdCache();
     }
+
+    @Override
+    public Cache getCache() {
+        return getRelProdCache();
+    }
+
+    @Override
+    public CacheManager<?> getCacheManager() {
+        return cacheManager;
+    }
 }
diff --git a/...ava/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/FixedPointEnumerationProvider.java b/...ava/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/FixedPointEnumerationProvider.java
@@ -0,0 +1,32 @@
+/*
+ *  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.*;
+import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.AbstractNextStateDescriptor;
+
+public interface FixedPointEnumerationProvider extends MddTransformationProvider<AbstractNextStateDescriptor> {
+    MddHandle compute(
+            AbstractNextStateDescriptor.Postcondition initializer,
+            AbstractNextStateDescriptor nextStateRelation,
+            MddVariableHandle highestAffectedVariable
+    );
+
+    Cache getCache();
+
+    CacheManager<?> getCacheManager();
+}
diff --git a/...ava/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/GeneralizedSaturationProvider.java b/...ava/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 FixedPointEnumerationProvider {
     public static boolean verbose = false;
 
     private MddVariableOrder variableOrder;
@@ -541,4 +541,14 @@ public long getHitCount() {
 
         return new RelProdCache(cacheManager);
     }
+
+    @Override
+    public Cache getCache() {
+        return getRelProdCache();
+    }
+
+    @Override
+    public CacheManager<?> getCacheManager() {
+        return cacheManager;
+    }
 }
diff --git a/...ain/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/SimpleSaturationProvider.java b/...ain/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 FixedPointEnumerationProvider {
     public static boolean verbose = false;
 
     private MddVariableOrder variableOrder;
@@ -546,4 +546,14 @@ public long getHitCount() {
 
         return new RelProdCache(cacheManager);
     }
+
+    @Override
+    public Cache getCache() {
+        return getRelProdCache();
+    }
+
+    @Override
+    public CacheManager<?> getCacheManager() {
+        return cacheManager;
+    }
 }
diff --git a/...ommon/src/main/java/hu/bme/mit/theta/common/visualization/writer/AbstractGraphWriter.java b/...ommon/src/main/java/hu/bme/mit/theta/common/visualization/writer/AbstractGraphWriter.java
@@ -15,12 +15,12 @@
  */
 package hu.bme.mit.theta.common.visualization.writer;
 
+import hu.bme.mit.theta.common.visualization.Graph;
+
 import java.io.File;
 import java.io.FileNotFoundException;
 import java.io.PrintWriter;
 
-import hu.bme.mit.theta.common.visualization.Graph;
-
 /**
  * Base class for writing graphs.
  */
@@ -33,17 +33,14 @@ public abstract class AbstractGraphWriter implements GraphWriter {
     public final void writeFile(final Graph graph, final String fileName)
             throws FileNotFoundException {
         final File file = new File(fileName);
-        PrintWriter printWriter = null;
-        try {
-            printWriter = new PrintWriter(file);
+        writeFile(graph, file);
+    }
+
+    public final void writeFile(final Graph graph, final File file)
+            throws FileNotFoundException {
+        try (PrintWriter printWriter = new PrintWriter(file)) {
             final String graphAsString = writeString(graph);
             printWriter.write(graphAsString);
-        } catch (final FileNotFoundException e) {
-            throw e;
-        } finally {
-            if (printWriter != null) {
-                printWriter.close();
-            }
         }
     }
 

diff --git a/...is/src/main/java/hu/bme/mit/theta/frontend/petrinet/analysis/VariableOrderingFactory.java b/...is/src/main/java/hu/bme/mit/theta/frontend/petrinet/analysis/VariableOrderingFactory.java
@@ -16,6 +16,7 @@
 package hu.bme.mit.theta.frontend.petrinet.analysis;
 
 import com.koloboke.collect.map.hash.HashObjObjMaps;
+import hu.bme.mit.theta.frontend.petrinet.model.Identified;
 import hu.bme.mit.theta.frontend.petrinet.model.PetriNet;
 import hu.bme.mit.theta.frontend.petrinet.model.Place;
 
@@ -28,11 +29,15 @@
 import java.util.stream.Collectors;
 
 public final class VariableOrderingFactory {
-    public static List<Place> fromFile(String orderingPath, PetriNet petriNet) throws Exception {
+    public static List<Place> fromPathString(String orderingPath, PetriNet petriNet) throws Exception {
         final File orderingFile = new File(orderingPath);
         if (!orderingFile.exists()) {
             throw new IOException("Cannot open ordering file: " + orderingPath);
         }
+        return fromFile(orderingFile, petriNet);
+    }
+
+    public static List<Place> fromFile(File orderingFile, PetriNet petriNet) throws Exception {
         List<String> orderingIds = Files.readAllLines(orderingFile.toPath());
         orderingIds.removeIf(s -> s.trim().isEmpty());
         if (orderingIds.size() != petriNet.getPlaces().size()) {
@@ -41,7 +46,7 @@ public static List<Place> fromFile(String orderingPath, PetriNet petriNet) throw
         Map<String, Place> placeIdMap = HashObjObjMaps.newImmutableMap(petriNet
                 .getPlaces()
                 .stream()
-                .collect(Collectors.toMap(p -> p.getId(), p -> p)));
+                .collect(Collectors.toMap(Identified::getId, p -> p)));
         final List<Place> ordering = new ArrayList<>(orderingIds.size());
         for (String s : orderingIds) {
             Place p = placeIdMap.get(s);

diff --git a/.../petrinet-analysis/src/test/java/hu/bme/mit/theta/frontend/petrinet/analysis/BfsTest.java b/.../petrinet-analysis/src/test/java/hu/bme/mit/theta/frontend/petrinet/analysis/BfsTest.java
@@ -48,7 +48,7 @@ public void testBfs() throws Exception {
 
         assertEquals(1, petriNets.size());
 
-        final List<Place> ordering = VariableOrderingFactory.fromFile(getClass().getResource(TestData.ORDERINGPATH).toURI().getPath(), petriNets.get(0));
+        final List<Place> ordering = VariableOrderingFactory.fromPathString(getClass().getResource(TestData.ORDERINGPATH).toURI().getPath(), petriNets.get(0));
         // 	ordering = new ArrayList<>(petriNets.get(0).getPlaces());
         // ordering.sort((p1, p2) -> String.CASE_INSENSITIVE_ORDER.compare(reverseString(p1.getId()),
         // 	reverseString(p2.getId())));

diff --git a/.../src/test/java/hu/bme/mit/theta/frontend/petrinet/analysis/GeneralizedSaturationTest.java b/.../src/test/java/hu/bme/mit/theta/frontend/petrinet/analysis/GeneralizedSaturationTest.java
@@ -22,8 +22,8 @@
 import hu.bme.mit.delta.mdd.LatticeDefinition;
 import hu.bme.mit.delta.mdd.MddInterpreter;
 import hu.bme.mit.delta.mdd.MddVariableDescriptor;
-import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.GeneralizedSaturationProvider;
 import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.CursorRelationalProductProvider;
+import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.GeneralizedSaturationProvider;
 import hu.bme.mit.theta.frontend.petrinet.model.PetriNet;
 import hu.bme.mit.theta.frontend.petrinet.model.Place;
 import hu.bme.mit.theta.frontend.petrinet.pnml.PetriNetParser;
@@ -48,7 +48,7 @@ public void testGS() throws Exception {
 
         assertEquals(1, petriNets.size());
 
-        final List<Place> ordering = VariableOrderingFactory.fromFile(getClass().getResource(TestData.ORDERINGPATH).toURI().getPath(), petriNets.get(0));
+        final List<Place> ordering = VariableOrderingFactory.fromPathString(getClass().getResource(TestData.ORDERINGPATH).toURI().getPath(), petriNets.get(0));
         // 	ordering = new ArrayList<>(petriNets.get(0).getPlaces());
         // ordering.sort((p1, p2) -> String.CASE_INSENSITIVE_ORDER.compare(reverseString(p1.getId()),
         // 	reverseString(p2.getId())));

diff --git a/...lysis/src/test/java/hu/bme/mit/theta/frontend/petrinet/analysis/SimpleSaturationTest.java b/...lysis/src/test/java/hu/bme/mit/theta/frontend/petrinet/analysis/SimpleSaturationTest.java
@@ -47,7 +47,7 @@ public void testSS() throws Exception {
         assertEquals(1, petriNets.size());
 
         final List<Place> ordering =
-                VariableOrderingFactory.fromFile(getClass().getResource(TestData.ORDERINGPATH).toURI().getPath(),
+                VariableOrderingFactory.fromPathString(getClass().getResource(TestData.ORDERINGPATH).toURI().getPath(),
                         petriNets.get(0));
         // 	ordering = new ArrayList<>(petriNets.get(0).getPlaces());
         // ordering.sort((p1, p2) -> String.CASE_INSENSITIVE_ORDER.compare(reverseString(p1.getId()),

diff --git a/...olver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/SmtLibSolverManager.java b/...olver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/SmtLibSolverManager.java
@@ -18,13 +18,7 @@
 import com.google.common.collect.ImmutableList;
 import hu.bme.mit.theta.common.Tuple2;
 import hu.bme.mit.theta.common.logging.Logger;
-import hu.bme.mit.theta.solver.HornSolver;
-import hu.bme.mit.theta.solver.ItpSolver;
-import hu.bme.mit.theta.solver.Solver;
-import hu.bme.mit.theta.solver.SolverBase;
-import hu.bme.mit.theta.solver.SolverFactory;
-import hu.bme.mit.theta.solver.SolverManager;
-import hu.bme.mit.theta.solver.UCSolver;
+import hu.bme.mit.theta.solver.*;
 import hu.bme.mit.theta.solver.smtlib.impl.bitwuzla.BitwuzlaSmtLibSolverInstaller;
 import hu.bme.mit.theta.solver.smtlib.impl.boolector.BoolectorSmtLibSolverInstaller;
 import hu.bme.mit.theta.solver.smtlib.impl.cvc4.CVC4SmtLibSolverInstaller;
@@ -43,17 +37,11 @@
 import java.lang.reflect.InvocationTargetException;
 import java.nio.file.Files;
 import java.nio.file.Path;
-import java.util.HashMap;
-import java.util.HashSet;
-import java.util.List;
-import java.util.Map;
-import java.util.Set;
+import java.util.*;
 import java.util.stream.Collectors;
 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.*;
 
 public final class SmtLibSolverManager extends SolverManager {
 
@@ -77,14 +65,12 @@ public final class SmtLibSolverManager extends SolverManager {
     }
 
     private final Path home;
-    private final Logger logger;
     private final Map<String, SmtLibSolverInstaller> installers;
     private final Tuple2<String, GenericSmtLibSolverInstaller> genericInstaller;
     private final Set<SolverBase> instantiatedSolvers;
     private boolean closed = false;
 
     private SmtLibSolverManager(final Path home, final Logger logger) {
-        this.logger = logger;
         checkNotNull(home);
         checkArgument(Files.exists(home), "Home directory does not exist");
 
@@ -160,8 +146,7 @@ private static String decodeSolverName(final String name, final int part) {
 
     public static SmtLibSolverManager create(final Path home, final Logger logger)
             throws IOException {
-        createIfNotExists(home);
-        return new SmtLibSolverManager(home, logger);
+        return new SmtLibSolverManager(createIfNotExists(home), logger);
     }
 
     private static Path createIfNotExists(final Path path) throws IOException {

diff --git a/...lver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3SolverManager.java b/...lver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3SolverManager.java
@@ -15,12 +15,7 @@
  */
 package hu.bme.mit.theta.solver.z3legacy;
 
-import hu.bme.mit.theta.solver.ItpSolver;
-import hu.bme.mit.theta.solver.Solver;
-import hu.bme.mit.theta.solver.SolverBase;
-import hu.bme.mit.theta.solver.SolverFactory;
-import hu.bme.mit.theta.solver.SolverManager;
-import hu.bme.mit.theta.solver.UCSolver;
+import hu.bme.mit.theta.solver.*;
 
 import java.util.HashSet;
 import java.util.Set;

diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3SolverManager.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3SolverManager.java
@@ -15,13 +15,7 @@
  */
 package hu.bme.mit.theta.solver.z3;
 
-import hu.bme.mit.theta.solver.HornSolver;
-import hu.bme.mit.theta.solver.ItpSolver;
-import hu.bme.mit.theta.solver.Solver;
-import hu.bme.mit.theta.solver.SolverBase;
-import hu.bme.mit.theta.solver.SolverFactory;
-import hu.bme.mit.theta.solver.SolverManager;
-import hu.bme.mit.theta.solver.UCSolver;
+import hu.bme.mit.theta.solver.*;
 
 import java.util.HashSet;
 import java.util.Set;

diff --git a/subprojects/xsts/xsts-cli/build.gradle.kts b/subprojects/xsts/xsts-cli/build.gradle.kts
@@ -27,11 +27,13 @@ dependencies {
     implementation(project(":theta-analysis"))
     implementation(project(":theta-core"))
     implementation(project(":theta-common"))
+    implementation(project(":theta-solver"))
     implementation(project(":theta-solver-z3-legacy"))
+    implementation(project(":theta-solver-z3"))
     implementation(project(":theta-solver-smtlib"))
-    implementation(project(":theta-solver"))
+    implementation(project(":theta-solver-javasmt"))
 }
 
 application {
-    mainClass.set("hu.bme.mit.theta.xsts.cli.XstsCli")
+    mainClass.set("hu.bme.mit.theta.xsts.cli.XstsCliMainKt")
 }