Conversion to BA format?

[JakeGinesin]

Are there any existing tools to convert HOA to the BA format?

[adl]

I believe @pierreganty might have some script for that.

[pierreganty]

See here: https://github.com/Mazzocchi/FORKLIFT/blob/master/hoaftoba.awk It assumes you first preprocess your automaton with autfilt --split-edges then what's left to do is "just" some rewriting. The rewriting is what the above AWK script accomplishes.

[adl]

Inspired from Pierre's script, I think the following untested Python script should work. It uses Spot's python bindings to read the input (which can be any format supported by Spot), do the split, and print the result in BA format. To keep labels short, it prints the unique BDD identifier that Spot uses internally to represent those labels. It will also convert transition-based acceptance to state-based acceptance.

#!/usr/bin/env python3
import spot, sys

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)

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)

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)

[JakeGinesin]

Sweet, thanks so much! This seems to work nicely

[pierreganty]

I would support to include the above script in the next spot release. However, I would push back any effort to integrate it in the C++ codebase since it would send the message you are supporting a new input format (which I would not recommend). However, if the user really wants BA format, there is a Python script provided as a courtesy. Incidentally, it showcases the Python interface.

[adl]

I was considering adding this script, and a C++ version, to the code examples :-)

[pierreganty]

As code examples that make sense, actually.

[adl]

This code and some variant with separate_edges() instead of split_edges() can now be found at https://spot.lre.epita.fr/tut25.html