User Tools

Site Tools


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ω+ bω. 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]
b,[0]->[2]
b,[2]->[2]
[1]
[2]

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.1516770997.txt.gz · Last modified: 2018/01/24 13:16 by admin