Refactored statistics and cex/witness output into its own class

settings.gradle.kts

@@ -18,6 +18,7 @@ include(
         "xcfa/xcfa-analysis",
         "xcfa/xcfa-cli",
         "xcfa/cat",
+        "xcfa/xcfa-utils",
 
         "xta/xta",
         "xta/xta-analysis",

subprojects/xcfa/xcfa-analysis/build.gradle.kts

@@ -9,4 +9,5 @@ dependencies {
     compile(project(":theta-cat"))
     compile(project(":theta-common"))
     compile(project(":theta-solver-smtlib"))
+    compile(project(":theta-xcfa-utils"))
 }

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/algorithmselection/AbstractPortfolio.java

@@ -1,21 +1,28 @@
 package hu.bme.mit.theta.xcfa.analysis.algorithmselection;
 
 import com.google.common.base.Stopwatch;
+import hu.bme.mit.theta.analysis.Trace;
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
+import hu.bme.mit.theta.analysis.expl.ExplState;
 import hu.bme.mit.theta.common.OsHelper;
 import hu.bme.mit.theta.common.Tuple2;
 import hu.bme.mit.theta.common.logging.ConsoleLogger;
 import hu.bme.mit.theta.common.logging.Logger;
+import hu.bme.mit.theta.solver.SolverFactory;
 import hu.bme.mit.theta.solver.SolverManager;
 import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager;
 import hu.bme.mit.theta.solver.solververifying.VerifyingSolverManager;
 import hu.bme.mit.theta.solver.z3.Z3SolverManager;
+import hu.bme.mit.theta.xcfa.analysis.declarative.XcfaDeclarativeAction;
+import hu.bme.mit.theta.xcfa.analysis.declarative.XcfaDeclarativeState;
+import hu.bme.mit.theta.xcfa.analysis.utils.OutputHandler;
 import hu.bme.mit.theta.xcfa.model.XCFA;
 
 import java.io.BufferedWriter;
 import java.io.File;
 import java.io.FileWriter;
 import java.io.IOException;
+import java.io.OutputStream;
 import java.nio.file.Path;
 import java.time.Duration;
 import java.util.Optional;
@@ -29,22 +36,26 @@
  */
 public abstract class AbstractPortfolio {
 	protected final ConsoleLogger logger;
-	private final File configurationTxt;
-	private final File configurationCsv;
 	protected final String modelName;
 	protected final String smtlibHome;
 
-	public AbstractPortfolio(Logger.Level logLevel, String basicFileName, String modelName, String smtlibHome) throws Exception {
+	public AbstractPortfolio(Logger.Level logLevel, String modelName, String smtlibHome) throws Exception {
 		logger = new ConsoleLogger(logLevel);
 		closeAndRegisterAllSolverManagers(smtlibHome, logger);
-		configurationTxt = new File(basicFileName + ".portfolio.txt");
-		configurationCsv = new File(basicFileName + ".portfolio.csv");
 		this.modelName = modelName;
 		this.smtlibHome = smtlibHome;
 	}
 
 	public abstract hu.bme.mit.theta.analysis.algorithm.SafetyResult<?,?> executeAnalysis(XCFA xcfa, Duration initializationTime) throws Exception;
 
+	public void outputResultFiles(SafetyResult<?, ?> status, String refinementSolver) throws Exception {
+		if (status!=null && status.isUnsafe()) {
+			OutputHandler.getInstance().writeCounterexamples(status, refinementSolver);
+		} else if(status!=null && status.isSafe()) {
+			OutputHandler.getInstance().writeDummyCorrectnessWitness();
+		}
+	}
+
 	/**
 	 *
 	 * @param configuration
@@ -137,46 +148,11 @@ protected Tuple2<Result, Optional<SafetyResult<?,?>>> executeConfiguration(Cegar
 		logger.write(Logger.Level.RESULT, System.lineSeparator());
 		logger.write(Logger.Level.RESULT, System.lineSeparator());
 
-		writeCsvLine(configuration, timeout, timeTaken, cpuTimeTaken, result);
-		writeTxtLine(configuration, timeout, timeTaken, cpuTimeTaken, result);
+		OutputHandler.getInstance().writeCsvLine(configuration, timeout, timeTaken, cpuTimeTaken, result);
+		OutputHandler.getInstance().writeTxtLine(configuration, timeout, timeTaken, cpuTimeTaken, result);
 		return Tuple2.of(result, Optional.ofNullable(safetyResult));
 	}
 
-	private void writeTxtLine(CegarConfiguration configuration, long timeout, long timeTaken, long cpuTimeTaken, Result result) {
-		if(configurationTxt==null) return;
-		StringBuilder stringBuilder = new StringBuilder();
-		stringBuilder.append(configuration);
-		stringBuilder.append(", timeout (ms, cputime): ").append(timeout);
-		stringBuilder.append(", walltime taken (ms): ").append(timeTaken);
-		stringBuilder.append(", cputime taken (s): ").append(cpuTimeTaken);
-		stringBuilder.append(", result: ").append(result);
-		stringBuilder.append(System.lineSeparator());
-
-		try (BufferedWriter bw = new BufferedWriter(new FileWriter(configurationTxt, true))) {
-			bw.write(stringBuilder.toString());
-		} catch (IOException e) {
-			e.printStackTrace();
-		}
-	}
-
-	private void writeCsvLine(CegarConfiguration configuration, long timeout, long timeTaken, long cpuTimeTaken, Result result) {
-		if(configurationCsv==null) return;
-		StringBuilder stringBuilder = new StringBuilder();
-		stringBuilder.append(modelName).append("\t");
-		stringBuilder.append(configuration).append("\t");
-		stringBuilder.append(timeout).append("\t");
-		stringBuilder.append(timeTaken).append("\t");
-		stringBuilder.append(cpuTimeTaken).append("\t");
-		stringBuilder.append(result).append("\t");
-		stringBuilder.append(System.lineSeparator());
-
-		try (BufferedWriter bw = new BufferedWriter(new FileWriter(configurationCsv, true))) {
-			bw.write(stringBuilder.toString());
-		} catch (IOException e) {
-			e.printStackTrace();
-		}
-	}
-
 	public static void closeAndRegisterAllSolverManagers(String home, Logger logger) throws Exception {
 		SolverManager.closeAll();
 		// register solver managers

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/algorithmselection/CegarConfiguration.java

@@ -10,7 +10,7 @@
 import hu.bme.mit.theta.xcfa.analysis.common.XcfaConfigBuilder;
 import hu.bme.mit.theta.xcfa.model.XCFA;
 
-class CegarConfiguration {
+public class CegarConfiguration {
 	public final XcfaConfigBuilder.Domain domain;
 	public final XcfaConfigBuilder.Refinement refinement;
 	public final XcfaConfigBuilder.Search search;

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/algorithmselection/ComplexPortfolio.java

@@ -20,8 +20,8 @@ public class ComplexPortfolio extends AbstractPortfolio {
 	private long analysisTime; // in ms, init time subtracted from sumTime
 	private long startCpuTime;
 
-	public ComplexPortfolio(Logger.Level logLevel, String basicFileName, String modelName, String smtlibhome) throws Exception {
-		super(logLevel, basicFileName, modelName, smtlibhome); // registers solver factories
+	public ComplexPortfolio(Logger.Level logLevel, String modelName, String smtlibhome) throws Exception {
+		super(logLevel, modelName, smtlibhome); // registers solver factories
 	}
 
 	@Override
@@ -32,15 +32,19 @@ public ComplexPortfolio(Logger.Level logLevel, String basicFileName, String mode
 		startCpuTime = CpuTimeKeeper.getCurrentCpuTime()*1000;
 		analysisTime = sumTime - initializationTime.toMillis();
 
+		SafetyResult<?, ?> safetyResult;
 		if(ArchitectureConfig.arithmetic.equals(ArchitectureConfig.ArithmeticType.bitvector)) {
 			logger.write(Logger.Level.SUBSTEP, "Choosing bitvector arithmetic");
 			logger.write(Logger.Level.SUBSTEP, System.lineSeparator());
-			return bitvectorPath(xcfa);
+			safetyResult = bitvectorPath(xcfa);
 		} else {
 			logger.write(Logger.Level.SUBSTEP, "Choosing integer arithmetic");
 			logger.write(Logger.Level.SUBSTEP, System.lineSeparator());
-			return integerPath(xcfa);
+			safetyResult = integerPath(xcfa);
 		}
+		// TODO this will change if we start to use more solvers
+		outputResultFiles(safetyResult, "verify");
+		return safetyResult;
 	}
 
 	private SafetyResult<?, ?> integerPath(XCFA xcfa) throws Exception {

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/algorithmselection/Result.java

@@ -1,4 +1,4 @@
 package hu.bme.mit.theta.xcfa.analysis.algorithmselection;
 
-enum Result { UNKNOWN, TIMEOUT, STUCK, SUCCESS, OUTOFMEMORY }
+public enum Result { UNKNOWN, TIMEOUT, STUCK, SUCCESS, OUTOFMEMORY }
 

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/algorithmselection/SequentialPortfolio.java

@@ -19,8 +19,8 @@ public class SequentialPortfolio extends AbstractPortfolio {
 	private final long sumTime = 900*1000; // in ms, with initialization time
 	private long analysisTime; // in ms, init time subtracted from sumTime
 
-	public SequentialPortfolio(Logger.Level logLevel, String basicFileName, String modelName, String smtlibhome) throws Exception {
-		super(logLevel, basicFileName, modelName, smtlibhome); // registers solver factories
+	public SequentialPortfolio(Logger.Level logLevel, String modelName, String smtlibhome) throws Exception {
+		super(logLevel, modelName, smtlibhome); // registers solver factories
 
 		configurations[0] = new CegarConfiguration(
 				XcfaConfigBuilder.Domain.EXPL,
@@ -61,7 +61,7 @@ public SequentialPortfolio(Logger.Level logLevel, String basicFileName, String m
 	}
 
 	@Override
-	public SafetyResult<?, ?> executeAnalysis(XCFA xcfa, Duration initializationTime) {
+	public SafetyResult<?, ?> executeAnalysis(XCFA xcfa, Duration initializationTime) throws Exception {
 		logger.write(Logger.Level.MAINSTEP, "Executing sequential portfolio...");
 		logger.write(Logger.Level.MAINSTEP, System.lineSeparator());
 		long startCpuTime = CpuTimeKeeper.getCurrentCpuTime()*1000;
@@ -87,7 +87,9 @@ public SequentialPortfolio(Logger.Level logLevel, String basicFileName, String m
 				logger.write(Logger.Level.MAINSTEP, "Sequential portfolio successful, solver: " + configuration);
 				logger.write(Logger.Level.MAINSTEP, System.lineSeparator());
 
-				return result.get2().get();
+				SafetyResult<?, ?> safetyResult = result.get2().get();
+				outputResultFiles(safetyResult, "Z3");
+				return safetyResult;
 			}
 		}
 		logger.write(Logger.Level.MAINSTEP, "Sequential portfolio was unsuccessful");