diff --git a/NEWS b/NEWS index fe468f5464947e3f3acdbf8490ab4dfd29ce0e02..d5245502141d43e6922f5961c44db0ef95281edf 100644 --- a/NEWS +++ b/NEWS @@ -75,6 +75,11 @@ New in spot 2.3.5.dev (not yet released) We plan to enable 'a' by default in a future release, so a new option 'A' has been added to hide the acceptance condition. + - The print_dot() function has a new experimental option 'x' to + output labels are LaTeX formulas. This is meant to be used in + conjunction with the dot2tex tool. See + https://spot.lrde.epita.fr/oaut.html#dot2tex + - A new named property for automata called "original-states" can be used to record the origin of a state before transformation. It is currently defined by the degeneralization algorithms, and by diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 539f596e4a7506ccbeaa4fc0de46c744525dcdd2..314d59b581bdb3f1693fa1dde003a3e358817b26 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -579,6 +579,8 @@ digraph G { } #+end_example +** Converting dot output to images or pdf + This output should be processed with =dot= to be converted into a picture. For instance use =dot -Tpng= or =dot -Tpdf=. @@ -589,6 +591,8 @@ $txt #+RESULTS: [[file:oaut-dot1.png]] +** Customizing the dot output + This output can be customized by passing optional characters to the =--dot= option. For instance =v= requests a vertical layout (instead of the default horizontal layout), =c= requests circle states, =s= @@ -866,6 +870,63 @@ export SPOT_DOTDEFAULT='Brf(Lato)C(#ffffa0)' export SPOT_DOTEXTRA='edge[arrowhead=vee, arrowsize=.7]' #+END_SRC +** Working with =dot2tex= + :PROPERTIES: + :CUSTOM_ID: dot2tex + :END: + + +The [[https://github.com/kjellmf/dot2tex][=dot2tex= program]] interacts with GraphViz to converts 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 +is that this allows embedding math formulas into the graph, something +GraphViz alone cannot do. Another advantage is that you can then +easily edit the LaTeX figure, for instance to add additional graphical +elements. + +The =dot= formater of Spot has an option =x=, that is convenient to +use with =dot2tex=. This option causes labels to be rendered as LaTeX +mathematical formulas instead of ASCII text. + +#+BEGIN_SRC sh :exports code +ltl2tgba 'p0 U p1' --dot=x | dot2tex --autosize --nominsize > out.tex +#+END_SRC + +The above command should give you a LaTeX file that compiles to the +following figure: + +#+BEGIN_SRC sh :results silent :exports results + ltl2tgba 'p0 U p1' --dot=x | dot2tex --autosize --nominsize > dot2tex.tex + latexmk --pdf dot2tex.tex + convert -density 150 -trim dot2tex.pdf dot2tex.png + latexmk -C dot2tex.tex + rm -f dot2tex.tex +#+END_SRC +[[file:dot2tex.png]] + +Caveats: +- =dot2tex= should be called with option =--autosize= in order to + compute the size of each label before calling GraphViz to layout the + graph. This is because GraphViz cannot compute the correct size of + mathematical formulas. Unfortunately, the release of =dot2tex + 2.9.0= contains a bug where sizes are intepreted as integers instead + of floats. This can cause labels or shapes to disappear. This bug + of =dot2tex= was fixed in 2014, but at the time of writing + (summer 2017) no new release of =dot2tex= has been made. To work around this, + make sure you install =dot2tex= from its git repository: + #+BEGIN_SRC sh + git clone https://github.com/kjellmf/dot2tex.git + cd dot2tex + sudo python setup.py install + #+END_SRC +- 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: :CUSTOM_ID: stats diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 1c9d1bd2e36b5dd3efb823ff3113241d091fe691..4b31f9ae194d81e601167896d7dbc59d9f049762 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -63,20 +63,45 @@ namespace spot os << v; } - template + enum code_output {HTML, TEXT, LATEX}; + + template static void print_code(std::ostream& os, const acc_cond::acc_code& code, unsigned pos, std::function set_printer) { - const char* op = " | "; + const char* op_ = style == LATEX ? " \\lor " : " | "; auto& w = code[pos]; - const char* negated = ""; + const char* negated_pre = ""; + const char* negated_post = ""; + auto set_neg = [&]() { + if (style == LATEX) + { + negated_pre = "\\overline{"; + negated_post = "}"; + } + else + { + negated_pre = "!"; + } + }; bool top = pos == code.size() - 1; switch (w.sub.op) { case acc_cond::acc_op::And: - op = html ? " & " : " & "; + switch (style) + { + case HTML: + op_ = " & "; + break; + case TEXT: + op_ = " & "; + break; + case LATEX: + op_ = " \\land "; + break; + } SPOT_FALLTHROUGH; case acc_cond::acc_op::Or: { @@ -90,8 +115,8 @@ namespace spot if (first) first = false; else - os << op; - print_code(os, code, pos, set_printer); + os << op_; + print_code