diff --git a/NEWS b/NEWS index 4b20958f4..111c3acb1 100644 --- a/NEWS +++ b/NEWS @@ -192,6 +192,11 @@ New in spot 2.11.6.dev (not yet released) This version of Spot now declares its svg outputs as HTML to prevent Jypyter from wrapping them is images. + Documentation: + + - https://spot.lre.epita.fr/tut25.html is a new example showing + how to print an automaton in the "BA format" (used by Rabbit). + Bugs fixed: - tgba_determinize()'s use_simulation option would cause it to diff --git a/doc/Makefile.am b/doc/Makefile.am index 30c9cfa69..7abe05f9e 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -123,6 +123,7 @@ ORG_FILES = \ org/tut22.org \ org/tut23.org \ org/tut24.org \ + org/tut25.org \ org/tut30.org \ org/tut31.org \ org/tut40.org \ diff --git a/doc/org/.gitignore b/doc/org/.gitignore index 709eb9cc5..0d5e6944a 100644 --- a/doc/org/.gitignore +++ b/doc/org/.gitignore @@ -19,3 +19,4 @@ g++wrap *.fls sitemap.org plantuml.jar +toba.py diff --git a/doc/org/init.el.in b/doc/org/init.el.in index c46363096..53b4f64cd 100644 --- a/doc/org/init.el.in +++ b/doc/org/init.el.in @@ -179,7 +179,7 @@ up.html points to index.html, then the result is: :auto-preamble t) ("spot-static" :base-directory "@abs_top_srcdir@/doc/org/" - :base-extension "css\\|js\\|png\\|svg\\|jpg\\|gif\\|pdf" + :base-extension "css\\|js\\|png\\|svg\\|jpg\\|gif\\|pdf\\|py" :publishing-directory "@abs_top_srcdir@/doc/userdoc/" :recursive t :publishing-function org-publish-attachment) diff --git a/doc/org/tut.org b/doc/org/tut.org index c3833ff5d..918bf7fbb 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -34,6 +34,7 @@ three interfaces supported by Spot: shell commands, Python, or C++. - [[file:tut03.org][Constructing and transforming formulas]] - [[file:tut21.org][Custom print of an automaton]] +- [[file:tut25.org][Printing a Büchi automaton in the "BA format"]] - [[file:tut22.org][Creating an automaton by adding states and transitions]] - [[file:tut23.org][Creating an alternating automaton by adding states and transitions]] - [[file:tut24.org][Iterating over alternating automata]] diff --git a/doc/org/tut21.org b/doc/org/tut21.org index b9281b25e..677736aea 100644 --- a/doc/org/tut21.org +++ b/doc/org/tut21.org @@ -21,9 +21,9 @@ destination states, $\mathit{cond}$ is a BDD representing the label The interface available for those graph-based automata allows random access to any state of the graph, hence the code given bellow can do a simple loop over all states of the automaton. Spot also supports a -different kind of interface (not demonstrated here) to -[[file:tut50.org][iterate over automata that are constructed -on-the-fly]] and where such a loop would be impossible. +different kind of interface (not demonstrated here) to [[file:tut50.org][iterate over +automata that are constructed on-the-fly]] and where such a loop would +be impossible. First let's create an example automaton in HOA format. We use =-U= to request unambiguous automata, as this allows us to demonstrate how @@ -47,98 +47,98 @@ properties: stutter-invariant State: 0 [0] 1 [!0] 2 -[!0&1&2] 3 -[!0&!1&2] 4 -[!0&!2] 5 -[!0&!2] 6 +[!0&!2] 3 +[!0&!2] 4 +[!0&!1&2] 5 +[!0&1&2] 6 State: 1 [t] 1 {0 1} State: 2 [!1&!2] 2 -[!1&2] 2 {1} [1&!2] 2 {0} +[!1&2] 2 {1} [1&2] 2 {0 1} State: 3 -[!0&1&2] 3 -[!0&!1&2] 4 -[!0&!2] 5 -[!0&!2] 6 -[0&!2] 7 -[0&!1&2] 8 -[0&1&2] 9 -[0&!1&2] 10 -[0&1&!2] 11 -[0&!1&!2] 12 +[!0&!2] 3 +[!0&!1&2] 5 +[!0&1&2] 6 +[0&1&2] 7 +[0&!1&!2] 8 +[0&!1&2] 9 +[0&1&!2] 10 +[0&!1&2] 12 [0&!1&!2] 13 State: 4 -[!0&1&2] 3 -[!0&!1&2] 4 -[!0&!2] 5 -[!0&1&!2] 6 -[0&1&!2] 7 -[0&!1] 8 -[0&1&2] 9 -[0&!1&2] 10 -[0&1&!2] 11 -[0&!1&!2] 12 -[0&!1&!2] 14 -[!0&!1&!2] 15 +[!0&!2] 4 +[0&!2] 11 State: 5 -[!0&1&2] 3 -[!0&!1&2] 4 -[!0&!2] 5 -[0&!1&2] 8 -[0&1&2] 9 -[0&!1&2] 10 +[!0&!2] 3 +[!0&1&!2] 4 +[!0&!1&2] 5 +[!0&1&2] 6 +[0&1&2] 7 +[0&!1&!2] 8 +[0&!1&2] 9 +[0&1&!2] 10 [0&1&!2] 11 -[0&!1&!2] 12 -[0&!1&!2] 13 +[0&!1] 12 +[!0&!1&!2] 14 +[0&!1&!2] 15 State: 6 -[!0&!2] 6 -[0&!2] 7 +[!0&!2] 3 +[!0&!2] 4 +[!0&!1&2] 5 +[!0&1&2] 6 +[0&1&2] 7 +[0&!1&!2] 8 +[0&!1&2] 9 +[0&1&!2] 10 +[0&!2] 11 +[0&!1&2] 12 +[0&!1&!2] 13 State: 7 -[!2] 7 {0 1} +[1&2] 7 +[!1&!2] 8 +[!1&2] 9 +[1&!2] 10 +[!2] 11 +[!1&2] 12 +[!1&!2] 13 State: 8 -[!1] 8 {0 1} +[1&2] 7 +[!1&!2] 8 +[!1&2] 9 +[1&!2] 10 State: 9 -[!2] 7 -[!1&2] 8 -[1&2] 9 -[!1&2] 10 +[1&2] 7 +[!1&!2] 8 +[!1&2] 9 +[1&!2] 10 [1&!2] 11 -[!1&!2] 12 -[!1&!2] 13 +[!1&!2] 15 State: 10 -[1&!2] 7 -[1&2] 9 -[!1&2] 10 -[1&!2] 11 -[!1&!2] 12 -[!1&!2] 14 -State: 11 -[!1&2] 8 -[1&2] 9 -[!1&2] 10 -[1&!2] 11 -[!1&!2] 12 +[1&2] 7 +[!1&!2] 8 +[!1&2] 9 +[1&!2] 10 +[!1&2] 12 [!1&!2] 13 +State: 11 +[!2] 11 {0 1} State: 12 -[1&2] 9 -[!1&2] 10 -[1&!2] 11 -[!1&!2] 12 +[!1] 12 {0 1} State: 13 -[!1&2] 8 +[!1&2] 12 [!1&!2] 13 State: 14 -[1&!2] 7 -[!1&!2] 14 -State: 15 -[!0&1&!2] 6 -[0&1&!2] 7 -[0&!1&!2] 14 -[!0&!1&!2] 15 +[!0&1&!2] 4 +[0&1&!2] 11 +[!0&!1&!2] 14 +[0&!1&!2] 15 [0&!1&!2] 16 +State: 15 +[1&!2] 11 +[!1&!2] 15 State: 16 [!1&!2] 16 {0 1} --END-- @@ -166,7 +166,6 @@ corresponding BDD variable number, and then use for instance #include #include #include - #include #include void custom_print(std::ostream& out, spot::twa_graph_ptr& aut); @@ -273,16 +272,16 @@ State 0: label = !a acc sets = {} edge(0 -> 3) - label = !a & b & c + label = !a & !c acc sets = {} edge(0 -> 4) - label = !a & !b & c + label = !a & !c acc sets = {} edge(0 -> 5) - label = !a & !c + label = !a & !b & c acc sets = {} edge(0 -> 6) - label = !a & !c + label = !a & b & c acc sets = {} State 1: edge(1 -> 1) @@ -292,232 +291,232 @@ State 2: edge(2 -> 2) label = !b & !c acc sets = {} - edge(2 -> 2) - label = !b & c - acc sets = {1} edge(2 -> 2) label = b & !c acc sets = {0} + edge(2 -> 2) + label = !b & c + acc sets = {1} edge(2 -> 2) label = b & c acc sets = {0,1} State 3: edge(3 -> 3) - label = !a & b & c - acc sets = {} - edge(3 -> 4) - label = !a & !b & c + label = !a & !c acc sets = {} edge(3 -> 5) - label = !a & !c + label = !a & !b & c acc sets = {} edge(3 -> 6) - label = !a & !c + label = !a & b & c acc sets = {} edge(3 -> 7) - label = a & !c - acc sets = {} - edge(3 -> 8) - label = a & !b & c - acc sets = {} - edge(3 -> 9) label = a & b & c acc sets = {} - edge(3 -> 10) + edge(3 -> 8) + label = a & !b & !c + acc sets = {} + edge(3 -> 9) label = a & !b & c acc sets = {} - edge(3 -> 11) + edge(3 -> 10) label = a & b & !c acc sets = {} edge(3 -> 12) - label = a & !b & !c + label = a & !b & c acc sets = {} edge(3 -> 13) label = a & !b & !c acc sets = {} State 4: - edge(4 -> 3) - label = !a & b & c - acc sets = {} edge(4 -> 4) - label = !a & !b & c - acc sets = {} - edge(4 -> 5) label = !a & !c acc sets = {} - edge(4 -> 6) - label = !a & b & !c - acc sets = {} - edge(4 -> 7) - label = a & b & !c - acc sets = {} - edge(4 -> 8) - label = a & !b - acc sets = {} - edge(4 -> 9) - label = a & b & c - acc sets = {} - edge(4 -> 10) - label = a & !b & c - acc sets = {} edge(4 -> 11) - label = a & b & !c - acc sets = {} - edge(4 -> 12) - label = a & !b & !c - acc sets = {} - edge(4 -> 14) - label = a & !b & !c - acc sets = {} - edge(4 -> 15) - label = !a & !b & !c + label = a & !c acc sets = {} State 5: edge(5 -> 3) - label = !a & b & c - acc sets = {} - edge(5 -> 4) - label = !a & !b & c - acc sets = {} - edge(5 -> 5) label = !a & !c acc sets = {} - edge(5 -> 8) - label = a & !b & c + edge(5 -> 4) + label = !a & b & !c acc sets = {} - edge(5 -> 9) + edge(5 -> 5) + label = !a & !b & c + acc sets = {} + edge(5 -> 6) + label = !a & b & c + acc sets = {} + edge(5 -> 7) label = a & b & c acc sets = {} - edge(5 -> 10) + edge(5 -> 8) + label = a & !b & !c + acc sets = {} + edge(5 -> 9) label = a & !b & c acc sets = {} + edge(5 -> 10) + label = a & b & !c + acc sets = {} edge(5 -> 11) label = a & b & !c acc sets = {} edge(5 -> 12) - label = a & !b & !c + label = a & !b acc sets = {} - edge(5 -> 13) + edge(5 -> 14) + label = !a & !b & !c + acc sets = {} + edge(5 -> 15) label = a & !b & !c acc sets = {} State 6: - edge(6 -> 6) + edge(6 -> 3) label = !a & !c acc sets = {} + edge(6 -> 4) + label = !a & !c + acc sets = {} + edge(6 -> 5) + label = !a & !b & c + acc sets = {} + edge(6 -> 6) + label = !a & b & c + acc sets = {} edge(6 -> 7) + label = a & b & c + acc sets = {} + edge(6 -> 8) + label = a & !b & !c + acc sets = {} + edge(6 -> 9) + label = a & !b & c + acc sets = {} + edge(6 -> 10) + label = a & b & !c + acc sets = {} + edge(6 -> 11) label = a & !c acc sets = {} + edge(6 -> 12) + label = a & !b & c + acc sets = {} + edge(6 -> 13) + label = a & !b & !c + acc sets = {} State 7: edge(7 -> 7) - label = !c - acc sets = {0,1} -State 8: - edge(8 -> 8) - label = !b - acc sets = {0,1} -State 9: - edge(9 -> 7) - label = !c - acc sets = {} - edge(9 -> 8) - label = !b & c - acc sets = {} - edge(9 -> 9) label = b & c acc sets = {} - edge(9 -> 10) + edge(7 -> 8) + label = !b & !c + acc sets = {} + edge(7 -> 9) label = !b & c acc sets = {} + edge(7 -> 10) + label = b & !c + acc sets = {} + edge(7 -> 11) + label = !c + acc sets = {} + edge(7 -> 12) + label = !b & c + acc sets = {} + edge(7 -> 13) + label = !b & !c + acc sets = {} +State 8: + edge(8 -> 7) + label = b & c + acc sets = {} + edge(8 -> 8) + label = !b & !c + acc sets = {} + edge(8 -> 9) + label = !b & c + acc sets = {} + edge(8 -> 10) + label = b & !c + acc sets = {} +State 9: + edge(9 -> 7) + label = b & c + acc sets = {} + edge(9 -> 8) + label = !b & !c + acc sets = {} + edge(9 -> 9) + label = !b & c + acc sets = {} + edge(9 -> 10) + label = b & !c + acc sets = {} edge(9 -> 11) label = b & !c acc sets = {} - edge(9 -> 12) - label = !b & !c - acc sets = {} - edge(9 -> 13) + edge(9 -> 15) label = !b & !c acc sets = {} State 10: edge(10 -> 7) - label = b & !c - acc sets = {} - edge(10 -> 9) label = b & c acc sets = {} - edge(10 -> 10) + edge(10 -> 8) + label = !b & !c + acc sets = {} + edge(10 -> 9) label = !b & c acc sets = {} - edge(10 -> 11) + edge(10 -> 10) label = b & !c acc sets = {} edge(10 -> 12) - label = !b & !c + label = !b & c acc sets = {} - edge(10 -> 14) + edge(10 -> 13) label = !b & !c acc sets = {} State 11: - edge(11 -> 8) - label = !b & c - acc sets = {} - edge(11 -> 9) - label = b & c - acc sets = {} - edge(11 -> 10) - label = !b & c - acc sets = {} edge(11 -> 11) - label = b & !c - acc sets = {} - edge(11 -> 12) - label = !b & !c - acc sets = {} - edge(11 -> 13) - label = !b & !c - acc sets = {} + label = !c + acc sets = {0,1} State 12: - edge(12 -> 9) - label = b & c - acc sets = {} - edge(12 -> 10) - label = !b & c - acc sets = {} - edge(12 -> 11) - label = b & !c - acc sets = {} edge(12 -> 12) - label = !b & !c - acc sets = {} + label = !b + acc sets = {0,1} State 13: - edge(13 -> 8) + edge(13 -> 12) label = !b & c acc sets = {} edge(13 -> 13) label = !b & !c acc sets = {} State 14: - edge(14 -> 7) - label = b & !c - acc sets = {} - edge(14 -> 14) - label = !b & !c - acc sets = {} -State 15: - edge(15 -> 6) + edge(14 -> 4) label = !a & b & !c acc sets = {} - edge(15 -> 7) + edge(14 -> 11) label = a & b & !c acc sets = {} - edge(15 -> 14) - label = a & !b & !c - acc sets = {} - edge(15 -> 15) + edge(14 -> 14) label = !a & !b & !c acc sets = {} - edge(15 -> 16) + edge(14 -> 15) label = a & !b & !c acc sets = {} + edge(14 -> 16) + label = a & !b & !c + acc sets = {} +State 15: + edge(15 -> 11) + label = b & !c + acc sets = {} + edge(15 -> 15) + label = !b & !c + acc sets = {} State 16: edge(16 -> 16) label = !b & !c @@ -594,16 +593,16 @@ State 0: label = !a acc sets = {} edge(0 -> 3) - label = !a & b & c + label = !a & !c acc sets = {} edge(0 -> 4) - label = !a & !b & c + label = !a & !c acc sets = {} edge(0 -> 5) - label = !a & !c + label = !a & !b & c acc sets = {} edge(0 -> 6) - label = !a & !c + label = !a & b & c acc sets = {} State 1: edge(1 -> 1) @@ -613,232 +612,232 @@ State 2: edge(2 -> 2) label = !b & !c acc sets = {} - edge(2 -> 2) - label = !b & c - acc sets = {1} edge(2 -> 2) label = b & !c acc sets = {0} + edge(2 -> 2) + label = !b & c + acc sets = {1} edge(2 -> 2) label = b & c acc sets = {0,1} State 3: edge(3 -> 3) - label = !a & b & c - acc sets = {} - edge(3 -> 4) - label = !a & !b & c + label = !a & !c acc sets = {} edge(3 -> 5) - label = !a & !c + label = !a & !b & c acc sets = {} edge(3 -> 6) - label = !a & !c + label = !a & b & c acc sets = {} edge(3 -> 7) - label = a & !c - acc sets = {} - edge(3 -> 8) - label = a & !b & c - acc sets = {} - edge(3 -> 9) label = a & b & c acc sets = {} - edge(3 -> 10) + edge(3 -> 8) + label = a & !b & !c + acc sets = {} + edge(3 -> 9) label = a & !b & c acc sets = {} - edge(3 -> 11) + edge(3 -> 10) label = a & b & !c acc sets = {} edge(3 -> 12) - label = a & !b & !c + label = a & !b & c acc sets = {} edge(3 -> 13) label = a & !b & !c acc sets = {} State 4: - edge(4 -> 3) - label = !a & b & c - acc sets = {} edge(4 -> 4) - label = !a & !b & c - acc sets = {} - edge(4 -> 5) label = !a & !c acc sets = {} - edge(4 -> 6) - label = !a & b & !c - acc sets = {} - edge(4 -> 7) - label = a & b & !c - acc sets = {} - edge(4 -> 8) - label = a & !b - acc sets = {} - edge(4 -> 9) - label = a & b & c - acc sets = {} - edge(4 -> 10) - label = a & !b & c - acc sets = {} edge(4 -> 11) - label = a & b & !c - acc sets = {} - edge(4 -> 12) - label = a & !b & !c - acc sets = {} - edge(4 -> 14) - label = a & !b & !c - acc sets = {} - edge(4 -> 15) - label = !a & !b & !c + label = a & !c acc sets = {} State 5: edge(5 -> 3) - label = !a & b & c - acc sets = {} - edge(5 -> 4) - label = !a & !b & c - acc sets = {} - edge(5 -> 5) label = !a & !c acc sets = {} - edge(5 -> 8) - label = a & !b & c + edge(5 -> 4) + label = !a & b & !c acc sets = {} - edge(5 -> 9) + edge(5 -> 5) + label = !a & !b & c + acc sets = {} + edge(5 -> 6) + label = !a & b & c + acc sets = {} + edge(5 -> 7) label = a & b & c acc sets = {} - edge(5 -> 10) + edge(5 -> 8) + label = a & !b & !c + acc sets = {} + edge(5 -> 9) label = a & !b & c acc sets = {} + edge(5 -> 10) + label = a & b & !c + acc sets = {} edge(5 -> 11) label = a & b & !c acc sets = {} edge(5 -> 12) - label = a & !b & !c + label = a & !b acc sets = {} - edge(5 -> 13) + edge(5 -> 14) + label = !a & !b & !c + acc sets = {} + edge(5 -> 15) label = a & !b & !c acc sets = {} State 6: - edge(6 -> 6) + edge(6 -> 3) label = !a & !c acc sets = {} + edge(6 -> 4) + label = !a & !c + acc sets = {} + edge(6 -> 5) + label = !a & !b & c + acc sets = {} + edge(6 -> 6) + label = !a & b & c + acc sets = {} edge(6 -> 7) + label = a & b & c + acc sets = {} + edge(6 -> 8) + label = a & !b & !c + acc sets = {} + edge(6 -> 9) + label = a & !b & c + acc sets = {} + edge(6 -> 10) + label = a & b & !c + acc sets = {} + edge(6 -> 11) label = a & !c acc sets = {} + edge(6 -> 12) + label = a & !b & c + acc sets = {} + edge(6 -> 13) + label = a & !b & !c + acc sets = {} State 7: edge(7 -> 7) - label = !c - acc sets = {0,1} -State 8: - edge(8 -> 8) - label = !b - acc sets = {0,1} -State 9: - edge(9 -> 7) - label = !c - acc sets = {} - edge(9 -> 8) - label = !b & c - acc sets = {} - edge(9 -> 9) label = b & c acc sets = {} - edge(9 -> 10) + edge(7 -> 8) + label = !b & !c + acc sets = {} + edge(7 -> 9) label = !b & c acc sets = {} + edge(7 -> 10) + label = b & !c + acc sets = {} + edge(7 -> 11) + label = !c + acc sets = {} + edge(7 -> 12) + label = !b & c + acc sets = {} + edge(7 -> 13) + label = !b & !c + acc sets = {} +State 8: + edge(8 -> 7) + label = b & c + acc sets = {} + edge(8 -> 8) + label = !b & !c + acc sets = {} + edge(8 -> 9) + label = !b & c + acc sets = {} + edge(8 -> 10) + label = b & !c + acc sets = {} +State 9: + edge(9 -> 7) + label = b & c + acc sets = {} + edge(9 -> 8) + label = !b & !c + acc sets = {} + edge(9 -> 9) + label = !b & c + acc sets = {} + edge(9 -> 10) + label = b & !c + acc sets = {} edge(9 -> 11) label = b & !c acc sets = {} - edge(9 -> 12) - label = !b & !c - acc sets = {} - edge(9 -> 13) + edge(9 -> 15) label = !b & !c acc sets = {} State 10: edge(10 -> 7) - label = b & !c - acc sets = {} - edge(10 -> 9) label = b & c acc sets = {} - edge(10 -> 10) + edge(10 -> 8) + label = !b & !c + acc sets = {} + edge(10 -> 9) label = !b & c acc sets = {} - edge(10 -> 11) + edge(10 -> 10) label = b & !c acc sets = {} edge(10 -> 12) - label = !b & !c + label = !b & c acc sets = {} - edge(10 -> 14) + edge(10 -> 13) label = !b & !c acc sets = {} State 11: - edge(11 -> 8) - label = !b & c - acc sets = {} - edge(11 -> 9) - label = b & c - acc sets = {} - edge(11 -> 10) - label = !b & c - acc sets = {} edge(11 -> 11) - label = b & !c - acc sets = {} - edge(11 -> 12) - label = !b & !c - acc sets = {} - edge(11 -> 13) - label = !b & !c - acc sets = {} + label = !c + acc sets = {0,1} State 12: - edge(12 -> 9) - label = b & c - acc sets = {} - edge(12 -> 10) - label = !b & c - acc sets = {} - edge(12 -> 11) - label = b & !c - acc sets = {} edge(12 -> 12) - label = !b & !c - acc sets = {} + label = !b + acc sets = {0,1} State 13: - edge(13 -> 8) + edge(13 -> 12) label = !b & c acc sets = {} edge(13 -> 13) label = !b & !c acc sets = {} State 14: - edge(14 -> 7) - label = b & !c - acc sets = {} - edge(14 -> 14) - label = !b & !c - acc sets = {} -State 15: - edge(15 -> 6) + edge(14 -> 4) label = !a & b & !c acc sets = {} - edge(15 -> 7) + edge(14 -> 11) label = a & b & !c acc sets = {} - edge(15 -> 14) - label = a & !b & !c - acc sets = {} - edge(15 -> 15) + edge(14 -> 14) label = !a & !b & !c acc sets = {} - edge(15 -> 16) + edge(14 -> 15) label = a & !b & !c acc sets = {} + edge(14 -> 16) + label = a & !b & !c + acc sets = {} +State 15: + edge(15 -> 11) + label = b & !c + acc sets = {} + edge(15 -> 15) + label = !b & !c + acc sets = {} State 16: edge(16 -> 16) label = !b & !c @@ -849,6 +848,11 @@ State 16: rm -f tut21.hoa #+END_SRC +* Going further + +As another example of printing an autoamton, see our page about +[[file:tut25.org][printing a Büchi automaton in "BA format"]]. + # LocalWords: utf html args mathit src dst cond accsets tgba Fb Fc # LocalWords: acc Buchi BDDs bdd ap ithvar aut const num init bdict # LocalWords: varnum sep Templated diff --git a/doc/org/tut25.org b/doc/org/tut25.org new file mode 100644 index 000000000..c1ee1ecba --- /dev/null +++ b/doc/org/tut25.org @@ -0,0 +1,285 @@ +# -*- coding: utf-8 -*- +#+TITLE: Printing an automaton in "BA format" +#+DESCRIPTION: Code example for converting HOA into BA format +#+INCLUDE: setup.org +#+HTML_LINK_UP: tut.html +#+PROPERTY: header-args:sh :results verbatim :exports both +#+PROPERTY: header-args:python :results output :exports both +#+PROPERTY: header-args:C+++ :results verbatim + +The [[https://languageinclusion.org/doku.php?id=tools#the_ba_format][BA format]] is a textual representation of a Büchi automaton with +letter-based alphabet, and supported by tools like [[https://languageinclusion.org/doku.php?id=tools][RABIT]] or [[http://goal.im.ntu.edu.tw/wiki/doku.php][Goal]]. It +looks as follows: + +#+BEGIN_SRC dot :file tut25-aut.svg :exports results +digraph "" { + rankdir=LR + label=<[Büchi]> + labelloc="t" + node [shape="circle"] + node [style="filled", fillcolor="#ffffa0"] + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[fontsize=12] fontsize=12 stylesheet="spot.css" edge[arrowhead=vee, arrowsize=.7, fontsize=12] + I [label="", style=invis, width=0] + I -> 1 + 1 [label=, peripheries=2] + 2 [label=, peripheries=2] + 3 [label=] + 1 -> 2 [label=<ℓ₁>] + 2 -> 1 [label=<ℓ₃>] + 2 -> 3 [label=<ℓ₂>] + 3 -> 1 [label=<ℓ₃>] +} +#+END_SRC + +#+RESULTS: +[[file:tut25-aut.svg]] + +#+begin_example +s₁ +ℓ₁,s₁->s₂ +ℓ₃,s2->s1 +ℓ₂,s2->s3 +ℓ₃,s3->s1 +s₁ +s₂ +#+end_example + +The first line, ~s₁~ represents the initial state, the next block of +lines of the form ~letters,src->dst~ represent the transitions of the +automaton. End the last block of lines (containing ~s₁~ and ~s₂~ in +the above example), lists the accepting states of the automaton. + +In this format, the letters and the state can be arbitrary strings +that do not include the characters ~,~ or ~-~, or ~>~. The initial +state can be omitted (the source of the first transition is then +assumed to be initial), and the list of accepting states may be empty. + +Spot has no support for letter-based alphabet (instead it uses boolean +formulas over a set of atomtic propositions), so this format does not +really make any sense. + +As an example of [[file:tut21.org][how to custom print an automaton]], let us write a +small tool that will convert any Büchi automaton that Spot can read +(e.g., a neverclaim from Spin, or an HOA file) into this "BA format". + +Consider the following Büchi automaton obtained from the LTL formula +=a W G(b->c)=. + +#+NAME: tut25ex1 +#+BEGIN_SRC sh :exports code +ltl2tgba -B "a W G(b->c)" -d +#+END_SRC +#+BEGIN_SRC dot :file tut25ex1.svg :var txt=tut25ex1 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:tut25ex1.svg]] + +To create letters out of those formula labels, one trick is to split the transitions over +the $2^{\{a,b,c\}}$ possible valuations. + +#+NAME: tut25ex2 +#+BEGIN_SRC sh :exports code +ltl2tgba -B "a W G(b->c)" | autfilt --split-edges -d +#+END_SRC +#+BEGIN_SRC dot :file tut25ex2.svg :var txt=tut25ex2 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:tut25ex2.svg]] + +Then each label can now be considered as a letter. + +* Convertion in Python + + +#+NAME: toba.py +#+begin_src python :exports code :eval no + #!/usr/bin/env python3 + import spot, sys + + # Read the input automaton from standard input, or from a supplied filename. + argc = len(sys.argv) + if argc < 2: + filename = "-" + elif argc == 2: + filename = sys.argv[1] + else: + print("pass a single filename, or pipe to stdin", file=sys.stderr) + exit(1) + + aut = spot.automaton(filename) + + # Make sure the acceptance condition is Büchi. Alternatively, + # allow "t" acceptance (where every state is accepting), since we + # can interpret this as a Büchi automaton in which all states are + # marked as accepting. + acc = aut.acc() + if not (acc.is_buchi() or acc.is_t()): + print(f"unsupported acceptance: {acc.get_acceptance()}", file=sys.stderr) + exit(1) + + # Transition-based acceptance is not supported by this format; + # convert to state-based if it isn't already. + aut = spot.sbacc(aut) + + # We want one minterm per edge, as those will become letters + aut = spot.split_edges(aut) + + # Now simply output the automaton in the BA format + print(aut.get_init_state_number()) + for e in aut.edges(): + print(f"{e.cond.id()},{e.src}->{e.dst}") + for s in range(aut.num_states()): + if acc.accepting(aut.state_acc_sets(s)): + print(s) +#+end_src + +#+RESULTS: + +Let's assume the above script has been saved as [[file:toba.py][=toba.py=]]. + +#+begin_src sh :noweb yes :results silent :exports results +cat >toba.py <<'EOF' +<> +EOF +chmod 0755 toba.py +#+end_src + +We can now convert our previous example in BA format. + +#+begin_src sh +ltl2tgba -B "a W G(b->c)" | ./toba.py +#+end_src + +#+RESULTS: +#+begin_example +1 +19,0->0 +21,0->0 +22,0->0 +23,0->0 +24,0->0 +10,0->0 +19,1->0 +21,1->0 +22,1->0 +23,1->1 +24,1->1 +25,1->1 +10,1->1 +0 +1 +#+end_example + +The BDD ~e.cond~ that encodes the Boolean formula labels each edge ~e~ +have been printed using ~e.cond.id()~: this is the integer identifier +that uniquely denote each formula. This identifier is good enough to +make letters unique and keep the file short. However, if you prefer to +print the formula instead, replace =e.cond.id()= by +=spot.bdd_format_formula(aut.get_dict(), e.cond)=. + +* Conversion in C++ + +Here is a C++ function that prints =aut= on =out= in BA format, using +the same logic as in the previous section. + +#+NAME: printba +#+BEGIN_SRC C++ + #include + #include + #include + #include + + void print_ba_format(std::ostream& out, spot::twa_graph_ptr aut) + { + // The input should have Büchi acceptance. Alternatively, + // allow "t" acceptance since we can interpret this as a Büchi automaton + // where all states are accepting. + const spot::acc_cond& acc = aut->acc(); + if (!(acc.is_buchi() || acc.is_t())) + throw std::runtime_error("unsupported acceptance condition"); + + // The BA format only support state-based acceptance, so get rid + // of transition-based acceptance if we have some. + aut = spot::sbacc(aut); + + // We want one minterm per edge, as those will become letters + aut = spot::split_edges(aut); + + out << aut->get_init_state_number() << '\n'; + for (auto& e: aut->edges()) + out << e.cond.id() << ',' << e.src << "->" << e.dst << '\n'; + + unsigned ns = aut->num_states(); + for (unsigned s = 0; s < ns; ++s) + if (acc.accepting(aut->state_acc_sets(s))) + out << s << '\n'; + } +#+END_SRC + +#+begin_src sh :results silent :exports results +ltl2tgba -B "a W G(b->c)" >tut25.hoa +#+end_src + +Now what remains to be done is to read some input automaton, so we +can print it: + +#+NAME: maincpp +#+BEGIN_SRC C++ :noweb strip-export :cmdline "tut25.hoa" :exports results :exports both + #include + <> + int main(int argc, const char** argv) + { + if (argc > 2) + { + std::cerr << "pass a single filename, or pipe to stdin\n"; + return 1; + } + const char* filename = "-"; + if (argc == 2) + filename = argv[1]; + spot::parsed_aut_ptr pa = parse_aut(filename, spot::make_bdd_dict()); + if (pa->format_errors(std::cerr)) + return 1; + if (pa->aborted) + { + std::cerr << "--ABORT-- read\n"; + return 1; + } + print_ba_format(std::cout, pa->aut); + return 0; + } +#+END_SRC + +Unsurprisingly running the above code on our example automaton +produces the same output. + +#+RESULTS: maincpp +#+begin_example +1 +19,0->0 +21,0->0 +22,0->0 +23,0->0 +24,0->0 +10,0->0 +19,1->0 +21,1->0 +22,1->0 +23,1->1 +24,1->1 +25,1->1 +10,1->1 +0 +1 +#+end_example + +#+begin_src sh :results silent :exports results +rm -f tut25.hoa +#+end_src