From 64cb80aa7e4426c506368d2551e388eb9ecad3d2 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 16 Jul 2013 11:58:28 +0000
Subject: [PATCH] Interface and stub for EC computation in explicit engine.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7047 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/ECComputer.java        | 55 +++++++++++++++++++
 prism/src/explicit/ECComputerDefault.java | 65 +++++++++++++++++++++++
 2 files changed, 120 insertions(+)
 create mode 100644 prism/src/explicit/ECComputer.java
 create mode 100644 prism/src/explicit/ECComputerDefault.java

diff --git a/prism/src/explicit/ECComputer.java b/prism/src/explicit/ECComputer.java
new file mode 100644
index 00000000..6acffa0c
--- /dev/null
+++ b/prism/src/explicit/ECComputer.java
@@ -0,0 +1,55 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package explicit;
+
+import java.util.BitSet;
+import java.util.List;
+
+/**
+ * Abstract class for classes that compute (M)ECs, i.e. (maximal) end components,
+ * for a nondeterministic model such as an MDP.
+ */
+public abstract class ECComputer
+{
+	/**
+	 * Static method to create a new ECComputer object.
+	 */
+	public static ECComputer createSCCComputer(NondetModel model)
+	{
+		return new ECComputerDefault(model);
+	}
+
+	/**
+	 * Compute MECs and store them. They can be retrieved using {@link #getMECs()}.
+	 */
+	public abstract void computeMECs();
+
+	/**
+	 * Get the list of computed MECs.
+	 */
+	public abstract List<BitSet> getMECs();
+}
diff --git a/prism/src/explicit/ECComputerDefault.java b/prism/src/explicit/ECComputerDefault.java
new file mode 100644
index 00000000..f73c8efa
--- /dev/null
+++ b/prism/src/explicit/ECComputerDefault.java
@@ -0,0 +1,65 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	* Mateusz Ujma <mateusz.ujma@cs.ox.ac.uk> (University of Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package explicit;
+
+import java.util.ArrayList;
+import java.util.BitSet;
+import java.util.List;
+
+/**
+ * Maximal end component computer for a nondeterministic model such as MDP.
+ */
+public class ECComputerDefault extends ECComputer
+{
+	/* The model to compute (M)ECs for */
+	private NondetModel model;
+	/* Computed list of MECs */
+	private List<BitSet> mecs = new ArrayList<BitSet>();
+
+	/**
+	 * Build (M)EC computer for a given model.
+	 */
+	public ECComputerDefault(NondetModel model)
+	{
+		this.model = model;
+	}
+
+	// Methods for SCCComputer interface
+
+	@Override
+	public void computeMECs()
+	{
+		// TODO
+	}
+
+	@Override
+	public List<BitSet> getMECs()
+	{
+		return mecs;
+	}
+}