[[start|{{:home.png?16}}]][[start| Main]]
[[usage|{{:imac.png?16}}]][[usage|How to Use ROLL in Command Line]]
[[how_to_use|{{:pencil.png?16}}]][[how_to_use|How to Use ROLL in JAVA Program]]
[[release|{{:tool.png?16}}]][[release| Tool ]]
[[contact|{{:letter.png?16}}]][[contact| Contact ]]


====== Command Line Usage ======

The standard way for executing ROLL from command line is
<code>
java -jar ROLL.jar command input_files [options]
</code>
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 [[play|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 [[http://www.languageinclusion.org/doku.php?id=tools|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 [[http://adl.github.io/hoaf/|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 [[complement|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:
<code>
java -jar ROLL.jar learn aut.ba
</code>

==== Help ====

ROLL can be launched by using the command
<code>
 java -jar ROLL.jar
</code>
,  which is equal to the following two commands:
<code>
java -jar ROLL.jar -h
java -jar ROLL.jar help
</code>
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
<code>
-log <file>
</code>

==== 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
<code>
-out <file>
</code>



==== 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<sup>$</sup> learner [4] based on the DFA learning and the L<sup>ω</sup> learner [6] based on three canonical FDFA learning algorithms [4].
The default learning algorithm for Büchi automata in ROLL is the L<sup>ω</sup> learner.
For the L<sup>ω</sup> 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<sup>$</sup> learner to learn Büchi automata. We remark that the DFA learning algorithm used for L<sup>$</sup> learner is an improved version of L<sup>*</sup> algorithm [1].
An example of the use of the L<sup>$</sup> learner is the following, which chooses a classification tree to store the results of membership queries during the learning procedure. 
<code>
java -jar ROLL.jar learn aut.ba -tree -ldollar
</code>

==== 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<sup>ω</sup> 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<sup>ω</sup> learner [9]. 
An example is given below.
<code>
java -jar ROLL.jar learn aut.ba -table -periodic -ldba
</code>


==== 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.
<code>
java -jar ROLL.jar learn aut.ba -table -periodic -lazyeq
</code>

==== 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 [[http://www.languageinclusion.org/doku.php?id=tools|RABIT]] tool and the standard [[http://adl.github.io/hoaf/|HANOI format]].
The two formats are identified by their file extensions **.ba** and **.hoa** respectively.