Layout nodes in GraphViz (dot) state graph by their rank.

[Feature][TLC]

tlatools/src/tlc2/util/DotStateWriter.java

@@ -28,6 +28,7 @@ package tlc2.util;
 
 import java.io.IOException;
 import java.util.HashMap;
+import java.util.HashSet;
 import java.util.Map;
 import java.util.Set;
 
@@ -50,6 +51,9 @@ public class DotStateWriter extends StateWriter {
 	// time, adding new actions as we find out about them.
 	private final Map<String, Integer> actionToColors = new HashMap<>();
 	
+	// A mapping from ranks to nodes.
+	private final Map<Short, Set<Long>> rankToNodes = new HashMap<>();
+
 	// Determines whether or not transition edges should be colorized in the state
 	// graph.
 	private final boolean colorize;
@@ -112,6 +116,12 @@ public class DotStateWriter extends StateWriter {
 		this.writer.append(states2dot(state));
 		this.writer.append("\"]");
 		this.writer.append("\n");
+		
+		maintainRanks(state);
+	}
+	
+	protected void maintainRanks(final TLCState state) {
+		rankToNodes.computeIfAbsent(state.level, k -> new HashSet<Long>()).add(state.fingerPrint());
 	}
 
 	/* (non-Javadoc)
@@ -175,6 +185,8 @@ public class DotStateWriter extends StateWriter {
 			this.writer.append("\"]");
 			this.writer.append(";\n");
 		}
+		
+		maintainRanks(state);
 	}
 	
 	/**
@@ -277,6 +289,13 @@ public class DotStateWriter extends StateWriter {
 	 * @see tlc2.util.IStateWriter#close()
 	 */
 	public void close() {
+		for (final Set<Long> entry : rankToNodes.values()) {
+			this.writer.append("{rank = same; ");
+			for (final Long l : entry) {
+				this.writer.append(l + ";");
+			}
+			this.writer.append("}\n");
+		}
 		this.writer.append("}\n"); // closes the main subgraph.
 		// We only need the legend if the edges are colored by action and there is more
 		// than a single action.

tlatools/test/tlc2/tool/DumpAsDotTest.dot

@@ -68,6 +68,10 @@ color="white";
 -2066378075513578053 -> -2066378075513578053 [style="dashed"];
 -2066378075513578053 [label="/\\ b = TRUE
 /\\ x = 5"];
+{rank = same; 1377963776297717291;5040481953810085374;8671809759910816123;3365478001808954030;6816998822487979083;609737673425276830;3881310712274735899;7147721571019581646;}
+{rank = same; -4210745456684007285;}
+{rank = same; -7819220713745958050;}
+{rank = same; -2066378075513578053;}
 }
 subgraph cluster_legend {graph[style=bold];label = "Next State Actions" style="solid"
 node [ labeljust="l" colorscheme="paired12" style=filled shape=record ]

tlatools/test/tlc2/tool/DumpAsDotTest.java

@@ -33,7 +33,6 @@ import java.io.File;
 import java.io.FileInputStream;
 import java.io.IOException;
 import java.io.InputStream;
-import java.nio.charset.Charset;
 import java.util.Arrays;
 
 import org.junit.Test;