diff options
Diffstat (limited to 'assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner')
8 files changed, 800 insertions, 0 deletions
diff --git a/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/BasicLearner.java b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/BasicLearner.java new file mode 100644 index 0000000..4a3b6bc --- /dev/null +++ b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/BasicLearner.java @@ -0,0 +1,307 @@ +package basiclearner; + +import java.io.File; +import java.io.FileNotFoundException; +import java.io.IOException; +import java.io.PrintWriter; +import java.util.Calendar; +import java.util.Collection; +import java.util.Random; + +import net.automatalib.automata.transout.MealyMachine; +import net.automatalib.commons.dotutil.DOT; +import net.automatalib.util.graphs.dot.GraphDOT; +import net.automatalib.words.Alphabet; +import net.automatalib.words.Word; +import net.automatalib.words.impl.SimpleAlphabet; + +import com.google.common.collect.Lists; + +import de.learnlib.acex.analyzers.AcexAnalyzers; +import de.learnlib.algorithms.kv.mealy.KearnsVaziraniMealy; +import de.learnlib.algorithms.lstargeneric.ce.ObservationTableCEXHandlers; +import de.learnlib.algorithms.lstargeneric.closing.ClosingStrategies; +import de.learnlib.algorithms.lstargeneric.mealy.ExtensibleLStarMealy; +import de.learnlib.algorithms.ttt.mealy.TTTLearnerMealy; +import de.learnlib.api.EquivalenceOracle; +import de.learnlib.api.LearningAlgorithm; +import de.learnlib.api.MembershipOracle.MealyMembershipOracle; +import de.learnlib.api.SUL; +import de.learnlib.eqtests.basic.WMethodEQOracle; +import de.learnlib.eqtests.basic.WpMethodEQOracle; +import de.learnlib.eqtests.basic.mealy.RandomWalkEQOracle; +import de.learnlib.experiments.Experiment.MealyExperiment; +import de.learnlib.oracles.DefaultQuery; +import de.learnlib.oracles.ResetCounterSUL; +import de.learnlib.oracles.SULOracle; +import de.learnlib.oracles.SymbolCounterSUL; +import de.learnlib.statistics.Counter; + +/** + * General learning testing framework. All basic settings are at the top of this file and can be configured + * by hard-coding or by simply changing them from your own code. + * + * Based on the learner experiment setup of Joshua Moerman, https://gitlab.science.ru.nl/moerman/Learnlib-Experiments + * + * @author Ramon Janssen + */ +public class BasicLearner { + //***********************************************************************************// + // Learning settings (hardcoded, simply set to a different value to change learning) // + //***********************************************************************************// + /** + * name to give to the resulting .dot-file and .pdf-file (extensions are added automatically) + */ + public static String + FINAL_MODEL_FILENAME = "learnedModel", + INTERMEDIATE_HYPOTHESIS_FILENAME = "hypothesis"; + /** + * For controlled experiments only: store every hypotheses as a file. Useful for 'debugging' + * if the learner does not terminate (hint: the TTT-algorithm produces many hypotheses). + */ + public static boolean saveAllHypotheses = true; + /** + * For random walk, the chance to reset after every input + */ + public static double randomWalk_chanceOfResetting = 0.1; + /** + * For random walk, the number of symbols that is tested in total (divided over multiple traces). + */ + public static int randomWalk_numberOfSymbols = 300; + /** + * MaxDepth-parameter for W-method and Wp-method. Typically not larger than 3. Decrease for quicker runs. + */ + public static int w_wp_methods_maxDepth = 2; + + //*****************************************// + // Predefined learning and testing methods // + //*****************************************// + /** + * The learning algorithms. LStar is the basic algorithm, TTT performs much faster + * but is a bit more inaccurate and produces more intermediate hypotheses, so test well) + */ + public enum LearningMethod { LStar, RivestSchapire, TTT, KearnsVazirani } + /** + * The testing algorithms. Random walk is the simplest, but performs badly on large models: + * the chance of hitting a erroneous long trace is very small. WMethod and WpMethod are + * smarter. UserQueries asks the user for which inputs to try as counter-example: have a + * look at the hypothesis, and try to think of one + */ + public enum TestingMethod { RandomWalk, WMethod, WpMethod, UserQueries } + + public static LearningAlgorithm<MealyMachine<?, String, ?, String>, String, Word<String>> loadLearner( + LearningMethod learningMethod, MealyMembershipOracle<String,String> sulOracle, Alphabet<String> alphabet) { + switch (learningMethod){ + case LStar: + return new ExtensibleLStarMealy<String, String>(alphabet, sulOracle, Lists.<Word<String>>newArrayList(), ObservationTableCEXHandlers.CLASSIC_LSTAR, ClosingStrategies.CLOSE_SHORTEST); + case RivestSchapire: + return new ExtensibleLStarMealy<String, String>(alphabet, sulOracle, Lists.<Word<String>>newArrayList(), ObservationTableCEXHandlers.RIVEST_SCHAPIRE, ClosingStrategies.CLOSE_SHORTEST); + case TTT: + return new TTTLearnerMealy<String, String>(alphabet, sulOracle, AcexAnalyzers.LINEAR_FWD); + case KearnsVazirani: + return new KearnsVaziraniMealy<String, String>(alphabet, sulOracle, false, AcexAnalyzers.LINEAR_FWD); + default: + throw new RuntimeException("No learner selected"); + } + } + + public static EquivalenceOracle<MealyMachine<?, String, ?, String>, String, Word<String>> loadTester( + TestingMethod testMethod, SUL<String,String> sul, MealyMembershipOracle<String,String> sulOracle) { + switch (testMethod){ + // simplest method, but doesn't perform well in practice, especially for large models + case RandomWalk: + return new RandomWalkEQOracle<>(randomWalk_chanceOfResetting, randomWalk_numberOfSymbols, true, new Random(123456l), sul); + // Other methods are somewhat smarter than random testing: state coverage, trying to distinguish states, etc. + case WMethod: + return new WMethodEQOracle.MealyWMethodEQOracle<>(w_wp_methods_maxDepth, sulOracle); + case WpMethod: + return new WpMethodEQOracle.MealyWpMethodEQOracle<>(w_wp_methods_maxDepth, sulOracle); + case UserQueries: + return new UserEQOracle(sul); + default: + throw new RuntimeException("No test oracle selected!"); + } + } + + /** + * Simple example of running a learning experiment + * @param learner Learning algorithm, wrapping the SUL + * @param eqOracle Testing algorithm, wrapping the SUL + * @param alphabet Input alphabet + * @throws IOException if the result cannot be written + */ + public static void runSimpleExperiment( + LearningAlgorithm<MealyMachine<?, String, ?, String>, String, Word<String>> learner, + EquivalenceOracle<MealyMachine<?, String, ?, String>, String, Word<String>> eqOracle, + Alphabet<String> alphabet) throws IOException { + MealyExperiment<String, String> experiment + = new MealyExperiment<String, String>(learner, eqOracle, alphabet); + experiment.run(); + System.out.println("Ran " + experiment.getRounds().getCount() + " rounds"); + produceOutput(FINAL_MODEL_FILENAME, experiment.getFinalHypothesis(), alphabet, true); + } + + /** + * Simple example of running a learning experiment + * @param sul Direct access to SUL + * @param learningMethod One of the default learning methods from this class + * @param testingMethod One of the default testing methods from this class + * @param alphabet Input alphabet + * @throws IOException if the result cannot be written + */ + public static void runSimpleExperiment ( + SUL<String,String> sul, + LearningMethod learningMethod, + TestingMethod testingMethod, + Collection<String> alphabet + ) throws IOException { + Alphabet<String> learlibAlphabet = new SimpleAlphabet<String>(alphabet); + LearningSetup learningSetup = new LearningSetup(sul, learningMethod, testingMethod, learlibAlphabet); + runSimpleExperiment(learningSetup.learner, learningSetup.eqOracle, learlibAlphabet); + } + + /** + * More detailed example of running a learning experiment. Starts learning, and then loops testing, + * and if counterexamples are found, refining again. Also prints some statistics about the experiment + * @param learner learner Learning algorithm, wrapping the SUL + * @param eqOracle Testing algorithm, wrapping the SUL + * @param nrSymbols A counter for the number of symbols that have been sent to the SUL (for statistics) + * @param nrResets A counter for the number of resets that have been sent to the SUL (for statistics) + * @param alphabet Input alphabet + * @throws IOException + */ + public static void runControlledExperiment( + LearningAlgorithm<MealyMachine<?, String, ?, String>, String, Word<String>> learner, + EquivalenceOracle<MealyMachine<?, String, ?, String>, String, Word<String>> eqOracle, + Counter nrSymbols, Counter nrResets, + Alphabet<String> alphabet) throws IOException { + try { + // prepare some counters for printing statistics + int stage = 0; + long lastNrResetsValue = 0, lastNrSymbolsValue = 0; + + // start the actual learning + learner.startLearning(); + + while(true) { + // store hypothesis as file + if(saveAllHypotheses) { + String outputFilename = INTERMEDIATE_HYPOTHESIS_FILENAME + stage; + produceOutput(outputFilename, learner.getHypothesisModel(), alphabet, false); + System.out.println("model size " + learner.getHypothesisModel().getStates().size()); + } + + // Print statistics + System.out.println(stage + ": " + Calendar.getInstance().getTime()); + // Log number of queries/symbols + System.out.println("Hypothesis size: " + learner.getHypothesisModel().size() + " states"); + long roundResets = nrResets.getCount() - lastNrResetsValue, roundSymbols = nrSymbols.getCount() - lastNrSymbolsValue; + System.out.println("learning queries/symbols: " + nrResets.getCount() + "/" + nrSymbols.getCount() + + "(" + roundResets + "/" + roundSymbols + " this learning round)"); + lastNrResetsValue = nrResets.getCount(); + lastNrSymbolsValue = nrSymbols.getCount(); + + // Search for CE + DefaultQuery<String, Word<String>> ce = eqOracle.findCounterExample(learner.getHypothesisModel(), alphabet); + + // Log number of queries/symbols + roundResets = nrResets.getCount() - lastNrResetsValue; + roundSymbols = nrSymbols.getCount() - lastNrSymbolsValue; + System.out.println("testing queries/symbols: " + nrResets.getCount() + "/" + nrSymbols.getCount() + + "(" + roundResets + "/" + roundSymbols + " this testing round)"); + lastNrResetsValue = nrResets.getCount(); + lastNrSymbolsValue = nrSymbols.getCount(); + + if(ce == null) { + // No counterexample found, stop learning + System.out.println("\nFinished learning!"); + produceOutput(FINAL_MODEL_FILENAME, learner.getHypothesisModel(), alphabet, true); + break; + } else { + // Counterexample found, rinse and repeat + System.out.println(); + stage++; + learner.refineHypothesis(ce); + } + } + } catch (Exception e) { + String errorHypName = "hyp.before.crash.dot"; + produceOutput(errorHypName, learner.getHypothesisModel(), alphabet, true); + throw e; + } + } + + /** + * More detailed example of running a learning experiment. Starts learning, and then loops testing, + * and if counterexamples are found, refining again. Also prints some statistics about the experiment + * @param sul Direct access to SUL + * @param learningMethod One of the default learning methods from this class + * @param testingMethod One of the default testing methods from this class + * @param alphabet Input alphabet + * @param alphabet Input alphabet + * @throws IOException + */ + public static void runControlledExperiment( + SUL<String,String> sul, + LearningMethod learningMethod, + TestingMethod testingMethod, + Collection<String> alphabet + ) throws IOException { + Alphabet<String> learnlibAlphabet = new SimpleAlphabet<String>(alphabet); + LearningSetup learningSetup = new LearningSetup(sul, learningMethod, testingMethod, learnlibAlphabet); + runControlledExperiment(learningSetup.learner, learningSetup.eqOracle, learningSetup.nrSymbols, learningSetup.nrResets, learnlibAlphabet); + } + + /** + * Produces a dot-file and a PDF (if graphviz is installed) + * @param fileName filename without extension - will be used for the .dot and .pdf + * @param model + * @param alphabet + * @param verboseError whether to print an error explaing that you need graphviz + * @throws FileNotFoundException + * @throws IOException + */ + public static void produceOutput(String fileName, MealyMachine<?,String,?,String> model, Alphabet<String> alphabet, boolean verboseError) throws FileNotFoundException, IOException { + PrintWriter dotWriter = new PrintWriter(fileName + ".dot"); + GraphDOT.write(model, alphabet, dotWriter); + try { + DOT.runDOT(new File(fileName + ".dot"), "pdf", new File(fileName + ".pdf")); + } catch (Exception e) { + if (verboseError) { + System.err.println("Warning: Install graphviz to convert dot-files to PDF"); + System.err.println(e.getMessage()); + } + } + dotWriter.close(); + } + + /** + * Helper class to configure a learning and equivalence oracle. Tell it which learning and testing method you + * want, and it produces the corresponding oracles (and counters for statistics) as attributes. + */ + public static class LearningSetup { + public final EquivalenceOracle<MealyMachine<?, String, ?, String>, String, Word<String>> eqOracle; + public final LearningAlgorithm<MealyMachine<?, String, ?, String>, String, Word<String>> learner; + public final Counter nrSymbols, nrResets; + + public LearningSetup(SUL<String,String> sul, LearningMethod learningMethod, TestingMethod testingMethod, Alphabet<String> alphabet) { + // Wrap the SUL in a detector for non-determinism + SUL<String,String> nonDetSul = new NonDeterminismCheckingSUL<String,String>(sul); + // Wrap the SUL in counters for symbols/resets, so that we can record some statistics + SymbolCounterSUL<String, String> symbolCounterSul = new SymbolCounterSUL<>("symbol counter", nonDetSul); + ResetCounterSUL<String, String> resetCounterSul = new ResetCounterSUL<>("reset counter", symbolCounterSul); + nrSymbols = symbolCounterSul.getStatisticalData(); + nrResets = resetCounterSul.getStatisticalData(); + // we should use the sul only through those wrappers + sul = resetCounterSul; + // Most testing/learning-algorithms want a membership-oracle instead of a SUL directly + MealyMembershipOracle<String,String> sulOracle = new SULOracle<>(sul); + + // Choosing an equivalence oracle + eqOracle = loadTester(testingMethod, sul, sulOracle); + + // Choosing a learner + learner = loadLearner(learningMethod, sulOracle, alphabet); + } + } +} diff --git a/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/CacheInconsistencyException.java b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/CacheInconsistencyException.java new file mode 100644 index 0000000..67c2e73 --- /dev/null +++ b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/CacheInconsistencyException.java @@ -0,0 +1,60 @@ +package basiclearner; + +import net.automatalib.words.Word; + +/** + * Contains the full input for which non-determinism was observed, as well as the full new output + * and the (possibly shorter) old output with which it disagrees + * + * @author Ramon Janssen + */ +public class CacheInconsistencyException extends RuntimeException { + private final Word oldOutput, newOutput, input; + + public CacheInconsistencyException(Word input, Word oldOutput, Word newOutput) { + this.input = input; + this.oldOutput = oldOutput; + this.newOutput = newOutput; + } + + public CacheInconsistencyException(String message, Word input, Word oldOutput, Word newOutput) { + super(message); + this.input = input; + this.oldOutput = oldOutput; + this.newOutput = newOutput; + } + + + /** + * The shortest cached output word which does not correspond with the new output + * @return + */ + public Word getOldOutput() { + return this.oldOutput; + } + + /** + * The full new output word + * @return + */ + public Word getNewOutput() { + return this.newOutput; + } + + /** + * The shortest sublist of the input word which still shows non-determinism + * @return + */ + public Word getShortestInconsistentInput() { + int indexOfInconsistency = 0; + while (oldOutput.getSymbol(indexOfInconsistency).equals(newOutput.getSymbol(indexOfInconsistency))) { + indexOfInconsistency ++; + } + return this.input.subWord(0, indexOfInconsistency); + } + + @Override + public String toString() { + return "Non-determinism detected\nfull input:\n" + this.input + "\nfull new output:\n" + this.newOutput + "\nold output:\n" + this.oldOutput; + } +} diff --git a/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/ExampleExperiment.java b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/ExampleExperiment.java new file mode 100644 index 0000000..3f67622 --- /dev/null +++ b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/ExampleExperiment.java @@ -0,0 +1,41 @@ +package basiclearner; + +import com.google.common.collect.ImmutableSet; +import de.learnlib.api.SUL; + +import java.io.IOException; +import java.util.Collection; + +/** + * Created by ramon on 13-12-16. + */ +public class ExampleExperiment { + /** + * Example of how to call a learner in a simple way with this class. Learns the ExampleSUL. + * @param args + * @throws IOException + */ + public static void main(String [] args) throws IOException { + // Load the actual SUL-class + // For a SUL over a socket, use the SocketSUL-class + // You can also program an own SUL-class if you extend SUL<String,String> (or SUL<S,T> in + // general, with S and T the input and output types - but this class assumes strings) + SUL<String,String> sul = new ExampleSUL(); + + // the input alphabet + Collection<String> inputAlphabet = ImmutableSet.of("a", "b", "c"); + + try { + // runControlledExperiment for detailed statistics, runSimpleExperiment for just the result + BasicLearner.runControlledExperiment(sul, BasicLearner.LearningMethod.LStar, BasicLearner.TestingMethod.RandomWalk, inputAlphabet); + } finally { + if (sul instanceof AutoCloseable) { + try { + ((AutoCloseable) sul).close(); + } catch (Exception exception) { + // should not happen + } + } + } + } +} diff --git a/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/ExampleSUL.java b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/ExampleSUL.java new file mode 100644 index 0000000..8cfdbac --- /dev/null +++ b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/ExampleSUL.java @@ -0,0 +1,90 @@ +package basiclearner; + +import de.learnlib.api.SUL; +import de.learnlib.api.SULException; + +/** + * Example of a three-state system, hard-coded. + * + * @author Ramon Janssen + */ +public class ExampleSUL implements SUL<String, String> { + private enum State{s0,s1,s2}; + private State currentState; + private static boolean VERBOSE = false; + + @Override + public void pre() { + // add any code here that should be run at the beginning of every 'session', + // i.e. put the system in its initial state + if (VERBOSE) { + System.out.println("Starting SUL"); + } + currentState = State.s0; + } + + @Override + public void post() { + // add any code here that should be run at the end of every 'session' + if (VERBOSE) { + System.out.println("Shutting down SUL"); + } + } + + @Override + public String step(String input) throws SULException { + State previousState = this.currentState; + String output = makeTransition(input); + State nextState = this.currentState; + if (VERBOSE) { + System.out.println(previousState + " --" + input + "/" + output + "-> " + nextState); + } + return output; + } + + /** + * The behaviour of the SUL. It takes one input, and returns an output. It now + * contains a hardcoded state-machine (so the result is easy to check). To learn + * an external program/system, connect this method to the SUL (e.g. via sockets + * or stdin/stdout) and make it perform an actual input, and retrieve an actual + * output. + * @param input + * @return + */ + public String makeTransition(String input) { + switch (currentState) { + case s0: + switch(input) { + case "a": + currentState = State.s1; + return "x"; + case "b": + currentState = State.s2; + return "y"; + case "c": + return "z"; + } + case s1: + switch(input) { + case "a": + return "z"; + case "b": + currentState = State.s2; + return "y"; + case "c": + return "z"; + } + case s2: + switch(input) { + case "a": + return "z"; + case "b": + currentState = State.s0; + return "y"; + case "c": + return "z"; + } + } + throw new SULException(new IllegalArgumentException("Argument '" + input + "' was not handled")); + } +} diff --git a/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/NonDeterminismCheckingSUL.java b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/NonDeterminismCheckingSUL.java new file mode 100644 index 0000000..d4ea603 --- /dev/null +++ b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/NonDeterminismCheckingSUL.java @@ -0,0 +1,48 @@ +package basiclearner; + +import java.util.ArrayList; +import java.util.List; + +import de.learnlib.api.SUL; +import de.learnlib.api.SULException; + +/** + * SUL-wrapper to check for non-determinism, by use of an observation tree. + * + * @author Ramon Janssen + * + * @param <I> + * @param <O> + */ +public class NonDeterminismCheckingSUL<I,O> implements SUL<I,O> { + private final SUL<I,O> sul; + private final ObservationTree<I,O> root = new ObservationTree<I,O>(); + private final List<I> inputs = new ArrayList<>(); + private final List<O> outputs = new ArrayList<>(); + + public NonDeterminismCheckingSUL(SUL<I,O> sul) { + this.sul = sul; + } + + @Override + public void post() { + sul.post(); + // check for non-determinism: crashes if outputs are inconsistent with previous ones + root.addObservation(inputs, outputs); + inputs.clear(); + outputs.clear(); + } + + @Override + public void pre() { + sul.pre(); + } + + @Override + public O step(I input) throws SULException { + O result = sul.step(input); + inputs.add(input); + outputs.add(result); + return result; + } +} diff --git a/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/ObservationTree.java b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/ObservationTree.java new file mode 100644 index 0000000..9cb6ec6 --- /dev/null +++ b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/ObservationTree.java @@ -0,0 +1,118 @@ +package basiclearner; + +import java.util.HashMap; +import java.util.LinkedList; +import java.util.List; +import java.util.Map; + +import net.automatalib.words.Word; + +/** + * @author Ramon Janssen + * + * @param <I> the input type of the observations + * @param <O> the output type of the observations + */ +public class ObservationTree<I,O> { + private final ObservationTree<I,O> parent; + private final I parentInput; + private final O parentOutput; + private final Map<I, ObservationTree<I,O>> children; + private final Map<I, O> outputs; + + public ObservationTree() { + this(null, null, null); + } + + private ObservationTree(ObservationTree<I,O> parent, I parentInput, O parentOutput) { + this.children = new HashMap<>(); + this.outputs = new HashMap<>(); + this.parent = parent; + this.parentInput = parentInput; + this.parentOutput = parentOutput; + } + + /** + * @return The outputs observed from the root of the tree until this node + */ + private List<O> getOutputChain() { + if (this.parent == null) { + return new LinkedList<O>(); + } else { + List<O> parentChain = this.parent.getOutputChain(); + parentChain.add(parentOutput); + return parentChain; + } + } + + private List<I> getInputChain() { + if (this.parent == null) { + return new LinkedList<I>(); + } else { + List<I> parentChain = this.parent.getInputChain(); + parentChain.add(this.parentInput); + return parentChain; + } + } + + /** + * Add one input and output symbol and traverse the tree to the next node + * @param input + * @param output + * @return the next node + * @throws InconsistencyException + */ + public ObservationTree<I,O> addObservation(I input, O output) throws CacheInconsistencyException { + O previousOutput = this.outputs.get(input); + boolean createNewBranch = previousOutput == null; + if (createNewBranch) { + // input hasn't been queried before, make a new branch for it and traverse + this.outputs.put(input, output); + ObservationTree<I,O> child = new ObservationTree<I,O>(this, input, output); + this.children.put(input, child); + return child; + } else if (!previousOutput.equals(output)) { + // input is inconsistent with previous observations, throw exception + List<O> oldOutputChain = this.children.get(input).getOutputChain(); + List<O> newOutputChain = this.getOutputChain(); + List<I> inputChain = this.getInputChain(); + newOutputChain.add(output); + throw new CacheInconsistencyException(toWord(inputChain), toWord(oldOutputChain), toWord(newOutputChain)); + } else { + // input is consistent with previous observations, just traverse + return this.children.get(input); + } + } + + /** + * Add Observation to the tree + * @param inputs + * @param outputs + * @throws CacheInconsistencyException Inconsistency between new and stored observations + */ + public void addObservation(Word<I> inputs, Word<O> outputs) throws CacheInconsistencyException { + addObservation(inputs.asList(), outputs.asList()); + } + + + public void addObservation(List<I> inputs, List<O> outputs) throws CacheInconsistencyException { + if (inputs.isEmpty() && outputs.isEmpty()) { + return; + } else if (inputs.isEmpty() || outputs.isEmpty()) { + throw new RuntimeException("Input and output words should have the same length:\n" + inputs + "\n" + outputs); + } else { + I firstInput = inputs.get(0); + O firstOutput = outputs.get(0); + try { + this.addObservation(firstInput, firstOutput) + .addObservation(inputs.subList(1, inputs.size()), outputs.subList(1, outputs.size())); + } catch (CacheInconsistencyException e) { + throw new CacheInconsistencyException(toWord(inputs), e.getOldOutput(), toWord(outputs)); + } + } + } + + public static<T> Word<T> toWord(List<T> symbolList) { + return Word.fromList(symbolList); + } +} diff --git a/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/SocketSUL.java b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/SocketSUL.java new file mode 100644 index 0000000..f7f0ed5 --- /dev/null +++ b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/SocketSUL.java @@ -0,0 +1,80 @@ +package basiclearner; + +import java.io.BufferedReader; +import java.io.IOException; +import java.io.InputStreamReader; +import java.io.PrintWriter; +import java.net.InetAddress; +import java.net.Socket; +import java.net.UnknownHostException; + +import de.learnlib.api.SUL; +import de.learnlib.api.SULException; + +/** + * Socket interface to connect to an SUT/test adapter over TCP. + * + * As an example, type into a unix terminal "nc -vl {ip} {port}" (where {ip} and + * {port} are the chosen values), and run this socketSUL. You can now control the + * SUL through the terminal. + * @author Ramon Janssen + */ +public class SocketSUL implements SUL<String, String>, AutoCloseable { + private final BufferedReader SULoutput; + private final PrintWriter SULinput; + private final Socket socket; + private final boolean extraNewLine; + private final String resetCmd; + + /** + * Socket-interface for SUTs. Connects to a SUT (or test-adapter) + * @param ip the ip-address, for example InetAddress.getLoopbackAddress() for localhost + * @param port the tcp-port + * @param extraNewLine whether to print a newline after every input to the SUT + * @param resetCmd the command to send for resetting the SUT + * @throws UnknownHostException + * @throws IOException + */ + public SocketSUL(InetAddress ip, int port, boolean extraNewLine, String resetCmd) throws UnknownHostException, IOException { + this.socket = new Socket(ip, port); + this.SULoutput = new BufferedReader(new InputStreamReader(socket.getInputStream())); + this.SULinput = new PrintWriter(socket.getOutputStream(), true); + this.extraNewLine = extraNewLine; + this.resetCmd = resetCmd; + } + + @Override + public void post() { + if (extraNewLine) { + this.SULinput.write(this.resetCmd + System.lineSeparator()); + } else { + this.SULinput.write(this.resetCmd); + } + this.SULinput.flush(); + } + + @Override + public void pre() { + + } + + @Override + public String step(String input) throws SULException { + if (extraNewLine) { + this.SULinput.write(input + System.lineSeparator()); + } else { + this.SULinput.write(input); + } + this.SULinput.flush(); + try { + return this.SULoutput.readLine(); + } catch (IOException e) { + throw new SULException(e); + } + } + + @Override + public void close() throws Exception { + this.socket.close(); + } +} diff --git a/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/UserEQOracle.java b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/UserEQOracle.java new file mode 100644 index 0000000..a6c4be2 --- /dev/null +++ b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner/UserEQOracle.java @@ -0,0 +1,56 @@ +package basiclearner; + +import de.learnlib.api.EquivalenceOracle; +import de.learnlib.api.SUL; +import de.learnlib.oracles.DefaultQuery; +import net.automatalib.automata.transout.MealyMachine; +import net.automatalib.words.Word; + +import java.util.*; + +/** + * Created by ramon on 12-12-16. + */ +public class UserEQOracle implements EquivalenceOracle<MealyMachine<?, String, ?, String>, String, Word<String>> { + private final SUL<String,String> sul; + + public UserEQOracle(SUL<String,String> sul) { + this.sul = sul; + } + + @Override + public DefaultQuery<String, Word<String>> findCounterExample(MealyMachine<?, String, ?, String> hypothesis, Collection<? extends String> allowedInputs) { + System.out.println("Enter space-separated input sequence to try as a counter-example, or 'stop' to stop learning"); + Scanner userInputScanner = new Scanner(System.in); + do { + String userInput = userInputScanner.nextLine(); + if (userInput.equals("stop")) { + return null; + } else { + String[] sutInputs = userInput.split("\\s"); + if (sutInputs.length != 0) { + Word<String> input = Word.fromArray(sutInputs, 0, sutInputs.length); + Word<String> hypOutput = hypothesis.computeOutput(input); + Word<String> sulOutput = sulOutput(input); + System.out.println("SUL output: " + sulOutput); + if (!hypOutput.equals(sulOutput)) { + System.out.println(); + return new DefaultQuery<String, Word<String>>(Word.fromList(Collections.emptyList()), input, sulOutput); + } else { + System.out.println("Query '" + userInput + "' not a counterexample"); + } + } + } + } while (true); + } + + private Word<String> sulOutput(Word<String> inputs) { + sul.pre(); + List<String> output = new ArrayList<>(); + for (String input: inputs) { + output.add(sul.step(input)); + } + sul.post(); + return Word.fromList(output); + } +} |