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<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");
}

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.