Skip to content
Snippets Groups Projects
Commit c6a2bb62 authored by Thomas's avatar Thomas
Browse files

cleanup

parent 4b06c583
Branches
No related tags found
No related merge requests found
...@@ -25,22 +25,12 @@ public class DumpRFSAEQOracle<A extends FiniteStateAcceptor<?, I>, I> extends Ra ...@@ -25,22 +25,12 @@ public class DumpRFSAEQOracle<A extends FiniteStateAcceptor<?, I>, I> extends Ra
this.target = target; this.target = target;
} }
/**
* tries to short-hand the equivalence test, because minimal RFSA can be compared to some extent
*/
@Nullable @Nullable
@Override @Override
public DefaultQuery<I, Boolean> findCounterExample(A hypothesis, Collection<? extends I> inputs) { 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); DefaultQuery<I, Boolean> a = super.findCounterExample(hypothesis, inputs);
if (a == null) { // no counterexample using random words found
System.out.println(System.currentTimeMillis()-startTime); }
return a; return a;
} }
} }
/* 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;
}
}
}
...@@ -7,10 +7,6 @@ import de.learnlib.util.Experiment; ...@@ -7,10 +7,6 @@ import de.learnlib.util.Experiment;
import net.automatalib.automata.fsa.NFA; import net.automatalib.automata.fsa.NFA;
import net.automatalib.automata.fsa.impl.compact.CompactNFA; 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> { public class RFSALearnAndCompare<I> {
CompactNFA<I> target; CompactNFA<I> target;
......
...@@ -76,9 +76,9 @@ public class TimbukParser { ...@@ -76,9 +76,9 @@ public class TimbukParser {
RFSALearnAndCompare<String> learnAndCompare = new RFSALearnAndCompare<>(); RFSALearnAndCompare<String> learnAndCompare = new RFSALearnAndCompare<>();
learnAndCompare.setTarget(nfa); 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); 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> result = learnAndCompare.experiment.getFinalHypothesis();
NFA<?, String> result2 = learnAndCompare.experiment2.getFinalHypothesis(); NFA<?, String> result2 = learnAndCompare.experiment2.getFinalHypothesis();
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment