Commit 89fcd2b4 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

dot: replace large labels by "(label too long)"

Based on a report by Victor Khomenko.

* spot/twaalgos/dot.cc: Here.
* tests/core/readsave.test: Add test case.
* NEWS: Mention it.
parent f476483f
Pipeline #9230 passed with stages
in 129 minutes and 33 seconds
...@@ -42,6 +42,11 @@ New in spot 2.7.4.dev (not yet released) ...@@ -42,6 +42,11 @@ New in spot 2.7.4.dev (not yet released)
helpful to display automata as "graphs", e.g., when illustrating helpful to display automata as "graphs", e.g., when illustrating
algorithms that do not care about labels. algorithms that do not care about labels.
- print_dot will replace labels that have more 2048 characters by a
"(label too long)" string. This works around a limitation of
GraphViz that aborts when some label exceeds 16k characters, and
also helps making large automata more readable.
- A new complement() function that return automata with unspecified - A new complement() function that return automata with unspecified
acceptance condition. The output can be alternating only if the acceptance condition. The output can be alternating only if the
input was alternating. input was alternating.
......
...@@ -444,7 +444,15 @@ namespace spot ...@@ -444,7 +444,15 @@ namespace spot
print_sclatex_psl(os << '$', f) << '$'; print_sclatex_psl(os << '$', f) << '$';
return os; return os;
} }
return escape_for_output(os, str_psl(f)); // GraphViz (2.40.1) has a strict limit of 16k for label
// length. The limit we use below is more conservative,
// because (1) escaping the html element in the string
// (e.g., "&" -> "&amp;") can increase it a lot, and (2)
// a label of size 2048 is already unreasonable to display.
std::string s = str_psl(f);
if (s.size() > 2048)
s = "(label too long)";
return escape_for_output(os, s);
} }
std::ostream& std::ostream&
......
...@@ -1104,3 +1104,8 @@ digraph "a U b" { ...@@ -1104,3 +1104,8 @@ digraph "a U b" {
} }
EOF EOF
diff out expected diff out expected
f="{{!a;!b}:{{c <-> d} && {e xor f} && {m | {l && {k | {j <-> {i xor {g && h}"
f="$f}}}}} && {{n && o} | {!n && p}} && {q -> {r <-> s}}}:{[*0..1];t}}[]-> u"
ltl2tgba -f "$f" --dot=bar > out.dot
grep 'label too long' out.dot
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment