Add SVG!NodesOfDirectedMultiGraph.

[Feature]

Author: lemmy

.classpath

@@ -10,5 +10,8 @@
 	<classpathentry kind="lib" path="lib/gson-2.8.6.jar"/>
 	<classpathentry kind="lib" path="lib/hamcrest-core-1.3.jar"/>
 	<classpathentry kind="lib" path="lib/junit-4.13.jar"/>
+	<classpathentry kind="lib" path="lib/jungrapht-layout-1.4-SNAPSHOT.jar"/>
+	<classpathentry kind="lib" path="lib/jgrapht-core-1.5.1.jar"/>
+	<classpathentry kind="lib" path="lib/slf4j-api-1.7.30.jar"/>
 	<classpathentry kind="output" path="build"/>
 </classpath>

build.xml

@@ -28,7 +28,7 @@
 	</target>
 
 	<target name="compile" depends="download" description="compile the java module overwrites">
-		<javac srcdir="${src}" destdir="${build}/modules" classpath="${tlc}/tla2tools.jar:${lib}/gson-2.8.6.jar"
+		<javac srcdir="${src}" destdir="${build}/modules" classpath="${tlc}/tla2tools.jar:${lib}/gson-2.8.6.jar:${lib}/jgrapht-core-1.5.1.jar:${lib}/jungrapht-layout-1.4-SNAPSHOT.jar:${lib}/slf4j-api-1.7.30.jar"
            source="1.8"
            target="1.8"
            includeantruntime="false"/>
@@ -52,6 +52,21 @@
 		        <include name="**/*.class"/>
 			</patternset>
 		</unzip>
+		<unzip src="lib/jgrapht-core-1.5.1.jar" dest="${build}/deps">
+			<patternset>
+		        <include name="**/*.class"/>
+			</patternset>
+		</unzip>
+		<unzip src="lib/jungrapht-layout-1.4-SNAPSHOT.jar" dest="${build}/deps">
+			<patternset>
+		        <include name="**/*.class"/>
+			</patternset>
+		</unzip>
+		<unzip src="lib/slf4j-api-1.7.30.jar" dest="${build}/deps">
+			<patternset>
+		        <include name="**/*.class"/>
+			</patternset>
+		</unzip>
 		<jar jarfile="${dist}/CommunityModules-deps-${timestamp}.jar">
 			<fileset dir="${build}/modules/"
              includes="**/*.class"/>
@@ -91,6 +106,9 @@
 			<classpath>
 				<pathelement location="${tlc}/tla2tools.jar" />
                 <pathelement location="${lib}/gson-2.8.6.jar" />
+                <pathelement location="${lib}/jgrapht-core-1.5.1.jar" />
+                <pathelement location="${lib}/jungrapht-layout-1.4-SNAPSHOT.jar" />
+				<pathelement location="${lib}/slf4j-api-1.7.30.jar" />
 				<!-- The jar that has just been built by the dist target. -->
 				<pathelement location="${dist}/CommunityModules-${timestamp}.jar" />
 			</classpath>
@@ -119,7 +137,7 @@
 			<classpath>
 				<pathelement location="${tlc}/tla2tools.jar" />
 				<!-- The jar that has just been built by the dist target. -->
-				<pathelement location="${dist}/CommunityModules-${timestamp}.jar" />
+				<pathelement location="${dist}/CommunityModules-${timestamp}-deps.jar" />
 			</classpath>
 		</java>
 	    <fail message="ERROR: ShiViz test failed">

lib/jgrapht-core-1.5.1.jar

@@ -155,4 +155,23 @@ NodeOfRingNetwork(cx, cy, r, n, m) ==
     (**************************************************************************)
     [ x |-> 0, y |-> 0 ]
 
