Add basic prism.StateVector interface, supported by various types of state vector.

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

prism/src/prism/StateValues.java

@@ -34,7 +34,7 @@ import parser.ast.RelOp;
 
 // Interface for classes for state-indexed vectors of (integer or double) values
 
-public interface StateValues
+public interface StateValues extends StateVector
 {
 	StateValuesDV convertToStateValuesDV();
 	StateValuesMTBDD convertToStateValuesMTBDD();
@@ -55,6 +55,7 @@ public interface StateValues
 	double sumOverBDD(JDDNode filter);
 	double sumOverMTBDD(JDDNode mult);
 	StateValues sumOverDDVars(JDDVars sumVars, Model newModel) throws PrismException;
+	Object getValue(int i);
 	JDDNode getBDDFromInterval(String relOpString, double bound);
 	JDDNode getBDDFromInterval(RelOp relOp, double bound);
 	JDDNode getBDDFromInterval(double lo, double hi);

prism/src/prism/StateValuesDV.java

@@ -224,6 +224,19 @@ public class StateValuesDV implements StateValues
 
 	// METHODS TO ACCESS VECTOR DATA
 
+	@Override
+	public int getSize()
+	{
+		return values.getSize();
+	}
+	
+	@Override
+	public Object getValue(int i)
+	{
+		// TODO: cast to Integer or Double as required?
+		return values.getElement(i);
+	}
+	
 	// get vector
 
 	public DoubleVector getDoubleVector()

prism/src/prism/StateValuesMTBDD.java

@@ -246,6 +246,32 @@ public class StateValuesMTBDD implements StateValues
 
 	// METHODS TO ACCESS VECTOR DATA
 	
+	@Override
+	public int getSize()
+	{
+		return (int) model.getNumStates();
+	}
+	
+	@Override
+	public Object getValue(int i)
+	{
+		JDDNode dd = values;
+		ODDNode ptr = odd;
+		int o = 0;
+		for (int k = 0; k < numVars; k++) {
+			if (ptr.getEOff() > i - o) {
+				dd = dd.getIndex() > vars.getVarIndex(k) ? dd : dd.getElse();
+				ptr = ptr.getElse();
+			} else {
+				dd = dd.getIndex() > vars.getVarIndex(k) ? dd : dd.getThen();
+				o += ptr.getEOff();
+				ptr = ptr.getThen();
+			}
+		}
+		// TODO: cast to Integer or Double as required?
+		return dd.getValue();
+	}
+	
 	// get mtbdd
 	
 	public JDDNode getJDDNode()

prism/src/prism/StateValuesVoid.java

@@ -45,6 +45,18 @@ public class StateValuesVoid implements StateValues
 		this.value = value;
 	}
 	
+	@Override
+	public int getSize()
+	{
+		return 1;
+	}
+
+	@Override
+	public Object getValue(int i)
+	{
+		return value;
+	}
+
 	public Object getValue()
 	{
 		return value;

prism/src/prism/StateVector.java

@@ -0,0 +1,43 @@
+//==============================================================================
+//	
+//	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 prism;
+
+/**
+ * Interface for classes supporting read-access to state-indexed vectors of values. 
+ */
+public interface StateVector
+{
+	/**
+	 * Return the size of the vector (i.e. the number of elements).
+	 */
+	public int getSize();
+
+	/**
+	 * Get the value of the ith element of the vector, as an Object.
+	 */
+	public Object getValue(int i);
+}