diff --git a/asmlbenchmarks b/asmlbenchmarks new file mode 100644 index 0000000000000000000000000000000000000000..6982e39def2d560a949dd461e497485f995f3be4 --- /dev/null +++ b/asmlbenchmarks @@ -0,0 +1,22 @@ +file,origstates,forward states,forward rounds,mqueries,reverse states,reverse rounds,mqueries +../../asml/m106.dot,79,79,25,2980800,96,38,2494380 +../../asml/m135.dot,57,57,19,3115636,66,26,1754456 +../../asml/m158.dot,28,28,12,338013,35,16,281952 +../../asml/m159.dot,30,30,11,369680,37,17,311740 +../../asml/m164.dot,43,43,8,430544,48,22,575498 +../../asml/m172.dot,113,113,36,7166880,119,51,5936328 +../../asml/m183.dot,9,9,5,4368,11,7,5700 +../../asml/m185.dot,190,190,39,15340536,231,50,15922095 +../../asml/m196.dot,81,81,33,2573870,89,58,2970903 +../../asml/m199.dot,27,27,15,223008,36,18,264762 +../../asml/m201.dot,128,128,46,13830919,145,68,16272915 +../../asml/m217.dot,14,14,10,182643,22,12,207944 +../../asml/m22.dot,93,93,28,4605436,117,46,5020006 +../../asml/m34.dot,115,115,35,6555594,123,47,8157072 +../../asml/m41.dot,25,25,9,97550,34,13,147465 +../../asml/m45.dot,184,184,52,10515860,219,70,15981504 +../../asml/m49.dot,142,142,36,8028494,151,65,12654375 +../../asml/m54.dot,27,27,13,83237,29,21,131670 +../../asml/m76.dot,210,210,66,14901636,245,80,20917533 +../../asml/m95.dot,33,33,11,390710,39,18,306348 + diff --git a/asmlbenchmarks.csv b/asmlbenchmarks.csv new file mode 100644 index 0000000000000000000000000000000000000000..6982e39def2d560a949dd461e497485f995f3be4 --- /dev/null +++ b/asmlbenchmarks.csv @@ -0,0 +1,22 @@ +file,origstates,forward states,forward rounds,mqueries,reverse states,reverse rounds,mqueries +../../asml/m106.dot,79,79,25,2980800,96,38,2494380 +../../asml/m135.dot,57,57,19,3115636,66,26,1754456 +../../asml/m158.dot,28,28,12,338013,35,16,281952 +../../asml/m159.dot,30,30,11,369680,37,17,311740 +../../asml/m164.dot,43,43,8,430544,48,22,575498 +../../asml/m172.dot,113,113,36,7166880,119,51,5936328 +../../asml/m183.dot,9,9,5,4368,11,7,5700 +../../asml/m185.dot,190,190,39,15340536,231,50,15922095 +../../asml/m196.dot,81,81,33,2573870,89,58,2970903 +../../asml/m199.dot,27,27,15,223008,36,18,264762 +../../asml/m201.dot,128,128,46,13830919,145,68,16272915 +../../asml/m217.dot,14,14,10,182643,22,12,207944 +../../asml/m22.dot,93,93,28,4605436,117,46,5020006 +../../asml/m34.dot,115,115,35,6555594,123,47,8157072 +../../asml/m41.dot,25,25,9,97550,34,13,147465 +../../asml/m45.dot,184,184,52,10515860,219,70,15981504 +../../asml/m49.dot,142,142,36,8028494,151,65,12654375 +../../asml/m54.dot,27,27,13,83237,29,21,131670 +../../asml/m76.dot,210,210,66,14901636,245,80,20917533 +../../asml/m95.dot,33,33,11,390710,39,18,306348 + diff --git a/asmlbenchmarks.ods b/asmlbenchmarks.ods new file mode 100644 index 0000000000000000000000000000000000000000..d6b58924dcd4c8ba9077117eb2a8e67fefab3d49 Binary files /dev/null and b/asmlbenchmarks.ods differ diff --git a/learnlib/GraphvizParser.java b/learnlib/GraphvizParser.java index 81144c452f1a9b22c8fbe6d0f8458144a44e3f13..8a2e8d3e53c7e6c041194c051035dbcfec5bee05 100644 --- a/learnlib/GraphvizParser.java +++ b/learnlib/GraphvizParser.java @@ -68,6 +68,10 @@ public class GraphvizParser { } CompactDFA<String> createDFAfromMealy(List<String> accepting){ + return createDFAfromMealy(accepting, "0"); + } + + CompactDFA<String> createDFAfromMealy(List<String> accepting, String initial){ Set<String> inputs = new HashSet<>(); Set<String> outputs = new HashSet<>(); for(GraphvizParser.Edge e : edges){ @@ -79,20 +83,20 @@ public class GraphvizParser { List<String> inputList = Lists.newArrayList(inputs.iterator()); Alphabet<String> alphabet = Alphabets.fromList(inputList); - DFABuilder<Integer, String, CompactDFA<String>>.DFABuilder__1 builder = AutomatonBuilders.newDFA(alphabet).withInitial("0"); + DFABuilder<Integer, String, CompactDFA<String>>.DFABuilder__1 builder = AutomatonBuilders.newDFA(alphabet).withInitial(initial); for(GraphvizParser.Edge e : edges){ String[] io = e.label.split("/"); for (String o : outputs){ - if (e.from.equals("0") && e.to.equals("0") && accepting.contains(o) && accepting.contains(io[1].trim())) { + if (e.from.equals(initial) && e.to.equals(initial) && accepting.contains(o) && accepting.contains(io[1].trim())) { builder.from(e.from).on(io[0].trim()).to(e.to); - } else if (e.from.equals("0") && accepting.contains(o)) { + } else if (e.from.equals(initial) && accepting.contains(o)) { try { builder.from(e.from).on(io[0].trim()).to(e.to + "_" + io[1].trim()); } catch (IllegalStateException ignored) { } - } else if (e.to.equals("0") && accepting.contains(io[1].trim())) { + } else if (e.to.equals(initial) && accepting.contains(io[1].trim())) { builder.from(e.from + "_" + o).on(io[0].trim()).to(e.to); } else { builder.from(e.from + "_" + o).on(io[0].trim()).to(e.to + "_" + io[1].trim()); @@ -100,7 +104,7 @@ public class GraphvizParser { } if (accepting.contains(io[1].trim())){ - if (e.to.equals("0")) + if (e.to.equals(initial)) builder.withAccepting(e.to); else builder.withAccepting(e.to+"_"+io[1].trim()); @@ -111,13 +115,17 @@ public class GraphvizParser { } CompactDFA<String> createDFA(List<String> accepting){ + return createDFA(accepting, "0"); + } + + CompactDFA<String> createDFA(List<String> accepting, String initial){ Set<String> inputs = new HashSet<>(); edges.forEach(edge -> inputs.add(edge.label)); List<String> inputList = Lists.newArrayList(inputs.iterator()); Alphabet<String> alphabet = Alphabets.fromList(inputList); - DFABuilder<Integer, String, CompactDFA<String>>.DFABuilder__1 builder = AutomatonBuilders.newDFA(alphabet).withInitial("0"); + DFABuilder<Integer, String, CompactDFA<String>>.DFABuilder__1 builder = AutomatonBuilders.newDFA(alphabet).withInitial(initial); for(GraphvizParser.Edge e : edges){ builder.from(e.from).on(e.label).to(e.to); } @@ -127,14 +135,18 @@ public class GraphvizParser { return builder.create(); } - CompactDFA<String> createDFAAllAccepting(){ + CompactDFA<String> createDFAAllAccepting() { + return createDFAAllAccepting("0"); + } + + CompactDFA<String> createDFAAllAccepting(String initial){ Set<String> inputs = new HashSet<>(); edges.forEach(edge -> inputs.add(edge.label)); List<String> inputList = Lists.newArrayList(inputs.iterator()); Alphabet<String> alphabet = Alphabets.fromList(inputList); - DFABuilder<Integer, String, CompactDFA<String>>.DFABuilder__1 builder = AutomatonBuilders.newDFA(alphabet).withInitial("0"); + DFABuilder<Integer, String, CompactDFA<String>>.DFABuilder__1 builder = AutomatonBuilders.newDFA(alphabet).withInitial(initial); for(GraphvizParser.Edge e : edges){ builder.from(e.from).on(e.label).to(e.to); } diff --git a/learnlib/Kiss2Parser.java b/learnlib/Kiss2Parser.java new file mode 100644 index 0000000000000000000000000000000000000000..3548bfedf929cb0bf0083185af30c6c198973d13 --- /dev/null +++ b/learnlib/Kiss2Parser.java @@ -0,0 +1,78 @@ +import net.automatalib.automata.fsa.NFA; +import net.automatalib.automata.fsa.impl.compact.CompactDFA; +import net.automatalib.automata.fsa.impl.compact.CompactNFA; +import net.automatalib.visualization.Visualization; + +import java.io.IOException; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.*; + +/** + * It is *not* a general KISS2 parser, it only parses the things I needed for the mealy machines. + */ +public class Kiss2Parser extends GraphvizParser { + + Kiss2Parser(Path filename) throws IOException { + super(filename); + nodes = new HashSet<>(); + nodes2 = new HashSet<>(); + edges = new HashSet<>(); + + Scanner s = new Scanner(filename); + while(s.hasNextLine()){ + String line = s.nextLine(); + line = line.split("#",1)[0].trim(); + + if(line.isEmpty() || line.startsWith(".")) + continue; + + if(line.matches("\\p{Graph}+\\s+\\p{Graph}+\\s+\\p{Graph}+\\s+\\p{Graph}+")){ + int i = 0; + String input = line.split(" ")[i].trim(); + ++i; + + while (line.split(" ")[i].isEmpty()) + ++i; + String from = line.split(" ")[i].trim(); + ++i; + + while (line.split(" ")[i].isEmpty()) + ++i; + String to = line.split(" ")[i].trim(); + ++i; + + while (line.split(" ")[i].isEmpty()) + ++i; + String out = line.split(" ")[i].trim(); + + edges.add(new Edge(from, to, input + "/" + out)); + nodes2.add(from); + nodes2.add(to); + } + } + } + + public static void main(String[] args) throws IOException { + Kiss2Parser parser = new Kiss2Parser(Paths.get(args[0])); + CompactDFA<String> dfa = parser.createDFAfromMealy(Collections.singletonList("1"), "s_2_0"); + + Visualization.visualize(dfa); + + CompactNFA<String> nfa = FSAUtil.convert(dfa); + + RFSALearnAndCompare<String> learnAndCompare = new RFSALearnAndCompare<>(); + learnAndCompare.setTarget(nfa); + + learnAndCompare.learn((int) (1.5*learnAndCompare.target.getStates().size()), 200000); + + NFA<?, String> result = learnAndCompare.experiment.getFinalHypothesis(); + NFA<?, String> result2 = learnAndCompare.experiment2.getFinalHypothesis(); + + Visualization.visualize(result, learnAndCompare.target.getInputAlphabet()); + Visualization.visualize(result2, learnAndCompare.target.getInputAlphabet()); + + System.out.println(args[0] + "," + nfa.getStates().size() + "," + result.size() + "," + learnAndCompare.experiment.getRounds().getCount() + "," + learnAndCompare.mqOracle.getCounter().getCount() + "," + result2.size() + "," + learnAndCompare.experiment2.getRounds().getCount() + "," + learnAndCompare.mqOracle2.getCounter().getCount()); + + } +} diff --git a/nfabenchmarks_pgf2.csv b/nfabenchmarks_pgf2.csv new file mode 100644 index 0000000000000000000000000000000000000000..fbecea4f47a211cf450a2444f0b3ce125812337c --- /dev/null +++ b/nfabenchmarks_pgf2.csv @@ -0,0 +1,8 @@ +file,origstates,forwardstates,forward rounds,mqueries,reversestates,reverse rounds,mqueries2 +Ba4bPa0,4,4,3,174,4,3,145 +Ba4bPa1,3,4,2,27,3,2,21 +Ba4bPa4,16,16,7,3616,16,6,2260 +Ba4bPa6,40,36,16,23120,36,15,16473 +Ba4bPa10,125,88,43,305493,90,35,187889 +Ba4bPa11,89,67,26,136359,61,27,91485 +Ba4bPa12,165,101,57,448655,95,49,247566