Add GraphViz module.

Addresses Github issue #87
#87

build.xml

@@ -115,6 +115,8 @@
 			<sysproperty key="tlc2.TLC.ide" value="azure-pipeline"/>
 			<sysproperty key="util.ExecutionStatisticsCollector.id" value="01ed03e40ba44f278a934849dd2b1038"/>
 
+			<arg value="-fp"/>
+			<arg value="1"/>
 			<arg value="-metadir"/>
 			<arg value="${basedir}/build/states"/>
 			<arg value="-cleanup"/>

modules/GraphViz.tla

@@ -0,0 +1,6 @@
+---------------------------- MODULE GraphViz -------------------------------
+
+DotDiGraph(G, VL(_), EL(_)) ==
+	TRUE
+
+===============================================================================

modules/tlc2/overrides/GraphViz.java

@@ -0,0 +1,85 @@
+/*******************************************************************************
+ * Copyright (c) 2023 Microsoft Research. All rights reserved.
+ *
+ * The MIT License (MIT)
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+ * of the Software, and to permit persons to whom the Software is furnished to do
+ * so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * Contributors:
+ *   Markus Alexander Kuppe - initial API and implementation
+ ******************************************************************************/
+package tlc2.overrides;
+
+import tlc2.tool.EvalControl;
+import tlc2.util.FP64;
+import tlc2.value.impl.Applicable;
+import tlc2.value.impl.RecordValue;
+import tlc2.value.impl.SetEnumValue;
+import tlc2.value.impl.StringValue;
+import tlc2.value.impl.TupleValue;
+import tlc2.value.impl.Value;
+import tlc2.value.impl.ValueEnumeration;
+
+public class GraphViz {
+
+	@TLAPlusOperator(identifier = "DotDiGraph", module = "GraphViz", warn = false)
+	public static Value dotDiGraph(final Value v1, final Value v2, final Value v3) throws Exception {
+		if (!(v1 instanceof RecordValue) || v1.toRcd() == null) {
+			throw new Exception("An DiGraph must be a record. Value given is of type: " + v1.getClass().getName());
+		}
+		final RecordValue g = (RecordValue) v1.toRcd();
+
+		if (!(v2 instanceof Applicable)) {
+			throw new Exception(
+					"Second parameter must be an Applicable. Value given is of type: " + v2.getClass().getName());
+		}
+		final Applicable vl = (Applicable) v2;
+
+		if (!(v3 instanceof Applicable)) {
+			throw new Exception(
+					"Third parameter must be an Applicable. Value given is of type: " + v2.getClass().getName());
+		}
+		final Applicable el = (Applicable) v3;
+
+		String dotString = "digraph MyGraph {";
+
+		// Nodes
+		// -3232796921283441800 [label="Some Node Label"];
+		final SetEnumValue nodes = (SetEnumValue) g.select(new StringValue("node")).toSetEnum().normalize();
+		ValueEnumeration elements = nodes.elements();
+		Value val = null;
+		while ((val = elements.nextElement()) != null) {
+			dotString += String.format("%s[label=%s];", val.fingerPrint(FP64.New()),
+					vl.apply(new Value[] { val }, EvalControl.Clear));
+		}
+
+		// Edges
+		// -3232796921283441800 -> 2338507365925255731 [label="Some Edge Label"];
+		final SetEnumValue edges = (SetEnumValue) g.select(new StringValue("edge")).toSetEnum().normalize();
+		elements = edges.elements();
+		while ((val = elements.nextElement()) != null) {
+			TupleValue tv = (TupleValue) val.toTuple();
+			dotString += String.format("%s->%s[label=%s];", tv.elems[0].fingerPrint(FP64.New()),
+					tv.elems[1].fingerPrint(FP64.New()), el.apply(new Value[] { tv }, EvalControl.Clear));
+		}
+
+		dotString += "}";
+
+		return new StringValue(dotString);
+	}
+}

modules/tlc2/overrides/TLCOverrides.java

@@ -45,14 +45,14 @@ public Class[] get() {
 			Json.resolves();
 			return new Class[] { IOUtils.class, SVG.class, SequencesExt.class, Json.class, Bitwise.class,
 					FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class,
-					DyadicRationals.class, Statistics.class, VectorClocks.class };
+					DyadicRationals.class, Statistics.class, VectorClocks.class, GraphViz.class };
 		} catch (NoClassDefFoundError e) {
 			// Remove this catch when this Class is moved to `TLC`.
 			System.out.println("gson dependencies of Json overrides not found, Json module won't work unless "
 					+ "the libraries in the lib/ folder of the CommunityModules have been added to the classpath of TLC.");
 		}
 		return new Class[] { IOUtils.class, SVG.class, SequencesExt.class, Bitwise.class, FiniteSetsExt.class,
 				Functions.class, CSV.class, Combinatorics.class, BagsExt.class, DyadicRationals.class,
-				Statistics.class, VectorClocks.class };
+				Statistics.class, VectorClocks.class, GraphViz.class };
 	}
 }

tests/AllTests.tla

@@ -18,6 +18,7 @@ EXTENDS SequencesExtTests,
         BagsExtTests,
         DyadicRationalsTests,
         StatisticsTests,
-        VectorClocksTests
+        VectorClocksTests,
+		GraphVizTests
 
 ===========================================

tests/GraphVizTests.tla

@@ -0,0 +1,10 @@
+------------------------- MODULE GraphVizTests -------------------------
+EXTENDS GraphViz, Sequences, Naturals, TLC
+
+ASSUME LET T == INSTANCE TLC IN T!PrintT("GraphViz")
+
+ASSUME LET G ==  [node |-> {1,2,3}, 
+                  edge |-> {<<1,2,1>>, <<2,3,2>>, <<2,1,3>>}]
+       IN DotDiGraph(G, LAMBDA v : v, LAMBDA e: e[3] ) = "digraph MyGraph {-5002151522364771816[label=1];-2714544764469681861[label=2];-427540549684285478[label=3];-5002151522364771816->-2714544764469681861[label=1];-2714544764469681861->-5002151522364771816[label=3];-2714544764469681861->-427540549684285478[label=2];}"
+
+=============================================================================