diff options
Diffstat (limited to 'assignments/assignment2/Bounded Retransmission Protocol Tester/Source/brpcompare')
3 files changed, 193 insertions, 0 deletions
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); + } + +} |