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