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 Alphabet<String> inputAlphabet;
  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.Socket;
  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 = 8888;
  64         private static final boolean printNewLineAfterEveryInput = true; // print newlines in the socket connection
  65         private static final String resetCmd = "RES"; // 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 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 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 = true;
  90
  91         private static String stateCountStr;
  92         private static String methodStr;
  93         private static String testStr;
  94         private static long startTime;
  95
  96         public static void main(String [] args) throws IOException {
  97                 startTime = System.currentTimeMillis();
  98
  99                 if (args.length != 3) {
 100                         System.out.println("error: missing commandline arguments!");
 101                         return;
 102                 }
 103
 104                 /* this option reduces the number of inputs used by the learning
 105                  *
 106                  * this should result in a smaller model because these inputs
 107                  * are only valid in certain states.
 108                  */
 109                 stateCountStr = args[0];
 110                 int stateCount = 0;
 111                 if (args[0].equals("partial")) {
 112                         stateCount = 1;
 113                 } else if (args[0].equals("full")) {
 114                         stateCount = 2;
 115                 }
 116
 117                 /* learning method
 118                  *
 119                  * can be LStar, TTT, RS or KV
 120                  */
 121                 methodStr = args[1];
 122                 if (methodStr.equals("LStar")) {
 123                         learningAlgorithm = LearningMethod.LStar;
 124                 } else if (methodStr.equals("TTT")) {
 125                         learningAlgorithm = LearningMethod.TTT;
 126                 } else if (methodStr.equals("RS")) {
 127                         learningAlgorithm = LearningMethod.RivestSchapire;
 128                 } else if (methodStr.equals("KV")) {
 129                         learningAlgorithm = LearningMethod.KearnsVazirani;
 130                 }
 131
 132                 /* testing method
 133                  *
 134                  * can be: rand, wm, wpm
 135                  */
 136                 testStr = args[2];
 137                 if (testStr.equals("rand")) {
 138                         testMethod = TestingMethod.RandomWalk;
 139                 } else if (testStr.equals("wm")) {
 140                         testMethod = TestingMethod.WMethod;
 141                 } else if (testStr.equals("wpm")) {
 142                         testMethod = TestingMethod.WpMethod;
 143                 }
 144
 145                 System.out.println("settings:");
 146                 System.out.println("stateCount = "+stateCount);
 147                 System.out.println("learningMethod = "+methodStr);
 148                 System.out.println("testMethod = "+testStr);
 149
 150                 switch (stateCount) {
 151                         case 2:
 152                                 inputAlphabet = new SimpleAlphabet<String>(ImmutableSet.of(
 153                                         "SYN", "ACK",
 154                                         "DAT", "RST", "FIN"));
 155                         break;
 156                         case 1:
 157                                 inputAlphabet = new SimpleAlphabet<String>(ImmutableSet.of(
 158                                         "SYN", "ACK",
 159                                         "DAT"));
 160                         break;
 161                         default:
 162                                 inputAlphabet = new SimpleAlphabet<String>(ImmutableSet.of(
 163                                         "SYN", "ACK"));
 164                 }
 165
 166                 // Load the actual SUL-class, depending on which SUL-type is set at the top of this file
 167                 // You can also program an own SUL-class if you extend SUL<String,String> (or SUL<S,T> in
 168                 // general, with S and T the input and output types - you'll have to change some of the
 169                 // code below)
 170                 SUL<String,String> sul;
 171                 switch (sulType) {
 172                 case Example:
 173                         sul = new ExampleSUL();
 174                         break;
 175                 case Socket:
 176                         sul = new SocketSUL(socketIp, socketPort, printNewLineAfterEveryInput, resetCmd);
 177                         break;
 178                 default:
 179                         throw new RuntimeException("No SUL-type defined");
 180                 }
 181
 182                 // Wrap the SUL in a detector for non-determinism
 183                 sul = new NonDeterminismCheckingSUL<String,String>(sul);
 184                 // Wrap the SUL in counters for symbols/resets, so that we can record some statistics
 185                 SymbolCounterSUL<String, String> symbolCounterSul = new SymbolCounterSUL<>("symbol counter", sul);
 186                 ResetCounterSUL<String, String> resetCounterSul = new ResetCounterSUL<>("reset counter", symbolCounterSul);
 187                 Counter nrSymbols = symbolCounterSul.getStatisticalData(), nrResets = resetCounterSul.getStatisticalData();
 188                 // we should use the sul only through those wrappers
 189                 sul = resetCounterSul;
 190                 // Most testing/learning-algorithms want a membership-oracle instead of a SUL directly
 191                 MealyMembershipOracle<String,String> sulOracle = new SULOracle<>(sul);
 192
 193                 // Choosing an equivalence oracle
 194                 EquivalenceOracle<MealyMachine<?, String, ?, String>, String, Word<String>> eqOracle = null;
 195                 switch (testMethod){
 196                         // simplest method, but doesn't perform well in practice, especially for large models
 197                         case RandomWalk:
 198                                 eqOracle = new RandomWalkEQOracle<>(chanceOfResetting, numberOfSymbols, true, new Random(123456l), sul);
 199                                 break;
 200                         // Other methods are somewhat smarter than random testing: state coverage, trying to distinguish states, etc.
 201                         case WMethod:
 202                                 eqOracle = new WMethodEQOracle.MealyWMethodEQOracle<>(3, sulOracle);
 203                                 break;
 204                         case WpMethod:
 205                                 eqOracle = new WpMethodEQOracle.MealyWpMethodEQOracle<>(3, sulOracle);
 206                                 break;
 207                         default:
 208                                 throw new RuntimeException("No test oracle selected!");
 209                 }
 210
 211                 // Choosing a learner
 212                 LearningAlgorithm<MealyMachine<?, String, ?, String>, String, Word<String>> learner = null;
 213                 switch (learningAlgorithm){
 214                         case LStar:
 215                                 learner = new ExtensibleLStarMealy<>(inputAlphabet, sulOracle, Lists.<Word<String>>newArrayList(), ObservationTableCEXHandlers.CLASSIC_LSTAR, ClosingStrategies.CLOSE_SHORTEST);
 216                                 break;
 217                         case RivestSchapire:
 218                                 learner = new ExtensibleLStarMealy<>(inputAlphabet, sulOracle, Lists.<Word<String>>newArrayList(), ObservationTableCEXHandlers.RIVEST_SCHAPIRE, ClosingStrategies.CLOSE_SHORTEST);
 219                                 break;
 220                         case TTT:
 221                                 learner = new TTTLearnerMealy<>(inputAlphabet, sulOracle, AcexAnalyzers.LINEAR_FWD);
 222                                 break;
 223                         case KearnsVazirani:
 224                                 learner = new KearnsVaziraniMealy<>(inputAlphabet, sulOracle, false, AcexAnalyzers.LINEAR_FWD);
 225                                 break;
 226                         default:
 227                                 throw new RuntimeException("No learner selected");
 228                 }
 229
 230                 // Running the actual experiments!
 231                 if (runControlledExperiment) {
 232                         runControlledExperiment(learner, eqOracle, nrSymbols, nrResets, inputAlphabet);
 233                 } else {
 234                         runSimpleExperiment(learner, eqOracle, inputAlphabet);
 235                 }
 236         }
 237
 238         /**
 239          * Simple example of running a learning experiment
 240          * @param learner Learning algorithm, wrapping the SUL
 241          * @param eqOracle Testing algorithm, wrapping the SUL
 242          * @param alphabet Input alphabet
 243          * @throws IOException if the result cannot be written
 244          */
 245         public static void runSimpleExperiment(
 246                         LearningAlgorithm<MealyMachine<?, String, ?, String>, String, Word<String>> learner,
 247                         EquivalenceOracle<MealyMachine<?, String, ?, String>, String, Word<String>> eqOracle,
 248                         Alphabet<String> alphabet) throws IOException {
 249                 MealyExperiment<String, String> experiment = new MealyExperiment<String, String>(learner, eqOracle, alphabet);
 250                 experiment.run();
 251                 System.out.println("Ran " + experiment.getRounds().getCount() + " rounds");
 252                 produceOutput(OUTPUT_FILENAME, experiment.getFinalHypothesis(), alphabet, true);
 253         }
 254
 255         /**
 256          * More detailed example of running a learning experiment. Starts learning, and then loops testing,
 257          * and if counterexamples are found, refining again. Also prints some statistics about the experiment
 258          * @param learner learner Learning algorithm, wrapping the SUL
 259          * @param eqOracle Testing algorithm, wrapping the SUL
 260          * @param nrSymbols A counter for the number of symbols that have been sent to the SUL (for statistics)
 261          * @param nrResets A counter for the number of resets that have been sent to the SUL (for statistics)
 262          * @param alphabet Input alphabet
 263          * @throws IOException
 264          */
 265         public static void runControlledExperiment(
 266                         LearningAlgorithm<MealyMachine<?, String, ?, String>, String, Word<String>> learner,
 267                         EquivalenceOracle<MealyMachine<?, String, ?, String>, String, Word<String>> eqOracle,
 268                         Counter nrSymbols, Counter nrResets,
 269                         Alphabet<String> alphabet) throws IOException {
 270
 271                 // prepare some counters for printing statistics
 272                 int stage = 0;
 273                 long lastNrResetsValue = 0, lastNrSymbolsValue = 0;
 274
 275                 // start the actual learning
 276                 learner.startLearning();
 277
 278                 while(true) {
 279                         // store hypothesis as file
 280                         if(saveAllHypotheses) {
 281                                 String outputFilename = "hyp." + stage + ".obf.dot";
 282                                 PrintWriter output = new PrintWriter(outputFilename);
 283                                 produceOutput(outputFilename, learner.getHypothesisModel(), alphabet, false);
 284                                 output.close();
 285                         }
 286
 287                         // Print statistics
 288                         System.out.println(stage + ": " + Calendar.getInstance().getTime());
 289                         // Log number of queries/symbols
 290                         System.out.println("Hypothesis size: " + learner.getHypothesisModel().size() + " states");
 291                         long roundResets = nrResets.getCount() - lastNrResetsValue, roundSymbols = nrSymbols.getCount() - lastNrSymbolsValue;
 292                         System.out.println("learning queries/symbols: " + nrResets.getCount() + "/" + nrSymbols.getCount()
 293                                         + "(" + roundResets + "/" + roundSymbols + " this learning round)");
 294                         lastNrResetsValue = nrResets.getCount();
 295                         lastNrSymbolsValue = nrSymbols.getCount();
 296
 297                         // Search for CE
 298                         DefaultQuery<String, Word<String>> ce = eqOracle.findCounterExample(learner.getHypothesisModel(), alphabet);
 299
 300                         // Log number of queries/symbols
 301                         roundResets = nrResets.getCount() - lastNrResetsValue;
 302                         roundSymbols = nrSymbols.getCount() - lastNrSymbolsValue;
 303                         System.out.println("testing queries/symbols: " + nrResets.getCount() + "/" + nrSymbols.getCount()
 304                                         + "(" + roundResets + "/" + roundSymbols + " this testing round)");
 305                         lastNrResetsValue = nrResets.getCount();
 306                         lastNrSymbolsValue = nrSymbols.getCount();
 307
 308                         if(ce == null) {
 309                                 // No counterexample found, stop learning
 310                                 System.out.println("\nFinished learning!");
 311                                 produceOutput(OUTPUT_FILENAME, learner.getHypothesisModel(), alphabet, true);
 312                                 break;
 313                         } else {
 314                                 // Counterexample found, rinse and repeat
 315                                 System.out.println();
 316                                 stage++;
 317                                 learner.refineHypothesis(ce);
 318                         }
 319                 }
 320         }
 321
 322         /**
 323          * Produces a dot-file and a PDF (if graphviz is installed)
 324          * @param fileName filename without extension - will be used for the .dot and .pdf
 325          * @param model
 326          * @param alphabet
 327          * @param verboseError whether to print an error explaing that you need graphviz
 328          * @throws FileNotFoundException
 329          * @throws IOException
 330          */
 331         public static void produceOutput(String fileName, MealyMachine<?,String,?,String> model, Alphabet<String> alphabet, boolean verboseError) throws FileNotFoundException, IOException {
 332                 long time = (System.currentTimeMillis()-startTime)/1000L;
 333                 GraphDOT.write(model, alphabet, new PrintWriter(fileName + "." + stateCountStr + "." + methodStr + "." + testStr + "." + time + "sec" + ".dot"));
 334                 try {
 335                         DOT.runDOT(new File(fileName + "." + stateCountStr + "." + methodStr + "." + testStr + "." + time + "sec" + ".dot"), "pdf", new File(fileName + "." + stateCountStr + "." + methodStr + "." + testStr + "." + time + "sec" + ".pdf"));
 336                 } catch (Exception e) {
 337                         if (verboseError) {
 338                                 System.err.println("Warning: Install graphviz to convert dot-files to PDF");
 339                                 System.err.println(e.getMessage());
 340                         }
 341                 }
 342         }
 343 }