Added StateStorage interface

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

prism/src/explicit/ConstructModel.java

@@ -125,7 +125,7 @@ public class ConstructModel
 		// Model info
 		ModelType modelType;
 		// State storage
-		IndexedSet<State> states;
+		StateStorage<State> states;
 		LinkedList<State> explore;
 		State state, stateNew;
 		// Explicit model storage

prism/src/explicit/IndexedSet.java

@@ -28,13 +28,11 @@ package explicit;
 
 import java.util.*;
 
-import parser.State;
-
 /**
  * Class storing an indexed set of objects of type T.
  * Typically used for storing state space during reachability.
  */
-public class IndexedSet<T>
+public class IndexedSet<T> implements StateStorage<T>
 {
 	private Map<T, Integer> set;
 	private int indexOfLastAdd;
@@ -50,11 +48,13 @@ public class IndexedSet<T>
 		indexOfLastAdd = -1;
 	}
 
+	@Override
 	public void clear()
 	{
 		set.clear();
 	}
 	
+	@Override
 	public boolean add(T state)
 	{
 		Integer i = set.get(state);
@@ -68,16 +68,19 @@ public class IndexedSet<T>
 		}
 	}
 
+	@Override
 	public boolean contains(T state)
 	{
 			return set.get(state) != null;
 	}
 
+	@Override
 	public int getIndexOfLastAdd()
 	{
 		return indexOfLastAdd;
 	}
 
