org: add a new code example
This addresses on item of #14. * doc/org/tut20.org: New file. * doc/Makefile.am: Add it. * doc/org/tut.org: Link to it. * doc/org/.dir-locals.el.in, doc/org/init.el.in: Fix some PATH issues.
This commit is contained in:
Alexandre Duret-Lutz
parent
9f32021e0f
commit
60bd9dd606
5 changed files with 327 additions and 8 deletions
|
|
@ -84,6 +84,7 @@ ORG_FILES = \
|
|||
org/tut01.org \
|
||||
org/tut02.org \
|
||||
org/tut10.org \
|
||||
org/tut20.org \
|
||||
org/satmin.org \
|
||||
org/satmin.tex \
|
||||
org/setup.org \
|
||||
|
|
|
|||
|
|
@ -5,9 +5,10 @@
|
|||
(org-mode . ((whitespace-style face empty trailing)
|
||||
(eval .
|
||||
(progn
|
||||
(setq org-babel-sh-command (concat "PATH=../../src/bin"
|
||||
path-separator
|
||||
"$PATH sh"))
|
||||
(setenv "PATH"
|
||||
(concat "@abs_top_builddir@/src/bin"
|
||||
path-separator
|
||||
(getenv "PATH")))
|
||||
(setenv "PYTHONPATH"
|
||||
(concat "@abs_top_builddir@/wrap/python/.libs:@abs_top_builddir@/wrap/python:@abs_top_srcdir@/wrap/python:"
|
||||
(getenv "PYTHONPATH")))
|
||||
|
|
@ -22,8 +23,9 @@
|
|||
(dot . t)
|
||||
(C . t)))))
|
||||
(org-confirm-babel-evaluate . nil)
|
||||
(org-babel-python-command . "/usr/bin/python3")
|
||||
(org-babel-python-command . "@PYTHON@")
|
||||
(org-babel-C++-compiler . "./g++wrap")
|
||||
(shell-file-name . "@SHELL@")
|
||||
(org-publish-project-alist
|
||||
. (("spot-html"
|
||||
:base-directory "."
|
||||
|
|
|
|||
|
|
@ -21,12 +21,12 @@
|
|||
(C . t)))
|
||||
(setq org-confirm-babel-evaluate nil)
|
||||
|
||||
(setq org-babel-sh-command
|
||||
(concat "PATH=@abs_top_builddir@/src/bin" path-separator "$PATH sh"))
|
||||
|
||||
(setq org-babel-python-command "/usr/bin/python3")
|
||||
(setq org-babel-python-command "@PYTHON@")
|
||||
(setq org-babel-C++-compiler "./g++wrap")
|
||||
(setq shell-file-name "@SHELL@")
|
||||
|
||||
(setenv "PATH"
|
||||
(concat "@abs_top_builddir@/src/bin" path-separator (getenv "PATH")))
|
||||
(setenv "PYTHONPATH"
|
||||
(concat "@abs_top_builddir@/wrap/python/.libs:@abs_top_builddir@/wrap/python:@abs_top_srcdir@/wrap/python:"
|
||||
(getenv "PYTHONPATH")))
|
||||
|
|
|
|||
|
|
@ -16,3 +16,4 @@ three interfaces supported by Spot: shell commands, Python, or C++.
|
|||
- [[file:tut01.org][Parsing and Printing LTL Formulas]]
|
||||
- [[file:tut02.org][Relabeling Formulas]]
|
||||
- [[file:tut10.org][Translating an LTL formula into a never claim]]
|
||||
- [[file:tut20.org][Converting a never claim into HOA]]
|
||||
|
|
|
|||
315
doc/org/tut20.org
Normal file
315
doc/org/tut20.org
Normal file
|
|
@ -0,0 +1,315 @@
|
|||
#+TITLE: Converting a never claim into HOA
|
||||
#+SETUPFILE: setup.org
|
||||
#+HTML_LINK_UP: tut.html
|
||||
|
||||
The goal is to start from a never claim, as produced by Spin, e.g.:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
spin -f '[]<>foo U bar' > tut20.never
|
||||
cat tut20.never
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
never { /* []<>foo U bar */
|
||||
T0_init:
|
||||
do
|
||||
:: atomic { ((bar)) -> assert(!((bar))) }
|
||||
:: (1) -> goto T0_S53
|
||||
od;
|
||||
accept_S42:
|
||||
do
|
||||
:: (1) -> goto T0_S42
|
||||
od;
|
||||
T0_S42:
|
||||
do
|
||||
:: ((foo)) -> goto accept_S42
|
||||
:: (1) -> goto T0_S42
|
||||
od;
|
||||
T0_S53:
|
||||
do
|
||||
:: (1) -> goto T0_S53
|
||||
:: ((bar) && (foo)) -> goto accept_S42
|
||||
:: ((bar)) -> goto T0_S42
|
||||
od;
|
||||
accept_all:
|
||||
skip
|
||||
}
|
||||
#+end_example
|
||||
|
||||
and convert this into an automaton in [[file:hoa.org][the HOA format]].
|
||||
|
||||
Note that the automaton parser of Spot can read automata written
|
||||
either as never claims, in LBTT's format or in the HOA format, and
|
||||
there is no need to specify which format you expect. Even if our
|
||||
example use a never claim as input, the code we write will work with
|
||||
any of those formats.
|
||||
|
||||
* Shell
|
||||
|
||||
This is very simple: [[file:autfilt.org][=autfilt=]] can read automata in any of the
|
||||
supported formats, so all we have to do is to request the HOA output
|
||||
with =-H=:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
autfilt -H tut20.never
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
HOA: v1
|
||||
States: 5
|
||||
Start: 0
|
||||
AP: 2 "bar" "foo"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc complete
|
||||
--BODY--
|
||||
State: 0
|
||||
[0] 1
|
||||
[t] 2
|
||||
State: 1 {0}
|
||||
[t] 1
|
||||
State: 2
|
||||
[t] 2
|
||||
[0&1] 3
|
||||
[0] 4
|
||||
State: 3 {0}
|
||||
[t] 4
|
||||
State: 4
|
||||
[1] 3
|
||||
[t] 4
|
||||
--END--
|
||||
#+end_example
|
||||
|
||||
* Python
|
||||
|
||||
Another one-liner. The =spot.automaton()= function reads a single
|
||||
automaton, and each automaton has a =to_str()= method that can print
|
||||
in =hoa=, =lbtt=, =spin= (for never claim) or =dot=.
|
||||
|
||||
#+BEGIN_SRC python :results output :exports both
|
||||
import spot
|
||||
print(spot.automaton('tut20.never').to_str('hoa'))
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
HOA: v1
|
||||
States: 5
|
||||
Start: 0
|
||||
AP: 2 "bar" "foo"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc complete
|
||||
--BODY--
|
||||
State: 0
|
||||
[0] 1
|
||||
[t] 2
|
||||
State: 1 {0}
|
||||
[t] 1
|
||||
State: 2
|
||||
[t] 2
|
||||
[0&1] 3
|
||||
[0] 4
|
||||
State: 3 {0}
|
||||
[t] 4
|
||||
State: 4
|
||||
[1] 3
|
||||
[t] 4
|
||||
--END--
|
||||
#+end_example
|
||||
|
||||
* C++
|
||||
|
||||
Parsing an automaton is almost similar to [[file:tut01.org][parsing an LTL formula]]. The
|
||||
=hoa_parse()= function (despite the name, it can actually read never
|
||||
claims, or the LBTT or HOA formats) takes a filename, a reference to a
|
||||
=hoa_parse_error_list= object to populate (should errors be found) and
|
||||
a BDD dictionary (to be discussed later on this page). It returns a
|
||||
shared pointer to a structure that has two fields: =aborted= is a
|
||||
Boolean telling if the input automaton was voluntarily aborted (a
|
||||
feature of [[file:hoa.org][the HOA format]]), and =aut= is the actual automaton. The
|
||||
shared pointer returned by =hoa_parse()= might be null (in which case
|
||||
the the =hoa_parse_error_list= is guaranteed not to be empty), but
|
||||
since the parser performs some error recovery it is likely that an
|
||||
automaton is returned even in the presence of parse errors.
|
||||
|
||||
#+BEGIN_SRC C++ :results verbatim :exports both
|
||||
#include <string>
|
||||
#include <iostream>
|
||||
#include "hoaparse/public.hh"
|
||||
#include "twaalgos/hoa.hh"
|
||||
|
||||
int main()
|
||||
{
|
||||
std::string input = "tut20.never";
|
||||
spot::hoa_parse_error_list pel;
|
||||
spot::bdd_dict_ptr dict = spot::make_bdd_dict();
|
||||
spot::hoa_aut_ptr h = hoa_parse(input, pel, dict);
|
||||
if (spot::format_hoa_parse_errors(std::cerr, input, pel))
|
||||
return 1;
|
||||
// This cannot occur when reading a never claim, but
|
||||
// it could while reading a HOA file.
|
||||
if (h->aborted)
|
||||
{
|
||||
std::cerr << "--ABORT-- read" << '\n';
|
||||
return 1;
|
||||
}
|
||||
spot::print_hoa(std::cout, h->aut) << '\n';
|
||||
return 0;
|
||||
}
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
HOA: v1
|
||||
States: 5
|
||||
Start: 0
|
||||
AP: 2 "bar" "foo"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc complete
|
||||
--BODY--
|
||||
State: 0
|
||||
[0] 1
|
||||
[t] 2
|
||||
State: 1 {0}
|
||||
[t] 1
|
||||
State: 2
|
||||
[t] 2
|
||||
[0&1] 3
|
||||
[0] 4
|
||||
State: 3 {0}
|
||||
[t] 4
|
||||
State: 4
|
||||
[1] 3
|
||||
[t] 4
|
||||
--END--
|
||||
#+end_example
|
||||
|
||||
In automata, transitions guards are represented by BDDs. The role of
|
||||
=bdd_dict= object is to keep track of the correspondence between BDD
|
||||
variables and atomic propositions such as =foo= and =bar= in the above
|
||||
example. So each automaton has a shared pointer to some =bdd_dict=
|
||||
(this shared pointer is what the =bdd_dict_ptr= type is), and
|
||||
operations between automata (like a product) can only work on automata
|
||||
that share the same pointer. Here, when we call the automaton parser,
|
||||
we supply the =bdd_dict_ptr= that should be used to do the mapping
|
||||
between atomic propositions and BDD variables. Atomic propositions
|
||||
that were not already registered will get a new BDD variable number,
|
||||
and while existing atomic propositions will reuse the existing
|
||||
variable.
|
||||
|
||||
In the example for [[file:tut10.org][translating LTL into BA]], we did not specify any
|
||||
=bdd_dict=, because the =translator= object will create a new one by
|
||||
default. However it is possible to supply such a =bdd_dict= to the
|
||||
translator as well. Similarly, in the Python bindings, there is a
|
||||
global =bdd_dict= that is implicitly used for all operations, but it
|
||||
can be specified if needed.
|
||||
|
||||
* Additional comments
|
||||
|
||||
There are actually different C++ interfaces to the automaton parser,
|
||||
depending on your use case. For instance the parser is able to read a
|
||||
stream of automata stored in the same file, so that they could be
|
||||
processed in a loop. For this, you would instanciate a
|
||||
=hoa_stream_parser= object and call its =parse()= method in a loop.
|
||||
Each call to this method will either return one automaton, or
|
||||
=nullptr= if there is no more automaton to read. The =hoa_parse()=
|
||||
function is actually a simple wrapper that instanciate
|
||||
=hoa_stream_parser= and calls =parse()= once.
|
||||
|
||||
|
||||
In Python, you can easily iterate over a file containing multiple
|
||||
automata by doing:
|
||||
|
||||
#+BEGIN_SRC python :results output :exports code
|
||||
import spot
|
||||
for aut in spot.automata('tut20.never'):
|
||||
print(aut.to_str('hoa'))
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
HOA: v1
|
||||
States: 5
|
||||
Start: 0
|
||||
AP: 2 "bar" "foo"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc complete
|
||||
--BODY--
|
||||
State: 0
|
||||
[0] 1
|
||||
[t] 2
|
||||
State: 1 {0}
|
||||
[t] 1
|
||||
State: 2
|
||||
[t] 2
|
||||
[0&1] 3
|
||||
[0] 4
|
||||
State: 3 {0}
|
||||
[t] 4
|
||||
State: 4
|
||||
[1] 3
|
||||
[t] 4
|
||||
--END--
|
||||
#+end_example
|
||||
|
||||
In fact =spot.automaton()= is just a wrapper around =spot.automata()=
|
||||
to return only the first automaton.
|
||||
|
||||
Still in Python, both =spot.automaton()= and =spot.automata()= can
|
||||
accept three types of arguments:
|
||||
- file names (such as in the above examples)
|
||||
- commands that output automata on their standard output. Those can
|
||||
be any shell expression, and must have '=|=' as their last
|
||||
character. For instance here is how to convert Spin's output into
|
||||
LBTT's formula without using temporary files.
|
||||
#+BEGIN_SRC python :results output :exports both
|
||||
import spot
|
||||
print(spot.automaton('spin -f "[]<>p0" |').to_str('lbtt'))
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
: 2 1
|
||||
: 0 1 -1
|
||||
: 1 p0
|
||||
: 0 t
|
||||
: -1
|
||||
: 1 0 0 -1
|
||||
: 0 t
|
||||
: -1
|
||||
:
|
||||
|
||||
- a string that includes new lines, in which case it is assumed
|
||||
to describe an automaton, and is passed directly to the parser:
|
||||
|
||||
#+BEGIN_SRC python :results output :exports both
|
||||
import spot
|
||||
print(spot.automaton("""
|
||||
HOA: v1
|
||||
States: 2
|
||||
Start: 0
|
||||
AP: 1 "a"
|
||||
Acceptance: 1 Inf(0)
|
||||
--BODY--
|
||||
State: 0
|
||||
[0] 1
|
||||
State: 1 {0}
|
||||
[t] 1
|
||||
--END--
|
||||
""").to_str('spin'))
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
: never {
|
||||
: T0_init:
|
||||
: if
|
||||
: :: ((a)) -> goto accept_all
|
||||
: fi;
|
||||
: accept_all:
|
||||
: skip
|
||||
: }
|
||||
:
|
||||
Loading…
Add table
Add a link
Reference in a new issue