From 1b5dc955e6e91c341bc2fb377684d70bc22d53c2 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 31 Aug 2012 09:18:43 +0000
Subject: [PATCH] Few extra methods in StateValues.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5622 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/StateValues.java | 80 +++++++++++++++++++++++++++++
 1 file changed, 80 insertions(+)

diff --git a/prism/src/explicit/StateValues.java b/prism/src/explicit/StateValues.java
index 7fe52326..6be220c4 100644
--- a/prism/src/explicit/StateValues.java
+++ b/prism/src/explicit/StateValues.java
@@ -707,6 +707,46 @@ public class StateValues
 		}
 	}
 
+	/**
+	 * Modify the vector by applying 'plus' with a constant.
+	 */
+	public void plusConstant(int val) throws PrismException
+	{
+		if (type instanceof TypeInt) {
+			for (int i = 0; i < size; i++) {
+				valuesI[i] += val;
+			}
+		} else if (type instanceof TypeDouble) {
+			for (int i = 0; i < size; i++) {
+				valuesD[i] += val;
+			}
+		} else {
+			throw new PrismException("Operator + can not be applied to Boolean vectors");
+		}
+	}
+
+	/**
+	 * Modify the vector by applying 'plus' with a constant.
+	 */
+	public void plusConstant(double val) throws PrismException
+	{
+		if (type instanceof TypeInt) {
+			// Change type
+			valuesD = new double[size];
+			type = TypeDouble.getInstance();
+			for (int i = 0; i < size; i++) {
+				valuesD[i] = valuesI[i] + val;
+			}
+			valuesI = null;
+		} else if (type instanceof TypeDouble) {
+			for (int i = 0; i < size; i++) {
+				valuesD[i] += val;
+			}
+		} else {
+			throw new PrismException("Operator + can not be applied to Boolean vectors");
+		}
+	}
+
 	/**
 	 * Modify the vector by applying 'minus' with operand {@code sv}.
 	 */
@@ -781,6 +821,46 @@ public class StateValues
 		}
 	}
 
+	/**
+	 * Modify the vector by applying 'times' with a constant.
+	 */
+	public void timesConstant(int val) throws PrismException
+	{
+		if (type instanceof TypeInt) {
+			for (int i = 0; i < size; i++) {
+				valuesI[i] *= val;
+			}
+		} else if (type instanceof TypeDouble) {
+			for (int i = 0; i < size; i++) {
+				valuesD[i] *= val;
+			}
+		} else {
+			throw new PrismException("Operator + can not be applied to Boolean vectors");
+		}
+	}
+
+	/**
+	 * Modify the vector by applying 'times' with a constant.
+	 */
+	public void timesConstant(double val) throws PrismException
+	{
+		if (type instanceof TypeInt) {
+			// Change type
+			valuesD = new double[size];
+			type = TypeDouble.getInstance();
+			for (int i = 0; i < size; i++) {
+				valuesD[i] = valuesI[i] * val;
+			}
+			valuesI = null;
+		} else if (type instanceof TypeDouble) {
+			for (int i = 0; i < size; i++) {
+				valuesD[i] *= val;
+			}
+		} else {
+			throw new PrismException("Operator + can not be applied to Boolean vectors");
+		}
+	}
+
 	/**
 	 * Modify the vector by applying 'divide' with operand {@code sv}.
 	 */