From e5d4d3dc3d07780095cabda26b8777bd429637c6 Mon Sep 17 00:00:00 2001
From: Mateusz Ujma <mateusz.ujma@cs.ox.ac.uk>
Date: Tue, 16 Jul 2013 23:45:52 +0000
Subject: [PATCH] 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             |  9 ++++++
 prism-examples/mec-tests/2.pm             | 11 ++++++++
 prism-examples/mec-tests/3.pm             | 12 ++++++++
 prism-examples/mec-tests/4.pm             | 13 +++++++++
 prism/src/explicit/ECComputerDefault.java | 34 ++++++++++++++++++++++-
 5 files changed, 78 insertions(+), 1 deletion(-)
 create mode 100644 prism-examples/mec-tests/1.pm
 create mode 100644 prism-examples/mec-tests/2.pm
 create mode 100644 prism-examples/mec-tests/3.pm
 create mode 100644 prism-examples/mec-tests/4.pm

diff --git a/prism-examples/mec-tests/1.pm b/prism-examples/mec-tests/1.pm
new file mode 100644
index 00000000..55c1b431
--- /dev/null
+++ b/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
diff --git a/prism-examples/mec-tests/2.pm b/prism-examples/mec-tests/2.pm
new file mode 100644
index 00000000..cc273835
--- /dev/null
+++ b/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
diff --git a/prism-examples/mec-tests/3.pm b/prism-examples/mec-tests/3.pm
new file mode 100644
index 00000000..bebf016b
--- /dev/null
+++ b/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
diff --git a/prism-examples/mec-tests/4.pm b/prism-examples/mec-tests/4.pm
new file mode 100644
index 00000000..101f840e
--- /dev/null
+++ b/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
diff --git a/prism/src/explicit/ECComputerDefault.java b/prism/src/explicit/ECComputerDefault.java
index f73c8efa..324dbf16 100644
--- a/prism/src/explicit/ECComputerDefault.java
+++ b/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;
+	}
 }