From ac914c719d401c44cb2633127952b022bf563ff3 Mon Sep 17 00:00:00 2001
From: René den Hertog
Date: Thu, 26 Oct 2017 17:34:51 +0200
Subject: 'Bounded Retransmission Protocol' Blob
---
.../Source/brpcompare/BRPCompare.java | 38 ++++++++
.../Source/brpcompare/GraphvizParser.java | 101 +++++++++++++++++++++
.../Source/brpcompare/HashAlphabet.java | 54 +++++++++++
3 files changed, 193 insertions(+)
create mode 100755 assignments/assignment2/Bounded Retransmission Protocol Tester/Source/brpcompare/BRPCompare.java
create mode 100755 assignments/assignment2/Bounded Retransmission Protocol Tester/Source/brpcompare/GraphvizParser.java
create mode 100755 assignments/assignment2/Bounded Retransmission Protocol Tester/Source/brpcompare/HashAlphabet.java
(limited to 'assignments/assignment2/Bounded Retransmission Protocol Tester/Source/brpcompare')
diff --git a/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/brpcompare/BRPCompare.java b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/brpcompare/BRPCompare.java
new file mode 100755
index 0000000..78d822b
--- /dev/null
+++ b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/brpcompare/BRPCompare.java
@@ -0,0 +1,38 @@
+package brpcompare;
+
+import com.google.common.collect.ImmutableSet;
+import net.automatalib.util.automata.Automata;
+import net.automatalib.words.Word;
+
+import java.io.File;
+import java.io.IOException;
+import java.nio.file.Paths;
+import java.util.Collection;
+
+/**
+ * Created by petra on 14-12-16.
+ */
+public class BRPCompare {
+
+ public static void main(String[] args) throws IOException {
+// String model1 = "/hypothesis0.dot",
+// model2 = "/hypothesis1.dot";
+ String model1 = "/Final Model Of " + args[0] + ".dot",
+ model2 = "/Final Model Of Reference.dot";
+ Collection<String> inputAlphabet = ImmutableSet.of("IACK", "IREQ_0_0_0", "IREQ_0_0_1", "IREQ_0_1_0", "IREQ_0_1_1", "IREQ_1_0_0", "IREQ_1_0_1", "IREQ_1_1_0", "IREQ_1_1_1", "ISENDFRAME", "ITIMEOUT");
+
+ GraphvizParser p = new GraphvizParser(Paths.get(new File("").getAbsolutePath().concat(model1)));
+ GraphvizParser p2 = new GraphvizParser(Paths.get(new File("").getAbsolutePath().concat(model2)));
+ try {
+ Word<String> compareResult = Automata.findSeparatingWord(p.createMachine(), p2.createMachine(), inputAlphabet);
+ if(compareResult == null) {
+ System.out.println("The automata are equal!");
+ } else {
+ System.out.println("The automata are not equal! A counterexample is: " + compareResult);
+ }
+ } catch (NullPointerException e) {
+ e.printStackTrace();
+ System.err.println("Did you compare with the right input alphabet?");
+ }
+ }
+}
diff --git a/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/brpcompare/GraphvizParser.java b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/brpcompare/GraphvizParser.java
new file mode 100755
index 0000000..49c29c7
--- /dev/null
+++ b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/brpcompare/GraphvizParser.java
@@ -0,0 +1,101 @@
+package brpcompare;
+
+import com.google.common.collect.Lists;
+import net.automatalib.automata.transout.impl.compact.CompactMealy;
+import net.automatalib.util.automata.builders.AutomatonBuilders;
+import net.automatalib.util.automata.builders.MealyBuilder;
+import net.automatalib.words.Alphabet;
+import net.automatalib.words.impl.Alphabets;
+
+import java.io.File;
+import java.io.IOException;
+import java.nio.file.Path;
+import java.util.*;
+
+/**
+ * A class which is just able to parse the output generated by LearnLib (why is this not included in LearnLib itself?
+ * I have no clue.) It is *not* a general graphviz parser, it only parses the things I needed for the mealy machines.
+ */
+public class GraphvizParser {
+ public static class Edge {
+ public final String from;
+ public final String to;
+ public final String label;
+ Edge(String b, String e, String l){
+ from = b;
+ to = e;
+ label = l;
+ }
+ }
+
+ public final Set<String> nodes;
+ public final Set<Edge> edges;
+ public String initialState;
+
+ GraphvizParser(Path filename) throws IOException {
+ File file = new File(filename.toString());
+ if (!file.exists()) {
+ throw new RuntimeException("File '" + filename + "' does not exist");
+ }
+ if (file.isDirectory()) {
+ throw new RuntimeException("File " + filename + "' is a directory");
+ }
+
+ nodes = new HashSet<>();
+ edges = new HashSet<>();
+
+ Scanner s = new Scanner(filename);
+ while(s.hasNextLine()){
+ String line = s.nextLine();
+
+ if(!line.contains("label")) continue;
+
+ if(line.contains("->")){
+ int e1 = line.indexOf('-');
+ int e2 = line.indexOf('[');
+ int b3 = line.indexOf('"');
+ int e3 = line.lastIndexOf('"');
+
+ String from = line.substring(0, e1).trim();
+ String to = line.substring(e1+2, e2).trim();
+ String label = line.substring(b3+1, e3).trim();
+
+ // First read state will be the initial one.
+ if(initialState == null) initialState = from;
+
+ nodes.add(from);
+ nodes.add(to);
+ edges.add(new Edge(from, to, label));
+ } else {
+ int end = line.indexOf('[');
+ if(end <= 0) continue;
+ String node = line.substring(0, end).trim();
+
+ nodes.add(node);
+ }
+ }
+ }
+
+ CompactMealy<String, String> createMachine(){
+ Set<String> inputs = new HashSet<>();
+ for(Edge e : edges){
+ String[] io = e.label.split("/");
+ inputs.add(io[0].trim());
+ }
+
+ List<String> inputList = Lists.newArrayList(inputs.iterator());
+ Alphabet<String> alphabet = new HashAlphabet<>(Alphabets.fromList(inputList));
+
+ MealyBuilder<?, String, ?, String, CompactMealy<String, String>>.MealyBuilder__1 builder = AutomatonBuilders.<String, String>newMealy(alphabet).withInitial(initialState);
+
+ for(Edge e : edges){
+ String[] io = e.label.split("/");
+
+ builder.from(e.from).on(io[0].trim()).withOutput(io[1].trim()).to(e.to);
+ }
+
+ return builder.create();
+ }
+
+}
+
diff --git a/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/brpcompare/HashAlphabet.java b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/brpcompare/HashAlphabet.java
new file mode 100755
index 0000000..46742d2
--- /dev/null
+++ b/assignments/assignment2/Bounded Retransmission Protocol Tester/Source/brpcompare/HashAlphabet.java
@@ -0,0 +1,54 @@
+package brpcompare;
+
+import net.automatalib.words.Alphabet;
+import net.automatalib.words.abstractimpl.AbstractAlphabet;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+
+/**
+ * Created by joshua on 14/07/2016.
+ * I noticed that getSymbolIndex was called a lot. So I optimized for that, with a look up structure.
+ * Too bad it wasn't in LearnLib already.
+ */
+public class HashAlphabet<I> extends AbstractAlphabet<I> {
+ private final ArrayList<I> symbols;
+ private final HashMap<I, Integer> indices;
+
+ public HashAlphabet(Alphabet<I> in) {
+ symbols = new ArrayList<>(in);
+ indices = new HashMap<>(in.size());
+ for (int i = 0; i < symbols.size(); i++) {
+ indices.put(symbols.get(i), i);
+ }
+ }
+
+ @Override
+ public I getSymbol(int index) {
+ return symbols.get(index);
+ }
+
+ @Override
+ public int getSymbolIndex(I symbol) {
+ return indices.get(symbol);
+ }
+
+ @Override
+ public int size() {
+ return symbols.size();
+ }
+
+ /* (non-Javadoc)
+ * @see net.automatalib.words.abstractimpl.AbstractAlphabet#writeToArray(int, java.lang.Object[], int, int)
+ */
+ @Override
+ public void writeToArray(int offset, Object[] array, int tgtOfs, int num) {
+ System.arraycopy(symbols, offset, array, tgtOfs, num);
+ }
+
+ @Override
+ public boolean containsSymbol(I symbol) {
+ return indices.containsKey(symbol);
+ }
+
+}
--
cgit v1.2.3