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ω+ 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, 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.

Set up ROLL in Eclipse

This tutorial has been tested on the following distributions:

  • Ubuntu 16.04 LTS, 64-bits

Prerequisites

  • Java Development Kit (only tested with JDK 8.0)
  • Javacc plugin in Eclipse
  • Maven Integration for Eclipse
  • SPOT (only if you want to run some JUnit tests via autfilt in SPOT)

Set up ROLL in Eclipse

1. Use following command to clone the repository to your local file system.

  `git clone https://github.com/ISCAS-PMC/roll-library

2. Import roll-library as Maven Existing Projects.

Now you should be able to run ROLL as a java application by choosing run.main.ROLL as the main class.

Acknowledgement

We use Java profiler in the project.

how_to_use.1516958583.txt.gz · Last modified: 2018/01/26 17:23 by liyong