From 11e8f9592fc307bd73b8626f3169333657046d24 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 18 May 2019 13:46:33 +0200 Subject: [PATCH] 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. --- NEWS | 7 ++++++- spot/twaalgos/dot.cc | 10 +++++++++- tests/core/readsave.test | 5 +++++ 3 files changed, 20 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index 38f926b82..86b8b9fe9 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,11 @@ New in spot 2.7.4.dev (not yet released) - Nothing yet. + Library: + + - 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. New in spot 2.7.4 (2019-04-27) diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index badbaa1d1..f0b5550b2 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -440,7 +440,15 @@ namespace spot print_sclatex_psl(os << '$', f) << '$'; 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., "&" -> "&") 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& diff --git a/tests/core/readsave.test b/tests/core/readsave.test index 55c985170..579c95d72 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -1085,3 +1085,8 @@ digraph "a U b" { } EOF 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