Skip to content

AddAutomataOperation

Jump to bottom
Daniel Dietsch edited this page Feb 11, 2022 · 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

We construct states in our automata library according to the interface documentation of the IStateFactory.

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.

The most basic interface for the construction of on-demand operations is the INwaOutgoingLetterAndTransitionProvider, a more developer-friendly variation is the INwaSuccessorStateProvider. Examples for implementations are the BuchiComplementFKVNwa and the BuchiComplementNCSBNwa.

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 IOperation and will throw an AssertionError if the method returned false. Note that we only test the IOperation that is explicitly called in the .ats file, i.e., we ignore subcalls to other IOperations.

Manual tests

A typical example for a test suite is the AutomataScriptTestSuite. It executes all .ats files from the folders that are hardcoded in this test suite .java file. You run the test suite by opening this file in Eclipse and selecting "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. Furthermore you can see the line coverage of your tests.

Run benchmarks on multiple files

In order to evaluate automata operations on several (hundreds, thousands) automata we also use our testing framework (see above). Typically, you have to provide two ingredients for an evaluation.

  1. Automata. You will find automata produced by Ultimate Automizer in our automata benchmark repository. If these are not appropriate for your purpose, ask Matthias for other automata.
  2. Support for statistics data. Use the AutomataOperationStatistics to collect interesting information, e.g., about input and output, of your operation.

Writing the operation that you want to evaluate into several (hundreds, thousands) of automata files can be tedious. Therefore the Automata Script interpreter has a special mode in which all operations written in the .ats file are ignored and a user-defined expression is executed. In this expression $1 refers to the first automaton that is defined in the .ats file, $2 refers to the second automaton, etc. You find examples for preference files (.epf) that enable this special mode in the Automata Script preference file folder.

Using your preference files, you write a test suite analogously to, e.g., the BuchiComplementationTestSuite, the BuchiIsIncludedTestSuite, or the AutomataMinimizationTestSuite. Please note that the name of operations typically occurs twice. First as name of the preference file, but second in a filter of the output CSV.

Next, you run the testfile as explained in the section on tests. However, for your benchmarks you probably want to drop the -ea argument for the Java Virtual Machine.

After the test suite was run successfully, you find the output in the your trunk/source/UltimateTest/target/surefire-reports/ folder. The output also includes a CSV file that contains the collected statistics data of all operations.

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