Fixed bugs in MEC computation

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7109 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/ECComputerDefault.java

@@ -29,7 +29,11 @@ package explicit;
 
 import java.util.ArrayList;
 import java.util.BitSet;
+import java.util.HashMap;
+import java.util.HashSet;
 import java.util.List;
+import java.util.Map;
+import java.util.Set;
 
 import explicit.SCCComputer.SCCMethod;
 
@@ -52,21 +56,104 @@ public class ECComputerDefault extends ECComputer
 	}
 
 	// Methods for SCCComputer interface
+	// Algorithm based on the one found in Luca de Alfaro Ph.D Thesis
 
 	@Override
 	public void computeMECs()
 	{
+		SubNondetModel submodel = null;
+		List<BitSet> L = new ArrayList<BitSet>();
+		
+		BitSet initialModel = new BitSet();
+		initialModel.set(0, model.getNumStates());
+		L.add(initialModel);
+		
+		boolean changed = true;
+		while(changed) {
+			changed = false;
+			BitSet E = L.remove(0);
+			submodel = restrict(model, E);
+			List<BitSet> sccs = translateStates(submodel, computeSCCs(submodel));
+			L = replaceEWithSCCs(L, E, sccs);
+			changed = canLBeChanged(L,E);
+		}
+		mecs = L;
+	}
+	
+	private Set<BitSet> processedSCCs = new HashSet<BitSet>();
+	
+	private boolean canLBeChanged(List<BitSet> L, BitSet E) {
+		processedSCCs.add(E);
+		for(int i=0;i<L.size();i++) {
+			if(!processedSCCs.contains(L.get(i))) {
+				return true;
+			}
+		} 
+		return false;
+	}
+	
+	private List<BitSet> replaceEWithSCCs(List<BitSet> L, BitSet E, List<BitSet> sccs) {
+		if(sccs.size() > 0) {
+			List<BitSet> toAdd = new ArrayList<BitSet>();
+			for(int i=0;i<sccs.size();i++) {
+				if(!L.contains(sccs.get(i))) {
+					toAdd.add(sccs.get(i));
+				}
+			}
+			if(toAdd.size() > 0) {
+				L.addAll(toAdd);
+			}
+		}
+		return L;
+	}
+	
+	private SubNondetModel restrict(NondetModel model, BitSet states) {
+		Map<Integer,BitSet> actions = new HashMap<Integer,BitSet>();
+		BitSet initialStates = new BitSet();
+		initialStates.set(states.nextSetBit(0));
+		
+		boolean changed = true;
+		while(changed) {
+			changed = false;
+			actions.clear();
+			for(int i=0;i<model.getNumStates();i++) {
+				BitSet act = new BitSet();
+				if(states.get(i)) {
+					for(int j=0;j<model.getNumChoices(i);j++) {
+						if(model.allSuccessorsInSet(i, j, states)) {
+							act.set(j);
+						}
+					}
+					if(act.cardinality() == 0) {
+						states.clear(i);
+						changed = true;
+					} 
+					actions.put(i,act);
+				}
+			}
+		}
+		
+		return new SubNondetModel(model, states, actions, initialStates);
+	}
+	
+	private List<BitSet> computeSCCs(NondetModel model) {
 		SCCComputer sccc = SCCComputer.createSCCComputer(SCCMethod.TARJAN, model);
 		sccc.computeSCCs();
+		return sccc.getSCCs();
+	}
 	
-		List<BitSet> sccs = sccc.getSCCs();
-		
+	private List<BitSet> translateStates(SubNondetModel model, List<BitSet> sccs) {
+		List<BitSet> r = new ArrayList<BitSet>();
 		for(int i=0;i<sccs.size();i++) {
-			if(isMEC(sccs.get(i))) {
-				System.out.println("SCCs " + sccs.get(i));
-				mecs.add(sccs.get(i));
+			BitSet set = sccs.get(i);
+			BitSet set2 = new BitSet();
+			r.add(set2);
+			for(int j=set.nextSetBit(0); j>=0; j=set.nextSetBit(j+1)) { 
+				set2.set(model.translateState(j));
+				
 			}
 		}
+		return r;
 	}
 	
 	@Override