diff --git a/prism/src/prism/StateValues.java b/prism/src/prism/StateValues.java index a0024f42..717f160a 100644 --- a/prism/src/prism/StateValues.java +++ b/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); diff --git a/prism/src/prism/StateValuesDV.java b/prism/src/prism/StateValuesDV.java index fe11ab18..87c075b0 100644 --- a/prism/src/prism/StateValuesDV.java +++ b/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() diff --git a/prism/src/prism/StateValuesMTBDD.java b/prism/src/prism/StateValuesMTBDD.java index 38d8eb86..9fe9fe1c 100644 --- a/prism/src/prism/StateValuesMTBDD.java +++ b/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() diff --git a/prism/src/prism/StateValuesVoid.java b/prism/src/prism/StateValuesVoid.java index 796c93c0..a9ebe9da 100644 --- a/prism/src/prism/StateValuesVoid.java +++ b/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; diff --git a/prism/src/prism/StateVector.java b/prism/src/prism/StateVector.java new file mode 100644 index 00000000..30386584 --- /dev/null +++ b/prism/src/prism/StateVector.java @@ -0,0 +1,43 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (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); +}