diff --git a/learnlib/DumpRFSAEQOracle.java b/learnlib/DumpRFSAEQOracle.java
index a9823fda9396632f03875e6dcc84caed9a1c00d4..f2856e8422b6d48904d1532c0d72d18fa08deaa2 100644
--- a/learnlib/DumpRFSAEQOracle.java
+++ b/learnlib/DumpRFSAEQOracle.java
@@ -33,6 +33,7 @@ public class DumpRFSAEQOracle<A extends FiniteStateAcceptor<?, I>, I, D> extends
@Override
public DefaultQuery<I, D> findCounterExample(A hypothesis, Collection<? extends I> inputs) {
if (target.getStates().size() == hypothesis.getStates().size()) {
+ // TODO
return null;
}
diff --git a/learnlib/GenRFSA.java b/learnlib/GenRFSA.java
index 7816d27321058bca9e637bb6ccf2d2e2755fea60..050e4a9f467877572caf83cd0741a28386e900ba 100644
--- a/learnlib/GenRFSA.java
+++ b/learnlib/GenRFSA.java
@@ -1,26 +1,74 @@
+import com.google.common.collect.Sets;
+import net.automatalib.automata.fsa.impl.compact.CompactDFA;
import net.automatalib.automata.fsa.impl.compact.CompactNFA;
import net.automatalib.util.automata.builders.FSABuilder;
import net.automatalib.visualization.Visualization;
+import java.util.*;
+
public class GenRFSA<A extends CompactNFA<I>, S, I> {
- public CompactNFA<I> reverse(A source){
- FSABuilder<Integer, I, CompactNFA<I>> builder = new FSABuilder<>(new CompactNFA<>(source.getInputAlphabet(), source.getStates().size()));
+ public CompactNFA<I> reverse(A original){
+ FSABuilder<Integer, I, CompactNFA<I>> builder = new FSABuilder<>(new CompactNFA<>(original.getInputAlphabet(), original.getStates().size()));
- for (int a : source.getStates()) {
- if (source.isAccepting(a))
+ for (int a : original.getStates()) {
+ if (original.isAccepting(a))
builder.withInitial(a);
- for (I i: source.getInputAlphabet())
- for (int c : source.getTransitions(a, i))
+ for (I i: original.getInputAlphabet())
+ for (int c : original.getTransitions(a, i))
builder.from(c).on(i).to(a);
}
-
- builder.withAccepting(source.getInitialStates().toArray());
+ original.getInitialStates().forEach(builder::withAccepting);
return builder.create();
}
- public
+ public CompactNFA<I> canonicalize(A original){
+ FSABuilder<Integer, I, CompactNFA<I>> builder = new FSABuilder<>(new CompactNFA<>(original.getInputAlphabet()));
+
+ Map<BitSet, Integer> outMap = new HashMap<>();
+
+ CompactDFA<I> out = new CompactDFA<I>(original.getInputAlphabet());
+ NFAs.determinize(original, original.getInputAlphabet(), out, false, outMap);
+
+ Set<BitSet> detStates = outMap.keySet();
+ Set<BitSet> coverableStates = new HashSet<>();
+ for (BitSet testState : detStates) {
+ Set<BitSet> usingStates = new HashSet<>(outMap.keySet());
+ usingStates.remove(testState);
+ //kind a subset-sum
+ Set<Set<BitSet>> powersets = Sets.powerSet(usingStates);
+ for (Set<BitSet> set : powersets) {
+ BitSet sum = new BitSet();
+ set.forEach(s -> sum.or(s));
+ if (sum.equals(testState)){
+ coverableStates.add(testState);
+ break;
+ }
+ }
+ }
+ detStates.removeAll(coverableStates);
+
+ //initial states
+ BitSet initBs = new BitSet();
+ original.getInitialStates().forEach(initBs::set);
+
+ for (BitSet s : detStates) {
+ BitSet tmp = (BitSet) s.clone();
+ //initial states
+ tmp.or(initBs);
+ if (s.equals(initBs))
+ builder.withInitial(s);
+
+ //final states
+ if ()
+ builder.withAccepting(s);
+ }
+
+ //TODO transitions
+
+ return builder.create();
+ }
public static void main(String[] args) {
RandomNFAGen c = new RandomNFAGen(10);
@@ -29,5 +77,6 @@ public class GenRFSA<A extends CompactNFA<I>, S, I> {
Visualization.visualize(nfa);
Visualization.visualize(genRFSA.reverse(nfa));
+ Visualization.visualize(genRFSA.canonicalize(nfa));
}
}
diff --git a/learnlib/NFAs.java b/learnlib/NFAs.java
new file mode 100644
index 0000000000000000000000000000000000000000..c6031e67c783448307016c0bfbf1eb2702ffb36a
--- /dev/null
+++ b/learnlib/NFAs.java
@@ -0,0 +1,160 @@
+/* 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;
+ }
+ }
+}