diff --git a/prism/src/automata/finite/DeterministicFiniteAutomaton.java b/prism/src/automata/finite/DeterministicFiniteAutomaton.java index 082554c5..0ffc27ea 100644 --- a/prism/src/automata/finite/DeterministicFiniteAutomaton.java +++ b/prism/src/automata/finite/DeterministicFiniteAutomaton.java @@ -1,8 +1,12 @@ package automata.finite; +import java.util.BitSet; import java.util.HashSet; +import java.util.LinkedHashSet; +import java.util.Set; public class DeterministicFiniteAutomaton extends FiniteAutomaton> { + @Override public HashSet getSuccessors(State state) { HashSet result = new HashSet(); @@ -51,4 +55,121 @@ public class DeterministicFiniteAutomaton extends FiniteAutomaton toNFA() { + NondeterministicFiniteAutomaton nfa = new NondeterministicFiniteAutomaton(); + + //for(Symbol ap: getApList()){ + // nfa.addAp(ap); + //} + nfa.setApList(apList); + + for(State state: getStates()) { + nfa.addState(state); + if(isAcceptingState(state)) { + nfa.addAcceptingState(state); + } + } + nfa.addInitialState(getInitialState()); + + for(SingleEdge edge : edges) { + LinkedHashSet sinkSet = new LinkedHashSet(); + sinkSet.add(edge.getSink()); + MultiEdge nfaEdge = new MultiEdge(edge.getSource(), edge.getLabel(), sinkSet); + + State source = edge.getSource(); + State sink = edge.getSink(); + nfa.getIncomingEdges().get(sink).add(nfaEdge); + nfa.getOutgoingEdges().get(source).add(nfaEdge); + } + + nfa.generateEdges(); + return nfa; + } + + /** + * DFA minimization as in Brzozowski'63 + * @return the DFA with a minimal number of states + */ + public DeterministicFiniteAutomaton minimize() { + //reverse + NondeterministicFiniteAutomaton reversed = toNFA(); + reversed.reverse(); + + //Powerset construction for the reversed automaton + NondeterministicFiniteAutomaton minimalReversedDFA = reversed.determinize().toNFA(); + //reverse the reversed DFA + minimalReversedDFA.reverse(); + //Powerset construction for the reversed^2 automaton + DeterministicFiniteAutomaton minimized = minimalReversedDFA.determinize(); + //Make automaton complete + minimized.complete(); + return minimized; + } + + public Set getPredecessors(Set states, EdgeLabel symbol) { + return states.stream() + .map(state -> getPredecessors(state, symbol)) + .reduce( + new HashSet(), + (m1, m2) -> { + m1.addAll(m2); + return m1; + }); + } + + public void complete() { + trim(); + + if(states.isEmpty()) { + //If automaton is empty add one initial state with a true loop + State trap = newState(); + addInitialState(trap); + SingleEdge trapEdge = new SingleEdge<>(trap, new EdgeLabel<>(true) ,trap); + addEdge(trapEdge); + } else { + // Create trap state with self-loop + State trap = newState(); + //System.out.println("The trap is " + trap); + + /* + MultiEdge selfLoop = new MultiEdge<>(trap, new EdgeLabel(true), trapSingleton); + mergeEdge(selfLoop); + */ + + // This will be used to iterate over the values + BitSet value = new BitSet(); + value.set(0, apList.size(), false); + + // Save if an edge to the trap state has been added + boolean edgeToTrapState = false; + // Iterate over all possible values + while(value.cardinality() <= apList.size()) { + //System.out.println(value + " " + outgoingEdges); + EdgeLabel label = new EdgeLabel(apList, value); + for(State state : states) { + if(getSuccessors(state, label).size() == 0) { + SingleEdge trapEdge = new SingleEdge<>(state, new EdgeLabel<>(label), trap); + addEdge(trapEdge); + if(state != trap) { + edgeToTrapState = true; + } + //System.out.println(" Adding " + trapEdge); + } + } + + // Increase value, set the first clear bit and unset everything behind + int firstUnsetBit = value.nextClearBit(0); + value.set(firstUnsetBit); + for(int i = 0; i { } public boolean intersects(EdgeLabel other) { + if(isTrue() || other.isTrue()) { + return true; + } + + if(isFalse()) { + if(other.isFalse()) { + return true; + } + } + ArrayList relevantSymbols = relevantSymbols(); relevantSymbols.retainAll(other.relevantSymbols()); @@ -164,4 +174,34 @@ public class EdgeLabel { } return result.toString(); } + + @Override + public boolean equals(Object o) { + if(o instanceof EdgeLabel) { + @SuppressWarnings("unchecked") + EdgeLabel other = (EdgeLabel)o; + + //Check for default cases + if(isTrue()) { + return other.isTrue(); + } + if(isFalse()) { + return other.isFalse(); + } + + //Check for non-default cases + return getValue().equals(other.getValue()) && + getRelevant().equals(other.getRelevant()); + } else { + return false; + } + } + + @Override + public int hashCode() { + if(isTrue()) { return 0;} + if(isFalse()) {return -1;} + + return value.hashCode() ^ relevant.hashCode(); + } } diff --git a/prism/src/automata/finite/FiniteAutomaton.java b/prism/src/automata/finite/FiniteAutomaton.java index 84cf9628..82f465a0 100644 --- a/prism/src/automata/finite/FiniteAutomaton.java +++ b/prism/src/automata/finite/FiniteAutomaton.java @@ -6,6 +6,7 @@ import java.util.HashSet; import java.util.LinkedList; import java.util.List; import java.util.Queue; +import java.util.Set; import java.util.Stack; public abstract class FiniteAutomaton> { @@ -195,12 +196,53 @@ public abstract class FiniteAutomaton> { public HashSet getPredecessors(State state) { HashSet result = new HashSet(); + + if(!incomingEdges.containsKey(state)) { + incomingEdges.put(state, new HashSet<>()); + } + for(Edge edge : incomingEdges.get(state)) { result.add(edge.getSource()); } return result; } + /** + * get the predecessors for a certain state and label + * @param state the sink state + * @param label the label for which the source states should be collected + * @return the predecessors + */ + public Set getPredecessors(State state, EdgeLabel label) { + Set result = new HashSet(); + for(Edge edge : incomingEdges.get(state)) { + //If edge label agrees with label, add source state + if(edge.getLabel().equals(label)) { + result.add(edge.getSource()); + } + } + return result; + } + + /** + * get the predecessors for a set of possible sink states and a label + * @param set of the sink states + * @param label the label for which the source states should be collected + * @return the predecessors + */ + public Set getPredecssors(Set states, EdgeLabel label) { + Set result = new HashSet(); + for(State state : states) { + result.addAll(getPredecessors(state, label)); + } + return result; + } + + /** + * get the predecessors for a set of possible sink states regardless the label + * @param set of the sink states + * @return the predecessors + */ public HashSet getSuccessors(HashSet states) { HashSet result = new HashSet(); for(State state : states) { @@ -216,7 +258,7 @@ public abstract class FiniteAutomaton> { } return result; } - + public HashSet getPredecessors(HashSet states) { HashSet result = new HashSet(); for(State state : states) { @@ -302,6 +344,29 @@ public abstract class FiniteAutomaton> { return longestSuccLength+1; } + public Set> getIncomingEdgeLabels(State state) { + Set> result = new HashSet>(); + for(Edge edge : getIncomingEdges(state)) { + result.add(edge.getLabel()); + } + return result; + } + + public Set> getIncomingEdgeLabels(Set states) { + Set> result = new HashSet>(); + for(State state : states) { + result.addAll(getIncomingEdgeLabels(state)); + } + return result; + } + + public Set> getOutgoingEdgeLabels(State state) { + Set> result = new HashSet>(); + for(Edge edge : getOutgoingEdges(state)) { + result.add(edge.getLabel()); + } + return result; + } /** * trim reduces the automaton to all its reachable and co-reachable states and the corresponding edges diff --git a/prism/src/automata/finite/MultiEdge.java b/prism/src/automata/finite/MultiEdge.java index 698a9018..0e52d0b1 100644 --- a/prism/src/automata/finite/MultiEdge.java +++ b/prism/src/automata/finite/MultiEdge.java @@ -58,4 +58,21 @@ public class MultiEdge extends Edge { return result.toString(); } + @Override + public int hashCode() { + int result = super.hashCode(); + return result ^ sinks.hashCode(); + } + + @Override + public boolean equals(Object o) { + if(o instanceof MultiEdge) { + @SuppressWarnings("unchecked") + MultiEdge other = (MultiEdge)o; + return super.equals(other) && + getSinks().equals(other.getSinks()); + } else { + return false; + } + } } diff --git a/prism/src/automata/finite/NondeterministicFiniteAutomaton.java b/prism/src/automata/finite/NondeterministicFiniteAutomaton.java index ae3d0818..7405b416 100644 --- a/prism/src/automata/finite/NondeterministicFiniteAutomaton.java +++ b/prism/src/automata/finite/NondeterministicFiniteAutomaton.java @@ -3,13 +3,13 @@ package automata.finite; import java.util.BitSet; import java.util.HashMap; import java.util.HashSet; +import java.util.Iterator; import java.util.LinkedList; +import java.util.Set; import parser.ast.Expression; import parser.ast.ExpressionLabel; import parser.ast.ExpressionRegular; - -import automata.finite.MultiEdge; /** * Class to store a non-deterministic finite automaton. */ @@ -270,6 +270,9 @@ public class NondeterministicFiniteAutomaton extends FiniteAutomaton getSuccessors(State state) { HashSet result = new HashSet(); + if(!outgoingEdges.containsKey(state)) { + outgoingEdges.put(state, new HashSet>()); + } for(MultiEdge edge : outgoingEdges.get(state)) { result.addAll(edge.getSinks()); } @@ -297,16 +300,37 @@ public class NondeterministicFiniteAutomaton extends FiniteAutomaton edge : edges) { - // For each sink ... + Iterator> it = edges.iterator(); + Set> toAdd = new HashSet>(); + while(it.hasNext()) { + //For each sink ... + MultiEdge edge = it.next(); for(State sink : edge.getSinks()) { // ... build a source singleton set ... HashSet source = new HashSet(); source.add(edge.getSource()); // ... and add the corresponding multiedge ... - mergeEdge(new MultiEdge(sink, edge.getLabel(), source)); + //mergeEdge(new MultiEdge(sink, edge.getLabel(), source)); + MultiEdge reversedEdge = new MultiEdge(sink, edge.getLabel(), source); + toAdd.add(reversedEdge); } - unmergeEdge(edge); + // Unmerge edge + it.remove(); + //unmergeOutgoingEdge(edge); + //unmergeIncomingEdge(edge); + } + + //for(MultiEdge edge : edges) { + //addEdge(edge); + //} + //Clear unsynchronized edges + outgoingEdges.clear(); + incomingEdges.clear(); + + edges.addAll(toAdd); + for(MultiEdge edge : edges) { + mergeOutgoingEdge(edge); + mergeIncomingEdge(edge); } } @@ -319,10 +343,20 @@ public class NondeterministicFiniteAutomaton extends FiniteAutomaton dfa = new DeterministicFiniteAutomaton(); + //Take over the symbols + dfa.setApList(apList); + // The new initial state is the set of all old initial states State dfaInitState = dfa.newState(initialStates.toString()); dfa.addInitialState(dfaInitState); nfaStates.put(dfaInitState, initialStates); + // The new initial state is accepting iff it contains an old accepting state + for(State initNfaState : initialStates) { + if(isAcceptingState(initNfaState)) { + dfa.addAcceptingState(dfaInitState); + break; + } + } // Now we expand everything we have not seen yet LinkedList toExplore = new LinkedList<>(); @@ -425,7 +459,7 @@ public class NondeterministicFiniteAutomaton extends FiniteAutomaton extends Edge { return result.toString(); } + + @Override + public int hashCode() { + int result = super.hashCode(); + return result ^ sink.hashCode(); + } + + @Override + public boolean equals(Object o) { + if(o instanceof SingleEdge) { + @SuppressWarnings("unchecked") + SingleEdge other = (SingleEdge)o; + return super.equals(other) && + getSink().equals(other.getSink()); + } else { + return false; + } + } }