From 33b824064871d79cd2a7dfa49729db9b51f9abca Mon Sep 17 00:00:00 2001 From: RipplB Date: Fri, 2 Aug 2024 10:12:34 +0200 Subject: [PATCH] Migrate XstsCli to Clikt --- build.gradle.kts | 8 +- .../algorithm/mdd/fixedpoint/BfsProvider.java | 12 +- .../FixedPointEnumerationProvider.java | 32 + .../GeneralizedSaturationProvider.java | 12 +- .../fixedpoint/SimpleSaturationProvider.java | 12 +- .../writer/AbstractGraphWriter.java | 19 +- .../analysis/VariableOrderingFactory.java | 9 +- .../frontend/petrinet/analysis/BfsTest.java | 2 +- .../analysis/GeneralizedSaturationTest.java | 4 +- .../analysis/SimpleSaturationTest.java | 2 +- .../solver/smtlib/SmtLibSolverManager.java | 23 +- .../solver/z3legacy/Z3SolverManager.java | 7 +- .../mit/theta/solver/z3/Z3SolverManager.java | 8 +- subprojects/xsts/xsts-cli/build.gradle.kts | 6 +- .../hu/bme/mit/theta/xsts/cli/XstsCli.java | 998 ------------------ .../bme/mit/theta/xsts/cli/XstsMetrics.java | 49 - .../mit/theta/xsts/cli/XstsCliBaseCommand.kt | 92 ++ .../bme/mit/theta/xsts/cli/XstsCliBounded.kt | 133 +++ .../hu/bme/mit/theta/xsts/cli/XstsCliCegar.kt | 113 ++ .../bme/mit/theta/xsts/cli/XstsCliHeader.kt | 87 ++ .../hu/bme/mit/theta/xsts/cli/XstsCliMain.kt | 42 + .../hu/bme/mit/theta/xsts/cli/XstsCliMdd.kt | 184 ++++ .../bme/mit/theta/xsts/cli/XstsCliMetrics.kt | 69 ++ .../xsts/cli/optiongroup/InputOptions.kt | 63 ++ .../xsts/cli/optiongroup/OutputOptions.kt | 45 + .../PetrinetDependencyOutputOptions.kt | 38 + 26 files changed, 965 insertions(+), 1104 deletions(-) create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/FixedPointEnumerationProvider.java delete mode 100644 subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java delete mode 100644 subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsMetrics.java create mode 100644 subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBaseCommand.kt create mode 100644 subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBounded.kt create mode 100644 subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliCegar.kt create mode 100644 subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliHeader.kt create mode 100644 subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMain.kt create mode 100644 subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMdd.kt create mode 100644 subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMetrics.kt create mode 100644 subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/InputOptions.kt create mode 100644 subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/OutputOptions.kt create mode 100644 subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/PetrinetDependencyOutputOptions.kt diff --git a/build.gradle.kts b/build.gradle.kts index 966ef38137..994dfd4087 100644 --- a/build.gradle.kts +++ b/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" + ) } } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/BfsProvider.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/BfsProvider.java index 8214ca8712..924f0e2441 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/BfsProvider.java +++ b/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 { +public final class BfsProvider implements FixedPointEnumerationProvider { public static boolean verbose = false; private final CacheManager> 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/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/FixedPointEnumerationProvider.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/FixedPointEnumerationProvider.java new file mode 100644 index 0000000000..13beedeab9 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/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 { + MddHandle compute( + AbstractNextStateDescriptor.Postcondition initializer, + AbstractNextStateDescriptor nextStateRelation, + MddVariableHandle highestAffectedVariable + ); + + Cache getCache(); + + CacheManager getCacheManager(); +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/GeneralizedSaturationProvider.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/GeneralizedSaturationProvider.java index 69e650188e..cbbe2f88c4 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/GeneralizedSaturationProvider.java +++ b/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 { +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/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/SimpleSaturationProvider.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/SimpleSaturationProvider.java index adf4e47688..9f98756f89 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/SimpleSaturationProvider.java +++ b/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 { +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/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/visualization/writer/AbstractGraphWriter.java b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/visualization/writer/AbstractGraphWriter.java index 16b632e91a..00a133c923 100644 --- a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/visualization/writer/AbstractGraphWriter.java +++ b/subprojects/common/common/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/subprojects/frontends/petrinet-frontend/petrinet-analysis/src/main/java/hu/bme/mit/theta/frontend/petrinet/analysis/VariableOrderingFactory.java b/subprojects/frontends/petrinet-frontend/petrinet-analysis/src/main/java/hu/bme/mit/theta/frontend/petrinet/analysis/VariableOrderingFactory.java index 6c4654a470..15b1608336 100644 --- a/subprojects/frontends/petrinet-frontend/petrinet-analysis/src/main/java/hu/bme/mit/theta/frontend/petrinet/analysis/VariableOrderingFactory.java +++ b/subprojects/frontends/petrinet-frontend/petrinet-analysis/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 fromFile(String orderingPath, PetriNet petriNet) throws Exception { + public static List 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 fromFile(File orderingFile, PetriNet petriNet) throws Exception { List orderingIds = Files.readAllLines(orderingFile.toPath()); orderingIds.removeIf(s -> s.trim().isEmpty()); if (orderingIds.size() != petriNet.getPlaces().size()) { @@ -41,7 +46,7 @@ public static List fromFile(String orderingPath, PetriNet petriNet) throw Map placeIdMap = HashObjObjMaps.newImmutableMap(petriNet .getPlaces() .stream() - .collect(Collectors.toMap(p -> p.getId(), p -> p))); + .collect(Collectors.toMap(Identified::getId, p -> p))); final List ordering = new ArrayList<>(orderingIds.size()); for (String s : orderingIds) { Place p = placeIdMap.get(s); diff --git a/subprojects/frontends/petrinet-frontend/petrinet-analysis/src/test/java/hu/bme/mit/theta/frontend/petrinet/analysis/BfsTest.java b/subprojects/frontends/petrinet-frontend/petrinet-analysis/src/test/java/hu/bme/mit/theta/frontend/petrinet/analysis/BfsTest.java index 02bbb83780..2a89944cd9 100644 --- a/subprojects/frontends/petrinet-frontend/petrinet-analysis/src/test/java/hu/bme/mit/theta/frontend/petrinet/analysis/BfsTest.java +++ b/subprojects/frontends/petrinet-frontend/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 ordering = VariableOrderingFactory.fromFile(getClass().getResource(TestData.ORDERINGPATH).toURI().getPath(), petriNets.get(0)); + final List 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/subprojects/frontends/petrinet-frontend/petrinet-analysis/src/test/java/hu/bme/mit/theta/frontend/petrinet/analysis/GeneralizedSaturationTest.java b/subprojects/frontends/petrinet-frontend/petrinet-analysis/src/test/java/hu/bme/mit/theta/frontend/petrinet/analysis/GeneralizedSaturationTest.java index a802d0028d..8b1fb204f9 100644 --- a/subprojects/frontends/petrinet-frontend/petrinet-analysis/src/test/java/hu/bme/mit/theta/frontend/petrinet/analysis/GeneralizedSaturationTest.java +++ b/subprojects/frontends/petrinet-frontend/petrinet-analysis/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 ordering = VariableOrderingFactory.fromFile(getClass().getResource(TestData.ORDERINGPATH).toURI().getPath(), petriNets.get(0)); + final List 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/subprojects/frontends/petrinet-frontend/petrinet-analysis/src/test/java/hu/bme/mit/theta/frontend/petrinet/analysis/SimpleSaturationTest.java b/subprojects/frontends/petrinet-frontend/petrinet-analysis/src/test/java/hu/bme/mit/theta/frontend/petrinet/analysis/SimpleSaturationTest.java index a3c7cfb1fc..491c32c286 100644 --- a/subprojects/frontends/petrinet-frontend/petrinet-analysis/src/test/java/hu/bme/mit/theta/frontend/petrinet/analysis/SimpleSaturationTest.java +++ b/subprojects/frontends/petrinet-frontend/petrinet-analysis/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 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/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/SmtLibSolverManager.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/SmtLibSolverManager.java index 8f2499c012..5f408ea538 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/SmtLibSolverManager.java +++ b/subprojects/solver/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 installers; private final Tuple2 genericInstaller; private final Set 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/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3SolverManager.java b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3SolverManager.java index 421cd163f9..312f8424e2 100644 --- a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3SolverManager.java +++ b/subprojects/solver/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 index 890408b304..75a64916e2 100644 --- 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 index 1016451f40..b3a2eec787 100644 --- 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") } diff --git a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java deleted file mode 100644 index 3459a39cec..0000000000 --- a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java +++ /dev/null @@ -1,998 +0,0 @@ -/* - * 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.xsts.cli; - -import com.beust.jcommander.JCommander; -import com.beust.jcommander.Parameter; -import com.beust.jcommander.ParameterException; -import com.google.common.base.Preconditions; -import com.google.common.base.Stopwatch; -import com.koloboke.collect.set.hash.HashObjSets; -import hu.bme.mit.delta.collections.IntObjCursor; -import hu.bme.mit.delta.java.mdd.JavaMddFactory; -import hu.bme.mit.delta.java.mdd.MddHandle; -import hu.bme.mit.delta.java.mdd.MddNode; -import hu.bme.mit.delta.java.mdd.MddVariableOrder; -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.Action; -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.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.bounded.BoundedChecker; -import hu.bme.mit.theta.analysis.algorithm.bounded.BoundedCheckerBuilderKt; -import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr; -import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics; -import hu.bme.mit.theta.analysis.algorithm.chc.HornChecker; -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.analysis.algorithm.mdd.fixedpoint.BfsProvider; -import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.GeneralizedSaturationProvider; -import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.SimpleSaturationProvider; -import hu.bme.mit.theta.analysis.expl.ExplState; -import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy; -import hu.bme.mit.theta.analysis.utils.ArgVisualizer; -import hu.bme.mit.theta.analysis.utils.MddNodeVisualizer; -import hu.bme.mit.theta.analysis.utils.TraceVisualizer; -import hu.bme.mit.theta.common.CliUtils; -import hu.bme.mit.theta.common.OsHelper; -import hu.bme.mit.theta.common.logging.ConsoleLogger; -import hu.bme.mit.theta.common.logging.Logger; -import hu.bme.mit.theta.common.logging.NullLogger; -import hu.bme.mit.theta.common.table.BasicTableWriter; -import hu.bme.mit.theta.common.table.TableWriter; -import hu.bme.mit.theta.common.visualization.Graph; -import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter; -import hu.bme.mit.theta.frontend.petrinet.analysis.PtNetDependency2Gxl; -import hu.bme.mit.theta.frontend.petrinet.analysis.PtNetSystem; -import hu.bme.mit.theta.frontend.petrinet.analysis.VariableOrderingFactory; -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; -import hu.bme.mit.theta.frontend.petrinet.pnml.PnmlParseException; -import hu.bme.mit.theta.frontend.petrinet.pnml.XMLPnmlToPetrinet; -import hu.bme.mit.theta.frontend.petrinet.xsts.PetriNetToXSTS; -import hu.bme.mit.theta.solver.SolverFactory; -import hu.bme.mit.theta.solver.SolverManager; -import hu.bme.mit.theta.solver.SolverPool; -import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager; -import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; -import hu.bme.mit.theta.solver.z3legacy.Z3SolverManager; -import hu.bme.mit.theta.xsts.XSTS; -import hu.bme.mit.theta.xsts.analysis.XstsAction; -import hu.bme.mit.theta.xsts.analysis.XstsState; -import hu.bme.mit.theta.xsts.analysis.XstsToRelationsKt; -import hu.bme.mit.theta.xsts.analysis.concretizer.XstsStateSequence; -import hu.bme.mit.theta.xsts.analysis.concretizer.XstsTraceConcretizerUtil; -import hu.bme.mit.theta.xsts.analysis.config.XstsConfig; -import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder; -import hu.bme.mit.theta.xsts.analysis.hu.bme.mit.theta.xsts.analysis.XstsToMonolithicExprKt; -import hu.bme.mit.theta.xsts.analysis.mdd.XstsMddChecker; -import hu.bme.mit.theta.xsts.dsl.XstsDslManager; - -import javax.imageio.ImageIO; -import java.awt.image.BufferedImage; -import java.io.*; -import java.nio.file.Path; -import java.util.ArrayList; -import java.util.List; -import java.util.Set; -import java.util.concurrent.TimeUnit; -import java.util.stream.Stream; - -import static hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder.*; - -public class XstsCli { - - private static final String JAR_NAME = "theta-xsts-cli.jar"; - private final String[] args; - private final TableWriter writer; - - //////////// CONFIGURATION OPTIONS BEGIN //////////// - - //////////// input task //////////// - - @Parameter(names = {"--model"}, description = "Path of the input model (XSTS or Pnml)", required = true) - String model; - - @Parameter(names = {"--property"}, description = "Input property as a string or a file (*.prop)") - String property; - - @Parameter(names = "--id", description = "Id of the input model") - String id = ""; - - @Parameter(names = "--ordering", description = "Path of the input variable ordering") - String orderingPath; - - //////////// algorithm selection //////////// - - @Parameter(names = {"--algorithm"}, description = "Algorithm selection") - Algorithm algorithm = Algorithm.CEGAR; - - //////////// output data and statistics //////////// - - @Parameter(names = {"--loglevel"}, description = "Detailedness of logging") - Logger.Level logLevel = Logger.Level.SUBSTEP; - - @Parameter(names = {"--benchmark"}, description = "Benchmark mode (only print metrics)") - Boolean benchmarkMode = false; - - @Parameter(names = {"--cex"}, description = "Write concrete counterexample to a file") - String cexfile = null; - - @Parameter(names = {"--header"}, description = "Print only a header (for benchmarks)", help = true) - boolean headerOnly = false; - - @Parameter(names = "--metrics", description = "Print metrics about the XSTS without running the algorithm") - boolean metrics = false; - - @Parameter(names = "--stacktrace", description = "Print full stack trace in case of exception") - boolean stacktrace = false; - - @Parameter(names = "--version", description = "Display version", help = true) - boolean versionInfo = false; - - @Parameter(names = {"--visualize"}, description = "Write proof or counterexample to file in dot format") - String dotfile = null; - - //////////// CEGAR configuration options //////////// - - @Parameter(names = {"--domain"}, description = "Abstract domain") - Domain domain = Domain.PRED_CART; - - @Parameter(names = {"--refinement"}, description = "Refinement strategy") - Refinement refinement = Refinement.SEQ_ITP; - - @Parameter(names = {"--search"}, description = "Search strategy") - Search search = Search.BFS; - - @Parameter(names = {"--refinement-solver"}, description = "Refinement solver name") - String refinementSolver = "Z3"; - - @Parameter(names = {"--abstraction-solver"}, description = "Abstraction solver name") - String abstractionSolver = "Z3"; - - @Parameter(names = {"--smt-home"}, description = "The path of the solver registry") - String solverHome = SmtLibSolverManager.HOME.toAbsolutePath().toString(); - - @Parameter(names = "--no-stuck-check") - boolean noStuckCheck = false; - - @Parameter(names = {"--predsplit"}, description = "Predicate splitting") - PredSplit predSplit = PredSplit.WHOLE; - - @Parameter(names = {"--initialmarking"}, description = "Initial marking of the Petri net") - String initialMarking = ""; - - @Parameter(names = "--maxenum", description = "Maximal number of explicitly enumerated successors (0: unlimited)") - Integer maxEnum = 0; - - @Parameter(names = "--autoexpl", description = "Predicate to explicit switching strategy") - AutoExpl autoExpl = AutoExpl.NEWOPERANDS; - - @Parameter(names = {"--initprec"}, description = "Initial precision") - InitPrec initPrec = InitPrec.EMPTY; - - @Parameter(names = "--prunestrategy", description = "Strategy for pruning the ARG after refinement") - PruneStrategy pruneStrategy = PruneStrategy.LAZY; - - @Parameter(names = "--optimizestmts", description = "Turn statement optimization on or off") - OptimizeStmts optimizeStmts = OptimizeStmts.ON; - - //////////// symbolic configuration options //////////// - - @Parameter(names = "--iterationStrategy", description = "The state space generation algorithm to use (BFS, Saturation or " + - "GeneralizedSaturation)") - IterationStrategy iterationStrategy = IterationStrategy.GSAT; - - //////////// petri net output options //////////// - - @Parameter(names = "--depgxl", description = - "Generate GXL representation of (extended) dependency graph for variable ordering in the" + - " specified file") - String depGxl; - - @Parameter(names = "--depgxlgsat", description = - "Generate GXL representation of (extended) dependency graph for variable ordering in the" + - " specified file") - String depGxlGsat; - - @Parameter(names = "--depmat", - description = "Generate dependency matrix from the model as a CSV file to the specified path") - String depMat; - - @Parameter(names = "--depmatpng", - description = "Generate dependency matrix from the model as a PNG file to the specified path") - String depMatPng; - - //////////// CONFIGURATION OPTIONS END //////////// - - private Logger logger; - - public XstsCli(final String[] args) { - this.args = args; - writer = new BasicTableWriter(System.out, ",", "\"", "\""); - } - - public static void main(final String[] args) { - final XstsCli mainApp = new XstsCli(args); - mainApp.run(); - } - - private void run() { - - try { - JCommander.newBuilder().addObject(this).programName(JAR_NAME).build().parse(args); - logger = benchmarkMode ? NullLogger.getInstance() : new ConsoleLogger(logLevel); - } catch (final ParameterException ex) { - System.out.println("Invalid parameters, details:"); - System.out.println(ex.getMessage()); - ex.usage(); - return; - } - - if (headerOnly) { - printHeader(algorithm); - return; - } - - if (versionInfo) { - CliUtils.printVersion(System.out); - return; - } - - try { - - if (algorithm == Algorithm.CEGAR || algorithm == Algorithm.BMC || algorithm == Algorithm.KINDUCTION || algorithm == Algorithm.IMC || algorithm == Algorithm.CHC) { - runCegarOrBoundedAnalysis(); - } else if (algorithm == Algorithm.MDD) { - if (model.endsWith(".pnml")) { - runPetrinetMddAnalysis(); - } else { - runXstsMddAnalysis(); - } - } else { - throw new UnsupportedOperationException("Algorithm not supported: " + algorithm); - } - - } catch (final Throwable ex) { - printError(ex); - System.exit(1); - } - } - - private void runCegarOrBoundedAnalysis() throws Exception { - final Stopwatch sw = Stopwatch.createStarted(); - - final XSTS xsts = loadXSTSModel(); - - if (metrics) { - XstsMetrics.printMetrics(logger, xsts); - return; - } - - registerAllSolverManagers(solverHome, logger); - final SolverFactory abstractionSolverFactory = SolverManager.resolveSolverFactory(abstractionSolver); - final SolverFactory refinementSolverFactory = SolverManager.resolveSolverFactory(refinementSolver); - - final SafetyResult> status; - if (algorithm == Algorithm.CEGAR) { - final XstsConfig configuration = buildConfiguration(xsts, abstractionSolverFactory, refinementSolverFactory); - status = check(configuration); - } else if (algorithm == Algorithm.BMC || algorithm == Algorithm.KINDUCTION || algorithm == Algorithm.IMC) { - final BoundedChecker checker = buildBoundedChecker(xsts, abstractionSolverFactory); - status = checker.check(null); - } else if (algorithm == Algorithm.CHC) { - final SafetyChecker, ?> checker = buildHornChecker(xsts, abstractionSolverFactory); - status = checker.check(null); - } else { - throw new UnsupportedOperationException("Algorithm not supported: " + algorithm); - } - - sw.stop(); - printCegarOrBoundedResult(status, xsts, sw.elapsed(TimeUnit.MILLISECONDS)); - if (status.isUnsafe() && cexfile != null) { - writeCex(status.asUnsafe(), xsts); - } - if (dotfile != null && algorithm == Algorithm.CEGAR) { - writeVisualStatus((SafetyResult, ? extends Trace>) status, dotfile); - } - } - - private void runXstsMddAnalysis() throws Exception { - final Stopwatch sw = Stopwatch.createStarted(); - - final XSTS xsts = loadXSTSModel(); - - if (metrics) { - XstsMetrics.printMetrics(logger, xsts); - return; - } - - final MddChecker.IterationStrategy mddIterationStrategy; - switch (iterationStrategy) { - case BFS -> mddIterationStrategy = MddChecker.IterationStrategy.BFS; - case SAT -> mddIterationStrategy = MddChecker.IterationStrategy.SAT; - case GSAT -> mddIterationStrategy = MddChecker.IterationStrategy.GSAT; - default -> - throw new UnsupportedOperationException("Iteration strategy not supported: " + iterationStrategy); - } - - final SafetyResult status; - try (var solverPool = new SolverPool(Z3LegacySolverFactory.getInstance())) { - final XstsMddChecker checker = XstsMddChecker.create(xsts, solverPool, logger, mddIterationStrategy); - status = checker.check(null); - sw.stop(); - } - - printSymbolicResult(status, xsts, sw.elapsed(TimeUnit.MILLISECONDS)); - if (dotfile != null) { - writeXstsMddVisualStatus(status, dotfile); - } - } - - private void runPetrinetMddAnalysis() throws Exception { - final Stopwatch totalTimer = Stopwatch.createStarted(); - - final List petriNets = loadPetriNetModel(); - final List ordering = loadOrdering(petriNets); - - final PtNetSystem system = new PtNetSystem(petriNets.get(0), ordering); - - if (depGxl != null) { - createDepGxl(system); - } - - if (depGxlGsat != null) { - createDepGxlGSat(system); - } - - if (depMat != null) { - createDepMat(system); - } - - if (depMatPng != null) { - createDepMatPng(system); - } - - final MddVariableOrder variableOrder = JavaMddFactory.getDefault().createMddVariableOrder(LatticeDefinition.forSets()); - ordering.forEach(p -> variableOrder.createOnTop(MddVariableDescriptor.create(p))); - - final Stopwatch ssgTimer = Stopwatch.createStarted(); - - switch (iterationStrategy) { - // TODO: NODE COUNT IN MDD!!!! - case BFS: { - final BfsProvider bfs = new BfsProvider(variableOrder); - - final MddHandle stateSpace = bfs.compute(system.getInitializer(), - system.getTransitions(), - variableOrder.getDefaultSetSignature().getTopVariableHandle() - ); - - ssgTimer.stop(); - totalTimer.stop(); - - printSymbolicResult(writer, - variableOrder, - system, - stateSpace, - bfs, - totalTimer.elapsed(TimeUnit.MICROSECONDS), - ssgTimer.elapsed(TimeUnit.MICROSECONDS) - ); - } - break; - case SAT: { - final SimpleSaturationProvider ss = new SimpleSaturationProvider(variableOrder); - - final MddHandle stateSpace = ss.compute(system.getInitializer(), - system.getTransitions(), - variableOrder.getDefaultSetSignature().getTopVariableHandle() - ); - - ssgTimer.stop(); - totalTimer.stop(); - - printSymbolicResult(writer, - variableOrder, - system, - stateSpace, - ss, - totalTimer.elapsed(TimeUnit.MICROSECONDS), - ssgTimer.elapsed(TimeUnit.MICROSECONDS) - ); - } - break; - case GSAT: { - final GeneralizedSaturationProvider gs = new GeneralizedSaturationProvider(variableOrder); - - final MddHandle stateSpace = gs.compute(system.getInitializer(), - system.getTransitions(), - variableOrder.getDefaultSetSignature().getTopVariableHandle() - ); - - ssgTimer.stop(); - totalTimer.stop(); - - printSymbolicResult(writer, - variableOrder, - system, - stateSpace, - gs, - totalTimer.elapsed(TimeUnit.MICROSECONDS), - ssgTimer.elapsed(TimeUnit.MICROSECONDS) - ); - } - break; - - } - } - - private SafetyResult, ? extends Trace> check(XstsConfig configuration) throws Exception { - try { - return configuration.check(); - } catch (final Exception ex) { - String message = ex.getMessage() == null ? "(no message)" : ex.getMessage(); - throw new Exception("Error while running algorithm: " + ex.getClass().getSimpleName() + " " + message, ex); - } - } - - private void printHeader(Algorithm algorithm) { - if (algorithm == Algorithm.CEGAR) { - printCegarHeader(); - } else { - printSymbolicHeader(); - } - } - - private void printCegarHeader() { - Stream.of("Result", "TimeMs", "AlgoTimeMs", "AbsTimeMs", "RefTimeMs", "Iterations", - "ArgSize", "ArgDepth", "ArgMeanBranchFactor", "CexLen", "Vars").forEach(writer::cell); - writer.newRow(); - } - - // TODO: NODE COUNT IN MDD!!!! - private void printSymbolicHeader() { - switch (iterationStrategy) { - case BFS: - writer.cell("id"); - writer.cell("modelPath"); - writer.cell("modelName"); - writer.cell("stateSpaceSize"); - writer.cell("finalMddSize"); - writer.cell("totalTimeUs"); - writer.cell("ssgTimeUs"); - writer.cell("nodeCount"); - writer.cell("unionCacheSize"); - writer.cell("unionQueryCount"); - writer.cell("unionHitCount"); - writer.cell("relProdCacheSize"); - writer.cell("relProdQueryCount"); - writer.cell("relProdHitCount"); - writer.newRow(); - break; - case SAT: - case GSAT: - writer.cell("id"); - writer.cell("modelPath"); - writer.cell("modelName"); - writer.cell("stateSpaceSize"); - writer.cell("finalMddSize"); - writer.cell("totalTimeUs"); - writer.cell("ssgTimeUs"); - writer.cell("nodeCount"); - writer.cell("unionCacheSize"); - writer.cell("unionQueryCount"); - writer.cell("unionHitCount"); - writer.cell("saturateCacheSize"); - writer.cell("saturateQueryCount"); - writer.cell("saturateHitCount"); - writer.cell("relProdCacheSize"); - writer.cell("relProdQueryCount"); - writer.cell("relProdHitCount"); - writer.cell("saturatedNodeCount"); - writer.newRow(); - break; - } - } - - private XSTS loadXSTSModel() throws Exception { - InputStream propStream = null; - Preconditions.checkNotNull(property, "No property defined. Did you select the correct algorithm? (Default is CEGAR)"); - try { - if (property.endsWith(".prop")) propStream = new FileInputStream(property); - else propStream = new ByteArrayInputStream(("prop { " + property + " }").getBytes()); - - if (model.endsWith(".pnml")) { - final PetriNet petriNet = XMLPnmlToPetrinet.parse(model, initialMarking); - return PetriNetToXSTS.createXSTS(petriNet, propStream); - } else { - - try (SequenceInputStream inputStream = new SequenceInputStream(new FileInputStream(model), propStream)) { - return XstsDslManager.createXsts(inputStream); - } - } - - } catch (Exception ex) { - throw new Exception("Could not parse XSTS: " + ex.getMessage(), ex); - } finally { - if (propStream != null) propStream.close(); - } - } - - private List loadPetriNetModel() throws Exception { - final File pnmlFile = new File(model); - final List petriNets; - try { - petriNets = PetriNetParser.loadPnml(pnmlFile).parsePTNet(); - } catch (PnmlParseException e) { - throw new Exception("Invalid PNML: " + e.getMessage()); - } catch (Exception e) { - throw new Exception("An error occured while loading the modelPath: " + e.getMessage()); - } - - if (petriNets.isEmpty()) { - throw new Exception("No Petri net found in the PNML document."); - } - - return petriNets; - } - - private List loadOrdering(final List petriNets) throws Exception { - final List ordering; - if (orderingPath == null) { - logger.write(Logger.Level.INFO, "[WARNING] No ordering specified, using default order."); - ordering = new ArrayList<>(petriNets.get(0).getPlaces()); - ordering.sort((p1, p2) -> String.CASE_INSENSITIVE_ORDER.compare(reverseString(p1.getId()), - reverseString(p2.getId()) - )); - } else { - try { - ordering = VariableOrderingFactory.fromFile(orderingPath, petriNets.get(0)); - } catch (IOException e) { - throw new Exception("Error reading ordering file: " + e.getMessage()); - } catch (Exception e) { - throw new Exception(e.getMessage()); - } - } - return ordering; - } - - private XstsConfig buildConfiguration(final XSTS xsts, final SolverFactory abstractionSolverFactory, final SolverFactory refinementSolverFactory) throws Exception { - // set up stopping analysis if it is stuck on same ARGs and precisions - //if (noStuckCheck) { - //ArgCexCheckHandler.instance.setArgCexCheck(false, false); - //} else { - //ArgCexCheckHandler.instance.setArgCexCheck(true, refinement.equals(Refinement.MULTI_SEQ)); - // } - - try { - return new XstsConfigBuilder(domain, refinement, abstractionSolverFactory, refinementSolverFactory) - .maxEnum(maxEnum).autoExpl(autoExpl).initPrec(initPrec).pruneStrategy(pruneStrategy) - .search(search).predSplit(predSplit).optimizeStmts(optimizeStmts).logger(logger).build(xsts); - } catch (final Exception ex) { - throw new Exception("Could not create configuration: " + ex.getMessage(), ex); - } - } - - private BoundedChecker buildBoundedChecker(final XSTS xsts, final SolverFactory abstractionSolverFactory) { - final MonolithicExpr monolithicExpr = XstsToMonolithicExprKt.toMonolithicExpr(xsts); - final BoundedChecker checker; - switch (algorithm) { - case BMC -> checker = BoundedCheckerBuilderKt.buildBMC( - monolithicExpr, - abstractionSolverFactory.createSolver(), - val -> XstsToMonolithicExprKt.valToState(xsts, val), - (val1, val2) -> XstsToMonolithicExprKt.valToAction(xsts, val1, val2), - logger - ); - case KINDUCTION -> checker = BoundedCheckerBuilderKt.buildKIND( - monolithicExpr, - abstractionSolverFactory.createSolver(), - abstractionSolverFactory.createSolver(), - val -> XstsToMonolithicExprKt.valToState(xsts, val), - (val1, val2) -> XstsToMonolithicExprKt.valToAction(xsts, val1, val2), - logger - ); - case IMC -> checker = BoundedCheckerBuilderKt.buildIMC( - monolithicExpr, - abstractionSolverFactory.createSolver(), - abstractionSolverFactory.createItpSolver(), - val -> XstsToMonolithicExprKt.valToState(xsts, val), - (val1, val2) -> XstsToMonolithicExprKt.valToAction(xsts, val1, val2), - logger - ); - default -> - throw new UnsupportedOperationException("Algorithm " + algorithm + " not supported"); - } - return checker; - } - - private SafetyChecker, ?> buildHornChecker(final XSTS xsts, final SolverFactory abstractionSolverFactory) { - final var checker = new HornChecker( - XstsToRelationsKt.toRelations(xsts), - abstractionSolverFactory, - logger - ); - return (SafetyChecker, Void>) prec -> { - final var result = checker.check(null); - if (result.isSafe()) { - return SafetyResult.safe(EmptyWitness.getInstance()); - } else if (result.isUnsafe()) { - // TODO: create trace from proof - return SafetyResult.unsafe(Trace.of( - List.of(XstsState.of(ExplState.top(), false, false)), - List.of() - ), EmptyWitness.getInstance()); - } else { - return SafetyResult.unknown(); - } - }; - } - - private void printCegarOrBoundedResult(final SafetyResult> status, final XSTS sts, final long totalTimeMs) { - final CegarStatistics stats = (CegarStatistics) - status.getStats().orElse(new CegarStatistics(0, 0, 0, 0)); - if (benchmarkMode) { - writer.cell(status.isSafe()); - writer.cell(totalTimeMs); - writer.cell(stats.getAlgorithmTimeMs()); - writer.cell(stats.getAbstractorTimeMs()); - writer.cell(stats.getRefinerTimeMs()); - writer.cell(stats.getIterations()); - if (status.getWitness() instanceof ARG arg) { - writer.cell(arg.size()); - writer.cell(arg.getDepth()); - writer.cell(arg.getMeanBranchingFactor()); - } else { - writer.cell(""); - writer.cell(""); - writer.cell(""); - } - if (status.isUnsafe()) { - writer.cell(status.asUnsafe().getCex().length() + ""); - } else { - writer.cell(""); - } - writer.cell(sts.getVars().size()); - writer.newRow(); - } - } - - private void printSymbolicResult(final SafetyResult status, final XSTS sts, final long totalTimeMs) { - final MddAnalysisStatistics stats = (MddAnalysisStatistics) - status.getStats().orElse(new MddAnalysisStatistics(0L, 0L, 0L, 0L, 0L)); - if (benchmarkMode) { - writer.cell(status.isSafe()); - writer.cell(totalTimeMs); - writer.cell(status.getWitness().size()); - writer.cell(stats.getViolatingSize()); - writer.cell(stats.getStateSpaceSize()); - writer.cell(stats.getHitCount()); - writer.cell(stats.getQueryCount()); - writer.cell(stats.getCacheSize()); - if (status.isUnsafe()) { - writer.cell(status.asUnsafe().getCex().length() + ""); - } else { - writer.cell(""); - } - writer.cell(sts.getVars().size()); - writer.newRow(); - } - } - - private void printSymbolicResult( - TableWriter writer, - MddVariableOrder variableOrder, - PtNetSystem system, - MddHandle result, - GeneralizedSaturationProvider provider, - long totalTime, - long ssgTime - ) { - String id = this.id; - String modelPath = this.model; - String modelName = system.getName(); - - Long stateSpaceSize = MddInterpreter.calculateNonzeroCount(result); - long nodeCount = variableOrder.getMddGraph().getUniqueTableSize(); - - long unionCacheSize = variableOrder.getDefaultUnionProvider().getCacheSize(); - long unionQueryCount = variableOrder.getDefaultUnionProvider().getQueryCount(); - long unionHitCount = variableOrder.getDefaultUnionProvider().getHitCount(); - - long saturateCacheSize = provider.getSaturateCache().getCacheSize(); - long saturateQueryCount = provider.getSaturateCache().getQueryCount(); - long saturateHitCount = provider.getSaturateCache().getHitCount(); - - long relProdCacheSize = provider.getSaturateCache().getCacheSize(); - long relProdQueryCount = provider.getSaturateCache().getQueryCount(); - long relProdHitCount = provider.getSaturateCache().getHitCount(); - - final Set nodes = MddNodeCollector.collectNodes(result); - long finalMddSize = nodes.size(); - - final Set saturatedNodes = provider.getSaturatedNodes(); - long saturatedNodeCount = saturatedNodes.size() + 2; - - writer.cell(id); - writer.cell(modelPath); - writer.cell(modelName); - writer.cell(stateSpaceSize); - writer.cell(finalMddSize); - writer.cell(totalTime); - writer.cell(ssgTime); - writer.cell(nodeCount); - writer.cell(unionCacheSize); - writer.cell(unionQueryCount); - writer.cell(unionHitCount); - writer.cell(saturateCacheSize); - writer.cell(saturateQueryCount); - writer.cell(saturateHitCount); - writer.cell(relProdCacheSize); - writer.cell(relProdQueryCount); - writer.cell(relProdHitCount); - writer.cell(saturatedNodeCount); - writer.newRow(); - } - - private void printSymbolicResult( - TableWriter writer, - MddVariableOrder variableOrder, - PtNetSystem system, - MddHandle result, - SimpleSaturationProvider provider, - long totalTime, - long ssgTime - ) { - String id = this.id; - String modelPath = this.model; - String modelName = system.getName(); - - Long stateSpaceSize = MddInterpreter.calculateNonzeroCount(result); - long nodeCount = variableOrder.getMddGraph().getUniqueTableSize(); - - long unionCacheSize = variableOrder.getDefaultUnionProvider().getCacheSize(); - long unionQueryCount = variableOrder.getDefaultUnionProvider().getQueryCount(); - long unionHitCount = variableOrder.getDefaultUnionProvider().getHitCount(); - - long saturateCacheSize = provider.getSaturateCache().getCacheSize(); - long saturateQueryCount = provider.getSaturateCache().getQueryCount(); - long saturateHitCount = provider.getSaturateCache().getHitCount(); - - long relProdCacheSize = provider.getSaturateCache().getCacheSize(); - long relProdQueryCount = provider.getSaturateCache().getQueryCount(); - long relProdHitCount = provider.getSaturateCache().getHitCount(); - - - final Set nodes = MddNodeCollector.collectNodes(result); - long finalMddSize = nodes.size(); - - final Set saturatedNodes = provider.getSaturatedNodes(); - long saturatedNodeCount = saturatedNodes.size() + 2; - - writer.cell(id); - writer.cell(modelPath); - writer.cell(modelName); - writer.cell(stateSpaceSize); - writer.cell(finalMddSize); - writer.cell(totalTime); - writer.cell(ssgTime); - writer.cell(nodeCount); - writer.cell(unionCacheSize); - writer.cell(unionQueryCount); - writer.cell(unionHitCount); - writer.cell(saturateCacheSize); - writer.cell(saturateQueryCount); - writer.cell(saturateHitCount); - writer.cell(relProdCacheSize); - writer.cell(relProdQueryCount); - writer.cell(relProdHitCount); - writer.cell(saturatedNodeCount); - writer.newRow(); - } - - private void printSymbolicResult( - TableWriter writer, - MddVariableOrder variableOrder, - PtNetSystem system, - MddHandle result, - BfsProvider provider, - long totalTime, - long ssgTime - ) { - String id = this.id; - String modelPath = this.model; - String modelName = system.getName(); - - Long stateSpaceSize = MddInterpreter.calculateNonzeroCount(result); - long nodeCount = variableOrder.getMddGraph().getUniqueTableSize(); - - long unionCacheSize = variableOrder.getDefaultUnionProvider().getCacheSize(); - long unionQueryCount = variableOrder.getDefaultUnionProvider().getQueryCount(); - long unionHitCount = variableOrder.getDefaultUnionProvider().getHitCount(); - - long relProdCacheSize = provider.getRelProdCache().getCacheSize(); - long relProdQueryCount = provider.getRelProdCache().getQueryCount(); - long relProdHitCount = provider.getRelProdCache().getHitCount(); - - final Set nodes = MddNodeCollector.collectNodes(result); - long finalMddSize = nodes.size(); - - writer.cell(id); - writer.cell(modelPath); - writer.cell(modelName); - writer.cell(stateSpaceSize); - writer.cell(finalMddSize); - writer.cell(totalTime); - writer.cell(ssgTime); - writer.cell(nodeCount); - writer.cell(unionCacheSize); - writer.cell(unionQueryCount); - writer.cell(unionHitCount); - writer.cell(relProdCacheSize); - writer.cell(relProdQueryCount); - writer.cell(relProdHitCount); - writer.newRow(); - } - - private void printError(final Throwable ex) { - final String message = ex.getMessage() == null ? "" : ex.getMessage(); - if (benchmarkMode) { - writer.cell("[EX] " + ex.getClass().getSimpleName() + ": " + message); - writer.newRow(); - } else { - logger.write(Logger.Level.RESULT, "%s occurred, message: %s%n", ex.getClass().getSimpleName(), message); - if (stacktrace) { - final StringWriter errors = new StringWriter(); - ex.printStackTrace(new PrintWriter(errors)); - logger.write(Logger.Level.RESULT, "Trace:%n%s%n", errors.toString()); - } else { - logger.write(Logger.Level.RESULT, "Use --stacktrace for stack trace%n"); - } - } - } - - private void writeCex(final SafetyResult.Unsafe status, final XSTS xsts) throws FileNotFoundException { - - @SuppressWarnings("unchecked") final Trace, XstsAction> trace = (Trace, XstsAction>) status.getCex(); - final XstsStateSequence concrTrace = XstsTraceConcretizerUtil.concretize(trace, Z3LegacySolverFactory.getInstance(), xsts); - final File file = new File(cexfile); - try (PrintWriter printWriter = new PrintWriter(file)) { - printWriter.write(concrTrace.toString()); - } - } - - private void writeXstsMddVisualStatus(final SafetyResult status, final String filename) - throws FileNotFoundException { - final Graph graph = status.isSafe() ? MddNodeVisualizer.create().visualize(status.asSafe().getWitness().getMdd().getNode()) - : MddNodeVisualizer.create().visualize(status.asUnsafe().getCex().getMdd().getNode()); - GraphvizWriter.getInstance().writeFile(graph, filename); - } - - private void writeVisualStatus(final SafetyResult, ? extends Trace> status, final String filename) - throws FileNotFoundException { - final Graph graph = status.isSafe() ? ArgVisualizer.getDefault().visualize(status.asSafe().getWitness()) - : TraceVisualizer.getDefault().visualize(status.asUnsafe().getCex()); - GraphvizWriter.getInstance().writeFile(graph, filename); - } - - private static String reverseString(String str) { - StringBuilder sb = new StringBuilder(str); - sb.reverse(); - return sb.toString(); - } - - private static class MddNodeCollector { - public static Set collectNodes(MddHandle root) { - Set ret = HashObjSets.newUpdatableSet(); - collect(root.getNode(), ret); - return ret; - } - - private static void collect(MddNode node, Set result) { - if (!result.add(node)) { - return; - } - - if (!node.isTerminal()) { - for (IntObjCursor c = node.cursor(); c.moveNext(); ) { - collect(c.value(), result); - } - } - } - } - - private void createDepGxl(PtNetSystem system) throws Exception { - try { - final File gxlFile = new File(depGxl); - if (!gxlFile.exists()) { - gxlFile.createNewFile(); - } - final PrintStream gxlOutput = new PrintStream(gxlFile); - - // TODO: this would be better with the PetriNet file only. - gxlOutput.print(PtNetDependency2Gxl.toGxl(system, false)); - gxlOutput.close(); - } catch (IOException e) { - throw new Exception("Error creating GXL file: " + e.getMessage()); - } - } - - private void createDepGxlGSat(PtNetSystem system) throws Exception { - try { - final File gxlFile = new File(depGxlGsat); - if (!gxlFile.exists()) { - gxlFile.createNewFile(); - } - final PrintStream gxlOutput = new PrintStream(gxlFile); - - // TODO: this would be better with the PetriNet file only. - gxlOutput.print(PtNetDependency2Gxl.toGxl(system, true)); - gxlOutput.close(); - } catch (IOException e) { - throw new Exception("Error creating GXL file: " + e.getMessage()); - } - } - - private void createDepMat(PtNetSystem system) throws Exception { - try { - final File depMatFile = new File(depMat); - if (!depMatFile.exists()) { - depMatFile.createNewFile(); - } - final PrintStream depMatOutput = new PrintStream(depMatFile); - - // TODO: this would be better with the PetriNet file only. - depMatOutput.print(system.printDependencyMatrixCsv()); - depMatOutput.close(); - } catch (IOException e) { - throw new Exception("Error creating dependency matrix file: " + e.getMessage()); - } - } - - private void createDepMatPng(PtNetSystem system) throws Exception { - if (system.getPlaceCount() < 10000 && system.getTransitionCount() < 10000) { - try { - final BufferedImage image = system.dependencyMatrixImage(1); - ImageIO.write(image, "PNG", new File(depMatPng)); - } catch (IOException e) { - throw new Exception("Error creating dependency matrix file: " + e.getMessage()); - } - } else { - logger.write(Logger.Level.INFO, "[WARNING] Skipping image generation because the model size exceeds 10k places or " + - "transitions."); - } - } - - - private void registerAllSolverManagers(String home, Logger logger) throws Exception { - SolverManager.closeAll(); - SolverManager.registerSolverManager(Z3SolverManager.create()); - if (OsHelper.getOs() == OsHelper.OperatingSystem.LINUX) { - SmtLibSolverManager smtLibSolverManager = SmtLibSolverManager.create(Path.of(home), logger); - SolverManager.registerSolverManager(smtLibSolverManager); - } - } - -} diff --git a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsMetrics.java b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsMetrics.java deleted file mode 100644 index d249c6de11..0000000000 --- a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsMetrics.java +++ /dev/null @@ -1,49 +0,0 @@ -/* - * 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.xsts.cli; - -import hu.bme.mit.theta.common.logging.Logger; -import hu.bme.mit.theta.core.type.arraytype.ArrayType; -import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.core.type.bvtype.BvType; -import hu.bme.mit.theta.core.type.inttype.IntType; -import hu.bme.mit.theta.core.utils.StmtCounterVisitor; -import hu.bme.mit.theta.xsts.XSTS; - -public final class XstsMetrics { - - private XstsMetrics() { - } - - public static void printMetrics(Logger logger, XSTS xsts) { - logger.write(Logger.Level.RESULT, "Vars: %s%n", xsts.getVars().size()); - logger.write(Logger.Level.RESULT, " Bool vars: %s%n", - xsts.getVars().stream().filter(v -> v.getType() instanceof BoolType).count()); - logger.write(Logger.Level.RESULT, " Int vars: %s%n", - xsts.getVars().stream().filter(v -> v.getType() instanceof IntType).count()); - logger.write(Logger.Level.RESULT, " Bitvector vars: %s%n", - xsts.getVars().stream().filter(v -> v.getType() instanceof BvType).count()); - logger.write(Logger.Level.RESULT, " Array vars: %s%n", - xsts.getVars().stream().filter(v -> v.getType() instanceof ArrayType).count()); - logger.write(Logger.Level.RESULT, " Ctrl vars: %s%n", xsts.getCtrlVars().size()); - logger.write(Logger.Level.RESULT, "Tran statements: %s%n", - xsts.getTran().accept(StmtCounterVisitor.getInstance(), null)); - logger.write(Logger.Level.RESULT, "Env statements: %s%n", - xsts.getEnv().accept(StmtCounterVisitor.getInstance(), null)); - logger.write(Logger.Level.RESULT, "Init statements: %s%n", - xsts.getInit().accept(StmtCounterVisitor.getInstance(), null)); - } -} diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBaseCommand.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBaseCommand.kt new file mode 100644 index 0000000000..6dd838af9c --- /dev/null +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBaseCommand.kt @@ -0,0 +1,92 @@ +/* + * 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.xsts.cli + +import com.github.ajalt.clikt.core.CliktCommand +import com.github.ajalt.clikt.parameters.groups.provideDelegate +import com.github.ajalt.clikt.parameters.options.default +import com.github.ajalt.clikt.parameters.options.option +import com.github.ajalt.clikt.parameters.options.versionOption +import com.github.ajalt.clikt.parameters.types.file +import hu.bme.mit.theta.analysis.Trace +import hu.bme.mit.theta.analysis.algorithm.SafetyResult +import hu.bme.mit.theta.common.logging.ConsoleLogger +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.common.logging.NullLogger +import hu.bme.mit.theta.common.table.BasicTableWriter +import hu.bme.mit.theta.solver.SolverManager +import hu.bme.mit.theta.solver.javasmt.JavaSMTSolverManager +import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager +import hu.bme.mit.theta.xsts.XSTS +import hu.bme.mit.theta.xsts.analysis.XstsAction +import hu.bme.mit.theta.xsts.analysis.XstsState +import hu.bme.mit.theta.xsts.analysis.concretizer.XstsTraceConcretizerUtil +import hu.bme.mit.theta.xsts.cli.optiongroup.InputOptions +import hu.bme.mit.theta.xsts.cli.optiongroup.OutputOptions +import java.io.File +import java.io.PrintWriter + +abstract class XstsCliBaseCommand(name: String? = null, help: String = "") : + CliktCommand(name = name, help = help, printHelpOnEmptyArgs = true) { + + init { + versionOption(javaClass.`package`.implementationVersion ?: "unknown") + } + + protected val inputOptions by InputOptions() + protected val outputOptions by OutputOptions() + protected val solver: String by option(help = "The solver to use for the check").default("Z3") + private val smtHome: File by option().file().default(SmtLibSolverManager.HOME.toFile()) + protected val logger: Logger by lazy { + if (outputOptions.benchmarkMode) NullLogger.getInstance() else ConsoleLogger(outputOptions.logLevel) + } + protected val writer = BasicTableWriter(System.out, ",", "\"", "\"") + + fun printError(exception: Exception) { + val message = exception.message ?: "" + val exceptionName = exception.javaClass.simpleName + if (outputOptions.benchmarkMode) { + writer.cell("[EX] $exceptionName: $message") + writer.newRow() + return + } + logger.write(Logger.Level.RESULT, "%s occurred, message: %s%n", exceptionName, message) + if (outputOptions.stacktrace) { + logger.write(Logger.Level.RESULT, "Trace:%n%s%n", exception.stackTraceToString()) + } else { + logger.write(Logger.Level.RESULT, "Use --stacktrace for stack trace%n") + } + } + + fun registerSolverManagers() { + SolverManager.registerSolverManager(hu.bme.mit.theta.solver.z3.Z3SolverManager.create()) + SolverManager.registerSolverManager(hu.bme.mit.theta.solver.z3legacy.Z3SolverManager.create()) + SolverManager.registerSolverManager(SmtLibSolverManager.create(smtHome.toPath(), logger)) + SolverManager.registerSolverManager(JavaSMTSolverManager.create()) + } + + protected fun writeCex(status: SafetyResult<*, *>, xsts: XSTS) { + if (outputOptions.cexfile == null || status.isSafe) return + val trace = status.asUnsafe().cex as Trace, XstsAction> + val concreteTrace = + XstsTraceConcretizerUtil.concretize(trace, SolverManager.resolveSolverFactory(solver), xsts) + val file: File = outputOptions.cexfile!! + PrintWriter(file).use { printWriter -> + printWriter.write(concreteTrace.toString()) + } + } +} 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 new file mode 100644 index 0000000000..564f0fd9e9 --- /dev/null +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBounded.kt @@ -0,0 +1,133 @@ +/* + * 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.xsts.cli + +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.expl.ExplState +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.solver.SolverManager +import hu.bme.mit.theta.xsts.XSTS +import hu.bme.mit.theta.xsts.analysis.XstsAction +import hu.bme.mit.theta.xsts.analysis.XstsState +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 java.util.concurrent.TimeUnit +import kotlin.system.exitProcess + +typealias S = XstsState + +class XstsCliBounded : XstsCliBaseCommand( + name = "BOUNDED", + help = "Bounded model checking algorithms" +) { + + enum class Algorithm { + BMC { + + override fun buildChecker( + monolithicExpr: MonolithicExpr, solverFactory: SolverFactory, + valToState: (Valuation) -> S, biValToAction: (Valuation, Valuation) -> XstsAction, + logger: Logger + ) = buildBMC(monolithicExpr, solverFactory.createSolver(), valToState, biValToAction, logger) + }, + IMC { + + override fun buildChecker( + monolithicExpr: MonolithicExpr, solverFactory: SolverFactory, + valToState: (Valuation) -> S, biValToAction: (Valuation, Valuation) -> XstsAction, + logger: Logger + ) = buildKIND( + monolithicExpr, solverFactory.createSolver(), solverFactory.createSolver(), valToState, biValToAction, + logger + ) + }, + KINDUCTION { + + override fun buildChecker( + monolithicExpr: MonolithicExpr, solverFactory: SolverFactory, + valToState: (Valuation) -> S, biValToAction: (Valuation, Valuation) -> XstsAction, + logger: Logger + ) = buildIMC( + monolithicExpr, solverFactory.createSolver(), solverFactory.createItpSolver(), valToState, + biValToAction, logger + ) + }; + + abstract fun buildChecker( + monolithicExpr: MonolithicExpr, solverFactory: SolverFactory, valToState: (Valuation) -> S, + biValToAction: (Valuation, Valuation) -> XstsAction, logger: Logger + ): BoundedChecker + } + + private val algorithm by option().enum().required() + + private fun printResult(status: SafetyResult>, sts: XSTS, totalTimeMs: Long) { + if (!outputOptions.benchmarkMode) return + val stats = status.stats.orElse(CegarStatistics(0, 0, 0, 0)) as CegarStatistics + listOf( + status.isSafe, + totalTimeMs, + stats.algorithmTimeMs, + stats.abstractorTimeMs, + stats.refinerTimeMs, + stats.iterations, + "", + "", + "", + if (status.isUnsafe) writer.cell("${status.asUnsafe().cex!!.length()}") else "", + sts.vars.size, + ).forEach(writer::cell) + writer.newRow() + } + + override fun run() { + try { + doRun() + } catch (e: Exception) { + printError(e) + exitProcess(1) + } + } + + private fun doRun() { + registerSolverManagers() + val solverFactory = SolverManager.resolveSolverFactory(solver) + val xsts = inputOptions.loadXsts() + val sw = Stopwatch.createStarted() + val checker = algorithm.buildChecker( + xsts.toMonolithicExpr(), solverFactory, xsts::valToState, + xsts::valToAction, + logger + ) + val result = checker.check() + sw.stop() + printResult(result, xsts, sw.elapsed(TimeUnit.MILLISECONDS)) + writeCex(result, xsts) + } + +} \ No newline at end of file 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 new file mode 100644 index 0000000000..387256a479 --- /dev/null +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliCegar.kt @@ -0,0 +1,113 @@ +/* + * 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.xsts.cli + +import com.github.ajalt.clikt.parameters.options.default +import com.github.ajalt.clikt.parameters.options.option +import com.github.ajalt.clikt.parameters.types.enum +import com.github.ajalt.clikt.parameters.types.int +import com.google.common.base.Stopwatch +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.SafetyResult +import hu.bme.mit.theta.analysis.algorithm.arg.ARG +import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics +import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy +import hu.bme.mit.theta.analysis.utils.ArgVisualizer +import hu.bme.mit.theta.analysis.utils.TraceVisualizer +import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter +import hu.bme.mit.theta.solver.SolverManager +import hu.bme.mit.theta.xsts.XSTS +import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder +import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder.* +import java.util.concurrent.TimeUnit +import kotlin.system.exitProcess + +class XstsCliCegar : XstsCliBaseCommand( + name = "CEGAR", + help = "Model checking using the CEGAR (CounterExample Guided Abstraction Refinement) loop algorithm" +) { + + private val domain: Domain by option(help = "Abstraction domain to use").enum().default(Domain.PRED_CART) + private val refinement: Refinement by option(help = "Refinement strategy to use").enum() + .default(Refinement.SEQ_ITP) + private val search: Search by option(help = "Search strategy to use").enum().default(Search.BFS) + private val refinementSolver: String? by option(help = "Use a different solver for abstraction") + private val abstractionSolver: String? by option(help = "Use a different solver for refinement") + private val predsplit: PredSplit by option().enum().default(PredSplit.WHOLE) + private val maxenum: Int by option().int().default(0) + private val autoexpl: AutoExpl by option().enum().default(AutoExpl.NEWOPERANDS) + private val initprec: InitPrec by option().enum().default(InitPrec.EMPTY) + private val prunestrategy: PruneStrategy by option().enum().default(PruneStrategy.LAZY) + private val optimizestmts: OptimizeStmts by option().enum().default(OptimizeStmts.ON) + + private fun printResult(status: SafetyResult?, out Trace<*, *>?>, sts: XSTS, totalTimeMs: Long) { + if (!outputOptions.benchmarkMode) return + val stats = status.stats.orElse(CegarStatistics(0, 0, 0, 0)) as CegarStatistics + listOf( + status.isSafe, + totalTimeMs, + stats.algorithmTimeMs, + stats.abstractorTimeMs, + stats.refinerTimeMs, + stats.iterations, + status.witness!!.size(), + status.witness!!.depth, + status.witness!!.meanBranchingFactor, + if (status.isUnsafe) writer.cell("${status.asUnsafe().cex!!.length()}") else "", + sts.vars.size, + ).forEach(writer::cell) + writer.newRow() + } + + private fun writeVisualStatus( + status: SafetyResult?, out Trace?> + ) { + if (outputOptions.visualize == null) return + val graph = if (status.isSafe) ArgVisualizer.getDefault().visualize(status.asSafe().witness) + else TraceVisualizer.getDefault().visualize(status.asUnsafe().cex) + GraphvizWriter.getInstance().writeFile(graph, outputOptions.visualize!!) + } + + override fun run() { + try { + doRun() + } catch (e: Exception) { + printError(e) + exitProcess(1) + } + } + + private fun doRun() { + registerSolverManagers() + val abstractionSolverFactory = SolverManager.resolveSolverFactory(abstractionSolver ?: solver) + val refinementSolverFactory = SolverManager.resolveSolverFactory(refinementSolver ?: solver) + val xsts = inputOptions.loadXsts() + val config = + XstsConfigBuilder(domain, refinement, abstractionSolverFactory, refinementSolverFactory).maxEnum(maxenum) + .autoExpl(autoexpl).initPrec(initprec).pruneStrategy(prunestrategy).search(search).predSplit(predsplit) + .optimizeStmts(optimizestmts).logger(logger).build(xsts) + val sw = Stopwatch.createStarted() + val result = config.check() + sw.stop() + printResult(result, xsts, sw.elapsed(TimeUnit.MILLISECONDS)) + writeCex(result, xsts) + writeVisualStatus(result) + } + +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliHeader.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliHeader.kt new file mode 100644 index 0000000000..79aca0c869 --- /dev/null +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliHeader.kt @@ -0,0 +1,87 @@ +/* + * 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.xsts.cli + +import com.github.ajalt.clikt.core.CliktCommand +import com.github.ajalt.clikt.parameters.options.default +import com.github.ajalt.clikt.parameters.options.option +import com.github.ajalt.clikt.parameters.types.enum +import hu.bme.mit.theta.common.table.BasicTableWriter + +class XstsCliHeader : CliktCommand(name = "header") { + + private val writer = BasicTableWriter(System.out, ",", "\"", "\"") + + enum class Algorithm { CEGAR, MDD, BOUNDED } + enum class IterationStrategy { + BFS, SAT, GSAT + } + + private val algorithm: Algorithm by option( + help = "Whether to print header for cegar or symbolic based algorithms" + ).enum().default(Algorithm.CEGAR) + private val iterationStrategy: IterationStrategy by option( + "--iterationStrategy", + help = "The state space generation algorithm for symbolic checking" + ).enum().default(IterationStrategy.GSAT) + + override fun run() { + when (algorithm) { + Algorithm.CEGAR, Algorithm.BOUNDED -> printCegarHeader() + Algorithm.MDD -> printSymbolicHeader() + } + } + + private fun printCegarHeader() { + listOf( + "Result", "TimeMs", "AlgoTimeMs", "AbsTimeMs", "RefTimeMs", "Iterations", + "ArgSize", "ArgDepth", "ArgMeanBranchFactor", "CexLen", "Vars" + ).forEach(writer::cell) + writer.newRow() + } + + private fun printSymbolicHeader() { + listOf( + "id", + "modelPath", + "modelName", + "stateSpaceSize", + "finalMddSize", + "totalTimeUs", + "ssgTimeUs", + "nodeCount", + "unionCacheSize", + "unionQueryCount", + "unionHitCount", + ).forEach(writer::cell) + if (iterationStrategy in setOf(IterationStrategy.GSAT, IterationStrategy.SAT)) { + listOf( + "saturateCacheSize", + "saturateQueryCount", + "saturateHitCount" + ).forEach(writer::cell) + } + listOf( + "relProdCacheSize", + "relProdQueryCount", + "relProdHitCount", + ).forEach(writer::cell) + if (iterationStrategy in setOf(IterationStrategy.GSAT, IterationStrategy.SAT)) { + listOf("saturatedNodeCount").forEach(writer::cell) + } + } +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMain.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMain.kt new file mode 100644 index 0000000000..8a8fe9c38d --- /dev/null +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMain.kt @@ -0,0 +1,42 @@ +/* + * 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.xsts.cli + +import com.github.ajalt.clikt.core.CliktCommand +import com.github.ajalt.clikt.core.subcommands +import com.github.ajalt.clikt.parameters.options.deprecated +import com.github.ajalt.clikt.parameters.options.option + +class XstsCliMainCommand : CliktCommand() { + + val algorithm by option(eager = true).deprecated( + "--algorithm switch is now deprecated, use the respective subcommands", error = true + ) + val metrics by option(eager = true).deprecated( + "--metrics switch is now deprecated, use the `metrics` subcommand", error = true + ) + val header by option(eager = true).deprecated( + "--header switch is now deprecated, use the `header` subcommand", error = true + ) + + override fun run() = Unit + +} + +fun main(args: Array) = + XstsCliMainCommand().subcommands(XstsCliCegar(), XstsCliMdd(), XstsCliBounded(), XstsCliHeader(), XstsCliMetrics()) + .main(args) \ No newline at end of file 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 new file mode 100644 index 0000000000..e82b6b6dca --- /dev/null +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMdd.kt @@ -0,0 +1,184 @@ +/* + * 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.xsts.cli + +import com.github.ajalt.clikt.parameters.groups.provideDelegate +import com.github.ajalt.clikt.parameters.options.default +import com.github.ajalt.clikt.parameters.options.option +import com.github.ajalt.clikt.parameters.types.enum +import com.github.ajalt.clikt.parameters.types.file +import com.google.common.base.Stopwatch +import hu.bme.mit.delta.java.mdd.JavaMddFactory +import hu.bme.mit.delta.java.mdd.MddHandle +import hu.bme.mit.delta.java.mdd.MddNode +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.MddChecker +import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.* +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.frontend.petrinet.analysis.PtNetDependency2Gxl +import hu.bme.mit.theta.frontend.petrinet.analysis.PtNetSystem +import hu.bme.mit.theta.frontend.petrinet.analysis.VariableOrderingFactory +import hu.bme.mit.theta.frontend.petrinet.model.PetriNet +import hu.bme.mit.theta.frontend.petrinet.model.Place +import hu.bme.mit.theta.xsts.cli.optiongroup.PetrinetDependencyOutputOptions +import java.io.File +import java.io.PrintStream +import java.util.* +import java.util.concurrent.TimeUnit +import javax.imageio.ImageIO +import kotlin.system.exitProcess + +class XstsCliMdd : XstsCliBaseCommand( + name = "MDD", + help = "Model checking using the MDD (Multi-value Decision Diagrams) method" +) { + + private val ordering: File? by option(help = "Path of the input variable ordering").file( + mustExist = true, canBeDir = false, mustBeReadable = true + ) + private val iterationStrategy: MddChecker.IterationStrategy by option( + help = "The state space generation algorithm to use" + ).enum().default(MddChecker.IterationStrategy.GSAT) + private val dependencyOutput by PetrinetDependencyOutputOptions() + + private fun loadOrdering(petriNet: PetriNet): List = + if (ordering == null) petriNet.places.sortedWith { p1: Place, p2: Place -> + String.CASE_INSENSITIVE_ORDER.compare( + p1.id.reversed(), p2.id.reversed() + ) + } else VariableOrderingFactory.fromFile(ordering, petriNet) + + private fun petrinetAnalysis() { + val totalTimer = Stopwatch.createStarted() + val petriNet = inputOptions.loadPetriNet()[0] + val effectiveOrdering = loadOrdering(petriNet) + val system = PtNetSystem(petriNet, effectiveOrdering) + createDepGxl(system) + createDepGxlGSat(system) + createDepMat(system) + createDepMatPng(system) + val variableOrder = JavaMddFactory.getDefault().createMddVariableOrder(LatticeDefinition.forSets()) + effectiveOrdering.forEach { variableOrder.createOnTop(MddVariableDescriptor.create(it)) } + val ssgTimer = Stopwatch.createStarted() + val provider: FixedPointEnumerationProvider = when (iterationStrategy) { + MddChecker.IterationStrategy.BFS -> BfsProvider(variableOrder) + MddChecker.IterationStrategy.SAT -> SimpleSaturationProvider(variableOrder) + MddChecker.IterationStrategy.GSAT -> GeneralizedSaturationProvider(variableOrder) + } + val stateSpace = provider.compute( + system.initializer, system.transitions, variableOrder.defaultSetSignature.topVariableHandle + ) + ssgTimer.stop() + totalTimer.stop() + + val unionProvider = variableOrder.defaultUnionProvider + listOf( + outputOptions.id, + inputOptions.model.path, + system.name, + MddInterpreter.calculateNonzeroCount(stateSpace), + numberOfNodes(stateSpace), + totalTimer.elapsed(TimeUnit.MICROSECONDS), + ssgTimer.elapsed(TimeUnit.MICROSECONDS), + variableOrder.mddGraph.uniqueTableSize, + unionProvider.cacheSize, + unionProvider.queryCount, + unionProvider.hitCount, + ).forEach(writer::cell) + if (iterationStrategy in setOf(MddChecker.IterationStrategy.GSAT, MddChecker.IterationStrategy.SAT)) { + listOf( + provider.cache.cacheSize, + provider.cache.queryCount, + provider.cache.hitCount + ).forEach(writer::cell) + } + listOf( + provider.cache.cacheSize, + provider.cache.queryCount, + provider.cache.hitCount + ).forEach(writer::cell) + if (iterationStrategy in setOf(MddChecker.IterationStrategy.GSAT, MddChecker.IterationStrategy.SAT)) { + val collector: MutableSet = mutableSetOf() + provider.cacheManager.forEachCache { + (it as SaturationCache).saturateCache.clearSelectively { _, _, res -> + collector.add( + res + ); false + } + } + listOf(collector.size).forEach(writer::cell) + } + } + + private fun createDepMatPng(system: PtNetSystem) { + if (dependencyOutput.depMatPng == null) return + if (system.placeCount > 10000 || system.transitionCount > 10000) { + logger.write( + Logger.Level.INFO, "[WARNING] Skipping image generation because the model size exceeds 10k places or " + + "transitions." + ) + return + } + ImageIO.write(system.dependencyMatrixImage(1), "PNG", dependencyOutput.depMatPng) + } + + private fun createDepMat(system: PtNetSystem) { + val file = dependencyOutput.depMat ?: return + file.createNewFile() + with(PrintStream(file)) { print(system.printDependencyMatrixCsv()) } + } + + private fun createDepGxlGSat(system: PtNetSystem) { + val file = dependencyOutput.depGxlGsat ?: return + file.createNewFile() + with(PrintStream(file)) { print(PtNetDependency2Gxl.toGxl(system, true)) } + } + + private fun createDepGxl(system: PtNetSystem) { + val file = dependencyOutput.depGxl ?: return + file.createNewFile() + with(PrintStream(file)) { print(PtNetDependency2Gxl.toGxl(system, false)) } + } + + override fun run() { + try { + if (inputOptions.isPnml()) petrinetAnalysis() + } catch (e: Exception) { + printError(e) + exitProcess(1) + } + } + + private fun numberOfNodes(root: MddHandle): Int { + val result: MutableSet = mutableSetOf() + val stack = Stack() + stack.push(root.node) + + while (stack.isNotEmpty()) { + val current = stack.pop() + if (!result.add(current) || current.isTerminal) continue + val cursor = current.cursor() + while (cursor.moveNext()) { + stack.push(cursor.value()) + } + } + + return result.size + } +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMetrics.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMetrics.kt new file mode 100644 index 0000000000..33a2af151a --- /dev/null +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMetrics.kt @@ -0,0 +1,69 @@ +/* + * 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.xsts.cli + +import com.github.ajalt.clikt.core.CliktCommand +import com.github.ajalt.clikt.parameters.groups.provideDelegate +import hu.bme.mit.theta.common.logging.ConsoleLogger +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.type.arraytype.ArrayType +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.core.type.bvtype.BvType +import hu.bme.mit.theta.core.type.inttype.IntType +import hu.bme.mit.theta.core.utils.StmtCounterVisitor +import hu.bme.mit.theta.xsts.cli.optiongroup.InputOptions + +class XstsCliMetrics : CliktCommand(name = "metrics") { + + private val inputOptions by InputOptions() + + override fun run() { + val logger = ConsoleLogger(Logger.Level.VERBOSE) + val xsts = inputOptions.loadXsts() + logger.write(Logger.Level.RESULT, "Vars: %s%n", xsts.vars.size) + logger.write( + Logger.Level.RESULT, " Bool vars: %s%n", + xsts.vars.stream().filter { v: VarDecl<*> -> v.type is BoolType }.count() + ) + logger.write( + Logger.Level.RESULT, " Int vars: %s%n", + xsts.vars.stream().filter { v: VarDecl<*> -> v.type is IntType }.count() + ) + logger.write( + Logger.Level.RESULT, " Bitvector vars: %s%n", + xsts.vars.stream().filter { v: VarDecl<*> -> v.type is BvType }.count() + ) + logger.write( + Logger.Level.RESULT, " Array vars: %s%n", + xsts.vars.stream().filter { v: VarDecl<*> -> v.type is ArrayType<*, *> }.count() + ) + logger.write(Logger.Level.RESULT, " Ctrl vars: %s%n", xsts.ctrlVars.size) + logger.write( + Logger.Level.RESULT, "Tran statements: %s%n", + xsts.tran.accept(StmtCounterVisitor.getInstance(), null) + ) + logger.write( + Logger.Level.RESULT, "Env statements: %s%n", + xsts.env.accept(StmtCounterVisitor.getInstance(), null) + ) + logger.write( + Logger.Level.RESULT, "Init statements: %s%n", + xsts.init.accept(StmtCounterVisitor.getInstance(), null) + ) + } +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/InputOptions.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/InputOptions.kt new file mode 100644 index 0000000000..e8c9082007 --- /dev/null +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/InputOptions.kt @@ -0,0 +1,63 @@ +/* + * 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.xsts.cli.optiongroup + +import com.github.ajalt.clikt.parameters.groups.OptionGroup +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.file +import com.github.ajalt.clikt.parameters.types.inputStream +import hu.bme.mit.theta.frontend.petrinet.model.PetriNet +import hu.bme.mit.theta.frontend.petrinet.pnml.PetriNetParser +import hu.bme.mit.theta.frontend.petrinet.pnml.XMLPnmlToPetrinet +import hu.bme.mit.theta.frontend.petrinet.xsts.PetriNetToXSTS +import hu.bme.mit.theta.xsts.XSTS +import hu.bme.mit.theta.xsts.dsl.XstsDslManager +import java.io.* + +class InputOptions : OptionGroup( + name = "Input options", + help = "Options related to model and property input" +) { + + val model: File by option( + help = "Path of the input model (XSTS or Pnml). Extension should be .pnml to be handled as petri-net input" + ).file(mustExist = true, canBeDir = false).required() + private val propertyFile: InputStream? by option( + help = "Path of the property file (XSTS or Pnml). Has priority over --property" + ).inputStream() + private val property: String? by option(help = "Input property as a string. Ignored if --property-file is defined") + private val initialmarking: String by option(help = "Initial marking of the pnml model").default("") + + fun isPnml() = model.path.endsWith("pnml") + + fun loadXsts(): XSTS { + val propertyStream = if (propertyFile != null) propertyFile else (if (property != null) ByteArrayInputStream( + "prop { $property }".toByteArray() + ) else null) + if (isPnml()) { + val petriNet = XMLPnmlToPetrinet.parse(model.absolutePath, initialmarking) + return PetriNetToXSTS.createXSTS(petriNet, propertyStream) + } + return XstsDslManager.createXsts( + SequenceInputStream(FileInputStream(model), propertyStream ?: InputStream.nullInputStream()) + ) + } + + fun loadPetriNet(): MutableList = PetriNetParser.loadPnml(model).parsePTNet() +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/OutputOptions.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/OutputOptions.kt new file mode 100644 index 0000000000..f3b3eff52c --- /dev/null +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/OutputOptions.kt @@ -0,0 +1,45 @@ +/* + * 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.xsts.cli.optiongroup + +import com.github.ajalt.clikt.parameters.groups.OptionGroup +import com.github.ajalt.clikt.parameters.options.default +import com.github.ajalt.clikt.parameters.options.flag +import com.github.ajalt.clikt.parameters.options.option +import com.github.ajalt.clikt.parameters.types.boolean +import com.github.ajalt.clikt.parameters.types.enum +import com.github.ajalt.clikt.parameters.types.file +import hu.bme.mit.theta.common.logging.Logger +import java.io.File + +class OutputOptions : OptionGroup( + name = "Output options", + help = "Options related to output and statistics" +) { + + val logLevel: Logger.Level by option(help = "Detailedness of logging").enum() + .default(Logger.Level.SUBSTEP) + val benchmarkMode: Boolean by option( + "--benchmark", help = "Quiet mode, output will be just the result metrics" + ).boolean().default(false) + + val cexfile: File? by option(help = "Write concrete counterexample to a file").file() + val stacktrace: Boolean by option(help = "Print stack trace of exceptions").flag() + val visualize: File? by option(help = "Write proof or counterexample to file in dot format").file() + val id: String by option(help = "ID of the input model. Used for symbolic output").default("") + +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/PetrinetDependencyOutputOptions.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/PetrinetDependencyOutputOptions.kt new file mode 100644 index 0000000000..fef333cccb --- /dev/null +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/PetrinetDependencyOutputOptions.kt @@ -0,0 +1,38 @@ +/* + * 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.xsts.cli.optiongroup + +import com.github.ajalt.clikt.parameters.groups.OptionGroup +import com.github.ajalt.clikt.parameters.options.option +import com.github.ajalt.clikt.parameters.types.file +import java.io.File + +class PetrinetDependencyOutputOptions : OptionGroup() { + + val depGxl: File? by option( + help = "Generate GXL representation of (extended) dependency graph for variable ordering" + ).file(mustExist = false, canBeDir = false, mustBeWritable = true) + val depGxlGsat: File? by option( + help = "Generate GXL representation of (extended) dependency graph for variable ordering" + ).file(mustExist = false, canBeDir = false, mustBeWritable = true) + val depMat: File? by option(help = "Generate dependency matrix from the model as a CSV file").file( + mustExist = false, canBeDir = false, mustBeWritable = true + ) + val depMatPng: File? by option(help = "Generate dependency matrix from the model as a PNG file").file( + mustExist = false, canBeDir = false, mustBeWritable = true + ) +} \ No newline at end of file