Main How to Use ROLL in Command Line How to Use ROLL in JAVA Program Tool Contact
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.
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);
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--
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);
// 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"); }
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.
We use Java profiler in the project.