From dbd22b0d4773dfdf361a38133eb91d5ea1ed1761 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hajdu=20=C3=81kos?= Date: Tue, 11 Aug 2020 17:13:27 +0200 Subject: [PATCH] Write STS counterexample --- build.gradle.kts | 2 +- .../analysis/StsTraceConcretizer.java | 2 +- .../java/hu/bme/mit/theta/sts/cli/StsCli.java | 44 ++++++++++++------- 3 files changed, 30 insertions(+), 18 deletions(-) diff --git a/build.gradle.kts b/build.gradle.kts index db6563c523..2414b35541 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -10,7 +10,7 @@ buildscript { allprojects { group = "hu.bme.mit.inf.theta" - version = "1.4.4" + version = "1.5" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } diff --git a/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/StsTraceConcretizer.java b/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/StsTraceConcretizer.java index bd641e2c3b..9156cf588e 100644 --- a/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/StsTraceConcretizer.java +++ b/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/StsTraceConcretizer.java @@ -26,7 +26,7 @@ import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation; import hu.bme.mit.theta.core.model.Valuation; import hu.bme.mit.theta.core.type.booltype.BoolExprs; -import hu.bme.mit.theta.solver.*; +import hu.bme.mit.theta.solver.SolverFactory; import hu.bme.mit.theta.sts.STS; public final class StsTraceConcretizer { diff --git a/subprojects/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java b/subprojects/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java index 0c5ba46e42..81f19140a8 100644 --- a/subprojects/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java +++ b/subprojects/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java @@ -15,12 +15,7 @@ */ package hu.bme.mit.theta.sts.cli; -import java.io.FileInputStream; -import java.io.FileNotFoundException; -import java.io.IOException; -import java.io.InputStream; -import java.io.PrintWriter; -import java.io.StringWriter; +import java.io.*; import java.util.concurrent.TimeUnit; import com.beust.jcommander.JCommander; @@ -29,8 +24,11 @@ import com.google.common.base.Stopwatch; 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.cegar.CegarStatistics; +import hu.bme.mit.theta.analysis.expl.ExplState; +import hu.bme.mit.theta.analysis.expr.ExprState; 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; @@ -43,6 +41,7 @@ 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.core.model.Valuation; import hu.bme.mit.theta.core.type.booltype.BoolExprs; import hu.bme.mit.theta.core.utils.ExprUtils; import hu.bme.mit.theta.solver.*; @@ -53,6 +52,8 @@ import hu.bme.mit.theta.sts.aiger.AigerToSts; import hu.bme.mit.theta.sts.aiger.elements.AigerSystem; import hu.bme.mit.theta.sts.aiger.utils.AigerCoi; +import hu.bme.mit.theta.sts.analysis.StsAction; +import hu.bme.mit.theta.sts.analysis.StsTraceConcretizer; import hu.bme.mit.theta.sts.dsl.StsDslManager; import hu.bme.mit.theta.sts.dsl.StsSpec; import hu.bme.mit.theta.sts.analysis.config.StsConfig; @@ -99,8 +100,8 @@ public class StsCli { @Parameter(names = {"--benchmark"}, description = "Benchmark mode (only print metrics)") Boolean benchmarkMode = false; - @Parameter(names = {"--visualize"}, description = "Write proof or counterexample to file in dot format") - String dotfile = null; + @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; @@ -140,8 +141,8 @@ private void run() { final SafetyResult status = configuration.check(); sw.stop(); printResult(status, sts, sw.elapsed(TimeUnit.MILLISECONDS)); - if (dotfile != null) { - writeVisualStatus(status, dotfile); + if (status.isUnsafe() && cexfile != null) { + writeCex(sts, status.asUnsafe()); } } catch (final Throwable ex) { printError(ex); @@ -218,11 +219,22 @@ private void printError(final Throwable ex) { } } - private void writeVisualStatus(final SafetyResult status, final String filename) - throws FileNotFoundException { - final Graph graph = status.isSafe() - ? new ArgVisualizer<>(State::toString, a -> "").visualize(status.asSafe().getArg()) - : new TraceVisualizer<>(State::toString, a -> "").visualize(status.asUnsafe().getTrace()); - GraphvizWriter.getInstance().writeFile(graph, filename); + private void writeCex(final STS sts, final SafetyResult.Unsafe status) { + @SuppressWarnings("unchecked") final Trace trace = (Trace) status.getTrace(); + final Trace concrTrace = StsTraceConcretizer.concretize(sts, trace, solverFactory); + final File file = new File(cexfile); + PrintWriter printWriter = null; + try { + printWriter = new PrintWriter(file); + for (Valuation state : concrTrace.getStates()) { + printWriter.println(state.toString()); + } + } catch (final FileNotFoundException e) { + printError(e); + } finally { + if (printWriter != null) { + printWriter.close(); + } + } } }