AddAutomataOperation

How-to add a new automata operation

Automata in Ultimate

The automata support in Ultimate is split into two "modules".

• The actual automata library which contains the implementations of automata and their operations. If you want to integrate our automata library in your tool, this module is sufficient.
• The Automata Script Interpreter which is a text-based user interface for the automata library. Automata Script is a file format that allows you to write down automata and to write down automata operations that should be executed by Ultimate. You can find several examples of these files on the Automata Library website

Add a new Operation

Implement an IOperation according to the conventions written in the class documentation. If your class file is stored in one of the following packages or subfolders, it will be immediately available to the Automata Script Interpreter.

• "de.uni_freiburg.informatik.ultimate.automata.alternating",
• "de.uni_freiburg.informatik.ultimate.automata.nestedword.buchi",
• "de.uni_freiburg.informatik.ultimate.automata.nestedword.operations",
• "de.uni_freiburg.informatik.ultimate.automata.petrinet",
• "de.uni_freiburg.informatik.ultimate.automata.tree.operations"

We note that automata operations in Automata Script are not case sensitive.

Timeout Management

Ultimate does not have any capabilities to kill running operations. Ultimate provides only a service that knows if the timeout specified by the caller is already overdue or the operations was cancelled externally for a different reason. The constructor or each operation should takes as first argument a AutomataLibraryServices object. The cancellation request is queried by mServices.getProgressAwareTimer().continueProcessing(). This method should be called in every time consuming loop. In case this method returns false the operation should throw a AutomataOperationCanceledException. Callers of automata operations will catch this exception and handle it accordingly.

Limitations of Automata Script

The types supported by the Automata Script Interpreter are

• bool
• int
• all types of automata supported by ultimate
• various kinds of words (word, lasso-shaped omega words, nested words, lasso-shaped omega nested words, trees) Hence, if your operation takes as input or returns a different type (e.g., HashSet of automata) you will not be able to use the operation in the Automata Script Interpreter.

On-demand Operations

TODO

bring everything that is visible from outside in a consistent state.

Every operation should check if