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:09] – [Learning Algorithms for Büchi automata] liyongusage [2018/11/15 20:21] (current) – [Lazy Equivalence Check] liyong
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.1542182945.txt.gz · Last modified: 2018/11/14 16:09 by liyong