Skip to content

AddAutomataOperation

Jump to bottom
Matthias Heizmann edited this page May 19, 2017 · 36 revisions

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 interface 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 operation was canceled externally for a different reason. The constructor for each operation should take as first argument an AutomataLibraryServices object, say, services. The cancelation request is queried by services.getProgressAwareTimer().continueProcessing(). This method should be called in every time-consuming loop. In case this method returns false the operation should throw an 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 the 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 acceptance 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 ω-automata?

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

Construction of states

TODO: Link to IStateFactory, write documentation there

Construction of automata for non-on-demand operations

If you want to construct an automaton, you can construct an instance of the NestedWordAutomaton class. This class provides 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 performed 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 a specific transition exists is costly (in fact, we do not check if a certain transition exists but 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: explain link to interface and nice implementation

Test operation on multiple files

We do not use unit tests in the automata library. Instead, we write for each operation a bunch of .ats files and use the testing framework of Ultimate to run the Automata Script interpreter on several files. In order to get a well-tested operation you should do two things:

  1. Use assert statements in you .ats file. A test run of an .ats file is considered erroneous if some assert statement was evaluated to false.
  2. Implement the checkResult(...) method of your IOperation. If you run the JavaVM with assertions enabled (parameter -ea), the Automata Script interpreter will run the checkResult methods after each run of an operation and will throw an AssertionError if the checkResult(...) method returned false.

Manual tests

A typical example for such a test suite is the AutomataScriptTestSuite. It executes all .ats files from the folders which are hardcoded in this test suite .java file. You run the testsuite by opening this file in Eclipse and "Run As > JUnit Plug-in Test" (not "JUnit Test"!). Do not forget to set the enable assertions (-ea) parameter for the Java virtual machine.

Automatic tests

Every night we run all .ats files that are in the trunk/examples/Automata/regression/ subfolder. You can see the results online (TODO find link). Furthermore you can see the line coverage of your tests (TODO find link).

Run benchmarks on multiple files

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 ω-words, nested words, lasso-shaped ω-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.
Clone this wiki locally