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