Skip to content
Snippets Groups Projects
Commit 29e1e632 authored by Markus Alexander Kuppe's avatar Markus Alexander Kuppe
Browse files

Do not print dot labels as HTML but plaintext to handle all of TLA+. 

[Bug][TLC]
parent 171babd5
Branches
Tags
No related merge requests found
Show whitespace changes
Inline Side-by-side
tlatools/src/tlc2/util/DotStateWriter.java
+ 20
− 20
View file @ 29e1e632
......@@ -110,9 +110,9 @@ public class DotStateWriter extends StateWriter {
// Marker the state as an initial state by using a filled style.
this.writer.append(Long.toString(state.fingerPrint()));
this.writer.append(" [style = filled]");
this.writer.append(" [label=<");
this.writer.append(state2html(state));
this.writer.append(">]");
this.writer.append(" [label=\"");
this.writer.append(states2dot(state));
this.writer.append("\"]");
this.writer.append("\n");
}
......@@ -172,10 +172,9 @@ public class DotStateWriter extends StateWriter {
if (successorStateIsNew) {
// Write the successor's label.
this.writer.append(successorsFP);
this.writer.append(" [label=<");
String stateStr = state2html(state);
this.writer.append(stateStr);
this.writer.append(">]");
this.writer.append(" [label=\"");
this.writer.append(states2dot(successor));
this.writer.append("\"]");
this.writer.append(";\n");
}
}
......@@ -256,19 +255,20 @@ public class DotStateWriter extends StateWriter {
/**
* Given a TLC state, generate a string representation suitable for a HTML DOT graph label.
*/
protected static String state2html(final TLCState state) {
final StringBuilder sb = new StringBuilder();
final Map<UniqueString, Value> valMap = state.getVals();
// Generate a string representation of state.
for (UniqueString key : valMap.keySet()) {
final String valString = (key.toString() + " = " + valMap.get(key).toString());
sb.append(valString);
// New line between variables.
sb.append("<br/>");
}
return sb.toString();
}
//TODO This cannot handle states with variables such as "active = (0 :> TRUE @@ 1 :> FALSE)".
// protected static String state2html(final TLCState state) {
// final StringBuilder sb = new StringBuilder();
// final Map<UniqueString, Value> valMap = state.getVals();
//
// // Generate a string representation of state.
// for (UniqueString key : valMap.keySet()) {
// final String valString = (key.toString() + " = " + valMap.get(key).toString());
// sb.append(valString);
// // New line between variables.
// sb.append("<br/>");
// }
// return sb.toString();
// }
protected static String states2dot(final TLCState state) {
// Replace "\" with "\\" and """ with "\"".
......
tlatools/test/tlc2/tool/DumpAsDotTest.dot
+ 54
− 22
View file @ 29e1e632
......@@ -3,52 +3,84 @@ edge [colorscheme="paired12"]
nodesep=0.35;
subgraph cluster_graph {
color="white";
609737673425276830 [style = filled] [label=<b = FALSE<br/>x = 0<br/>>]
6816998822487979083 [style = filled] [label=<b = TRUE<br/>x = 0<br/>>]
3365478001808954030 [style = filled] [label=<b = FALSE<br/>x = 1<br/>>]
8671809759910816123 [style = filled] [label=<b = TRUE<br/>x = 1<br/>>]
5040481953810085374 [style = filled] [label=<b = FALSE<br/>x = 2<br/>>]
1377963776297717291 [style = filled] [label=<b = TRUE<br/>x = 2<br/>>]
7147721571019581646 [style = filled] [label=<b = FALSE<br/>x = 3<br/>>]
3881310712274735899 [style = filled] [label=<b = TRUE<br/>x = 3<br/>>]
strict digraph DiskGraph {
edge [colorscheme="paired12"]
nodesep=0.35;
subgraph cluster_graph {
color="white";
609737673425276830 [style = filled] [label="/\\ b = FALSE
/\\ x = 0"]
6816998822487979083 [style = filled] [label="/\\ b = TRUE
/\\ x = 0"]
3365478001808954030 [style = filled] [label="/\\ b = FALSE
/\\ x = 1"]
8671809759910816123 [style = filled] [label="/\\ b = TRUE
/\\ x = 1"]
5040481953810085374 [style = filled] [label="/\\ b = FALSE
/\\ x = 2"]
1377963776297717291 [style = filled] [label="/\\ b = TRUE
/\\ x = 2"]
7147721571019581646 [style = filled] [label="/\\ b = FALSE
/\\ x = 3"]
3881310712274735899 [style = filled] [label="/\\ b = TRUE
/\\ x = 3"]
609737673425276830 -> 8671809759910816123 [label="B" color="2" fontcolor="2"];
609737673425276830 -> 609737673425276830 [style="dashed"];
609737673425276830 [label=<b = FALSE<br/>x = 0<br/>>];
609737673425276830 [label="/\\ b = FALSE
/\\ x = 0"];
6816998822487979083 -> 609737673425276830 [label="A" color="3" fontcolor="3"];
6816998822487979083 -> 6816998822487979083 [style="dashed"];
6816998822487979083 [label=<b = TRUE<br/>x = 0<br/>>];
6816998822487979083 [label="/\\ b = TRUE
/\\ x = 0"];
3365478001808954030 -> 1377963776297717291 [label="B" color="2" fontcolor="2"];
3365478001808954030 -> 3365478001808954030 [style="dashed"];
3365478001808954030 [label=<b = FALSE<br/>x = 1<br/>>];
3365478001808954030 [label="/\\ b = FALSE
/\\ x = 1"];
8671809759910816123 -> 3365478001808954030 [label="A" color="3" fontcolor="3"];
8671809759910816123 -> 8671809759910816123 [style="dashed"];
8671809759910816123 [label=<b = TRUE<br/>x = 1<br/>>];
8671809759910816123 [label="/\\ b = TRUE
/\\ x = 1"];
5040481953810085374 -> 3881310712274735899 [label="B" color="2" fontcolor="2"];
5040481953810085374 -> 5040481953810085374 [style="dashed"];
5040481953810085374 [label=<b = FALSE<br/>x = 2<br/>>];
5040481953810085374 [label="/\\ b = FALSE
/\\ x = 2"];
1377963776297717291 -> 5040481953810085374 [label="A" color="3" fontcolor="3"];
1377963776297717291 -> 1377963776297717291 [style="dashed"];
1377963776297717291 [label=<b = TRUE<br/>x = 2<br/>>];
1377963776297717291 [label="/\\ b = TRUE
/\\ x = 2"];
7147721571019581646 -> -4210745456684007285 [label="B" color="2" fontcolor="2"];
-4210745456684007285 [label=<b = FALSE<br/>x = 3<br/>>];
-4210745456684007285 [label="/\\ b = TRUE
/\\ x = 4"];
7147721571019581646 -> 7147721571019581646 [style="dashed"];
7147721571019581646 [label=<b = FALSE<br/>x = 3<br/>>];
7147721571019581646 [label="/\\ b = FALSE
/\\ x = 3"];
3881310712274735899 -> 7147721571019581646 [label="A" color="3" fontcolor="3"];
3881310712274735899 -> 3881310712274735899 [style="dashed"];
3881310712274735899 [label=<b = TRUE<br/>x = 3<br/>>];
3881310712274735899 [label="/\\ b = TRUE
/\\ x = 3"];
-4210745456684007285 -> -7819220713745958050 [label="A" color="3" fontcolor="3"];
-7819220713745958050 [label=<b = TRUE<br/>x = 4<br/>>];
-7819220713745958050 [label="/\\ b = FALSE
/\\ x = 4"];
-4210745456684007285 -> -4210745456684007285 [style="dashed"];
-4210745456684007285 [label=<b = TRUE<br/>x = 4<br/>>];
-4210745456684007285 [label="/\\ b = TRUE
/\\ x = 4"];
-7819220713745958050 -> -2066378075513578053 [label="B" color="2" fontcolor="2"];
-2066378075513578053 [label=<b = FALSE<br/>x = 4<br/>>];
-2066378075513578053 [label="/\\ b = TRUE
/\\ x = 5"];
-7819220713745958050 -> -7819220713745958050 [style="dashed"];
-7819220713745958050 [label=<b = FALSE<br/>x = 4<br/>>];
-7819220713745958050 [label="/\\ b = FALSE
/\\ x = 4"];
-2066378075513578053 -> -2066378075513578053 [style="dashed"];
-2066378075513578053 [label=<b = TRUE<br/>x = 5<br/>>];
-2066378075513578053 [label="/\\ b = TRUE
/\\ x = 5"];
}
subgraph cluster_legend {graph[style=bold];label = "Next State Actions" style="solid"
node [ labeljust="l" colorscheme="paired12" style=filled shape=record ]
A [label="A" fillcolor=3]
B [label="B" fillcolor=2]
}}}
subgraph cluster_legend {graph[style=bold];label = "Next State Actions" style="solid"
node [ labeljust="l" colorscheme="paired12" style=filled shape=record ]
A [label="A" fillcolor=3]
B [label="B" fillcolor=2]
}}
\ No newline at end of file
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment