Bugfixes for NFA/DFA-Library

* Reversing NFA: Fixed Iterating issue
* Determinisation: Fixed issue for initial and accepting state in DFA
* Determinisation: Take over APs
* Adding complete-Function for DFAs
* Other minor bugfixes
* Adding minor helper functions

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<Symbol> extends FiniteAutomaton<Symbol,SingleEdge<Symbol>> {
+	
 	@Override
 	public HashSet<State> getSuccessors(State state) {
 		HashSet<State> result = new HashSet<State>();
@@ -51,4 +55,121 @@ public class DeterministicFiniteAutomaton<Symbol> extends FiniteAutomaton<Symbol
 		outgoingEdges.get(source).add(edge);
 		incomingEdges.get(sink).add(edge);
 	}
+
+    public NondeterministicFiniteAutomaton<Symbol> toNFA() {
+        NondeterministicFiniteAutomaton<Symbol> nfa = new NondeterministicFiniteAutomaton<Symbol>();
+        
+        //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<Symbol> edge : edges) {
+            LinkedHashSet<State> sinkSet = new LinkedHashSet<State>();
+            sinkSet.add(edge.getSink());
+            MultiEdge<Symbol> nfaEdge = new MultiEdge<Symbol>(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<Symbol> minimize() {
+    	//reverse
+    	NondeterministicFiniteAutomaton<Symbol> reversed = toNFA();
+    	reversed.reverse();
+    	
+    	//Powerset construction for the reversed automaton
+    	NondeterministicFiniteAutomaton<Symbol> minimalReversedDFA = reversed.determinize().toNFA();
+    	//reverse the reversed DFA
+    	minimalReversedDFA.reverse();
+    	//Powerset construction for the reversed^2 automaton
+    	DeterministicFiniteAutomaton<Symbol> minimized = minimalReversedDFA.determinize();
+    	//Make automaton complete
+    	minimized.complete();
+    	return minimized;
+    }
+    
+    public Set<State> getPredecessors(Set<State> states, EdgeLabel<Symbol> symbol) {
+    	return states.stream()
+    				.map(state -> getPredecessors(state, symbol))
+    				.reduce(
+    						new HashSet<State>(),
+    						(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<Symbol> 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<Symbol> selfLoop = new MultiEdge<>(trap, new EdgeLabel<Symbol>(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<Symbol> label = new EdgeLabel<Symbol>(apList, value);
+				for(State state : states) {
+					if(getSuccessors(state, label).size() == 0) {
+						SingleEdge<Symbol> 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<firstUnsetBit; i++) {
+					value.clear(i);
+				}
+			}
+			
+			// Remove unnecessary trap state
+			if(!edgeToTrapState) {
+				removeState(trap);
+			}
+		}
+	}
 }

prism/src/automata/finite/EdgeLabel.java

@@ -137,6 +137,16 @@ public class EdgeLabel<Symbol> {
 	}
 	
 	public boolean intersects(EdgeLabel<Symbol> other) {
+		if(isTrue() || other.isTrue()) {
+			return true;
+		}
+
+		if(isFalse()) {
+			if(other.isFalse()) {
+				return true;
+			}
+		}
+		
 		ArrayList<Symbol> relevantSymbols = relevantSymbols();
 		relevantSymbols.retainAll(other.relevantSymbols());
 		
@@ -164,4 +174,34 @@ public class EdgeLabel<Symbol> {
 		}
 		return result.toString();
 	}
+	
+	@Override
+	public boolean equals(Object o) {
+		if(o instanceof EdgeLabel<?>) {
+			@SuppressWarnings("unchecked")
+			EdgeLabel<Symbol> other = (EdgeLabel<Symbol>)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();
+	}
 }

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<Symbol, E extends Edge<Symbol>> {
@@ -195,12 +196,53 @@ public abstract class FiniteAutomaton<Symbol, E extends Edge<Symbol>> {
 	
 	public HashSet<State> getPredecessors(State state) {
 		HashSet<State> result = new HashSet<State>();
+
+		if(!incomingEdges.containsKey(state)) {
+			incomingEdges.put(state, new HashSet<>());
+		}
+
 		for(Edge<Symbol> 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<State> getPredecessors(State state, EdgeLabel<Symbol> label) {
+		Set<State> result = new HashSet<State>();
+		for(Edge<Symbol> 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<State> getPredecssors(Set<State> states, EdgeLabel<Symbol> label) {
+		Set<State> result = new HashSet<State>();
+		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<State> getSuccessors(HashSet<State> states) {
 		HashSet<State> result = new HashSet<State>();
 		for(State state : states) {
@@ -216,7 +258,7 @@ public abstract class FiniteAutomaton<Symbol, E extends Edge<Symbol>> {
 		}
 		return result;
 	}
-	
+
 	public HashSet<State> getPredecessors(HashSet<State> states) {
 		HashSet<State> result = new HashSet<State>();
 		for(State state : states) {
@@ -302,6 +344,29 @@ public abstract class FiniteAutomaton<Symbol, E extends Edge<Symbol>> {
 		return longestSuccLength+1;
 	}
 	
+	public Set<EdgeLabel<Symbol>> getIncomingEdgeLabels(State state) {
+		Set<EdgeLabel<Symbol>> result = new HashSet<EdgeLabel<Symbol>>();
+		for(Edge<Symbol> edge : getIncomingEdges(state)) {
+			result.add(edge.getLabel());
+		}
+		return result;
+	}
+	
+	public Set<EdgeLabel<Symbol>> getIncomingEdgeLabels(Set<State> states) {
+		Set<EdgeLabel<Symbol>> result = new HashSet<EdgeLabel<Symbol>>();
+		for(State state : states) {
+			result.addAll(getIncomingEdgeLabels(state));
+		}
+		return result;
+	}
+
+	public Set<EdgeLabel<Symbol>> getOutgoingEdgeLabels(State state) {
+		Set<EdgeLabel<Symbol>> result = new HashSet<EdgeLabel<Symbol>>();
+		for(Edge<Symbol> 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

prism/src/automata/finite/MultiEdge.java

@@ -58,4 +58,21 @@ public class MultiEdge<Symbol> extends Edge<Symbol> {
 		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<Symbol> other = (MultiEdge<Symbol>)o;
+			return super.equals(other) &&
+					getSinks().equals(other.getSinks());
+		} else {
+			return false;
+		}
+	}
 }

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<Symbol> extends FiniteAutomaton<Sym
 	@Override
 	public HashSet<State> getSuccessors(State state) {
 		HashSet<State> result = new HashSet<State>();
+		if(!outgoingEdges.containsKey(state)) {
+			outgoingEdges.put(state, new HashSet<MultiEdge<Symbol>>());
+		}
 		for(MultiEdge<Symbol> edge : outgoingEdges.get(state)) {
 			result.addAll(edge.getSinks());
 		}
@@ -297,16 +300,37 @@ public class NondeterministicFiniteAutomaton<Symbol> extends FiniteAutomaton<Sym
 		setInitialStates(oldAccepting);
 		
 		// Build reversed edges
-		for(MultiEdge<Symbol> edge : edges) {
-			// For each sink ...
+		Iterator<MultiEdge<Symbol>> it = edges.iterator();
+		Set<MultiEdge<Symbol>> toAdd = new HashSet<MultiEdge<Symbol>>();
+		while(it.hasNext()) {
+			//For each sink ...
+			MultiEdge<Symbol> edge = it.next();
 			for(State sink : edge.getSinks()) {
 				// ... build a source singleton set ...
 				HashSet<State> source = new HashSet<State>();
 				source.add(edge.getSource());
 				// ... and add the corresponding multiedge ...
-				mergeEdge(new MultiEdge<Symbol>(sink, edge.getLabel(), source));
+				//mergeEdge(new MultiEdge<Symbol>(sink, edge.getLabel(), source));
+				MultiEdge<Symbol> reversedEdge = new MultiEdge<Symbol>(sink, edge.getLabel(), source);
+				toAdd.add(reversedEdge);
 			}
-			unmergeEdge(edge);
+			// Unmerge edge
+			it.remove();
+			//unmergeOutgoingEdge(edge);
+			//unmergeIncomingEdge(edge);
+		}
+		
+		//for(MultiEdge<Symbol> edge : edges) {
+			//addEdge(edge);
+		//}
+		//Clear unsynchronized edges
+		outgoingEdges.clear();
+		incomingEdges.clear();
+
+		edges.addAll(toAdd);
+		for(MultiEdge<Symbol> edge : edges) {
+				mergeOutgoingEdge(edge);
+				mergeIncomingEdge(edge);
 		}
 	}
 	
@@ -319,10 +343,20 @@ public class NondeterministicFiniteAutomaton<Symbol> extends FiniteAutomaton<Sym
 		
 		DeterministicFiniteAutomaton<Symbol> dfa = new DeterministicFiniteAutomaton<Symbol>();
 		
+		//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<State> toExplore = new LinkedList<>();
@@ -425,7 +459,7 @@ public class NondeterministicFiniteAutomaton<Symbol> extends FiniteAutomaton<Sym
     		
     		if (isAcceptingState(state)) { color = "red"; }
     		if (isInitialState(state)) { color = "blue"; }
-    		if (isAcceptingState(state) && isInitialState(state)) { color = "violett"; }
+    		if (isAcceptingState(state) && isInitialState(state)) { color = "violet"; }
     		
     		result.append(state
     				+ "[shape=box, color=" + color + ","

prism/src/automata/finite/SingleEdge.java

@@ -43,4 +43,22 @@ public class SingleEdge<Symbol> extends Edge<Symbol> {
 		
 		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<Symbol> other = (SingleEdge<Symbol>)o;
+			return super.equals(other) &&
+					getSink().equals(other.getSink());
+		} else {
+			return false;
+		}
+	}
 }