how_to_use
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revisionLast revisionBoth sides next revision | ||
how_to_use [2018/01/24 13:08] – admin | how_to_use [2018/01/29 11:22] – liyong | ||
---|---|---|---|
Line 8: | Line 8: | ||
- | Below we demonstrate how to use our learner to learn the ω-regular language L=a< | + | Below we demonstrate how to use our learner to learn the ω-regular language L=a< |
| | ||
=== Prepare a BA file === | === Prepare a BA file === | ||
Line 16: | Line 16: | ||
a, | a, | ||
a, | a, | ||
- | b, | + | a, |
b, | b, | ||
[1] | [1] | ||
[2] | [2] | ||
</ | </ | ||
+ | In ROLL, one can create the above Büchi automaton as follows: | ||
+ | <code java> | ||
+ | // first create an alphabet | ||
+ | Alphabet alphabet = new Alphabet(); | ||
+ | alphabet.addLetter(' | ||
+ | alphabet.addLetter(' | ||
+ | // 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(' | ||
+ | target.getState(fst).addTransition(alphabet.indexOf(' | ||
+ | target.getState(snd).addTransition(alphabet.indexOf(' | ||
+ | target.getState(thd).addTransition(alphabet.indexOf(' | ||
+ | target.setInitial(fst); | ||
+ | target.setFinal(snd); | ||
+ | target.setFinal(thd); | ||
+ | </ | ||
=== Prepare a HANOI file === | === Prepare a HANOI file === | ||
The input automaton should have only one initial state. | The input automaton should have only one initial state. | ||
Line 60: | Line 82: | ||
=== Call a learner and specify the BA construction === | === Call a learner and specify the BA construction === | ||
<code java> | <code java> | ||
- | // specify | + | // 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 | ||
+ | options.algorithm = Options.Algorithm.SYNTACTIC; | ||
+ | options.structure = Options.Structure.TREE; | ||
LearnerBase< | LearnerBase< | ||
if(options.algorithm == Options.Algorithm.NBA_LDOLLAR) { | if(options.algorithm == Options.Algorithm.NBA_LDOLLAR) { | ||
+ | // input teacher as a membership oracle for the learner | ||
| | ||
}else if(options.algorithm == Options.Algorithm.PERIODIC | }else if(options.algorithm == Options.Algorithm.PERIODIC | ||
Line 81: | Line 108: | ||
learner.startLearning(); | learner.startLearning(); | ||
timer.stop(); | timer.stop(); | ||
+ | // store the time spent by the learning algorithm | ||
options.stats.timeOfLearner += timer.getTimeElapsed(); | options.stats.timeOfLearner += timer.getTimeElapsed(); | ||
NBA hypothesis = null; | NBA hypothesis = null; | ||
while(true) { | while(true) { | ||
+ | // output table or tree structure in verbose mode | ||
options.log.verbose(" | options.log.verbose(" | ||
hypothesis = learner.getHypothesis(); | hypothesis = learner.getHypothesis(); | ||
- | // along with ce | + | |
options.log.println(" | options.log.println(" | ||
Query< | Query< | ||
boolean isEq = ceQuery.getQueryAnswer().get(); | boolean isEq = ceQuery.getQueryAnswer().get(); | ||
if(isEq) { | if(isEq) { | ||
- | // store statistics | + | // store statistics |
prepareStats(options, | prepareStats(options, | ||
break; | break; | ||
} | } | ||
ceQuery.answerQuery(null); | ceQuery.answerQuery(null); | ||
+ | // output the returned counterexample in verbose mode | ||
options.log.verbose(" | options.log.verbose(" | ||
timer.start(); | timer.start(); | ||
Line 105: | Line 135: | ||
options.log.println(" | options.log.println(" | ||
</ | </ | ||
+ | |||
+ | The complete code is the class roll.main.Executor. | ||
===== Acknowledgement ===== | ===== Acknowledgement ===== |
how_to_use.txt · Last modified: 2018/03/29 16:54 by liyong