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.

Where can I find finite automata?

We consider finite automata as a special case of nested word automata (resp. visibly pushdown automata) where the call alphabet is empty, the return alphabet is empty, there are no call transitions and there are no return transitions. We use the data structures for nested word automata to represent finite automata and you can use every operation for nested word automata also for finite automata. If you implement an operation that works only on finite automata, you might want to use the static NestedWordAutomataUtil.isFiniteAutomaton(....) method to check you operand(s) and throw an UnsupportedOperationException if the operand is not a finite automaton.

Nonetheless, the syntax of Automata Script allows you to define a finite automaton (without explicitly setting empty call/return alphabets). This syntax can be seen in our finite automata demonstration example.

Where can I find Büchi automata?

We do not encode the accepting condition in automata data structures. Hence every automaton can be seen as a Büchi automaton or as an automaton on finite words. Operations for Büchi automata have the prefix buchi (e.g., buchiAccepts, buchiIsEmpty) whereas operations on finite words do not have this prefix (e.g., accepts, isEmpty).

Do you support other types of omega automata?

Not yet, but if you want to implement support for these we are happy to assist you.

Construction of Automata for non-on-demand operations

If you want to construct an automaton, you can construct an instance of the NestedWordAutomata class, this class has methods for adding states and transitions.

Operations with on-demand construction of automata

In our applications, we often apply operations in a row. E.g., if we check an inclusion A ⊆ B, we check emptiness of an intersection where one operand is the complementation of a totalized and determinized input automaton B. If we would construct determinization of B explicitly this would probably be a waste of resources since in many cases the intersection does not have to see the full state space of the determinized automaton. In our program verification algorithm the problem is even more severe because the automaton B is not given explicitly and the check if specific transition exists is costly (in fact we do not check if a certain transition exists by we ask for all successors of a given state under a given symbol). We approach this problem by supporting on-demand automata implemementations. These implementations do not store all states and transitions of the automaton explicitly but must only be able to provide initial states and successor transitions for given states. TODO

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.