From bc626788af181d5f7e9e8b15977eee97db999ca1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 4 Sep 2017 21:40:22 +0200 Subject: [PATCH] dot: make 'x' compatible with 'b'/'r'/'R' * spot/twaalgos/dot.cc: Implement. * doc/org/oaut.org: Illustrate. * tests/core/dot2tex.test: Add some limited tests. --- doc/org/oaut.org | 20 ++++-- spot/twaalgos/dot.cc | 145 +++++++++++++++++++--------------------- tests/core/dot2tex.test | 3 +- 3 files changed, 86 insertions(+), 82 deletions(-) diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 3a1731d60..472008733 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -876,7 +876,7 @@ export SPOT_DOTEXTRA='edge[arrowhead=vee, arrowsize=.7]' :END: -The [[https://github.com/kjellmf/dot2tex][=dot2tex= program]] interacts with GraphViz to converts dot files +The [[https://github.com/kjellmf/dot2tex][=dot2tex= program]] interacts with GraphViz to convert dot files into TeX figures. The layout is still done by tools provided by GraphViz (i.e. =dot=, =neato=, =circo=, ...) but the actual rendering is done using LaTeX with the TikZ or PSTricks packages. One advantage @@ -905,6 +905,21 @@ following figure: #+END_SRC [[file:dot2tex.png]] +Here an example with bullets denoting acceptance sets, and SCCs: + +#+BEGIN_SRC sh :exports code +ltl2tgba -G -D '!a & FGa' --dot=sbarx | dot2tex --autosize --nominsize > out.tex +#+END_SRC + +#+BEGIN_SRC sh :results silent :exports results + ltl2tgba -G -D '!a & FGa' --dot=sbarx | dot2tex --autosize --nominsize > dot2tex2.tex + latexmk --pdf dot2tex2.tex + convert -density 150 -trim dot2tex2.pdf dot2tex2.png + latexmk -C dot2tex2.tex + rm -f dot2tex2.tex +#+END_SRC +[[file:dot2tex2.png]] + Caveats: - =dot2tex= should be called with option =--autosize= in order to compute the size of each label before calling GraphViz to layout the @@ -923,9 +938,6 @@ Caveats: - The default size of nodes seems slightly too big for our usage. Using =--nominsize= is just one way around it. Refer to the [[https://dot2tex.readthedocs.io/en/latest/][=dot2tex= manual]] for finer ways to set the node size. -- Currently the =x= option of Spot's =--dot= output cannot yet be - combined with the =r=, =R=, an =b= options used to display colored - bullets. (Patches are welcome.) * Statistics :PROPERTIES: diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index b8d1a593f..5e1aefee4 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -92,6 +92,7 @@ namespace spot bool dcircles_ = false; bool opt_scc_ = false; bool opt_html_labels_ = false; + bool opt_color_sets_ = false; bool opt_state_labels_ = false; bool opt_rainbow = false; bool opt_bullet = false; @@ -254,11 +255,11 @@ namespace spot opt_ordered_edges_ = true; break; case 'r': - opt_html_labels_ = true; + opt_color_sets_ = true; opt_rainbow = true; break; case 'R': - opt_html_labels_ = true; + opt_color_sets_ = true; opt_rainbow = false; break; case 's': @@ -280,6 +281,8 @@ namespace spot throw std::runtime_error (std::string("unknown option for print_dot(): ") + c); } + if (opt_color_sets_ && !opt_latex_) + opt_html_labels_ = true; if (opt_html_labels_) { nl_ = "
"; @@ -288,10 +291,6 @@ namespace spot } if (opt_latex_) { - if (opt_latex_ && opt_html_labels_) - throw std::runtime_error - (std::string("print_dot(): options 'r' and 'R' " - "are incompatible with 'x'")); nl_ = "\\\\{}"; label_pre_ = "texlbl=\""; label_post_ = '"'; @@ -305,11 +304,32 @@ namespace spot parse_opts(options ? options : "."); } + const char* + html_set_color(int v) const + { + if (opt_rainbow) + return palette[v % palette_mod]; + // Color according to Fin/Inf + if (inf_sets_.has(v)) + { + if (fin_sets_.has(v)) + return palette[2]; + else + return palette[0]; + } + else + { + return palette[1]; + } + } + void output_set(std::ostream& os, int v) const { v += opt_shift_sets_; - if (opt_bullet && (v >= 0) & (v <= MAX_BULLET)) + if (opt_html_labels_) + os << ""; + if (!opt_latex_ && opt_bullet && (v >= 0) & (v <= MAX_BULLET)) { static const char* const tab[MAX_BULLET + 1] = { "⓿", "❶", "❷", "❸", @@ -321,14 +341,21 @@ namespace spot }; os << tab[v]; } + else if (opt_latex_ && opt_bullet) + { + os << "\\accset{" << v << '}'; + } else { os << v; } + if (opt_html_labels_) + os << ""; } + void - output_set(acc_cond::mark_t a) const + output_mark(acc_cond::mark_t a) const { if (!opt_all_bullets) { @@ -354,55 +381,6 @@ namespace spot } } - const char* - html_set_color(int v) const - { - if (opt_rainbow) - return palette[(v + opt_shift_sets_) % palette_mod]; - // Color according to Fin/Inf - if (inf_sets_.has(v)) - { - if (fin_sets_.has(v)) - return palette[2]; - else - return palette[0]; - } - else - { - return palette[1]; - } - } - - void - output_html_set_aux(std::ostream& os, int v) const - { - os << ""; - output_set(os, v); - os << ""; - } - - void - output_html_set(int v) const - { - output_html_set_aux(os_, v); - } - - void - output_html_set(acc_cond::mark_t a) const - { - if (!opt_all_bullets) - os_ << '{'; - const char* space = ""; - for (auto v: a.sets()) - { - if (!opt_all_bullets) - os_ << space; - output_html_set(v); - space = ","; - } - if (!opt_all_bullets) - os_ << '}'; - } std::ostream& escape_for_output(std::ostream& os, const std::string& s) const @@ -567,11 +545,32 @@ namespace spot if (opt_html_labels_) std::tie(inf_sets_, fin_sets_) = aut_->get_acceptance().used_inf_fin_sets(); - if (opt_bullet && aut_->num_sets() <= MAX_BULLET) + // UTF-8 has no glyphs for circled numbers larger than MAX_BULLET. + if (opt_bullet && (aut_->num_sets() <= MAX_BULLET || opt_latex_)) opt_all_bullets = true; os_ << "digraph G {\n"; if (opt_latex_) - os_ << " d2tgraphstyle=\"every node/.style={align=center}\"\n"; + { + os_ << " d2tgraphstyle=\"every node/.style={align=center}\"\n"; + if (opt_bullet) + { + os_ << (" d2tdocpreamble=\"" + "\\DeclareRobustCommand{\\accset}[1]{" + "\\tikz[baseline=(num.base)]{\\node[fill=") + << (opt_color_sets_ ? "accset#1" : "black") + << (",draw=white,text=white,thin,circle,inner sep=1pt," + "font=\\bfseries\\sffamily] (num) {#1};}}"); + if (opt_color_sets_) + { + unsigned n = aut_->num_sets(); + for (unsigned i = 0; i < n; ++i) + os_ << "\n\\definecolor{accset" << i << "}{HTML}{" + << (html_set_color(i) + 1) << '}'; + } + if (opt_bullet) + os_ << "\"\n"; + } + } if (!opt_vertical_) os_ << " rankdir=LR\n"; if (name_ || opt_show_acc_) @@ -586,18 +585,16 @@ namespace spot if (name_) os_ << nl_; auto& acc = aut_->get_acceptance(); - if (opt_html_labels_) - acc.to_html(os_, [this](std::ostream& os, int v) - { - this->output_html_set_aux(os, v); - }); - else if (opt_latex_) - acc.to_latex(os_ << '$') << '$'; - else - acc.to_text(os_, [this](std::ostream& os, int v) + auto outset = [this](std::ostream& os, int v) { this->output_set(os, v); - }); + }; + if (opt_html_labels_) + acc.to_html(os_, outset); + else if (opt_latex_) + acc.to_latex(os_ << '$', outset) << '$'; + else + acc.to_text(os_, outset); } print_acceptance_for_human(); @@ -679,10 +676,7 @@ namespace spot if (acc) { os_ << nl_; - if (opt_html_labels_) - output_html_set(acc); - else - output_set(acc); + output_mark(acc); } if (opt_state_labels_) format_state_label(os_ << nl_, s); @@ -740,10 +734,7 @@ namespace spot { if (!opt_state_labels_) os_ << nl_; - if (opt_html_labels_) - output_html_set(a); - else - output_set(a); + output_mark(a); } os_ << label_post_; if (opt_ordered_edges_ || opt_numbered_edges_) diff --git a/tests/core/dot2tex.test b/tests/core/dot2tex.test index 5b4b723f4..50b393829 100755 --- a/tests/core/dot2tex.test +++ b/tests/core/dot2tex.test @@ -33,8 +33,9 @@ ltl2tgba 'a U b' --dot=scanx >out.dot dot2tex --autosize --nominsize out.dot >out.tex pdflatex out.tex -ltl2tgba 'p0 U p1' --dot=tax >out2.dot +ltl2tgba 'p0 U p1' --dot=tbarx >out2.dot dot2tex --autosize --nominsize out2.dot >out2.tex grep -F 'p_{0}' out2.tex grep -F 'mathsf{Inf}' out2.tex +grep -F 'accset0' out2.tex pdflatex out2.tex