Instantaenous rewards for DTMCs/MDPs (MTBDD engine only).

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

prism/include/PrismMTBDD.h

@@ -175,6 +175,14 @@ JNIEXPORT jlong JNICALL Java_mtbdd_PrismMTBDD_PM_1ProbUntil
 JNIEXPORT jlong JNICALL Java_mtbdd_PrismMTBDD_PM_1ProbCumulReward
   (JNIEnv *, jclass, jlong, jlong, jlong, jlong, jlong, jint, jlong, jint, jint);
 
+/*
+ * Class:     mtbdd_PrismMTBDD
+ * Method:    PM_ProbInstReward
+ * Signature: (JJJJIJII)J
+ */
+JNIEXPORT jlong JNICALL Java_mtbdd_PrismMTBDD_PM_1ProbInstReward
+  (JNIEnv *, jclass, jlong, jlong, jlong, jlong, jint, jlong, jint, jint);
+
 /*
  * Class:     mtbdd_PrismMTBDD
  * Method:    PM_ProbReachReward
@@ -199,6 +207,14 @@ JNIEXPORT jlong JNICALL Java_mtbdd_PrismMTBDD_PM_1NondetBoundedUntil
 JNIEXPORT jlong JNICALL Java_mtbdd_PrismMTBDD_PM_1NondetUntil
   (JNIEnv *, jclass, jlong, jlong, jlong, jlong, jint, jlong, jint, jlong, jint, jlong, jlong, jboolean);
 
+/*
+ * Class:     mtbdd_PrismMTBDD
+ * Method:    PM_NondetInstReward
+ * Signature: (JJJJJIJIJIIZ)J
+ */
+JNIEXPORT jlong JNICALL Java_mtbdd_PrismMTBDD_PM_1NondetInstReward
+  (JNIEnv *, jclass, jlong, jlong, jlong, jlong, jlong, jint, jlong, jint, jlong, jint, jint, jboolean);
+
 /*
  * Class:     mtbdd_PrismMTBDD
  * Method:    PM_NondetReachReward

prism/src/mtbdd/PM_NondetInstReward.cc

@@ -0,0 +1,140 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <dxp@cs.bham.uc.uk> (University of Birmingham)
+//	
+//------------------------------------------------------------------------------
+//	
+//	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
+//	
+//==============================================================================
+
+// includes
+#include "PrismMTBDD.h"
+#include <math.h>
+#include <util.h>
+#include <cudd.h>
+#include <dd.h>
+#include <odd.h>
+#include "PrismMTBDDGlob.h"
+#include "jnipointer.h"
+
+//------------------------------------------------------------------------------
+
+JNIEXPORT jlong __pointer JNICALL Java_mtbdd_PrismMTBDD_PM_1NondetInstReward
+(
+JNIEnv *env,
+jclass cls,
+jlong __pointer t,	// trans matrix
+jlong __pointer sr,	// state rewards
+jlong __pointer od,	// odd
+jlong __pointer ndm,	// nondeterminism mask
+jlong __pointer rv,	// row vars
+jint num_rvars,
+jlong __pointer cv,	// col vars
+jint num_cvars,
+jlong __pointer ndv,	// nondet vars
+jint num_ndvars,
+jint bound,			// time bound
+jboolean min		// min or max probabilities (true = min, false = max)
+)
+{
+	// cast function parameters
+	DdNode *trans = jlong_to_DdNode(t);		// trans matrix
+	DdNode *state_rewards = jlong_to_DdNode(sr);	// state rewards
+	ODDNode *odd = jlong_to_ODDNode(od);		// odd
+	DdNode *mask = jlong_to_DdNode(ndm);		// nondeterminism mask
+	DdNode **rvars = jlong_to_DdNode_array(rv);	// row vars
+	DdNode **cvars = jlong_to_DdNode_array(cv);	// col vars
+	DdNode **ndvars = jlong_to_DdNode_array(ndv);	// nondet vars
+
+	// mtbdds
+	DdNode *new_mask, *sol, *tmp;
+	// timing stuff
+	long start1, start2, start3, stop;
+	double time_taken, time_for_setup, time_for_iters;
+	// misc
+	int iters, i;
+	
+	// start clocks
+	start1 = start2 = util_cpu_time();
+	
+	// need to change mask because rewards are not necessarily in the range 0..1
+	Cudd_Ref(mask);
+	new_mask = DD_ITE(ddman, mask, DD_PlusInfinity(ddman), DD_Constant(ddman, 0));
+	
+	// initial solution is the state rewards
+	Cudd_Ref(state_rewards);
+	sol = state_rewards;
+	
+	// get setup time
+	stop = util_cpu_time();
+	time_for_setup = (double)(stop - start2)/1000;
+	start2 = stop;
+	
+	// start iterations
+	iters = 0;
+	PM_PrintToMainLog(env, "\nStarting iterations...\n");
+	
+	// note that we ignore max_iters as we know how any iterations _should_ be performed
+	for (iters = 0; iters < bound; iters++) {
+		
+//		PM_PrintToMainLog(env, "Iteration %d: ", iters);
+//		start3 = util_cpu_time();
+		
+		// matrix-vector multiply
+		Cudd_Ref(sol);
+		tmp = DD_PermuteVariables(ddman, sol, rvars, cvars, num_rvars);
+		Cudd_Ref(trans);
+		tmp = DD_MatrixMultiply(ddman, trans, tmp, cvars, num_cvars, MM_BOULDER);
+		
+		// do min/max
+		if (min) {
+			// mask stuff
+			Cudd_Ref(new_mask);
+			tmp = DD_Apply(ddman, APPLY_MAX, tmp, new_mask);
+			// abstract
+			tmp = DD_MinAbstract(ddman, tmp, ndvars, num_ndvars);
+		}
+		else {
+			// abstract
+			tmp = DD_MaxAbstract(ddman, tmp, ndvars, num_ndvars);
+		}
+		
+		// prepare for next iteration
+		Cudd_RecursiveDeref(ddman, sol);
+		sol = tmp;
+		
+//		PM_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters);
+	}
+	
+	// stop clocks
+	stop = util_cpu_time();
+	time_for_iters = (double)(stop - start2)/1000;
+	time_taken = (double)(stop - start1)/1000;
+	
+	// print iterations/timing info
+	PM_PrintToMainLog(env, "\nIterative method: %d iterations in %.2f seconds (average %.6f, setup %.2f)\n", iters, time_taken, time_for_iters/iters, time_for_setup);
+	
+	// free memory
+	Cudd_RecursiveDeref(ddman, new_mask);
+	
+	return ptr_to_jlong(sol);
+}
+
+//------------------------------------------------------------------------------

prism/src/mtbdd/PM_ProbInstReward.cc

@@ -0,0 +1,114 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <dxp@cs.bham.uc.uk> (University of Birmingham)
+//	
+//------------------------------------------------------------------------------
+//	
+//	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
+//	
+//==============================================================================
+
+// includes
+#include "PrismMTBDD.h"
+#include <math.h>
+#include <util.h>
+#include <cudd.h>
+#include <dd.h>
+#include <odd.h>
+#include "PrismMTBDDGlob.h"
+#include "jnipointer.h"
+
+//------------------------------------------------------------------------------
+
+JNIEXPORT jlong __pointer JNICALL Java_mtbdd_PrismMTBDD_PM_1ProbInstReward
+(
+JNIEnv *env,
+jclass cls,
+jlong __pointer t,	// trans matrix
+jlong __pointer sr,	// state rewards
+jlong __pointer od,	// odd
+jlong __pointer rv,	// row vars
+jint num_rvars,
+jlong __pointer cv,	// col vars
+jint num_cvars,
+jint bound			// time bound
+)
+{
+	// cast function parameters
+	DdNode *trans = jlong_to_DdNode(t);		// trans matrix
+	DdNode *state_rewards = jlong_to_DdNode(sr);	// state rewards
+	ODDNode *odd = jlong_to_ODDNode(od);		// odd
+	DdNode **rvars = jlong_to_DdNode_array(rv);	// row vars
+	DdNode **cvars = jlong_to_DdNode_array(cv);	// col vars
+
+	// mtbdds
+	DdNode *sol, *tmp;
+	// timing stuff
+	long start1, start2, start3, stop;
+	double time_taken, time_for_setup, time_for_iters;
+	// misc
+	int iters, i;
+	
+	// start clocks
+	start1 = start2 = util_cpu_time();
+	
+	// initial solution is the state rewards
+	Cudd_Ref(state_rewards);
+	sol = state_rewards;
+	
+	// get setup time
+	stop = util_cpu_time();
+	time_for_setup = (double)(stop - start2)/1000;
+	start2 = stop;
+	
+	// start iterations
+	iters = 0;
+	PM_PrintToMainLog(env, "\nStarting iterations...\n");
+	
+	// note that we ignore max_iters as we know how any iterations _should_ be performed
+	for (iters = 0; iters < bound; iters++) {
+		
+//		PM_PrintToMainLog(env, "Iteration %d: ", iters);
+//		start3 = util_cpu_time();
+		
+		// matrix-vector multiply
+		Cudd_Ref(sol);
+		tmp = DD_PermuteVariables(ddman, sol, rvars, cvars, num_rvars);
+		Cudd_Ref(trans);
+		tmp = DD_MatrixMultiply(ddman, trans, tmp, cvars, num_cvars, MM_BOULDER);
+		
+		// prepare for next iteration
+		Cudd_RecursiveDeref(ddman, sol);
+		sol = tmp;
+		
+//		PM_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters);
+	}
+	
+	// stop clocks
+	stop = util_cpu_time();
+	time_for_iters = (double)(stop - start2)/1000;
+	time_taken = (double)(stop - start1)/1000;
+	
+	// print iterations/timing info
+	PM_PrintToMainLog(env, "\nIterative method: %d iterations in %.2f seconds (average %.6f, setup %.2f)\n", iters, time_taken, time_for_iters/iters, time_for_setup);
+	
+	return ptr_to_jlong(sol);
+}
+
+//------------------------------------------------------------------------------

prism/src/mtbdd/PrismMTBDD.java

@@ -271,6 +271,15 @@ public class PrismMTBDD
 		return new JDDNode(ptr);
 	}
 
+	// pctl inst reward (probabilistic/dtmc)
+	private static native long PM_ProbInstReward(long trans, long sr, long odd, long rv, int nrv, long cv, int ncv, int time);
+	public static JDDNode ProbInstReward(JDDNode trans, JDDNode sr, ODDNode odd, JDDVars rows, JDDVars cols, int time) throws PrismException
+	{
+		long ptr = PM_ProbInstReward(trans.ptr(), sr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), time);
+		if (ptr == 0) throw new PrismException(getErrorMessage());
+		return new JDDNode(ptr);
+	}
+
 	// pctl reach reward (probabilistic/dtmc)
 	private static native long PM_ProbReachReward(long trans, long sr, long trr, long odd, long rv, int nrv, long cv, int ncv, long goal, long inf, long maybe);
 	public static JDDNode ProbReachReward(JDDNode trans, JDDNode sr, JDDNode trr, ODDNode odd, JDDVars rows, JDDVars cols, JDDNode goal, JDDNode inf, JDDNode maybe) throws PrismException
@@ -302,6 +311,15 @@ public class PrismMTBDD
 		return new JDDNode(ptr);
 	}
 	
+	// pctl inst reward (nondeterministic/mdp)
+	private static native long PM_NondetInstReward(long trans, long sr, long odd, long mask, long rv, int nrv, long cv, int ncv, long ndv, int nndv, int time, boolean minmax);
+	public static JDDNode NondetInstReward(JDDNode trans, JDDNode sr, ODDNode odd, JDDNode nondetMask, JDDVars rows, JDDVars cols, JDDVars nondet, int time, boolean minmax) throws PrismException
+	{
+		long ptr = PM_NondetInstReward(trans.ptr(), sr.ptr(), odd.ptr(), nondetMask.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), time, minmax);
+		if (ptr == 0) throw new PrismException(getErrorMessage());
+		return new JDDNode(ptr);
+	}
+
 	// pctl reach reward (nondeterministic/mdp)
 	private static native long PM_NondetReachReward(long trans, long sr, long trr, long odd, long mask, long rv, int nrv, long cv, int ncv, long ndv, int nndv, long goal, long inf, long maybe, boolean minmax);
 	public static JDDNode NondetReachReward(JDDNode trans, JDDNode sr, JDDNode trr, ODDNode odd, JDDNode nondetMask, JDDVars rows, JDDVars cols, JDDVars nondet, JDDNode goal, JDDNode inf, JDDNode maybe, boolean minmax) throws PrismException

prism/src/prism/NondetModelChecker.java

@@ -721,7 +721,9 @@ public class NondetModelChecker implements ModelChecker
 		// compute rewards
 		f = pctl.getOperand();
 		try {
-			if (f instanceof PCTLRewardReach)
+			if (f instanceof PCTLRewardInst)
+				rewards = checkPCTLRewardInst((PCTLRewardInst)f, stateRewards, transRewards, min);
+			else if (f instanceof PCTLRewardReach)
 				rewards = checkPCTLRewardReach((PCTLRewardReach)f, stateRewards, transRewards, min);
 			else
 				throw new PrismException("Unrecognised operator in R[] formula");
@@ -1057,6 +1059,25 @@ public class NondetModelChecker implements ModelChecker
 		probs.subtractFromOne();
 		return probs;
 	}
+	
+	// inst reward
+	
+	private StateProbs checkPCTLRewardInst(PCTLRewardInst pctl, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
+	{
+		int time; // time bound
+		StateProbs rewards = null;
+		
+		// get info from bounded until
+		time = pctl.getTime().evaluateInt(constantValues, null);
+		if (time < 0) {
+			throw new PrismException("Invalid bound " + time + " in instantaneous reward property");
+		}
+		
+		// compute rewards
+		rewards = computeInstRewards(trans, stateRewards, time, min);
+		
+		return rewards;
+	}
 
 	// reach reward
 	
@@ -1473,6 +1494,39 @@ public class NondetModelChecker implements ModelChecker
 		return probs;
 	}
 	
+	// compute rewards for inst reward
+	
+	private StateProbs computeInstRewards(JDDNode tr, JDDNode sr, int time, boolean min) throws PrismException
+	{
+		JDDNode rewardsMTBDD;
+		DoubleVector rewardsDV;
+		StateProbs rewards = null;
+		
+		// a trivial case: "=0"
+		if (time == 0) {
+			JDD.Ref(sr);
+			rewards = new StateProbsMTBDD(sr, model);
+		}
+		// otherwise we compute the actual rewards
+		else {
+			// compute the rewards
+			try {
+				switch (engine) {
+				case Prism.MTBDD:
+					rewardsMTBDD = PrismMTBDD.NondetInstReward(tr, sr, odd, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, time, min);
+					rewards = new StateProbsMTBDD(rewardsMTBDD, model);
+					break;
+				default: throw new PrismException("Engine does not support this numerical method");
+				}
+			}
+			catch (PrismException e) {
+				throw e;
+			}
+		}
+		
+		return rewards;
+	}
+	
 	// compute rewards for reach reward
 	
 	private StateProbs computeReachRewards(JDDNode tr, JDDNode tr01, JDDNode sr, JDDNode trr, JDDNode b, boolean min) throws PrismException

prism/src/prism/ProbModelChecker.java

@@ -727,6 +727,8 @@ public class ProbModelChecker implements ModelChecker
 		try {
 			if (f instanceof PCTLRewardCumul)
 				rewards = checkPCTLRewardCumul((PCTLRewardCumul)f, stateRewards, transRewards);
+			else if (f instanceof PCTLRewardInst)
+				rewards = checkPCTLRewardInst((PCTLRewardInst)f, stateRewards, transRewards);
 			else if (f instanceof PCTLRewardReach)
 				rewards = checkPCTLRewardReach((PCTLRewardReach)f, stateRewards, transRewards);
 			else
@@ -1061,6 +1063,25 @@ public class ProbModelChecker implements ModelChecker
 		return rewards;
 	}
 
+	// inst reward
+	
+	private StateProbs checkPCTLRewardInst(PCTLRewardInst pctl, JDDNode stateRewards, JDDNode transRewards) throws PrismException
+	{
+		int time; // time bound
+		StateProbs rewards = null;
+		
+		// get info from bounded until
+		time = pctl.getTime().evaluateInt(constantValues, null);
+		if (time < 0) {
+			throw new PrismException("Invalid bound " + time + " in instantaneous reward property");
+		}
+		
+		// compute rewards
+		rewards = computeInstRewards(trans, stateRewards, time);
+		
+		return rewards;
+	}
+
 	// reach reward
 	
 	private StateProbs checkPCTLRewardReach(PCTLRewardReach pctl, JDDNode stateRewards, JDDNode transRewards) throws PrismException
@@ -1439,6 +1460,39 @@ public class ProbModelChecker implements ModelChecker
 		return rewards;
 	}
 
+	// compute rewards for inst reward
+	
+	private StateProbs computeInstRewards(JDDNode tr, JDDNode sr, int time) throws PrismException
+	{
+		JDDNode rewardsMTBDD;
+		DoubleVector rewardsDV;
+		StateProbs rewards = null;
+		
+		// a trivial case: "=0"
+		if (time == 0) {
+			JDD.Ref(sr);
+			rewards = new StateProbsMTBDD(sr, model);
+		}
+		// otherwise we compute the actual rewards
+		else {
+			// compute the rewards
+			try {
+				switch (engine) {
+				case Prism.MTBDD:
+					rewardsMTBDD = PrismMTBDD.ProbInstReward(tr, sr, odd, allDDRowVars, allDDColVars, time);
+					rewards = new StateProbsMTBDD(rewardsMTBDD, model);
+					break;
+				default: throw new PrismException("Engine does not support this numerical method");
+				}
+			}
+			catch (PrismException e) {
+				throw e;
+			}
+		}
+		
+		return rewards;
+	}
+	
 	// compute rewards for reach reward
 	
 	private StateProbs computeReachRewards(JDDNode tr, JDDNode tr01, JDDNode sr, JDDNode trr, JDDNode b) throws PrismException