Merge visualization tool into cfa-cli

README.md

@@ -56,7 +56,7 @@ Each project contains a README.md in its root directory describing its purpose i
 
 |  | Common | CFA | STS | XTA |
 |--|--|--|--|--|
-| **Tools** |  | [`cfa-cli`](subprojects/cfa-cli), [`cfa-metrics`](subprojects/cfa-metrics), [`cfa2dot`](subprojects/cfa2dot) | [`sts-cli`](subprojects/sts-cli) | [`xta-cli`](subprojects/xta-cli) |
+| **Tools** |  | [`cfa-cli`](subprojects/cfa-cli), [`cfa-metrics`](subprojects/cfa-metrics) | [`sts-cli`](subprojects/sts-cli) | [`xta-cli`](subprojects/xta-cli) |
 | **Analyses** | [`analysis`](subprojects/analysis) | [`cfa-analysis`](subprojects/cfa-analysis) | [`sts-analysis`](subprojects/sts-analysis) | [`xta-analysis`](subprojects/xta-analysis) |
 | **Formalisms** | [`core`](subprojects/core), [`common`](subprojects/common) | [`cfa`](subprojects/cfa) | [`sts`](subprojects/sts) | [`xta`](subprojects/xta) |
 | **SMT solvers** | [`solver`](subprojects/solver), [`solver-z3`](subprojects/solver-z3) |

settings.gradle.kts

@@ -3,7 +3,6 @@ rootProject.name = "theta"
 include(
         "analysis",
         "cfa",
-        "cfa2dot",
         "cfa-analysis",
         "cfa-cli",
         "cfa-metrics",

subprojects/cfa-cli/README.md

@@ -75,8 +75,11 @@ In general, values between `5` to `50` perform well (see Section 3.1.1 of [our J
   - `CONJUNCTS`: Split predicates into conjuncts.
   - `ATOMS`: Split predicates into atoms.
 - `--precgranularity`: Granularity of the precision, possible values:
-  - `GLOBAL`: the same precision is applied in each location of the CFA.
-  - `LOCAL`: each location can have a possibly different precision.
+  - `GLOBAL`: The same precision is applied in each location of the CFA.
+  - `LOCAL`: Each location can have a possibly different precision.
+- `--visualize`: Visualize the CFA without running the algorithm.
+If the extension of the output file is `pdf`, `png` or `svg` an automatic visualization is performed, for which [GraphViz](../../doc/Build.md) has to be available on `PATH`.
+Otherwise, the output is simply in `dot` format.
 
 ### For developer usage
 

subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java

@@ -41,13 +41,16 @@
 import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.PredSplit;
 import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Refinement;
 import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Search;
+import hu.bme.mit.theta.cfa.analysis.utils.CfaVisualizer;
 import hu.bme.mit.theta.cfa.dsl.CfaDslManager;
 import hu.bme.mit.theta.common.logging.ConsoleLogger;
 import hu.bme.mit.theta.common.logging.Logger;
 import hu.bme.mit.theta.common.logging.Logger.Level;
 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.solver.*;
 import hu.bme.mit.theta.solver.z3.*;
 
@@ -99,6 +102,9 @@ public class CfaCli {
 	@Parameter(names = "--header", description = "Print only a header (for benchmarks)", help = true)
 	boolean headerOnly = false;
 
+	@Parameter(names = "--visualize", description = "Visualize CFA to this file without running the algorithm")
+	String visualize = null;
+
 	private Logger logger;
 
 	public CfaCli(final String[] args) {
@@ -122,6 +128,11 @@ private void run() {
 			return;
 		}
 
+		if (visualize != null) {
+			visualize();
+			return;
+		}
+
 		if (headerOnly) {
 			printHeader();
 			return;
@@ -145,6 +156,36 @@ private void run() {
 		}
 	}
 
+	private void visualize() {
+		try {
+			final CFA cfa = loadModel();
+			final Graph graph = CfaVisualizer.visualize(cfa);
+			String ext = getFileExtension(visualize.toLowerCase());
+			switch(ext) {
+				case "pdf":
+					GraphvizWriter.getInstance().writeFile(graph, visualize, GraphvizWriter.Format.PDF);
+					break;
+				case "png":
+					GraphvizWriter.getInstance().writeFile(graph, visualize, GraphvizWriter.Format.PNG);
+					break;
+				case "svg":
+					GraphvizWriter.getInstance().writeFile(graph, visualize, GraphvizWriter.Format.SVG);
+					break;
+				default:
+					GraphvizWriter.getInstance().writeFile(graph, visualize);
+					break;
+			}
+		} catch (final Throwable ex) {
+			printError(ex);
+		}
+	}
+
+	private String getFileExtension(String name) {
+		int lastIndexOf = name.lastIndexOf(".");
+		if (lastIndexOf == -1) return "";
+		return name.substring(lastIndexOf + 1);
+	}
+
 	private void printHeader() {
 		final String[] header = new String[]{"Result", "TimeMs", "AlgoTimeMs", "AbsTimeMs", "RefTimeMs", "Iterations",
 				"ArgSize", "ArgDepth", "ArgMeanBranchFactor", "CexLen"};