org: add an example of conversion to BA format
This script was first posted on https://github.com/adl/hoaf/issues/73 * doc/org/tut25.org: New file. * doc/Makefile.am: Add it. * doc/org/tut.org, doc/org/tut21.org, NEWS: Link to it. * doc/org/init.el.in: Install *.py files. * doc/org/.gitignore: Add toba.py.
This commit is contained in:
Alexandre Duret-Lutz
parent
06099f649e
commit
cb15840c56
7 changed files with 641 additions and 344 deletions
|
|
@ -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 \
|
||||
|
|
|
|||
1
doc/org/.gitignore
vendored
1
doc/org/.gitignore
vendored
|
|
@ -19,3 +19,4 @@ g++wrap
|
|||
*.fls
|
||||
sitemap.org
|
||||
plantuml.jar
|
||||
toba.py
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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]]
|
||||
|
|
|
|||
|
|
@ -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 <string>
|
||||
#include <iostream>
|
||||
#include <spot/parseaut/public.hh>
|
||||
#include <spot/twaalgos/hoa.hh>
|
||||
#include <spot/twa/bddprint.hh>
|
||||
|
||||
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
|
||||
|
|
|
|||
285
doc/org/tut25.org
Normal file
285
doc/org/tut25.org
Normal file
|
|
@ -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=<s₁>, peripheries=2]
|
||||
2 [label=<s₂>, peripheries=2]
|
||||
3 [label=<s₃>]
|
||||
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'
|
||||
<<toba.py>>
|
||||
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 <iostream>
|
||||
#include <spot/twa/twagraph.hh>
|
||||
#include <spot/twaalgos/sbacc.hh>
|
||||
#include <spot/twaalgos/split.hh>
|
||||
|
||||
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 <spot/parseaut/public.hh>
|
||||
<<printba>>
|
||||
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
|
||||
Loading…
Add table
Add a link
Reference in a new issue