+NodesOfDirectedMultiGraph(nodes, edges, width, height) ==
+    (**************************************************************************)
+    (* Example to layout a graph with the given Nodes and Edges:              *)
+    (*                                                                        *)
+    (*      Nodes == {"v1", "v2", "v3"}  \* v3 is not connected               *)
+    (*      Edges == {<<"v1", "v2">>, <<"v2", "v1">>}                         *)
+    (*      Graph == NodesOfDirectedMultiGraph(Nodes, Edges, 23, 42)          *)
+    (*                                                                        *)
+    (*      RN[ n \in Nodes ] ==                                              *)
+    (*           LET c == Graph[n]                                            *)
+    (*               node == Rect(c.x, c.y, 23, 42, <<>>)                     *)
+    (*           IN Group(<<node>>,  <<>>)                                    *)
+    (*                                                                        *)
+    (* For this operator's actual definition, please consult the Java module  *)
+    (* override at:                                                           *)
+    (*         modules/tlc2/overrides/SVG.java#directedMultiGraph             *)
+    (**************************************************************************)
+    CHOOSE f \in [ nodes -> [x: Int, y: Int] ]: TRUE
+
 =============================================================================

lib/jungrapht-layout-1.4-SNAPSHOT.jar

@@ -25,12 +25,26 @@
  ******************************************************************************/
 package tlc2.overrides;
 
+import java.util.Map;
+import java.util.stream.Collectors;
+
+import org.jgrapht.Graph;
+import org.jgrapht.graph.DefaultGraphType;
+import org.jgrapht.graph.builder.GraphTypeBuilder;
+import org.jgrapht.util.SupplierUtil;
+import org.jungrapht.visualization.layout.algorithms.TreeLayoutAlgorithm;
+import org.jungrapht.visualization.layout.model.LayoutModel;
+import org.jungrapht.visualization.layout.model.Point;
+import org.jungrapht.visualization.layout.model.Rectangle;
+
 import tlc2.value.impl.FcnRcdValue;
 import tlc2.value.impl.IntValue;
 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.ValueVec;
 import util.UniqueString;
 
 public final class SVG {
@@ -135,4 +149,39 @@ public static Value ringNetwork(IntValue cx, IntValue cy, IntValue r, IntValue n
 		final int y = (int) (cy.val + r.val * Math.sin(angle));
 		return new RecordValue(new UniqueString[] {UniqueString.of("x"), UniqueString.of("y")}, new Value[] {IntValue.gen(x), IntValue.gen(y)}, false);
 	}
+	
+	@TLAPlusOperator(identifier = "NodesOfDirectedMultiGraph", module = "SVG", warn = false)
+	public static Value directedMultiGraph(final SetEnumValue nodes, final SetEnumValue edges, final IntValue width, final IntValue height) throws Exception {
+		// https://jgrapht.org/guide/UserOverview#graph-structures
+		final Graph<Value, Integer> graph = GraphTypeBuilder.<Value, Integer>forGraphType(DefaultGraphType.directedMultigraph())
+				.edgeSupplier(SupplierUtil.createIntegerSupplier()).allowingSelfLoops(false).buildGraph();
+		
+		ValueVec elems = nodes.elems;
+		for (int i = 0; i < elems.size(); i++) {
+			graph.addVertex(elems.elementAt(i));
+		}
+		elems = edges.elems;
+		for (int i = 0; i < elems.size(); i++) {
+			TupleValue tuple = (TupleValue) elems.elementAt(i);
+			graph.addEdge(tuple.elems[0], tuple.elems[1]);
+		}
+
+		final LayoutModel<Value> layoutModel = LayoutModel.<Value>builder().size(1000, 1000).graph(graph).build();
+		TreeLayoutAlgorithm<Value> layoutAlgo = TreeLayoutAlgorithm.<Value>builder()
+				.vertexBoundsFunction(v -> Rectangle.of(-5, -5, width.val, height.val)).build();
+		layoutAlgo.visit(layoutModel);
+		final Map<Value, Point> locations = layoutModel.getLocations();
+		
+		return new FcnRcdValue(locations.entrySet().stream()
+				.collect(Collectors.toMap(
+						entry -> entry.getKey(), 
+						entry -> point2Value(entry.getValue()))));
+	}
+	
+	private static Value point2Value(final Point p) {
+		final int x = ((Double) p.x).intValue();
+		final int y = ((Double) p.y).intValue();
+		return new RecordValue(new UniqueString[] { UniqueString.of("x"), UniqueString.of("y") },
+				new Value[] { IntValue.gen(x), IntValue.gen(y) }, false);
+	}
 }

lib/slf4j-api-1.7.30.jar

@@ -133,7 +133,7 @@ ASSUME PrintT("IOUtilsTests!C!d")
 \* Run TLC with some spec depending on CommunityModules and CM on the classpath.
 \* Pass an environment variable to the nested spec.
 ASSUME(LET ret == IOEnvExec([SOME_NESTED_VAR |-> "SOME_VAL", B |-> "23"],
-                            <<"java", "-cp", "modules:build/modules:tlc/tla2tools.jar", "tlc2.TLC",
+                            <<"java", "-cp", "modules:build/deps:build/modules:tlc/tla2tools.jar", "tlc2.TLC",
                                           "-config", "Counter.cfg", "tests/nested/CounterCM">>)
                                                                  IN /\ PrintT(ret)
                                                                     /\ ret.exitValue = 0