Commit bc626788 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 290d7b56
......@@ -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:
......
......@@ -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_ = "<br/>";
......@@ -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 << "<font color=\"" << html_set_color(v) << "\">";
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 << "</font>";
}
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 << "<font color=\"" << html_set_color(v) << "\">";
output_set(os, v);
os << "</font>";
}
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)
auto outset = [this](std::ostream& os, int v)
{
this->output_html_set_aux(os, v);
});
this->output_set(os, v);
};
if (opt_html_labels_)
acc.to_html(os_, outset);
else if (opt_latex_)
acc.to_latex(os_ << '$') << '$';
acc.to_latex(os_ << '$', outset) << '$';
else
acc.to_text(os_, [this](std::ostream& os, int v)
{
this->output_set(os, v);
});
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_)
......
......@@ -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
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