Converting a never claim into HOA

This is very simple: autfilt can read automata in any of the supported formats, and outputs it in the HOA format by default:

autfilt tut20.never

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--

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.

import spot
print(spot.automaton('tut20.never').to_str('hoa'))

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--

Parsing an automaton is similar to parsing an LTL formula. The parse_aut() function takes a filename and a BDD dictionary (to be discussed later on this page). It returns a shared pointer to a structure that has a couple of important fields: aborted is a Boolean telling if the input automaton was voluntarily aborted (a feature of the HOA format), errors is a list of syntax errors that occurred while parsing the automaton (printing these errors is up to you), and aut is the actual automaton. The parser usually tries to recover from errors, so aut may not be null even if errors is non-empty.

#include <string>
#include <iostream>
#include <spot/parseaut/public.hh>
#include <spot/twaalgos/hoa.hh>

int main()
{
  spot::bdd_dict_ptr dict = spot::make_bdd_dict();
  spot::parsed_aut_ptr pa = parse_aut("tut20.never", dict);
  if (pa->format_errors(std::cerr))
    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;
}

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--

In the Spot representation of automata, transitions guards are represented by BDDs. The role of the 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 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.

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 instantiate a spot::automaton_stream_parser object and call its parse() method in a loop. Each call to this method will either return one spot::parsed_aut_ptr, or nullptr if there is no more automaton to read. The parse_aut() function is actually a simple convenience wrapper that instantiates an automaton_stream_parser and calls its parse() method once.

In Python, you can easily iterate over a file containing multiple automata by doing:

import spot
for aut in spot.automata('tut20.never'):
    print(aut.to_str('hoa'))

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--

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.

import spot
print(spot.automaton('spin -f "[]<>p0" |').to_str('lbtt'))

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:

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'))

never {
T0_init:
  if
  :: (a) -> goto accept_all
  fi;
accept_all:
  skip
}