Regular Omega Language Learning (ROLL)

User Tools

Site Tools

Trace:
usage

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
usage [2018/11/14 16:08] – [Data Structures to Store Membership Query Results] liyongusage [2018/11/15 20:21] (current) – [Lazy Equivalence Check] liyong
Line 75: Line 75:
 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. 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. +  * **-periodic**. Learning based on the periodic FDFA. 
-  * -syntactic. Learning based on the syntactic FDFA (**default setting**). +  * **-syntactic**. Learning based on the syntactic FDFA (**default setting**). 
-  * -recurrent. Learning based on the recurrent FDFA.+  * **-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]. 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].
Line 90: Line 90:
  
  
-  * -under. This method under-approximates the ultimately periodic words accepted by the conjectured FDFA. +  * **-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.+  * **-over**. It over-approximates the ultimately periodic words accepted by the conjectured FDFA.
  
 === Limit Deterministic Büchi Automata === === 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]. +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. An example is given below.
 <code> <code>
Line 105: Line 105:
  
 If you want to reuse the counterexample returned by the teacher as much as possible, you can use the 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 TESTED). +lazy equivalence check optimization as follows (NOT FULLY TESTED). 
-This option is not encouraged since it may result in larger output automaton.+This option is **not encouraged** since it may result in larger output automaton.
 <code> <code>
 java -jar ROLL.jar learn aut.ba -table -periodic -lazyeq java -jar ROLL.jar learn aut.ba -table -periodic -lazyeq
Line 114: Line 114:
  
 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. 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**+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 ==== ==== Verbose Log Level ====
usage.1542182926.txt.gz · Last modified: 2018/11/14 16:08 by liyong