The jhoaf Command-Line Tool
The jhoafparser Library for the Hanoi Omega-Automata Format (HOAF), version 1.1.1

The jhoafparser library provides a command-line interface to some of the functionality. This can be roughly divided into two broad areas:

We assume here that the reader is familiar with the basic concepts of the Hanoi Omega-Automata Format (HOAF).


Obtaining and invoking the command-line tool

We assume here that you have either downloaded the JAR or ZIP file from the website. With the JAR file, the command-line tool can be invoked via

java -jar jhoafparser-xx.yy.jar ...

where xx.yy is the version. For the ZIP file, the command-line tool can be invoked (on Linux or OS X) from unpacked top-level directory via

./jhoaf ...

In the sequel, for simplicity we use the latter notation, but you can substitute the invocation of the JAR file in the following examples.

Getting Help


./jhoaf help

you'll obtain a brief description of the supported commands and flags.

Input / Output

The command-line tool reads the file(s) specified on the command-line, performs the required processing and outputs the result to the standard output. The hyphen character '-' can be used instead of the filename for reading from standard input. Below, we provide some examples of invoking the command-line tool:

In the simplest case, the following command parses the automaton from automaton.hoa and prints the result (the parsed automaton without comments, extra whitespace, etc) to the console:

./jhoaf print automaton.hoa

In the next example, we pipe the output of some other tool to the input of jhoaf:

./some-hoa-producer | ./jhoaf print -

The output can be captured as usual to a file using redirection:

./some-hoa-producer | ./jhoaf print - > result.hoa

Note: Take care that you do not simultaneously read and write from/to the same file!

Commands and Flags

The general structure of invoking the command line-tool is

./jhoaf command flag(s) file(s)

Multiple automata

The HOA format supports the streaming of automata, i.e., the ability to represent a sequence of automata in a single file. This is useful when using tools as a component in a pipe. You can specify multiple files on the command-line, which will be read sequentially. Likewise, if there are multiple automata in a file (or read from the standard input), they will be processed one after another.

Note: If there is an error in one of the automata, the command-line tool will abort all processing!

Exit value

If you want to use the command-line tool in scripts, the value returned by the tool on exit is useful for diagnosing errors. The tool will return 0 for success/no errors. If there are errors during the processing of the automata, the value 1 will be returned. If there are problems with the invocation (invalid command-line arguments, ...), the value 2 will be returned.

Validating Automata

To check that an automaton in HOA format can be successfully parsed, run

./jhoaf parse automaton-file.hoa
Parsing OK

If everything went fine, the tool will output that parsing was OK, otherwise there will be an error message indicating what went wrong.

Upon success, the automaton

The semantic validations can be disabled by the command-line option --no-validate. The following command will only check the syntactic correctness according to the HOA format:

./jhoaf parse --no-validate automaton.hoa

Transforming the Automaton

Pretty-printing the Automaton

The simplest transformation is barely a transformation at all. Via

./jhoaf print automaton-file.hoa

the automaton is simply parsed and printed back to the standard output.

As comments and superfluous whitespace are ignored by the parser, this transforms the automaton into some kind of canonical form, with the different elements of the HOA format each placed on a single line.

Resolving Aliases

The command-line option --resolve-aliases activates a transformation that (1) removes the Alias: ? definitions and (2) resolves all @alias references in transition labels.

The following command reads the automaton, resolves the aliases and prints the resulting automaton:

./jhoaf print --resolve-aliases automaton-file.hoa

The option --resolve-aliases can be used with all other commands and options.

Simple Transformations

With the --transform=transform1,transform2,... option, one or more transformations can be specified. They will generally be applied to the automaton in order.

Some of the transformations are applied on-the-fly, i.e., they are performed without first having to parse and store the automaton in memory. Others are applied on the whole automaton, i.e., the automaton is first parsed, stored into memory and then manipulated. If there is a mix of transformations, some that are on-the-fly and some that are not, the non-on-the-fly transformation are batched first, applied in order and then, subsequently, the remaining on-the-fly transformations are applied in order. Most of the time, the ordering should not matter.

The supported transformations are:

Transforming Between Acceptance Conditions

In some cases it is possible to transform an automaton from one acceptance condition to another, without changing the underlying structure of the automaton. This is the case if, for particular automaton, the acceptance conditions differ syntactically but can be easily transformed:

./jhoaf convert-acceptance acceptance1,acceptance2,... automaton-file.hoa

Given one or more target acceptance conditions, attempts are made to transform the automaton to the target conditions, in order. For example, a Büchi automaton will be easily transformed to a Rabin automaton. The procedure is as follows:

  1. First the existing acceptance condition will be simplified, e.g., Inf(0)|t will be simplified to t
  2. Then, an attempt is made to bring the acceptance condition into one of the specified canonical forms. This can involve renaming, reordering or complementation of acceptance sets, as well as introducing new acceptance sets (for true/false) to use in the more complex acceptance conditions.
  3. The membership of transitions and states in the acceptance sets are then changed accordingly.

Note that this transformation relies only on the acceptance condition, no information about the use of the acceptance sets in the automaton (on states/transitions) is taken into account.

As an example, the acceptance condition

Acceptance: 3 (Inf(2) | (Fin(0) & Inf(!1))) & t

would be transformed into the Rabin condition (with convert-acceptance Rabin)

Acceptance: 4 Fin(0) & Inf(1) | Fin(2) & Inf(3)
acc-name: Rabin 2
by adding an empty acceptance set 0, renaming set 2 to 1 and set 0 to 2 and complementing set 1 to obtain set 3. The superfluous & t is removed as well.

Converting to Generalized-Büchi Acceptance

For all deterministic or non-deterministic automata, we can convert to an equivalent non-deterministic generalized-Büchi automaton, i.e., one with acc-name: generalized-Buchi. This transformation is applied on the syntactical level and introduces several copies of the automaton, each corresponding to one way of satisfying the original acceptance condition.

./jhoaf convert-to-buchi automaton-file.hoa

This transformation can be highly inefficient and is intended as a proof-of-concept implementation and for the conversion of rather small automata.

Tracing, Implementation Details

If you wish to implement your own transformations or want to use the jhoafparser library, it might be interesting to play around with the --trace option:

./jhoaf parse --trace automaton-file.hoa

If activated, tracing will output the sequence of method calls into the HOAConsumer by the parser. This can be used to study the correspondence of syntactical elements in the HOA format and the method calls.

The command-line utility is implemented in the class. It relies on the various HOAConsumers for the functionality and is a good entry-point for further investigations.

If you have further questions, find bugs or want to tell us about your use of the jhoafparser library, please feel free to contact us!

(c) 2014-2015 Joachim Klein <>, David Müller <>