Using the jhoafparser Library
The jhoafparser Library for the Hanoi Omega-Automata Format (HOAF), version 1.1.1

The jhoafparser library can be used to parse and process ω-automata in the HOA format. We assume here that the reader is familiar with the basic concepts of the Hanoi Omega-Automata Format (HOAF).

General Structure

The two main building blocks of the parser library are the parser and classes implementing the HOAConsumer interface. A HOAConsumer has methods corresponding to the various elements that can occur in a HOA automaton. While parsing, the parser calls each of these methods to indicate that this particular element has just occurred.

A Basic Parser

The most basic use of the jhoafparser library is shown in the following code snippet:

package jhoafparser.examples;

import jhoafparser.consumer.HOAConsumerPrint;
import jhoafparser.parser.HOAFParser;
import jhoafparser.parser.generated.ParseException;

/** The most basic HOA parser: Read an automaton from input and print it to the output. */
public class BasicParser1
{
    public static void main(String[] args) {
        try {
            HOAFParser.parseHOA(System.in, new HOAConsumerPrint(System.out));
        } catch (ParseException e) {
            System.out.println("ParseException: "+e);
        }
    }
}

The parser reads from System.in and calls into a HOAConsumerPrint object that just outputs the elements to System.out.

Chaining Multiple HOAConsumers: HOAIntermediate

The HOAIntermediate class, which itself implements the HOAConsumer interface, provides the basis for chaining multiple HOAConsumers, one after another, each reading the output of the previous one.

Consider the following example:

package jhoafparser.examples;

import java.util.List;

import jhoafparser.ast.AtomLabel;
import jhoafparser.ast.BooleanExpression;
import jhoafparser.consumer.HOAConsumer;
import jhoafparser.consumer.HOAConsumerException;
import jhoafparser.consumer.HOAConsumerNull;
import jhoafparser.consumer.HOAIntermediate;
import jhoafparser.parser.HOAFParser;
import jhoafparser.parser.generated.ParseException;

/** Demonstrating the use of HOAIntermediates */
public class BasicParser2
{
    static class CountStates extends HOAIntermediate {
        public int count = 0;

        public CountStates(HOAConsumer next) {
            super(next);
        }

        @Override
        public void addState(int id,
                             String info,
                             BooleanExpression<AtomLabel> labelExpr,
                             List<Integer> accSignature) throws HOAConsumerException {
            count++;
            next.addState(id, info, labelExpr, accSignature);
        }
    }

  public static void main(String[] args) {
        try {
            CountStates counter = new CountStates(new HOAConsumerNull());
            HOAFParser.parseHOA(System.in, counter);

            System.out.println("Number of state definitions = " + counter.count);
        } catch (ParseException e) {
            System.out.println("ParseException: "+e);
        }
    }
}

We define Counter as a HOAIntermediate. Its constructor takes the next HOAConsumer in the chain, which can again be a HOAIntermediate. Here, we are passing a HOAConsumerNull object, which does nothing when called, acting as a "no-operation" end of the consumer chain. Inside the Counter, we override the addState method, which is called for each State: definition in the automaton. We count the number of definitions and pass along the arguments to the next consumer. In the end, we just output the count of the definitions.

Handling Multiple Automata

Until now, we provided the parser with a single HOAConsumer, which is suitable if exactly one automaton should be parsed. To be able to parse multiple automata, we have to provide the parser with a factory that can be used to create HOAConsumer chains. These are recreated for each new automaton discovered in the stream:

package jhoafparser.examples;

import java.util.List;

import jhoafparser.ast.AtomLabel;
import jhoafparser.ast.BooleanExpression;
import jhoafparser.consumer.HOAConsumer;
import jhoafparser.consumer.HOAConsumerException;
import jhoafparser.consumer.HOAConsumerFactory;
import jhoafparser.consumer.HOAConsumerNull;
import jhoafparser.consumer.HOAIntermediate;
import jhoafparser.parser.HOAFParser;
import jhoafparser.parser.generated.ParseException;

/** Demonstrating the use of HOAConsumerFactory */
public class BasicParser3
{
    static class CountStates extends HOAIntermediate {
        public int count = 0;

        public CountStates(HOAConsumer next) {
            super(next);
        }

        public static HOAConsumerFactory getFactory(final HOAConsumerFactory next)
        {
            return new HOAConsumerFactory() {
                @Override
                public HOAConsumer getNewHOAConsumer()
                {
                    return new CountStates(next.getNewHOAConsumer());
                }
            };
        }

        @Override
        public void addState(int id,
                             String info,
                             BooleanExpression<AtomLabel> labelExpr,
                             List<Integer> accSignature) throws HOAConsumerException {
            count++;
            next.addState(id, info, labelExpr, accSignature);
        }

        @Override
        public void notifyEnd() {
            System.out.println("Number of state definitions = " + count);
        }
    }

    public static void main(String[] args) {
        try {
            HOAFParser.parseHOA(System.in,
                                CountStates.getFactory(HOAConsumerNull.getFactory()));
        } catch (ParseException e) {
            System.out.println("ParseException: "+e);
        }
    }
}

The HOAConsumer API

The starting point for learning about the HOAConsumer API is the JavaDoc documentation of the HOAConsumer interface.

Another good introduction is the source code of the HOAConsumerPrint class, as it translates back from the method calls in the HOAConsumer interface to the textual representation of the HOA format.

Some further tidbits that might be useful:


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>