001/* Copyright (C) 2013 TU Dortmund
002 * This file is part of LearnLib, http://www.learnlib.de/.
003 * 
004 * LearnLib is free software; you can redistribute it and/or
005 * modify it under the terms of the GNU Lesser General Public
006 * License version 3.0 as published by the Free Software Foundation.
007 * 
008 * LearnLib is distributed in the hope that it will be useful,
009 * but WITHOUT ANY WARRANTY; without even the implied warranty of
010 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
011 * Lesser General Public License for more details.
012 * 
013 * You should have received a copy of the GNU Lesser General Public
014 * License along with LearnLib; if not, see
015 * <http://www.gnu.de/documents/lgpl.en.html>.
016 */
017package de.learnlib.examples.example2;
018
019import java.io.IOException;
020import java.io.Writer;
021import java.lang.reflect.Method;
022import java.util.ArrayDeque;
023import java.util.ArrayList;
024import java.util.Deque;
025import java.util.List;
026import java.util.Random;
027
028import net.automatalib.automata.transout.MealyMachine;
029import net.automatalib.commons.dotutil.DOT;
030import net.automatalib.util.graphs.dot.GraphDOT;
031import net.automatalib.words.Word;
032import de.learnlib.algorithms.lstargeneric.ce.ObservationTableCEXHandlers;
033import de.learnlib.algorithms.lstargeneric.closing.ClosingStrategies;
034import de.learnlib.algorithms.lstargeneric.mealy.ExtensibleLStarMealy;
035import de.learnlib.api.EquivalenceOracle.MealyEquivalenceOracle;
036import de.learnlib.api.LearningAlgorithm.MealyLearner;
037import de.learnlib.api.SUL;
038import de.learnlib.cache.Caches;
039import de.learnlib.drivers.reflect.AbstractMethodInput;
040import de.learnlib.drivers.reflect.AbstractMethodOutput;
041import de.learnlib.drivers.reflect.SimplePOJOTestDriver;
042import de.learnlib.eqtests.basic.mealy.RandomWalkEQOracle;
043import de.learnlib.experiments.Experiment.MealyExperiment;
044import de.learnlib.oracles.ResetCounterSUL;
045import de.learnlib.oracles.SULOracle;
046import de.learnlib.statistics.SimpleProfiler;
047import de.learnlib.statistics.StatisticSUL;
048
049/**
050 * This example shows how a model of a Java class can be learned using the SUL
051 * (system under learning) interfaces and the random walks equivalence test.
052 *
053 * @author falkhowar
054 */
055public class Example {
056
057    /*
058     * The BoundedStringQueue is the class of which we are going to 
059     * infer a model. It wraps an ordinary queue of Strings, limiting
060     * its size to MAX_SIZE (3). Once the queue is full, additional 
061     * offers will be ignored.
062     * <p>
063     * However, the implementation uses the underlying queue in a strange
064     * way as the model will reveal.
065     */
066    public static class BoundedStringQueue {
067
068        // capacity
069        public static final int MAX_SIZE = 3;
070        // storage
071        private Deque<String> data = new ArrayDeque<>(3);
072
073        // add a String to the queue if capacity allows
074        public void offer(String s) {
075            if (data.size() < MAX_SIZE) {
076                data.offerFirst(s);
077            }
078        }
079
080        // get next element from queue (null for empty queue)
081        public String poll() {
082            return data.poll();
083        }
084    }
085    
086    
087    public static void main(String[] args) throws NoSuchMethodException, IOException {
088
089        // instantiate test driver
090        SimplePOJOTestDriver driver = new SimplePOJOTestDriver(
091                BoundedStringQueue.class.getConstructor());
092                
093        // create learning alphabet
094        Method mOffer = BoundedStringQueue.class.getMethod(
095                "offer", new Class<?>[]{String.class});
096        Method mPoll = BoundedStringQueue.class.getMethod(
097                "poll", new Class<?>[]{});
098                
099        // offer
100        AbstractMethodInput offer_a = driver.addInput("offer_a", mOffer, "a");
101        AbstractMethodInput offer_b = driver.addInput("offer_b", mOffer, "b");
102
103        // poll
104        AbstractMethodInput poll = driver.addInput("poll", mPoll);
105
106        // oracle for counting queries wraps sul
107        StatisticSUL<AbstractMethodInput, AbstractMethodOutput> statisticSul = 
108                new ResetCounterSUL<>("membership queries", driver);
109        
110        SUL<AbstractMethodInput, AbstractMethodOutput> effectiveSul = statisticSul;
111        // use caching in order to avoid duplicate queries
112        effectiveSul = Caches.createSULCache(driver.getInputs(), effectiveSul);
113        
114        SULOracle<AbstractMethodInput, AbstractMethodOutput> mqOracle = new SULOracle<>(effectiveSul);
115
116        // create initial set of suffixes
117        List<Word<AbstractMethodInput>> suffixes = new ArrayList<>();
118        suffixes.add(Word.fromSymbols(offer_a));
119        suffixes.add(Word.fromSymbols(offer_b));
120        suffixes.add(Word.fromSymbols(poll));
121
122        // construct L* instance (almost classic Mealy version)
123        // almost: we use words (Word<String>) in cells of the table 
124        // instead of single outputs.
125        MealyLearner<AbstractMethodInput, AbstractMethodOutput> lstar =
126                new ExtensibleLStarMealy<>(
127                driver.getInputs(), // input alphabet
128                mqOracle, // mq oracle
129                suffixes, // initial suffixes
130                ObservationTableCEXHandlers.CLASSIC_LSTAR, // handling of counterexamples
131                ClosingStrategies.CLOSE_FIRST // always choose first unclosedness found 
132                );
133
134        // create random walks equivalence test
135        MealyEquivalenceOracle<AbstractMethodInput, AbstractMethodOutput> randomWalks =
136                new RandomWalkEQOracle<>(
137                0.05, // reset SUL w/ this probability before a step 
138                10000, // max steps (overall)
139                false, // reset step count after counterexample 
140                new Random(46346293), // make results reproducible 
141                driver // system under learning
142                );
143
144        // construct a learning experiment from
145        // the learning algorithm and the random walks test.
146        // The experiment will execute the main loop of
147        // active learning
148        MealyExperiment<AbstractMethodInput, AbstractMethodOutput> experiment =
149                new MealyExperiment<>(lstar, randomWalks, driver.getInputs());
150
151        // turn on time profiling
152        experiment.setProfile(true);
153
154        // enable logging of models
155        experiment.setLogModels(true);
156
157        // run experiment
158        experiment.run();
159
160        // get learned model
161        MealyMachine<?, AbstractMethodInput, ?, AbstractMethodOutput> result = 
162                experiment.getFinalHypothesis();
163
164        // report results
165        System.out.println("-------------------------------------------------------");
166
167        // profiling
168        System.out.println(SimpleProfiler.getResults());
169
170        // learning statistics
171        System.out.println(experiment.getRounds().getSummary());
172        System.out.println(statisticSul.getStatisticalData().getSummary());
173
174        // model statistics
175        System.out.println("States: " + result.size());
176        System.out.println("Sigma: " + driver.getInputs().size());
177
178        // show model
179        System.out.println();
180        System.out.println("Model: ");
181        
182        GraphDOT.write(result, driver.getInputs(), System.out); // may throw IOException!
183        Writer w = DOT.createDotWriter(true);
184        GraphDOT.write(result, driver.getInputs(), w);
185        w.close();
186
187        System.out.println("-------------------------------------------------------");
188
189    }
190}