Trustworthy Intelligent Systems

Command Line Usage

The standard way for executing ROLL from command line is

java -jar ROLL.jar command input_files [options]

The available commands in ROLL are summarized as running modes in the following and the introduction of the options available in the tool is also provided.

Running Modes

There are several running modes in ROLL, namely helping mode, testing mode, playing mode, learning mode, converting mode, complementing mode, inclusion testing mode and sampling mode.

  • help. Show the help page (same as the option -h).
  • test n k. Test the learning algorithms implemented in the tool with n randomly generated Büchi automata of k states. This mode tries to expose possible bugs in the tool with generated input Büchi automata.
  • play. You play a teacher to teach ROLL to learn a language you have in mind. An example can be found here.
  • learn <aut.hoa|aut.ba>. Learn an input Büchi automaton whose language is equivalent to the input automaton <aut.hoa|aut.ba> with the help of RABIT tool.
  • convert A.ba B.ba. Convert the input files A.ba B.ba in the BA format to the files A.hoa B.hoa respectively in the HANOI format. The other direction is also possible.
  • complement <aut.hoa|aut.ba>. Complement the input Büchi automaton specified by the file <aut.hoa|aut.ba> based on the learning algorithms. An example can be found here.
  • include A.ba B.ba. Test the language inclusion between two Büchi automata specified in A.ba and B.ba.
  • sampeq e d. Learn the input Büchi automaton with the help of the PAC teacher based on word sampling.

For example, to learn a Büchi automaton given by the file aut.ba, a valid command line to use the learning algorithm is the following:

java -jar ROLL.jar learn aut.ba

Help

ROLL can be launched by using the command

 java -jar ROLL.jar

which is equal to the following two commands:

java -jar ROLL.jar -h
java -jar ROLL.jar help

All above commands will show help page.

Log

By default, all the execution details will be output by the Java object System.out. However, you can also save all the execution log information in the <file> by providing an option

-log <file>

Output an Automaton

By default, a learned or a complement automaton will be output along with the execution log information. But you can also save the learned automaton or the complement automaton into a given <file> by providing the option

-out <file>

Data Structures to Store Membership Query Results

ROLL supports both observation tables and classification trees to store membership query results. You can specify which data structure is going to be used in the learning procedure by following two options.

  • -table. Choose the observation tables (default setting).
  • -tree. Use classification trees.

Learning Algorithms for Büchi automata

There are two learning algorithms for Büchi automata in ROLL, namely the L^{$} learner4 based on the DFA learning and the LωL^ω learner6 based on three canonical FDFA learning algorithms4. The default learning algorithm for Büchi automata in ROLL is the LωL^ω learner. For the LωL^ω learner, you can choose one of the following three options to decide which canonical FDFA learner will be used to learn Büchi automata.

  • -periodic. Learning based on the periodic FDFA.
  • -syntactic. Learning based on the syntactic FDFA (default setting).
  • -recurrent. Learning based on the recurrent FDFA.

You can also use the option -ldollar instead to select the L^{$} learner to learn Büchi automata. We remark that the DFA learning algorithm used for the L^{$} learner is an improved version of the L* algorithm1. An example of the use of the L^{$} learner is the following, which chooses a classification tree to store the results of membership queries during the learning procedure.

java -jar ROLL.jar learn aut.ba -tree -ldollar

From an FDFA to a BA

In ROLL, you can also specify which method to transform an FDFA to a Büchi automaton in the LωL^ω learner by means of following two options.

  • -under. This method under-approximates the ultimately periodic words accepted by the conjectured FDFA.
  • -over. It over-approximates the ultimately periodic words accepted by the conjectured FDFA.

Limit Deterministic Büchi Automata

You can also get a limit deterministic Büchi automaton as the final output automaton by giving the option -ldba when using the LωL^ω learner9. An example is given below.

java -jar ROLL.jar learn aut.ba -table -periodic -ldba

Lazy Equivalence Check

If you want to reuse the counterexample returned by the teacher as much as possible, you can use the lazy equivalence check optimization as follows (NOT FULLY TESTED). This option is not encouraged since it may result in larger output automaton.

java -jar ROLL.jar learn aut.ba -table -periodic -lazyeq

Counterexample Analysis

When receiving a counterexample, the learner has to find a valid suffix of the counterexample as a new experiment in order to identify more states in the target automaton. By default, ROLL will use a linear search to find that suffix, but you can also choose to use binary search to do that by giving the option -bs (NOT FULLY TESTED).

Verbose Log Level

In ROLL, there is an option -v <value> with which you can set the verbosity level of the log output. The argument <value> is a value between 0 and 2, with 2 being the highest verbose log level. With the default verbose log level 0, there is a minimal output for the learning procedure. You can see a sequence of log messages like “Analyzing counterexample for FDFA learner…” telling you which stage the learning procedure gets with the verbose log level 1. You can see more details on the learning procedure with the verbose log level 2, such as the current observation table of the learner. However, with the verbose log level 2, you may see some word which is a sequence of unprintable characters. This is because we map every original input letter to an integer value as a character in our Alphabet object. Nonetheless, you can define the Alphabet object of the automata with printable characters when programming with the ROLL library.

Automata Format

ROLL accepts an automaton in the BA format defined on the webpage of RABIT tool and the standard HANOI format. The two formats are identified by their file extensions .ba and .hoa respectively.