320 lines
7.5 KiB
Org Mode
320 lines
7.5 KiB
Org Mode
# -*- coding: utf-8 -*-
|
|
#+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
|
|
=parse_aut()= function takes a filename, a reference to a
|
|
=parse_aut_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 =parse_aut()= might be null (in which case
|
|
the the =parse_aut_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 "parseaut/public.hh"
|
|
#include "twaalgos/hoa.hh"
|
|
|
|
int main()
|
|
{
|
|
std::string input = "tut20.never";
|
|
spot::parse_aut_error_list pel;
|
|
spot::bdd_dict_ptr dict = spot::make_bdd_dict();
|
|
spot::parsed_aut_ptr pa = parse_aut(input, pel, dict);
|
|
if (spot::format_parse_aut_errors(std::cerr, input, pel))
|
|
return 1;
|
|
// This cannot occur when reading a never claim, but
|
|
// it could while reading a HOA file.
|
|
if (pa->aborted)
|
|
{
|
|
std::cerr << "--ABORT-- read\n";
|
|
return 1;
|
|
}
|
|
spot::print_hoa(std::cout, pa->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
|
|
=automaton_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 =parse_aut()=
|
|
function is actually a simple convenience wrapper that instanciate
|
|
an =automaton_stream_parser= and calls its =parse()= method 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 (or multiple automata) 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
|
|
: }
|
|
:
|
|
|
|
#+BEGIN_SRC sh :results silent :exports results
|
|
rm -f tut20.never
|
|
#+END_SRC
|