[[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 ]]

====== How to use ROLL in JAVA Program ======


Below we demonstrate how to use our learner to learn the ω-regular language L=a<sup>ω</sup>+ ab<sup>ω</sup>. Please make sure you have all dependent libraries when you use ROLL.
  
=== Prepare a BA file ===
Every transition label should be exactly a string.
<code java>
[0]
a,[0]->[1]
a,[1]->[1]
a,[0]->[2]
b,[2]->[2]
[1]
[2]
</code>
In ROLL, one can create the above Büchi automaton as follows:
<code java>
// first create an alphabet
Alphabet alphabet = new Alphabet();
alphabet.addLetter('a');
alphabet.addLetter('b');
// create an NBA with alphabet
NBA target = new NBA(alphabet);
target.createState();
target.createState();
target.createState();
        
// add transitions for NBA recognizing a^w + ab^w
int fst = 0, snd = 1, thd = 2;
target.getState(fst).addTransition(alphabet.indexOf('a'), snd);
target.getState(fst).addTransition(alphabet.indexOf('a'), thd);
target.getState(snd).addTransition(alphabet.indexOf('a'), snd);
target.getState(thd).addTransition(alphabet.indexOf('b'), thd);
target.setInitial(fst);
target.setFinal(snd);
target.setFinal(thd);

</code>
=== Prepare a HANOI file ===
The input automaton should have only one initial state.
<code java>
HOA: v1
tool: "ROLL"
properties: explicit-labels state-acc trans-labels 
States: 3
Start: 0
acc-name: Buchi
Acceptance: 1 Inf(0)
AP: 1 "b"
--BODY--
State: 0
  [!0] 1
  [!0] 2
State: 1 {0}
  [!0] 1
State: 2 {0}
  [0] 2
--END--
</code>

=== Implement a teacher ===
If you want to use ROLL in verification or other areas, you should design a teacher to resolve the membership and equivalence queries.
<code java>
// Options instance to specify the learning algorithms etc
Options options = new Options();
//assume that the above automaton is in BA format then options.format == Format.BA
Parser parser = UtilParser.prepare(options, options.inputFile, options.format);
// get the NBA
NBA target = parser.parse();
// prepare RABIT as the BA teacher to answer queries
TeacherNBARABIT teacher = new TeacherNBARABIT(options, target);

</code>

=== Call a learner and specify the BA construction ===
<code java>
// use the under-approximation method to construct a BA from an FDFA
options.approximation = Options.Approximation.UNDER;
// set NBA learner, here we use tree-based syntactic FDFA learner
options.algorithm = Options.Algorithm.SYNTACTIC;
options.structure = Options.Structure.TREE;
LearnerBase<NBA> learner = null;
if(options.algorithm == Options.Algorithm.NBA_LDOLLAR) {
       // input teacher as a membership oracle for the learner
       learner = new LearnerNBALDollar(options, target.getAlphabet(), teacher);
}else if(options.algorithm == Options.Algorithm.PERIODIC
       || options.algorithm == Options.Algorithm.SYNTACTIC
       || options.algorithm == Options.Algorithm.RECURRENT) {
       learner = new LearnerNBALOmega(options, target.getAlphabet(), teacher);
} else {
       throw new UnsupportedOperationException("Unsupported BA Learner");
}
        
</code>

=== Learning loop ===
<code java>
        Timer timer = new Timer();
        options.log.println("Initializing learner...");
        timer.start();
        learner.startLearning();
        timer.stop();
        // store the time spent by the learning algorithm
        options.stats.timeOfLearner += timer.getTimeElapsed();
        NBA hypothesis = null;
        while(true) {
            // output table or tree structure in verbose mode 
            options.log.verbose("Table/Tree is both closed and consistent\n" + learner.toString());
            hypothesis = learner.getHypothesis();
        
            options.log.println("Resolving equivalence query for hypothesis (#Q=" + hypothesis.getStateSize() + ")...  ");
            Query<HashableValue> ceQuery = teacher.answerEquivalenceQuery(hypothesis);
            boolean isEq = ceQuery.getQueryAnswer().get();
            if(isEq) {
                // store statistics after learning is completed
                prepareStats(options, learner, hypothesis);
                break;
            }
            ceQuery.answerQuery(null);
            // output the returned counterexample in verbose mode
            options.log.verbose("Counterexample is: " + ceQuery.toString());
            timer.start();
            options.log.println("Refining current hypothesis...");
            learner.refineHypothesis(ceQuery);
            timer.stop();
            options.stats.timeOfLearner += timer.getTimeElapsed();
        }
        options.log.println("Learning completed...");	
</code>

The complete code is the class roll.main.Executor.

===== Acknowledgement =====
We use [[http://www.ej-technologies.com/products/jprofiler/overview.html

 | Java profiler]] in the project.