From 2bd70172cea7ff8889c6b0fced7d4729799bde18 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 21 Jul 2017 13:13:29 +0000
Subject: [PATCH] explicit.DTMC, refactor: move mvMult, mvMultGS, mvMultRew
 from DTMCExplicit to default methods in DTMC

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12091 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/DTMC.java         | 35 ++++++++++++++++++++++--
 prism/src/explicit/DTMCExplicit.java | 41 ----------------------------
 2 files changed, 32 insertions(+), 44 deletions(-)

diff --git a/prism/src/explicit/DTMC.java b/prism/src/explicit/DTMC.java
index fbaf05d5..603302df 100644
--- a/prism/src/explicit/DTMC.java
+++ b/prism/src/explicit/DTMC.java
@@ -142,7 +142,12 @@ public interface DTMC extends Model
 	 * @param subset Only do multiplication for these rows (ignored if null)
 	 * @param complement If true, {@code subset} is taken to be its complement (ignored if {@code subset} is null)
 	 */
-	public void mvMult(double vect[], double result[], BitSet subset, boolean complement);
+	public default void mvMult(double vect[], double result[], BitSet subset, boolean complement)
+	{
+		for (int s : new IterableStateSet(subset, getNumStates(), complement)) {
+			result[s] = mvMultSingle(s, vect);
+		}
+	}
 
 	/**
 	 * Do a single row of matrix-vector multiplication for
@@ -166,7 +171,26 @@ public interface DTMC extends Model
 	 * @param absolute If true, compute absolute, rather than relative, difference
 	 * @return The maximum difference between old/new elements of {@code vect}
 	 */
-	public double mvMultGS(double vect[], BitSet subset, boolean complement, boolean absolute);
+	public default double mvMultGS(double vect[], BitSet subset, boolean complement, boolean absolute)
+	{
+		double d, diff, maxDiff = 0.0;
+		for (int s : new IterableStateSet(subset, getNumStates(), complement)) {
+			d = mvMultJacSingle(s, vect);
+			diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d);
+			maxDiff = diff > maxDiff ? diff : maxDiff;
+			vect[s] = d;
+		}
+		// Use this code instead for backwards Gauss-Seidel
+		/*for (s = numStates - 1; s >= 0; s--) {
+			if (subset.get(s)) {
+				d = mvMultJacSingle(s, vect);
+				diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d);
+				maxDiff = diff > maxDiff ? diff : maxDiff;
+				vect[s] = d;
+			}
+		}*/
+		return maxDiff;
+	}
 
 	/**
 	 * Do a single row of Jacobi-style matrix-vector multiplication for
@@ -185,7 +209,12 @@ public interface DTMC extends Model
 	 * @param subset Only do multiplication for these rows (ignored if null)
 	 * @param complement If true, {@code subset} is taken to be its complement (ignored if {@code subset} is null)
 	 */
-	public void mvMultRew(double vect[], MCRewards mcRewards, double result[], BitSet subset, boolean complement);
+	public default void mvMultRew(double vect[], MCRewards mcRewards, double result[], BitSet subset, boolean complement)
+	{
+		for (int s : new IterableStateSet(subset, getNumStates(), complement)) {
+			result[s] = mvMultRewSingle(s, vect, mcRewards);
+		}
+	}
 
 	/**
 	 * Do a single row of matrix-vector multiplication and sum of action reward.
diff --git a/prism/src/explicit/DTMCExplicit.java b/prism/src/explicit/DTMCExplicit.java
index 3982e5c5..d5d46d15 100644
--- a/prism/src/explicit/DTMCExplicit.java
+++ b/prism/src/explicit/DTMCExplicit.java
@@ -29,14 +29,11 @@ package explicit;
 import java.io.FileWriter;
 import java.io.IOException;
 import java.util.AbstractMap;
-import java.util.BitSet;
 import java.util.Iterator;
 import java.util.Map;
 import java.util.TreeMap;
 import java.util.Map.Entry;
 
-import common.IterableStateSet;
-import explicit.rewards.MCRewards;
 import prism.ModelType;
 import prism.Pair;
 import prism.PrismException;
@@ -145,44 +142,6 @@ public abstract class DTMCExplicit extends ModelExplicit implements DTMC
 		return new AddDefaultActionToTransitionsIterator(getTransitionsIterator(s), null);
 	}
 
-	@Override
-	public void mvMult(double vect[], double result[], BitSet subset, boolean complement)
-	{
-		for (int s : new IterableStateSet(subset, numStates, complement)) {
-			result[s] = mvMultSingle(s, vect);
-		}
-	}
-
-	@Override
-	public double mvMultGS(double vect[], BitSet subset, boolean complement, boolean absolute)
-	{
-		double d, diff, maxDiff = 0.0;
-		for (int s : new IterableStateSet(subset, numStates, complement)) {
-			d = mvMultJacSingle(s, vect);
-			diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d);
-			maxDiff = diff > maxDiff ? diff : maxDiff;
-			vect[s] = d;
-		}
-		// Use this code instead for backwards Gauss-Seidel
-		/*for (s = numStates - 1; s >= 0; s--) {
-			if (subset.get(s)) {
-				d = mvMultJacSingle(s, vect);
-				diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d);
-				maxDiff = diff > maxDiff ? diff : maxDiff;
-				vect[s] = d;
-			}
-		}*/
-		return maxDiff;
-	}
-
-	@Override
-	public void mvMultRew(double vect[], MCRewards mcRewards, double result[], BitSet subset, boolean complement)
-	{
-		for (int s : new IterableStateSet(subset, numStates, complement)) {
-			result[s] = mvMultRewSingle(s, vect, mcRewards);
-		}
-	}
-
 	public class AddDefaultActionToTransitionsIterator implements Iterator<Map.Entry<Integer, Pair<Double, Object>>>
 	{
 		private Iterator<Entry<Integer, Double>> transIter;