+	@Override
 	public boolean isEmpty()
 	{
 		return set.isEmpty();
@@ -86,6 +89,7 @@ public class IndexedSet<T>
 	/**
 	 * Get the number of objects stored in the set.
 	 */
+	@Override
 	public int size()
 	{
 		return set.size();
@@ -94,6 +98,7 @@ public class IndexedSet<T>
 	/**
 	 * Get access to the underlying set of map entries. 
 	 */
+	@Override
 	public Set<Map.Entry<T, Integer>> getEntrySet()
 	{
 		return set.entrySet();
@@ -102,6 +107,7 @@ public class IndexedSet<T>
 	/**
 	 * Create an ArrayList of the states, ordered by index.
 	 */
+	@Override
 	public ArrayList<T> toArrayList()
 	{
 		ArrayList<T> list = new ArrayList<T>(set.size());
@@ -113,6 +119,7 @@ public class IndexedSet<T>
 	 * Create an ArrayList of the states, ordered by index, storing in the passed in list.
 	 * @param list An empty ArrayList in which to store the result.
 	 */
+	@Override
 	public void toArrayList(ArrayList<T> list)
 	{
 		int i, n;
@@ -130,6 +137,7 @@ public class IndexedSet<T>
 	 * Index in new list is permut[old_index].
 	 * @param permut Permutation to apply
 	 */
+	@Override
 	public ArrayList<T> toPermutedArrayList(int permut[])
 	{
 		ArrayList<T> list = new ArrayList<T>(set.size());
@@ -143,6 +151,7 @@ public class IndexedSet<T>
 	 * @param permut Permutation to apply
 	 * @param list An empty ArrayList in which to store the result.
 	 */
+	@Override
 	public void toPermutedArrayList(int permut[], ArrayList<T> list)
 	{
 		int i, n;
@@ -160,6 +169,7 @@ public class IndexedSet<T>
 	 * this returns a permutation (integer array) mapping current indices
 	 * to new indices under the sorting order.
 	 */
+	@Override
 	public int[] buildSortingPermutation()
 	{
 		int i, n;
@@ -181,6 +191,7 @@ public class IndexedSet<T>
 		return set.toString();
 	}
 
+	@Override
 	public int get(T t)
 	{
 		return set.get(t);

prism/src/explicit/StateStorage.java

@@ -0,0 +1,94 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of 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.*;
+
+/**
+ * Interface for storing an set of objects of type T.
+ * Typically used for storing state space during reachability.
+ */
+public interface StateStorage<T>
+{
+	public int get(T t);
+	
+	public boolean add(T state);
+	
+	public void clear();
+
+	public boolean contains(T state);
+
+	public int getIndexOfLastAdd();
+
+	public boolean isEmpty();
+
+	/**
+	 * Get the number of objects stored in the set.
+	 */
+	public int size();
+
+	/**
+	 * Get access to the underlying set of map entries. 
+	 */
+	public Set<Map.Entry<T, Integer>> getEntrySet();
+	
+	/**
+	 * Create an ArrayList of the states, ordered by index.
+	 */
+	public ArrayList<T> toArrayList();
+
+	/**
+	 * Create an ArrayList of the states, ordered by index, storing in the passed in list.
+	 * @param list An empty ArrayList in which to store the result.
+	 */
+	public void toArrayList(ArrayList<T> list);
+	
+	/**
+	 * Create an ArrayList of the states, ordered by permuted index.
+	 * Index in new list is permut[old_index].
+	 * @param permut Permutation to apply
+	 */
+	public ArrayList<T> toPermutedArrayList(int permut[]);
+
+	/**
+	 * Create an ArrayList of the states, ordered by permuted index, storing in the passed in list.
+	 * Index in new list is permut[old_index].
+	 * @param permut Permutation to apply
+	 * @param list An empty ArrayList in which to store the result.
+	 */
+	public void toPermutedArrayList(int permut[], ArrayList<T> list);
+	
+	/**
+	 * Build sort permutation. Assuming this was built as a sorted set,
+	 * this returns a permutation (integer array) mapping current indices
+	 * to new indices under the sorting order.
+	 */
+	public int[] buildSortingPermutation();
+	
+}

prism/src/param/ModelBuilder.java

@@ -41,6 +41,7 @@ import prism.PrismException;
 import prism.PrismLog;
 import prism.PrismSettings;
 import explicit.IndexedSet;
+import explicit.StateStorage;
 
 /**
  * Class to construct a parametric Markov model.
@@ -233,7 +234,7 @@ public final class ModelBuilder {
 	 * @param states list of states to be filled by this method
 	 * @throws PrismException thrown if problems in underlying methods occur
 	 */
-	private void reserveMemoryAndExploreStates(ModulesFile modulesFile, ParamModel model, ModelType modelType, SymbolicEngine engine, IndexedSet<State> states)
+	private void reserveMemoryAndExploreStates(ModulesFile modulesFile, ParamModel model, ModelType modelType, SymbolicEngine engine, StateStorage<State> states)
 	throws PrismException
 	{
 		boolean isNonDet = modelType == ModelType.MDP;
@@ -311,7 +312,7 @@ public final class ModelBuilder {
 		}
 
 		boolean isNonDet = modelType == ModelType.MDP;
-		IndexedSet<State> states = new IndexedSet<State>(true);
+		StateStorage<State> states = new IndexedSet<State>(true);
 		reserveMemoryAndExploreStates(modulesFile, model, modelType, engine, states);
 		int[] permut = states.buildSortingPermutation();
 		List<State> statesList = states.toPermutedArrayList(permut);

prism/src/pta/ForwardsReach.java

@@ -89,7 +89,7 @@ public class ForwardsReach
 	{
 		LocZone init, lz, lz2;
 		LinkedList<LocZone> X;
-		IndexedSet<LocZone> Yset;
+		StateStorage<LocZone> Yset;
 		//LocZoneSetOld Zset;
 		ReachabilityGraph graph;
 		int src, dest, count, dests[];
@@ -272,7 +272,7 @@ public class ForwardsReach
 		Zone z;
 		LocZone init, lz, lz2;
 		LinkedList<LocZone> Y;
-		IndexedSet<LocZone> Zset;
+		StateStorage<LocZone> Zset;
 		//LocZoneSetOld Zset;
 		ReachabilityGraph graph;
 		int cMax;

prism/src/pta/Modules2PTA.java

@@ -29,6 +29,7 @@ package pta;
 import java.util.*;
 
 import explicit.IndexedSet;
+import explicit.StateStorage;
 
 import parser.*;
 import parser.ast.*;
@@ -504,7 +505,7 @@ public class Modules2PTA extends PrismComponent
 		int numUpdates, numCommands, numElements;
 		// Stuff needed to do local reachability search
 		int src, dest;
-		IndexedSet<State> states;
+		StateStorage<State> states;
 		LinkedList<State> explore;
 		State state, stateNew;
 		int[] varMap;

prism/src/pta/PTAParallel.java

@@ -30,6 +30,7 @@ import java.util.*;
 
 import prism.PrismException;
 import explicit.IndexedSet;
+import explicit.StateStorage;
 
 /**
  * Class to perform the parallel composition of PTAs.
@@ -37,7 +38,7 @@ import explicit.IndexedSet;
 public class PTAParallel
 {
 	// All states
-	private IndexedSet<IndexPair> states;
+	private StateStorage<IndexPair> states;
 	// States to be explored
 	private LinkedList<IndexPair> explore;
 	// Component PTAs