diff --git a/prism/include/PrismMTBDD.h b/prism/include/PrismMTBDD.h index 3ff3a017..fd38d5ec 100644 --- a/prism/include/PrismMTBDD.h +++ b/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 diff --git a/prism/src/mtbdd/PM_NondetInstReward.cc b/prism/src/mtbdd/PM_NondetInstReward.cc new file mode 100644 index 00000000..39ed8c23 --- /dev/null +++ b/prism/src/mtbdd/PM_NondetInstReward.cc @@ -0,0 +1,140 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (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 +#include +#include +#include +#include +#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); +} + +//------------------------------------------------------------------------------ diff --git a/prism/src/mtbdd/PM_ProbInstReward.cc b/prism/src/mtbdd/PM_ProbInstReward.cc new file mode 100644 index 00000000..f31456fd --- /dev/null +++ b/prism/src/mtbdd/PM_ProbInstReward.cc @@ -0,0 +1,114 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (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 +#include +#include +#include +#include +#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); +} + +//------------------------------------------------------------------------------ diff --git a/prism/src/mtbdd/PrismMTBDD.java b/prism/src/mtbdd/PrismMTBDD.java index f487b349..4c3a0d21 100644 --- a/prism/src/mtbdd/PrismMTBDD.java +++ b/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 diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 8792fd69..5b890b4f 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/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 diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 191da56a..3eb1e1df 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/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