diff --git a/learnlib/DumpRFSAEQOracle.java b/learnlib/DumpRFSAEQOracle.java
index 9f2ae0f1d5f97b296fafc8c8777fe21bff13d880..5153f067e8ef15f3a718ec241dea2f3bf4316f6a 100644
--- a/learnlib/DumpRFSAEQOracle.java
+++ b/learnlib/DumpRFSAEQOracle.java
@@ -25,22 +25,12 @@ public class DumpRFSAEQOracle<A extends FiniteStateAcceptor<?, I>, I> extends Ra
this.target = target;
}
- /**
- * tries to short-hand the equivalence test, because minimal RFSA can be compared to some extent
- */
@Nullable
@Override
public DefaultQuery<I, Boolean> findCounterExample(A hypothesis, Collection<? extends I> inputs) {
- long startTime = System.currentTimeMillis();
- if (target.getStates().size() == hypothesis.getStates().size()) {
- // TODO
- return null;
- }
-
DefaultQuery<I, Boolean> a = super.findCounterExample(hypothesis, inputs);
-
- System.out.println(System.currentTimeMillis()-startTime);
-
+ if (a == null) { // no counterexample using random words found
+ }
return a;
}
}
diff --git a/learnlib/NFAs.java b/learnlib/NFAs.java
deleted file mode 100644
index c6031e67c783448307016c0bfbf1eb2702ffb36a..0000000000000000000000000000000000000000
--- a/learnlib/NFAs.java
+++ /dev/null
@@ -1,160 +0,0 @@
-/* Copyright (C) 2013-2019 TU Dortmund
- * This file is part of AutomataLib, http://www.automatalib.net/.
- *
- * Licensed under the Apache License, Version 2.0 (the "License");
- * you may not use this file except in compliance with the License.
- * You may obtain a copy of the License at
- *
- * http://www.apache.org/licenses/LICENSE-2.0
- *
- * Unless required by applicable law or agreed to in writing, software
- * distributed under the License is distributed on an "AS IS" BASIS,
- * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
- * See the License for the specific language governing permissions and
- * limitations under the License.
- */
-import java.util.ArrayDeque;
-import java.util.ArrayList;
-import java.util.BitSet;
-import java.util.Collection;
-import java.util.Deque;
-import java.util.HashMap;
-import java.util.List;
-import java.util.Map;
-
-import net.automatalib.automata.concepts.InputAlphabetHolder;
-import net.automatalib.automata.concepts.StateIDs;
-import net.automatalib.automata.fsa.MutableDFA;
-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.util.automata.Automata;
-import net.automatalib.words.Alphabet;
-
-public final class NFAs {
-
- private NFAs() {}
-
- public static <I> CompactDFA<I> determinize(NFA<?, I> nfa, Alphabet<I> inputAlphabet) {
- return determinize(nfa, inputAlphabet, false, true);
- }
-
- public static <I> CompactDFA<I> determinize(NFA<?, I> nfa,
- Alphabet<I> inputAlphabet,
- boolean partial,
- boolean minimize) {
- CompactDFA<I> result = new CompactDFA<>(inputAlphabet);
- determinize(nfa, inputAlphabet, result, partial, minimize);
- return result;
- }
-
- public static <I> void determinize(NFA<?, I> nfa,
- Collection<? extends I> inputs,
- MutableDFA<?, I> out,
- boolean partial,
- boolean minimize) {
- doDeterminize(nfa, inputs, out, partial);
- if (minimize) {
- Automata.invasiveMinimize(out, inputs);
- }
- }
-
- public static <I, SO> void determinize(NFA<?, I> nfa,
- Collection<? extends I> inputs,
- MutableDFA<SO, I> out,
- boolean partial,
- Map<BitSet, SO> outMap) {
- doDeterminize(nfa, inputs, out, partial, outMap);
- }
-
- public static <I, A extends NFA<?, I> & InputAlphabetHolder<I>> CompactDFA<I> determinize(A nfa) {
- return determinize(nfa, false, true);
- }
-
- public static <I, A extends NFA<?, I> & InputAlphabetHolder<I>> CompactDFA<I> determinize(A nfa,
- boolean partial,
- boolean minimize) {
- return determinize(nfa, nfa.getInputAlphabet(), partial, minimize);
- }
-
- public static <I> void determinize(NFA<?, I> nfa, Collection<? extends I> inputs, MutableDFA<?, I> out) {
- determinize(nfa, inputs, out, false, true);
- }
-
-
- private static <I, SI, SO> void doDeterminize(NFA<SI, I> nfa,
- Collection<? extends I> inputs,
- MutableDFA<SO, I> out,
- boolean partial) {
- Map<BitSet, SO> outStateMap = new HashMap<>();
- doDeterminize(nfa, inputs, out, partial, outStateMap);
- }
-
- private static <I, SI, SO> void doDeterminize(NFA<SI, I> nfa,
- Collection<? extends I> inputs,
- MutableDFA<SO, I> out,
- boolean partial,
- Map<BitSet, SO> outStateMap) {
-
- StateIDs<SI> stateIds = nfa.stateIDs();
-
- Deque<DeterminizeRecord<SI, SO>> stack = new ArrayDeque<>();
-
- List<SI> initList = new ArrayList<>(nfa.getInitialStates());
- BitSet initBs = new BitSet();
- for (SI init : initList) {
- initBs.set(stateIds.getStateId(init));
- }
-
- boolean initAcc = nfa.isAccepting(initList);
- SO initOut = out.addInitialState(initAcc);
-
- outStateMap.put(initBs, initOut);
-
- stack.push(new DeterminizeRecord<>(initList, initOut));
-
- while (!stack.isEmpty()) {
- DeterminizeRecord<SI, SO> curr = stack.pop();
-
- List<SI> inStates = curr.inputStates;
- SO outState = curr.outputState;
-
- for (I sym : inputs) {
- BitSet succBs = new BitSet();
- List<SI> succList = new ArrayList<>();
-
- for (SI inState : inStates) {
- for (SI succState : nfa.getSuccessors(inState, sym)) {
- int succId = stateIds.getStateId(succState);
- if (!succBs.get(succId)) {
- succBs.set(succId);
- succList.add(succState);
- }
- }
- }
-
- if (!partial || !succList.isEmpty()) {
- SO outSucc = outStateMap.get(succBs);
- if (outSucc == null) {
- outSucc = out.addState(nfa.isAccepting(succList));
- outStateMap.put(succBs, outSucc);
- stack.push(new DeterminizeRecord<>(succList, outSucc));
- }
- out.setTransition(outState, sym, outSucc);
- }
- }
- }
-
- }
-
- private static final class DeterminizeRecord<SI, SO> {
-
- private final List<SI> inputStates;
- private final SO outputState;
-
- DeterminizeRecord(List<SI> inputStates, SO outputState) {
- this.inputStates = inputStates;
- this.outputState = outputState;
- }
- }
-}
diff --git a/learnlib/RFSALearnAndCompare.java b/learnlib/RFSALearnAndCompare.java
index 88244cdb47b00c856b201828e776c128caa17a59..fcea3469dd93913133e53edbba8d560217f13f6b 100644
--- a/learnlib/RFSALearnAndCompare.java
+++ b/learnlib/RFSALearnAndCompare.java
@@ -7,10 +7,6 @@ import de.learnlib.util.Experiment;
import net.automatalib.automata.fsa.NFA;
import net.automatalib.automata.fsa.impl.compact.CompactNFA;
-import java.util.List;
-import java.util.function.Function;
-import java.util.function.Predicate;
-
public class RFSALearnAndCompare<I> {
CompactNFA<I> target;
diff --git a/learnlib/TimbukParser.java b/learnlib/TimbukParser.java
index a69a36e335f758f10fb57f7d18d5c1053a324f55..a476642747f25537bd88b0a03b7efd508fea24fc 100644
--- a/learnlib/TimbukParser.java
+++ b/learnlib/TimbukParser.java
@@ -76,9 +76,9 @@ public class TimbukParser {
RFSALearnAndCompare<String> learnAndCompare = new RFSALearnAndCompare<>();
learnAndCompare.setTarget(nfa);
- int maxTests = (int) Math.pow(learnAndCompare.target.getStates().size()*learnAndCompare.target.getInputAlphabet().size(), 2)*10*3*2+250000; // FIXME or beter equivalence oracle
+ int maxTests = learnAndCompare.target.getStates().size()*100000+250000;
System.out.println(maxTests);
- learnAndCompare.learn(3*learnAndCompare.target.getStates().size(), maxTests);
+ learnAndCompare.learn((int) (2.5*learnAndCompare.target.getStates().size()), maxTests);
NFA<?, String> result = learnAndCompare.experiment.getFinalHypothesis();
NFA<?, String> result2 = learnAndCompare.experiment2.getFinalHypothesis();