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

today

parent 4ef3fa63
Branches
No related tags found
No related merge requests found
...@@ -33,6 +33,7 @@ public class DumpRFSAEQOracle<A extends FiniteStateAcceptor<?, I>, I, D> extends ...@@ -33,6 +33,7 @@ public class DumpRFSAEQOracle<A extends FiniteStateAcceptor<?, I>, I, D> extends
@Override @Override
public DefaultQuery<I, D> findCounterExample(A hypothesis, Collection<? extends I> inputs) { public DefaultQuery<I, D> findCounterExample(A hypothesis, Collection<? extends I> inputs) {
if (target.getStates().size() == hypothesis.getStates().size()) { if (target.getStates().size() == hypothesis.getStates().size()) {
// TODO
return null; return null;
} }
......
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.automata.fsa.impl.compact.CompactNFA;
import net.automatalib.util.automata.builders.FSABuilder; import net.automatalib.util.automata.builders.FSABuilder;
import net.automatalib.visualization.Visualization; import net.automatalib.visualization.Visualization;
import java.util.*;
public class GenRFSA<A extends CompactNFA<I>, S, I> { public class GenRFSA<A extends CompactNFA<I>, S, I> {
public CompactNFA<I> reverse(A source){ public CompactNFA<I> reverse(A original){
FSABuilder<Integer, I, CompactNFA<I>> builder = new FSABuilder<>(new CompactNFA<>(source.getInputAlphabet(), source.getStates().size())); FSABuilder<Integer, I, CompactNFA<I>> builder = new FSABuilder<>(new CompactNFA<>(original.getInputAlphabet(), original.getStates().size()));
for (int a : source.getStates()) { for (int a : original.getStates()) {
if (source.isAccepting(a)) if (original.isAccepting(a))
builder.withInitial(a); builder.withInitial(a);
for (I i: source.getInputAlphabet()) for (I i: original.getInputAlphabet())
for (int c : source.getTransitions(a, i)) for (int c : original.getTransitions(a, i))
builder.from(c).on(i).to(a); builder.from(c).on(i).to(a);
} }
original.getInitialStates().forEach(builder::withAccepting);
builder.withAccepting(source.getInitialStates().toArray());
return builder.create(); 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) { public static void main(String[] args) {
RandomNFAGen c = new RandomNFAGen(10); RandomNFAGen c = new RandomNFAGen(10);
...@@ -29,5 +77,6 @@ public class GenRFSA<A extends CompactNFA<I>, S, I> { ...@@ -29,5 +77,6 @@ public class GenRFSA<A extends CompactNFA<I>, S, I> {
Visualization.visualize(nfa); Visualization.visualize(nfa);
Visualization.visualize(genRFSA.reverse(nfa)); Visualization.visualize(genRFSA.reverse(nfa));
Visualization.visualize(genRFSA.canonicalize(nfa));
} }
} }
/* 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;
}
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment