Write STS counterexample

ftsrg · Aug 11, 2020 · dbd22b0 · dbd22b0
1 parent ea2386c
commit dbd22b0
Show file tree

Hide file tree

Showing 3 changed files with 30 additions and 18 deletions.
diff --git 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/...rojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/StsTraceConcretizer.java b/...rojects/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
@@ -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<ExprState, StsAction> trace = (Trace<ExprState, StsAction>) status.getTrace();
+		final Trace<Valuation, StsAction> 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();
+			}
+		}
 	}
 }