MEC implementation

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

prism-examples/mec-tests/1.pm

@@ -0,0 +1,9 @@
+mdp
+
+module mec_tests
+
+	s : [0..1] init 0;
+	
+	[] s=0 -> 1.0 : (s'=0) ;
+	
+endmodule

prism-examples/mec-tests/2.pm

@@ -0,0 +1,11 @@
+mdp
+
+module mec_tests
+
+	s : [0..1] init 0;
+	
+	[] s=0 -> 1.0 : (s'=1) ;
+	[] s=1 -> 1.0 : (s'=0) ;
+	
+	
+endmodule

prism-examples/mec-tests/3.pm

@@ -0,0 +1,12 @@
+mdp
+
+module mec_tests
+
+	s : [0..2] init 0;
+	
+	[] s=0 -> 1.0 : (s'=1);
+	[] s=1 -> 1.0 : (s'=0);
+	[] s=0 -> 1.0 : (s'=2);
+	[] s=2 -> 1.0 : (s'=2);
+	
+endmodule

prism-examples/mec-tests/4.pm

@@ -0,0 +1,13 @@
+mdp
+
+module mec_tests
+
+	s : [0..2] init 0;
+	
+	[] s=0 -> 1.0 : (s'=1);
+	[] s=1 -> 1.0 : (s'=0);
+	[] s=0 -> 1.0 : (s'=2);
+	[] s=2 -> 1.0 : (s'=2);
+	[] s=2 -> 1.0 : (s'=1);
+	
+endmodule

prism/src/explicit/ECComputerDefault.java

@@ -31,6 +31,8 @@ import java.util.ArrayList;
 import java.util.BitSet;
 import java.util.List;
 
+import explicit.SCCComputer.SCCMethod;
+
 /**
  * Maximal end component computer for a nondeterministic model such as MDP.
  */
@@ -54,7 +56,17 @@ public class ECComputerDefault extends ECComputer
 	@Override
 	public void computeMECs()
 	{
-		// TODO
+		SCCComputer sccc = SCCComputer.createSCCComputer(SCCMethod.TARJAN, model);
+		sccc.computeSCCs();
+		
+		List<BitSet> sccs = sccc.getSCCs();
+		
+		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));
+			}
+		}
 	}
 
 	@Override
@@ -62,4 +74,24 @@ public class ECComputerDefault extends ECComputer
 	{
 		return mecs;
 	}
+	
+	private boolean isMEC(BitSet b) {
+		if(b.cardinality() == 0) return false;
+		
+		int state = b.nextSetBit(0);
+		while(state != -1) {
+			boolean atLeastOneAction = false;
+			for(int i=0;i<model.getNumChoices(state);i++) {
+				if(model.allSuccessorsInSet(state, i, b)) {
+					atLeastOneAction = true;
+				}
+			}
+			if(!atLeastOneAction) {
+				return false;
+			}
+			state = b.nextSetBit(state+1);
+		}
+		
+		return true;
+	}
 }