s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Added hybrid implementation of R=?[I] for DTMCs. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@706 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 18 years ago
parent
9df42b659e
commit
5acfb2ec78
4 changed files with 293 additions and 0 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 8
      prism/include/PrismHybrid.h
  2. 272
      prism/src/hybrid/PH_ProbInstReward.cc
  3. 9
      prism/src/hybrid/PrismHybrid.java
  4. 4
      prism/src/prism/ProbModelChecker.java

8
prism/include/PrismHybrid.h
View File

@ -167,6 +167,14 @@ JNIEXPORT jlong JNICALL Java_hybrid_PrismHybrid_PH_1ProbUntil
JNIEXPORT jlong JNICALL Java_hybrid_PrismHybrid_PH_1ProbCumulReward
(JNIEnv *, jclass, jlong, jlong, jlong, jlong, jlong, jint, jlong, jint, jint);
/*
* Class: hybrid_PrismHybrid
* Method: PH_ProbInstReward
* Signature: (JJJJIJII)J
*/
JNIEXPORT jlong JNICALL Java_hybrid_PrismHybrid_PH_1ProbInstReward
(JNIEnv *, jclass, jlong, jlong, jlong, jlong, jint, jlong, jint, jint);
/*
* Class: hybrid_PrismHybrid
* Method: PH_ProbReachReward

272
prism/src/hybrid/PH_ProbInstReward.cc
View File

@ -0,0 +1,272 @@
//==============================================================================
//
// Copyright (c) 2002-
// Authors:
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly 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 "PrismHybrid.h"
#include <math.h>
#include <util.h>
#include <cudd.h>
#include <dd.h>
#include <odd.h>
#include <dv.h>
#include "sparse.h"
#include "hybrid.h"
#include "PrismHybridGlob.h"
#include "jnipointer.h"
// local prototypes
static void mult_rec(HDDNode *hdd, int level, int row_offset, int col_offset);
static void mult_rm(RMSparseMatrix *rmsm, int row_offset, int col_offset);
static void mult_cmsr(CMSRSparseMatrix *cmsrsm, int row_offset, int col_offset);
// globals (used by local functions)
static HDDNode *zero;
static int num_levels;
static bool compact_sm;
static double *sm_dist;
static int sm_dist_shift;
static int sm_dist_mask;
static double *soln, *soln2;
//------------------------------------------------------------------------------
JNIEXPORT jlong __pointer JNICALL Java_hybrid_PrismHybrid_PH_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); // reachable states
DdNode **rvars = jlong_to_DdNode_array(rv); // row vars
DdNode **cvars = jlong_to_DdNode_array(cv); // col vars
// mtbdds
DdNode *tmp;
// model stats
int n;
long nnz;
// matrix mtbdd
HDDMatrix *hddm;
HDDNode *hdd;
// vectors
double *tmpsoln;
// timing stuff
long start1, start2, start3, stop;
double time_taken, time_for_setup, time_for_iters;
// misc
int i, j, iters;
double kb, kbt;
// start clocks
start1 = start2 = util_cpu_time();
// get number of states
n = odd->eoff + odd->toff;
// build hdd for matrix
PH_PrintToMainLog(env, "\nBuilding hybrid MTBDD matrix... ");
hddm = build_hdd_matrix(trans, rvars, cvars, num_rvars, odd, true);
hdd = hddm->top;
zero = hddm->zero;
num_levels = hddm->num_levels;
kb = hddm->mem_nodes;
kbt = kb;
PH_PrintToMainLog(env, "[levels=%d, nodes=%d] [%.1f KB]\n", hddm->num_levels, hddm->num_nodes, kb);
// add sparse matrices
PH_PrintToMainLog(env, "Adding explicit sparse matrices... ");
add_sparse_matrices(hddm, compact, false);
compact_sm = hddm->compact_sm;
if (compact_sm) {
sm_dist = hddm->dist;
sm_dist_shift = hddm->dist_shift;
sm_dist_mask = hddm->dist_mask;
}
kb = hddm->mem_sm;
kbt += kb;
PH_PrintToMainLog(env, "[levels=%d, num=%d%s] [%.1f KB]\n", hddm->l_sm, hddm->num_sm, compact_sm?", compact":"", kb);
// create solution/iteration vectors
// (solution is initialised to the state rewards)
PH_PrintToMainLog(env, "Allocating iteration vectors... ");
soln = mtbdd_to_double_vector(ddman, state_rewards, rvars, num_rvars, odd);
soln2 = new double[n];
kb = n*8.0/1024.0;
kbt += 2*kb;
PH_PrintToMainLog(env, "[2 x %.1f KB]\n", kb);
// print total memory usage
PH_PrintToMainLog(env, "TOTAL: [%.1f KB]\n", kbt);
// get setup time
stop = util_cpu_time();
time_for_setup = (double)(stop - start2)/1000;
start2 = stop;
// start iterations
PH_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++) {
// PH_PrintToMainLog(env, "Iteration %d: ", iters);
// start3 = util_cpu_time();
// initialise vector
for (i = 0; i < n; i++) {
soln2[i] = 0.0;
}
// do matrix vector multiply bit
mult_rec(hdd, 0, 0, 0);
// prepare for next iteration
tmpsoln = soln;
soln = soln2;
soln2 = tmpsoln;
// PH_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
PH_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
free_hdd_matrix(hddm);
delete soln2;
return ptr_to_jlong(soln);
}
//------------------------------------------------------------------------------
static void mult_rec(HDDNode *hdd, int level, int row_offset, int col_offset)
{
HDDNode *e, *t;
// if it's the zero node
if (hdd == zero) {
return;
}
// or if we've reached a submatrix
// (check for non-null ptr but, equivalently, we could just check if level==l_sm)
else if (hdd->sm.ptr) {
if (!compact_sm) {
mult_rm((RMSparseMatrix *)hdd->sm.ptr, row_offset, col_offset);
} else {
mult_cmsr((CMSRSparseMatrix *)hdd->sm.ptr, row_offset, col_offset);
}
return;
}
// or if we've reached the bottom
else if (level == num_levels) {
//printf("(%d,%d)=%f\n", row_offset, col_offset, hdd->type.val);
soln2[row_offset] += soln[col_offset] * hdd->type.val;
return;
}
// otherwise recurse
e = hdd->type.kids.e;
if (e != zero) {
mult_rec(e->type.kids.e, level+1, row_offset, col_offset);
mult_rec(e->type.kids.t, level+1, row_offset, col_offset+e->off.val);
}
t = hdd->type.kids.t;
if (t != zero) {
mult_rec(t->type.kids.e, level+1, row_offset+hdd->off.val, col_offset);
mult_rec(t->type.kids.t, level+1, row_offset+hdd->off.val, col_offset+t->off.val);
}
}
//-----------------------------------------------------------------------------------
static void mult_rm(RMSparseMatrix *rmsm, int row_offset, int col_offset)
{
int i2, j2, l2, h2;
int sm_n = rmsm->n;
int sm_nnz = rmsm->nnz;
double *sm_non_zeros = rmsm->non_zeros;
unsigned char *sm_row_counts = rmsm->row_counts;
int *sm_row_starts = (int *)rmsm->row_counts;
bool sm_use_counts = rmsm->use_counts;
unsigned int *sm_cols = rmsm->cols;
// loop through rows of submatrix
l2 = sm_nnz; h2 = 0;
for (i2 = 0; i2 < sm_n; i2++) {
// loop through entries in this row
if (!sm_use_counts) { l2 = sm_row_starts[i2]; h2 = sm_row_starts[i2+1]; }
else { l2 = h2; h2 += sm_row_counts[i2]; }
for (j2 = l2; j2 < h2; j2++) {
soln2[row_offset + i2] += soln[col_offset + sm_cols[j2]] * sm_non_zeros[j2];
//printf("(%d,%d)=%f\n", row_offset + i2, col_offset + sm_cols[j2], sm_non_zeros[j2]);
}
}
}
//-----------------------------------------------------------------------------------
static void mult_cmsr(CMSRSparseMatrix *cmsrsm, int row_offset, int col_offset)
{
int i2, j2, l2, h2;
int sm_n = cmsrsm->n;
int sm_nnz = cmsrsm->nnz;
unsigned char *sm_row_counts = cmsrsm->row_counts;
int *sm_row_starts = (int *)cmsrsm->row_counts;
bool sm_use_counts = cmsrsm->use_counts;
unsigned int *sm_cols = cmsrsm->cols;
// loop through rows of submatrix
l2 = sm_nnz; h2 = 0;
for (i2 = 0; i2 < sm_n; i2++) {
// loop through entries in this row
if (!sm_use_counts) { l2 = sm_row_starts[i2]; h2 = sm_row_starts[i2+1]; }
else { l2 = h2; h2 += sm_row_counts[i2]; }
for (j2 = l2; j2 < h2; j2++) {
soln2[row_offset + i2] += soln[col_offset + (int)(sm_cols[j2] >> sm_dist_shift)] * sm_dist[(int)(sm_cols[j2] & sm_dist_mask)];
//printf("(%d,%d)=%f\n", row_offset + i2, col_offset + (int)(sm_cols[j2] >> sm_dist_shift), sm_dist[(int)(sm_cols[j2] & sm_dist_mask)]);
}
}
}
//------------------------------------------------------------------------------

9
prism/src/hybrid/PrismHybrid.java
View File

@ -254,6 +254,15 @@ public class PrismHybrid
return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
}
// pctl cumulative reward (probabilistic/dtmc)
private static native long PH_ProbInstReward(long trans, long sr, long odd, long rv, int nrv, long cv, int ncv, int time);
public static DoubleVector ProbInstReward(JDDNode trans, JDDNode sr, ODDNode odd, JDDVars rows, JDDVars cols, int time) throws PrismException
{
long ptr = PH_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 DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
}
// pctl reach reward (probabilistic/dtmc)
private static native long PH_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 DoubleVector ProbReachReward(JDDNode trans, JDDNode sr, JDDNode trr, ODDNode odd, JDDVars rows, JDDVars cols, JDDNode goal, JDDNode inf, JDDNode maybe) throws PrismException

4
prism/src/prism/ProbModelChecker.java
View File

@ -1450,6 +1450,10 @@ public class ProbModelChecker extends StateModelChecker
rewardsDV = PrismSparse.ProbInstReward(tr, sr, odd, allDDRowVars, allDDColVars, time);
rewards = new StateProbsDV(rewardsDV, model);
break;
case Prism.HYBRID:
rewardsDV = PrismHybrid.ProbInstReward(tr, sr, odd, allDDRowVars, allDDColVars, time);
rewards = new StateProbsDV(rewardsDV, model);
break;
default:
throw new PrismException("Engine does not support this numerical method");
}

Write Preview
Loading…
Cancel
Save