a4/code/src/learner/Main.java

   1 package learner;
   2
   3 import java.io.File;
   4 import java.io.FileNotFoundException;
   5 import java.io.IOException;
   6 import java.io.PrintWriter;
   7 import java.net.InetAddress;
   8 import java.util.Arrays;
   9 import java.util.Calendar;
  10 import java.util.Random;
  11
  12 import net.automatalib.automata.transout.MealyMachine;
  13 import net.automatalib.commons.dotutil.DOT;
  14 import net.automatalib.graphs.concepts.GraphViewable;
  15 import net.automatalib.util.graphs.dot.GraphDOT;
  16 import net.automatalib.words.Alphabet;
  17 import net.automatalib.words.Word;
  18 import net.automatalib.words.impl.SimpleAlphabet;
  19
  20 import com.google.common.collect.ImmutableSet;
  21 import com.google.common.collect.Lists;
  22
  23 import de.learnlib.acex.analyzers.AcexAnalyzers;
  24 import de.learnlib.algorithms.kv.mealy.KearnsVaziraniMealy;
  25 import de.learnlib.algorithms.lstargeneric.ce.ObservationTableCEXHandlers;
  26 import de.learnlib.algorithms.lstargeneric.closing.ClosingStrategies;
  27 import de.learnlib.algorithms.lstargeneric.mealy.ExtensibleLStarMealy;
  28 import de.learnlib.algorithms.ttt.mealy.TTTLearnerMealy;
  29 import de.learnlib.api.EquivalenceOracle;
  30 import de.learnlib.api.LearningAlgorithm;
  31 import de.learnlib.api.MembershipOracle.MealyMembershipOracle;
  32 import de.learnlib.api.SUL;
  33 import de.learnlib.eqtests.basic.WMethodEQOracle;
  34 import de.learnlib.eqtests.basic.WpMethodEQOracle;
  35 import de.learnlib.eqtests.basic.mealy.RandomWalkEQOracle;
  36 import de.learnlib.experiments.Experiment.MealyExperiment;
  37 import de.learnlib.oracles.DefaultQuery;
  38 import de.learnlib.oracles.ResetCounterSUL;
  39 import de.learnlib.oracles.SULOracle;
  40 import de.learnlib.oracles.SymbolCounterSUL;
  41 import de.learnlib.statistics.Counter;
  42
  43 /**
  44  * General learning testing framework. The most important parameters are the input alphabet and the SUL (The
  45  * first two static attributes). Other settings can also be configured.
  46  *
  47  * Based on the learner experiment setup of Joshua Moerman, https://gitlab.science.ru.nl/moerman/Learnlib-Experiments
  48  *
  49  * @author Ramon Janssen
  50  */
  51 public class Main {
  52         //*****************//
  53         // SUL information //
  54         //*****************//
  55         // Defines the input alphabet, adapt for your socket (you can even use other types than string, if you
  56         // change the generic-values, e.g. make your SUL of type SUL<Integer, Float> for int-input and float-output
  57         private static final Alphabet<String> inputAlphabet = new SimpleAlphabet<String>(ImmutableSet.of("a", "b", "c"));
  58         // There are two SULs predefined, an example (see ExampleSul.java) and a socket SUL which connects to the SUL over socket
  59         private static final SULType sulType = SULType.Example;
  60         public enum SULType { Example, Socket }
  61         // For SULs over socket, the socket address/port can be set here
  62         private static final InetAddress socketIp = InetAddress.getLoopbackAddress();
  63         private static final int socketPort = 7890;
  64         private static final boolean printNewLineAfterEveryInput = true; // print newlines in the socket connection
  65         private static final String resetCmd = "RESET"; // the command to send over socket to reset sut
  66
  67         //*******************//
  68         // Learning settings //
  69         //*******************//
  70         // file for writing the resulting .dot-file and .pdf-file (extensions are added automatically)
  71         private static final String OUTPUT_FILENAME = "learnedModel";
  72         // the learning and testing algorithms. LStar is the basic algorithm, TTT performs much faster
  73         // but is a bit more inaccurate and produces more intermediate hypotheses, so test well)
  74         private static final LearningMethod learningAlgorithm = LearningMethod.LStar;
  75         public enum LearningMethod { LStar, RivestSchapire, TTT, KearnsVazirani }
  76         // Random walk is the simplest, but performs badly on large models: the chance of hitting a
  77         // erroneous long trace is very small
  78         private static final TestingMethod testMethod = TestingMethod.RandomWalk;
  79         public enum TestingMethod { RandomWalk, WMethod, WpMethod }
  80         // for random walk, the chance to do a reset after an input and the number of
  81         // inputs to test before accepting a hypothesis
  82         private static final double chanceOfResetting = 0.1;
  83         private static final int numberOfSymbols = 100;
  84         // Simple experiments produce very little feedback, controlled produces feedback after
  85         // every hypotheses and are better suited to adjust by programming
  86         private static final boolean runControlledExperiment = true;
  87         // For controlled experiments only: store every hypotheses as a file. Useful for 'debugging'
  88         // if the learner does not terminate (hint: the TTT-algorithm produces many hypotheses).
  89         private static final boolean saveAllHypotheses = false;
  90
  91         public static void main(String [] args) throws IOException {
  92                 // Load the actual SUL-class, depending on which SUL-type is set at the top of this file
  93                 // You can also program an own SUL-class if you extend SUL<String,String> (or SUL<S,T> in
  94                 // general, with S and T the input and output types - you'll have to change some of the
  95                 // code below)
  96                 SUL<String,String> sul;
  97                 switch (sulType) {
  98                 case Example:
  99                         sul = new ExampleSUL();
 100                         break;
 101                 case Socket:
 102                         sul = new SocketSUL(socketIp, socketPort, printNewLineAfterEveryInput, resetCmd);
 103                         break;
 104                 default:
 105                         throw new RuntimeException("No SUL-type defined");
 106                 }
 107
 108                 // Wrap the SUL in a detector for non-determinism
 109                 sul = new NonDeterminismCheckingSUL<String,String>(sul);
 110                 // Wrap the SUL in counters for symbols/resets, so that we can record some statistics
 111                 SymbolCounterSUL<String, String> symbolCounterSul = new SymbolCounterSUL<>("symbol counter", sul);
 112                 ResetCounterSUL<String, String> resetCounterSul = new ResetCounterSUL<>("reset counter", symbolCounterSul);
 113                 Counter nrSymbols = symbolCounterSul.getStatisticalData(), nrResets = resetCounterSul.getStatisticalData();
 114                 // we should use the sul only through those wrappers
 115                 sul = resetCounterSul;
 116                 // Most testing/learning-algorithms want a membership-oracle instead of a SUL directly
 117                 MealyMembershipOracle<String,String> sulOracle = new SULOracle<>(sul);
 118
 119                 // Choosing an equivalence oracle
 120                 EquivalenceOracle<MealyMachine<?, String, ?, String>, String, Word<String>> eqOracle = null;
 121                 switch (testMethod){
 122                         // simplest method, but doesn't perform well in practice, especially for large models
 123                         case RandomWalk:
 124                                 eqOracle = new RandomWalkEQOracle<>(chanceOfResetting, numberOfSymbols, true, new Random(123456l), sul);
 125                                 break;
 126                         // Other methods are somewhat smarter than random testing: state coverage, trying to distinguish states, etc.
 127                         case WMethod:
 128                                 eqOracle = new WMethodEQOracle.MealyWMethodEQOracle<>(3, sulOracle);
 129                                 break;
 130                         case WpMethod:
 131                                 eqOracle = new WpMethodEQOracle.MealyWpMethodEQOracle<>(3, sulOracle);
 132                                 break;
 133                         default:
 134                                 throw new RuntimeException("No test oracle selected!");
 135                 }
 136
 137                 // Choosing a learner
 138                 LearningAlgorithm<MealyMachine<?, String, ?, String>, String, Word<String>> learner = null;
 139                 switch (learningAlgorithm){
 140                         case LStar:
 141                                 learner = new ExtensibleLStarMealy<>(inputAlphabet, sulOracle, Lists.<Word<String>>newArrayList(), ObservationTableCEXHandlers.CLASSIC_LSTAR, ClosingStrategies.CLOSE_SHORTEST);
 142                                 break;
 143                         case RivestSchapire:
 144                                 learner = new ExtensibleLStarMealy<>(inputAlphabet, sulOracle, Lists.<Word<String>>newArrayList(), ObservationTableCEXHandlers.RIVEST_SCHAPIRE, ClosingStrategies.CLOSE_SHORTEST);
 145                                 break;
 146                         case TTT:
 147                                 learner = new TTTLearnerMealy<>(inputAlphabet, sulOracle, AcexAnalyzers.LINEAR_FWD);
 148                                 break;
 149                         case KearnsVazirani:
 150                                 learner = new KearnsVaziraniMealy<>(inputAlphabet, sulOracle, false, AcexAnalyzers.LINEAR_FWD);
 151                                 break;
 152                         default:
 153                                 throw new RuntimeException("No learner selected");
 154                 }
 155
 156                 // Running the actual experiments!
 157                 if (runControlledExperiment) {
 158                         runControlledExperiment(learner, eqOracle, nrSymbols, nrResets, inputAlphabet);
 159                 } else {
 160                         runSimpleExperiment(learner, eqOracle, inputAlphabet);
 161                 }
 162         }
 163
 164         /**
 165          * Simple example of running a learning experiment
 166          * @param learner Learning algorithm, wrapping the SUL
 167          * @param eqOracle Testing algorithm, wrapping the SUL
 168          * @param alphabet Input alphabet
 169          * @throws IOException if the result cannot be written
 170          */
 171         public static void runSimpleExperiment(
 172                         LearningAlgorithm<MealyMachine<?, String, ?, String>, String, Word<String>> learner,
 173                         EquivalenceOracle<MealyMachine<?, String, ?, String>, String, Word<String>> eqOracle,
 174                         Alphabet<String> alphabet) throws IOException {
 175                 MealyExperiment<String, String> experiment = new MealyExperiment<String, String>(learner, eqOracle, alphabet);
 176                 experiment.run();
 177                 System.out.println("Ran " + experiment.getRounds().getCount() + " rounds");
 178                 produceOutput(OUTPUT_FILENAME, experiment.getFinalHypothesis(), alphabet, true);
 179         }
 180
 181         /**
 182          * More detailed example of running a learning experiment. Starts learning, and then loops testing,
 183          * and if counterexamples are found, refining again. Also prints some statistics about the experiment
 184          * @param learner learner Learning algorithm, wrapping the SUL
 185          * @param eqOracle Testing algorithm, wrapping the SUL
 186          * @param nrSymbols A counter for the number of symbols that have been sent to the SUL (for statistics)
 187          * @param nrResets A counter for the number of resets that have been sent to the SUL (for statistics)
 188          * @param alphabet Input alphabet
 189          * @throws IOException
 190          */
 191         public static void runControlledExperiment(
 192                         LearningAlgorithm<MealyMachine<?, String, ?, String>, String, Word<String>> learner,
 193                         EquivalenceOracle<MealyMachine<?, String, ?, String>, String, Word<String>> eqOracle,
 194                         Counter nrSymbols, Counter nrResets,
 195                         Alphabet<String> alphabet) throws IOException {
 196
 197                 // prepare some counters for printing statistics
 198                 int stage = 0;
 199                 long lastNrResetsValue = 0, lastNrSymbolsValue = 0;
 200
 201                 // start the actual learning
 202                 learner.startLearning();
 203
 204                 while(true) {
 205                         // store hypothesis as file
 206                         if(saveAllHypotheses) {
 207                                 String outputFilename = "hyp." + stage + ".obf.dot";
 208                                 PrintWriter output = new PrintWriter(outputFilename);
 209                                 produceOutput(outputFilename, learner.getHypothesisModel(), alphabet, false);
 210                                 output.close();
 211                         }
 212
 213                         // Print statistics
 214                         System.out.println(stage + ": " + Calendar.getInstance().getTime());
 215                         // Log number of queries/symbols
 216                         System.out.println("Hypothesis size: " + learner.getHypothesisModel().size() + " states");
 217                         long roundResets = nrResets.getCount() - lastNrResetsValue, roundSymbols = nrSymbols.getCount() - lastNrSymbolsValue;
 218                         System.out.println("learning queries/symbols: " + nrResets.getCount() + "/" + nrSymbols.getCount()
 219                                         + "(" + roundResets + "/" + roundSymbols + " this learning round)");
 220                         lastNrResetsValue = nrResets.getCount();
 221                         lastNrSymbolsValue = nrSymbols.getCount();
 222
 223                         // Search for CE
 224                         DefaultQuery<String, Word<String>> ce = eqOracle.findCounterExample(learner.getHypothesisModel(), alphabet);
 225
 226                         // Log number of queries/symbols
 227                         roundResets = nrResets.getCount() - lastNrResetsValue;
 228                         roundSymbols = nrSymbols.getCount() - lastNrSymbolsValue;
 229                         System.out.println("testing queries/symbols: " + nrResets.getCount() + "/" + nrSymbols.getCount()
 230                                         + "(" + roundResets + "/" + roundSymbols + " this testing round)");
 231                         lastNrResetsValue = nrResets.getCount();
 232                         lastNrSymbolsValue = nrSymbols.getCount();
 233
 234                         if(ce == null) {
 235                                 // No counterexample found, stop learning
 236                                 System.out.println("\nFinished learning!");
 237                                 produceOutput(OUTPUT_FILENAME, learner.getHypothesisModel(), alphabet, true);
 238                                 break;
 239                         } else {
 240                                 // Counterexample found, rinse and repeat
 241                                 System.out.println();
 242                                 stage++;
 243                                 learner.refineHypothesis(ce);
 244                         }
 245                 }
 246         }
 247
 248         /**
 249          * Produces a dot-file and a PDF (if graphviz is installed)
 250          * @param fileName filename without extension - will be used for the .dot and .pdf
 251          * @param model
 252          * @param alphabet
 253          * @param verboseError whether to print an error explaing that you need graphviz
 254          * @throws FileNotFoundException
 255          * @throws IOException
 256          */
 257         public static void produceOutput(String fileName, MealyMachine<?,String,?,String> model, Alphabet<String> alphabet, boolean verboseError) throws FileNotFoundException, IOException {
 258                 GraphDOT.write(model, alphabet, new PrintWriter(OUTPUT_FILENAME + ".dot"));
 259                 try {
 260                         DOT.runDOT(new File(OUTPUT_FILENAME + ".dot"), "pdf", new File(OUTPUT_FILENAME + ".pdf"));
 261                 } catch (Exception e) {
 262                         if (verboseError) {
 263                                 System.err.println("Warning: Install graphviz to convert dot-files to PDF");
 264                                 System.err.println(e.getMessage());
 265                         }
 266                 }
 267         }
 268 }