Test-generation feature for XTA

settings.gradle.kts

@@ -18,6 +18,7 @@ include(
         "xta/xta",
         "xta/xta-analysis",
         "xta/xta-cli",
+        "xta/xta-testgen",
 
         "xsts/xsts",
         "xsts/xsts-analysis",
@@ -29,4 +30,4 @@ for (project in rootProject.children) {
     val projectName = projectPath.split("/").last()
     project.projectDir = file("subprojects/$projectPath")
     project.name = "${rootProject.name}-$projectName"
-}
+}

subprojects/common/common/src/main/java/hu/bme/mit/theta/common/visualization/NodeAttributes.java

@@ -28,9 +28,10 @@ public final class NodeAttributes {
 	private final int peripheries;
 	private final Shape shape;
 	private final Alignment alignment;
+	private final boolean invisible;
 
 	private NodeAttributes(final String label, final Color lineColor, final Color fillColor, final LineStyle lineStyle,
-						   final String font, final int peripheries, final Shape shape, final Alignment alignment) {
+						   final String font, final int peripheries, final Shape shape, final Alignment alignment, final boolean invisible) {
 		this.label = checkNotNull(label);
 		this.lineColor = checkNotNull(lineColor);
 		this.fillColor = checkNotNull(fillColor);
@@ -39,6 +40,7 @@ private NodeAttributes(final String label, final Color lineColor, final Color fi
 		this.peripheries = peripheries;
 		this.shape = checkNotNull(shape);
 		this.alignment = checkNotNull(alignment);
+		this.invisible = invisible;
 	}
 
 	public String getLabel() {
@@ -73,6 +75,8 @@ public Alignment getAlignment() {
 		return alignment;
 	}
 
+	public boolean getInvisible() { return invisible; }
+
 	public static Builder builder() {
 		return new Builder();
 	}
@@ -86,6 +90,7 @@ public static class Builder {
 		private int peripheries = 1;
 		private Shape shape = Shape.ELLIPSE;
 		private Alignment alignment = Alignment.CENTER;
+		private boolean invisible = false;
 
 		public Builder label(final String label) {
 			this.label = label;
@@ -127,8 +132,13 @@ public Builder alignment(final Alignment alignment) {
 			return this;
 		}
 
+		public Builder invisible(final boolean invisible) {
+			this.invisible = invisible;
+			return this;
+		}
+
 		public NodeAttributes build() {
-			return new NodeAttributes(label, lineColor, fillColor, lineStyle, font, peripheries, shape, alignment);
+			return new NodeAttributes(label, lineColor, fillColor, lineStyle, font, peripheries, shape, alignment, invisible);
 		}
 	}
 }

subprojects/common/common/src/main/java/hu/bme/mit/theta/common/visualization/writer/GraphvizWriter.java

@@ -149,6 +149,10 @@ private void printSimpleNode(final Node node, final StringBuilder sb) {
 		}
 		style += "filled";
 
+		if (attributes.getInvisible()) {
+			style = "invis," + style;
+		}
+
 		sb.append("\t\t").append(node.getId());
 		sb.append(" [label=\"").append(convertLabel(attributes.getLabel(), attributes.getAlignment())).append('\"');
 		if (attributes.getPeripheries() > 1) {

subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaAction.java

@@ -56,7 +56,7 @@
 
 public abstract class XtaAction extends StmtAction {
 
-	private static final VarDecl<RatType> DELAY = Var("_delay", Rat());
+	public static final VarDecl<RatType> DELAY = Var("_delay", Rat());
 
 	private final Collection<VarDecl<RatType>> clockVars;
 	private final List<Loc> sourceLocs;

subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/lazy/LazyXtaTestgenStatistics.java

@@ -0,0 +1,183 @@
+package hu.bme.mit.theta.xta.analysis.lazy;
+
+import com.google.common.base.Stopwatch;
+import hu.bme.mit.theta.analysis.algorithm.Statistics;
+import hu.bme.mit.theta.common.table.TableWriter;
+
+import static java.util.concurrent.TimeUnit.MILLISECONDS;
+
+public class LazyXtaTestgenStatistics extends Statistics {
+	private final LazyXtaStatistics stats;
+
+	private final Stopwatch testgenTimer;
+	private long testCasesGenerated;
+	private long testCases;
+	private long testCasesTotalLength;
+
+	public LazyXtaTestgenStatistics(LazyXtaStatistics stats) {
+		this.stats = stats;
+
+		testgenTimer = Stopwatch.createUnstarted();
+		testCases = 0;
+		testCasesTotalLength = 0;
+		testCasesGenerated = 0;
+
+		addStat("AlgorithmTimeInMs", this::getAlgorithmTimeInMs);
+		addStat("ExpandTimeInMs", this::getExpandTimeInMs);
+		addStat("CloseTimeInMs", this::getCloseTimeInMs);
+		addStat("ExpandExplRefinementTimeInMs", this::getExpandExplRefinementTimeInMs);
+		addStat("ExpandZoneRefinementTimeInMs", this::getExpandZoneRefinementTimeInMs);
+		addStat("CloseExplRefinementTimeInMs", this::getCloseExplRefinementTimeInMs);
+		addStat("CloseZoneRefinementTimeInMs", this::getCloseZoneRefinementTimeInMs);
+		addStat("CoverageChecks", this::getCoverageChecks);
+		addStat("CoverageAttempts", this::getCoverageAttempts);
+		addStat("CoverageSuccesses", this::getCoverageSuccesses);
+		addStat("ExplRefinementSteps", this::getExplRefinementSteps);
+		addStat("ZoneRefinementSteps", this::getZoneRefinementSteps);
+		addStat("ArgDepth", this::getArgDepth);
+		addStat("ArgNodes", this::getArgNodes);
+		addStat("ArgNodesExpanded", this::getArgNodesExpanded);
+
+		addStat("TestCasesGenerated", this::getTestCasesGenerated);
+		addStat("TestgenTimeInMs", this::getTestgenTimeInMs);
+		addStat("TestCases", this::getTestCases);
+		addStat("TestCasesTotalLength", this::getTestCasesTotalLength);
+	}
+
+	public long getAlgorithmTimeInMs() { return stats.getAlgorithmTimeInMs(); }
+
+	public long getExpandTimeInMs() {
+		return stats.getExpandTimeInMs();
+	}
+
+	public long getCloseTimeInMs() {
+		return stats.getCloseTimeInMs();
+	}
+
+	public long getExpandExplRefinementTimeInMs() {
+		return stats.getExpandExplRefinementTimeInMs();
+	}
+
+	public long getExpandZoneRefinementTimeInMs() {
+		return stats.getExpandZoneRefinementTimeInMs();
+	}
+
+	public long getCloseExplRefinementTimeInMs() {
+		return stats.getCloseExplRefinementTimeInMs();
+	}
+
+	public long getCloseZoneRefinementTimeInMs() {
+		return stats.getCloseZoneRefinementTimeInMs();
+	}
+
+	public long getCoverageChecks() {
+		return stats.getCoverageChecks();
+	}
+
+	public long getCoverageAttempts() {
+		return stats.getCoverageAttempts();
+	}
+
+	public long getCoverageSuccesses() {
+		return stats.getCoverageSuccesses();
+	}
+
+	public long getExplRefinementSteps() {
+		return stats.getExplRefinementSteps();
+	}
+
+	public long getZoneRefinementSteps() {
+		return stats.getZoneRefinementSteps();
+	}
+
+	public long getArgDepth() {
+		return stats.getArgDepth();
+	}
+
+	public long getArgNodes() {
+		return stats.getArgNodes();
+	}
+
+	public long getArgNodesExpanded() {
+		return stats.getArgNodesExpanded();
+	}
+
+
+	public long getTestCasesGenerated() { return testCasesGenerated; }
+
+	public long getTestgenTimeInMs() { return testgenTimer.elapsed(MILLISECONDS); }
+
+	public long getTestCases() { return testCases; }
+
+	public long getTestCasesTotalLength() { return testCasesTotalLength; }
+
+	public static void writeHeader(final TableWriter writer) {
+		writer.cell("AlgorithmTimeInMs");
+		writer.cell("ExpandTimeInMs");
+		writer.cell("CloseTimeInMs");
+		writer.cell("ExpandExplRefinementTimeInMs");
+		writer.cell("ExpandZoneRefinementTimeInMs");
+		writer.cell("CloseExplRefinementTimeInMs");
+		writer.cell("CloseZoneRefinementTimeInMs");
+		writer.cell("CoverageChecks");
+		writer.cell("CoverageAttempts");
+		writer.cell("CoverageSuccesses");
+		writer.cell("ExplRefinementSteps");
+		writer.cell("ZoneRefinementSteps");
+		writer.cell("ArgDepth");
+		writer.cell("ArgNodes");
+		writer.cell("ArgNodesExpanded");
+
+		writer.cell("TestCasesGenerated");
+		writer.cell("TestgenTimeInMs");
+		writer.cell("TestCases");
+		writer.cell("TestCasesTotalLength");
+
+		writer.newRow();
+	}
+
+	public void writeData(final TableWriter writer) {
+		writer.cell(getAlgorithmTimeInMs());
+		writer.cell(getExpandTimeInMs());
+		writer.cell(getCloseTimeInMs());
+		writer.cell(getExpandExplRefinementTimeInMs());
+		writer.cell(getExpandZoneRefinementTimeInMs());
+		writer.cell(getCloseExplRefinementTimeInMs());
+		writer.cell(getCloseZoneRefinementTimeInMs());
+		writer.cell(getCoverageChecks());
+		writer.cell(getCoverageAttempts());
+		writer.cell(getCoverageSuccesses());
+		writer.cell(getExplRefinementSteps());
+		writer.cell(getZoneRefinementSteps());
+		writer.cell(getArgDepth());
+		writer.cell(getArgNodes());
+		writer.cell(getArgNodesExpanded());
+
+		writer.cell(testCasesGenerated);
+		writer.cell(getTestgenTimeInMs());
+		writer.cell(testCases);
+		writer.cell(testCasesTotalLength);
+
+		writer.newRow();
+	}
+
+	public void startTestgen() {
+		testgenTimer.start();
+	}
+
+	public void stopTestgen() {
+		testgenTimer.stop();
+	}
+
+	public void testCaseGenerated() {
+		testCasesGenerated++;
+	}
+
+	public void setTestCases(long num) {
+		testCases = num;
+	}
+
+	public void addTestCaseLength(long length) {
+		testCasesTotalLength += length;
+	}
+}

subprojects/xta/xta-cli/build.gradle.kts

@@ -7,6 +7,7 @@ dependencies {
     compile(project(":theta-xta"))
     compile(project(":theta-xta-analysis"))
     compile(project(":theta-solver-z3"))
+    compile(project(":theta-xta-testgen"))
 }
 
 application {