how_to_use
This is an old revision of the document!
Main How to Use ROLL in Command Line How to Use ROLL in JAVA Program Tool 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; // specify FDFA learner, here we use tree-based periodic FDFA learner LearnerBase<NBA> learner = null; if(options.algorithm == Options.Algorithm.NBA_LDOLLAR) { learner = new LearnerNBALDollar(options, nba.getAlphabet(), teacher); }else if(options.algorithm == Options.Algorithm.PERIODIC || options.algorithm == Options.Algorithm.SYNTACTIC || options.algorithm == Options.Algorithm.RECURRENT) { learner = new LearnerNBALOmega(options, nba.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<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...");
The complete code is the class roll.main.Executor.
Acknowledgement
We use Java profiler in the project.
how_to_use.1516848196.txt.gz · Last modified: 2018/01/25 10:43 by liyong