'Bounded Retransmission Protocol' Blob

author: René den Hertog 2017-10-26 17:34:51 +0200
committer: René den Hertog 2017-10-26 17:34:51 +0200
commit: ac914c719d401c44cb2633127952b022bf563ff3 (patch)
tree: f7d2399b2ab6cddb86aa996096581a397ff407b9 /assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner
parent: Finish assignment 2, part 1 (diff)
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);
+    }
+}
author	René den Hertog	2017-10-26 17:34:51 +0200
committer	René den Hertog	2017-10-26 17:34:51 +0200
commit	ac914c719d401c44cb2633127952b022bf563ff3 (patch)
tree	f7d2399b2ab6cddb86aa996096581a397ff407b9 /assignments/assignment2/Bounded Retransmission Protocol Tester/Source/basiclearner
parent	Finish assignment 2, part 1 (diff)