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