From 8effa267f411b93d7f6b00600752ea5ed6bffe53 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 8 Dec 2009 10:29:49 +0000 Subject: [PATCH] Fixed bug in storage of action info for deadlocks + changes to internal storage. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1604 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/include/sparse.h | 2 +- prism/src/prism/Modules2MTBDD.java | 42 +++++++++++++++++------- prism/src/prism/NonProbModelChecker.java | 3 +- prism/src/sparse/PS_NondetUntil.cc | 6 ++-- 4 files changed, 37 insertions(+), 16 deletions(-) diff --git a/prism/include/sparse.h b/prism/include/sparse.h index 8eec3241..cbbc1838 100644 --- a/prism/include/sparse.h +++ b/prism/include/sparse.h @@ -172,7 +172,7 @@ CMSRSparseMatrix *build_cmsr_sparse_matrix(DdManager *ddman, DdNode *matrix, DdN CMSCSparseMatrix *build_cmsc_sparse_matrix(DdManager *ddman, DdNode *matrix, DdNode **rvars, DdNode **cvars, int num_vars, ODDNode *odd); NDSparseMatrix *build_nd_sparse_matrix(DdManager *ddman, DdNode *matrix, DdNode **rvars, DdNode **cvars, int num_vars, DdNode **ndvars, int num_ndvars, ODDNode *odd); NDSparseMatrix *build_sub_nd_sparse_matrix(DdManager *ddman, DdNode *mdp, DdNode *submdp, DdNode **rvars, DdNode **cvars, int num_vars, DdNode **ndvars, int num_ndvars, ODDNode *odd); -int *build_nd_action_vector(DdManager *ddman, DdNode *trans_actions, NDSparseMatrix *mdp_ndsm, DdNode **rvars, int num_vars, DdNode **ndvars, int num_ndvars, ODDNode *odd); +int *build_nd_action_vector(DdManager *ddman, DdNode *mdp, DdNode *trans_actions, NDSparseMatrix *mdp_ndsm, DdNode **rvars, DdNode **cvars, int num_vars, DdNode **ndvars, int num_ndvars, ODDNode *odd); RMSparseMatrix *build_rm_sparse_matrix(DdManager *ddman, DdNode *matrix, DdNode **rvars, DdNode **cvars, int num_vars, ODDNode *odd, bool transpose); CMSparseMatrix *build_cm_sparse_matrix(DdManager *ddman, DdNode *matrix, DdNode **rvars, DdNode **cvars, int num_vars, ODDNode *odd, bool transpose); diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index 5b3bdb1b..14beb336 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -77,7 +77,8 @@ public class Modules2MTBDD private JDDNode start; // dd for start state private JDDNode stateRewards[]; // dds for state rewards private JDDNode transRewards[]; // dds for transition rewards - private JDDNode transActions; // dd for transition action labels + private JDDNode transActions; // dd for transition action labels (MDPs) + private JDDNode transPerAction[]; // dds for transitions for each action (D/CTMCs) private JDDNode transInd; // dds for independent bits of trans private JDDNode transSynch[]; // dds for synch action parts of trans private JDDVars allDDRowVars; // all dd vars (rows) @@ -825,10 +826,11 @@ public class Modules2MTBDD transRewards[j] = JDD.Apply(JDD.PLUS, transRewards[j], sysDDs.synchs[i].rewards[j]); } } - // for dtmcs/ctmcs, final rewards are scaled by dividing by total prob/rate for each transition - // (this is how we compute "expected" reward for each transition) - // (this becomes an issue when a transition prob/rate is the sum of several component values (from different actions)) - // (for mdps, nondeterministic choices are always kept separate so this never occurs) + // For D/CTMCs, final rewards are scaled by dividing by total prob/rate for each transition + // (when individual transition rewards are computed, they are multiplied by individual probs/rates). + // Need to do this (for D/CTMCs) because transition prob/rate can be the sum of values from + // several different actions; this gives us the "expected" reward for each transition. + // (Note, for MDPs, nondeterministic choices are always kept separate so this never occurs.) if (modelType != ModelType.MDP) { n = modulesFile.getNumRewardStructs(); for (j = 0; j < n; j++) { @@ -849,18 +851,36 @@ public class Modules2MTBDD } } - // If required, we also build an MTBDD to store the action labels for each transition + // If required, we also build MTBDD(s) to store the action labels for each transition. + // The indexing of actions is as follows: + // independent ("tau", non-action-labelled) transitions have index 0; + // action-labelled transitions are 1-indexed using the ordering from the model file, + // i.e. adding 1 to the list of actions from modulesFile.getSynchs(). + // What is actually stored differs for each model type. + // For MDPs, we just store the action (index) for each state and nondet choice + // (as an MTBDD 'transActions' over allDDRowVars and allDDNondetVars, with terminals giving index). + // For D/CTMCs, we have store to store a copy of the transition matrix for each action + // (as numSynchs+1 MTBDDs 'transPerAction' over allDDRowVars/allDDColVars, with terminals giving prob/rate) + // because one global transition can come from several different actions. if (storeTransActions) { - if (modelType == ModelType.MDP) { + switch (modelType) { + case MDP: transActions = JDD.Constant(0); - JDD.Ref(sysDDs.ind.trans); - tmp = JDD.ThereExists(JDD.GreaterThan(sysDDs.ind.trans, 0), allDDColVars); - transActions = JDD.Apply(JDD.PLUS, transActions, JDD.Apply(JDD.TIMES, tmp, JDD.Constant(1))); + // Don't need to store info for independent (action-less) transitions + // as they are encoded as 0 anyway + //JDD.Ref(sysDDs.ind.trans); + //tmp = JDD.ThereExists(JDD.GreaterThan(sysDDs.ind.trans, 0), allDDColVars); + //transActions = JDD.Apply(JDD.PLUS, transActions, JDD.Apply(JDD.TIMES, tmp, JDD.Constant(1))); for (i = 0; i < numSynchs; i++) { JDD.Ref(sysDDs.synchs[i].trans); tmp = JDD.ThereExists(JDD.GreaterThan(sysDDs.synchs[i].trans, 0), allDDColVars); - transActions = JDD.Apply(JDD.PLUS, transActions, JDD.Apply(JDD.TIMES, tmp, JDD.Constant(2+i))); + transActions = JDD.Apply(JDD.PLUS, transActions, JDD.Apply(JDD.TIMES, tmp, JDD.Constant(1+i))); } + break; + case DTMC: + case CTMC: + // TODO: base on code for transInd and transSynch above + throw new PrismException("Not implemented yet"); } } diff --git a/prism/src/prism/NonProbModelChecker.java b/prism/src/prism/NonProbModelChecker.java index 040cdc9e..6165509b 100644 --- a/prism/src/prism/NonProbModelChecker.java +++ b/prism/src/prism/NonProbModelChecker.java @@ -248,11 +248,12 @@ public class NonProbModelChecker extends StateModelChecker JDD.Ref(transActions); tmp3 = JDD.Apply(JDD.TIMES, tmp3, transActions); int action = (int)JDD.FindMax(tmp3); - cexActions.add(action > 1 ? model.getSynchs().get(action - 2) : ""); + cexActions.add(action > 0 ? model.getSynchs().get(action - 1) : ""); JDD.Deref(tmp3); JDD.Deref(cexDDs.get(i)); } JDD.Deref(cexDDs.get(0)); + mainLog.println("Counterexample (action sequence): " + cexActions); result.setCounterexample(cexActions); } // Otherwise, convert list of BDDs to list of states diff --git a/prism/src/sparse/PS_NondetUntil.cc b/prism/src/sparse/PS_NondetUntil.cc index 5768fc8c..26601cec 100644 --- a/prism/src/sparse/PS_NondetUntil.cc +++ b/prism/src/sparse/PS_NondetUntil.cc @@ -82,7 +82,7 @@ jboolean min // min or max probabilities (true = min, false = max) long start1, start2, start3, stop; double time_taken, time_for_setup, time_for_iters; // adversary stuff - bool adv = false, adv_loop = false; + bool adv = true, adv_loop = false; FILE *fp_adv = NULL; int adv_l, adv_h; int *actions; @@ -128,7 +128,7 @@ jboolean min // min or max probabilities (true = min, false = max) Cudd_Ref(maybe); tmp = DD_Apply(ddman, APPLY_TIMES, trans_actions, maybe); // then convert to a vector of integer indices - actions = build_nd_action_vector(ddman, tmp, ndsm, rvars, num_rvars, ndvars, num_ndvars, odd); + actions = build_nd_action_vector(ddman, trans, tmp, ndsm, rvars, cvars, num_rvars, ndvars, num_ndvars, odd); Cudd_RecursiveDeref(ddman, tmp); kb = n*4.0/1024.0; kbt += kb; @@ -222,7 +222,7 @@ jboolean min // min or max probabilities (true = min, false = max) if (adv_loop) if (h1 > l1) for (k = adv_l; k < adv_h; k++) { fprintf(fp_adv, "%d %d %g", i, cols[k], non_zeros[k]); - if (actions != NULL) fprintf(fp_adv, " %s", actions[l1]>1?action_names[actions[l1]-2]:""); + if (actions != NULL) fprintf(fp_adv, " %s", actions[l1]>0?action_names[actions[l1]-1]:""); fprintf(fp_adv, "\n"); } }