[[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ω+ abω. Please make sure you have all dependent libraries when you use ROLL.
=== Prepare a BA file ===
Every transition label should be exactly a string.
[0]
a,[0]->[1]
a,[1]->[1]
a,[0]->[2]
b,[2]->[2]
[1]
[2]
In ROLL, one can create the above Büchi automaton as follows:
// 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);
=== Prepare a HANOI file ===
The input automaton should have only one initial state.
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--
=== 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.
// 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);
=== Call a learner and specify the BA construction ===
// 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 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");
}
=== Learning loop ===
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 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...");
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.