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:

• Validating an automaton (no syntax errors, declared properties are correct, ...)
• Transforming an automaton (translating from state- to transition-based acceptance, ...)

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

General

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

With

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

• has been successfully parsed (syntax conforms to the HOA format),
• properties specified in the header have been verified to be correct (violations of state-labels, trans-labels, implicit-labels, explicit-labels, state-acc, trans-acc, no-univ-branch, colored are currently detected; for the deterministic and complete properties, violations are currently only detected when implicit transition labels are used),
• if an acc-name header has been provided and is one of the standard acceptance conditions specified in the format, the correspondence with the Acceptance header has been verified
• the number, ordering and names of the states are valid with regard to the restrictions specified in the HOA format,
• if implicit transition labels are used, the required number is present,
• alias definitions are non-recursive and all aliases, atomic propositions and acceptance sets that are used are defined.

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:

• state-acc
  Transform to state-based acceptance. This transformation is applied on the stored automaton. The acceptance on transitions are pushed to the successor state, which will in general increase the number of states in the automaton. If the automaton already only uses state-based acceptance, the transformation is skipped.
• trans-acc
  Transform to transition-based acceptance. This transformation is applied on-the-fly. Acceptance on a state is combined with the acceptance on outgoing transitions. The number of states remains the same.
• explicit-labels
  Transform to explicit labels. This transformation is applied on the stored automaton. Replaces implicit transition labels by explicit labels. This transformation will introduce aliases for each of the implicit edge labels.
• deduce-properties
  Deduce properties and add in the properties: header. This transformation is applied on the stored automaton. Currently, the following properties will be deduced: state-labels, trans-labels, implicit-labels, explicit-labels, state-acc, trans-acc, univ-branch, no-univ-branch and in some cases (only implicit labels) deterministic, complete.
  This transformation is applied on the stored automaton.
• deduce-accname
  Tries to deduce one of the canonical acceptance conditions for the acc-name header.
  This transformation analyzes the Acceptance-header and checks whether a corresponding canonical acc-name can be used. If that is the case, the automaton with the deduced acc-name header is output.
  The acceptance conditions are tried in the following order:
  all, none, Buchi, co-Buchi, generalized-Buchi, generalized-co-Buchi, Rabin, Streett.
  The methods that are tried are the same as those described for the convert-acceptance command described below.
  This transformation is applied on-the-fly.
• dnf-acceptance
  Transform Acceptance condition into DNF (disjunctive normal form), i.e., a top-level disjunction of conjunctions of acceptance atoms. This transformation is applied on-the-fly. Note that this transformation can incur an exponential blow-up in the size of the Acceptance condition.
• add-property(p)
  Add property p to the automaton, where p can be any string. This transformation is applied on-the-fly.
• resolve-aliases
  Resolves aliases, same as the --resolve-aliases option. Using the --resolve-aliases option will resolve aliases as the very first step, while explicitly specifying the transformation provides control over the point at which aliases are resolved. This transformation is applied on-the-fly.

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

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 jhoafparser.tools.JHOAFCmdLine 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 <klein@tcs.inf.tu-dresden.de>, David Müller <david.mueller@tcs.inf.tu-dresden.de>