From 782dedbd5bee1e18986b8f0d31ee830080b22cea Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 10 Feb 2010 10:28:14 +0000 Subject: [PATCH] Storage of action info for D/CTMCs (code-level access only currently). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1730 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/NOTES | 3 +- prism/src/prism/Model.java | 4 ++- prism/src/prism/Modules2MTBDD.java | 21 +++++++++--- prism/src/prism/NondetModel.java | 3 ++ prism/src/prism/ProbModel.java | 53 +++++++++++++++++++++++++++--- prism/src/prism/StochModel.java | 18 ---------- 6 files changed, 73 insertions(+), 29 deletions(-) diff --git a/prism/NOTES b/prism/NOTES index 1f3b70f5..d65141ab 100644 --- a/prism/NOTES +++ b/prism/NOTES @@ -56,8 +56,7 @@ TODO: - fix adversary generation (de alfaro thesis) - add adversary generation for other engines -- make action storage optional (when required) -- action storage for D/CTMCs +- make action storage optional (when required e.g. for export) (especially for MCs) - lp stuff - plugin support for eclipse/lpsolve (in prism-multi?) - also look up lrs? diff --git a/prism/src/prism/Model.java b/prism/src/prism/Model.java index 86fe0482..b013165f 100644 --- a/prism/src/prism/Model.java +++ b/prism/src/prism/Model.java @@ -80,6 +80,7 @@ public interface Model JDDNode getTransRewards(int i); JDDNode getTransRewards(String s); JDDNode getTransActions(); + JDDNode[] getTransPerAction(); JDDVars[] getVarDDRowVars(); JDDVars[] getVarDDColVars(); JDDVars getVarDDRowVars(int i); @@ -104,7 +105,8 @@ public interface Model void doReachability(boolean extraReachInfo); void skipReachability(); void setReach(JDDNode reach); - void setTransActions(JDDNode transActions); + void setTransActions(JDDNode transActions); // MDPs only + void setTransPerAction(JDDNode[] transPerAction); // D/CTMCs only void filterReachableStates(); void findDeadlocks(); void fixDeadlocks(); diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index e3de9d33..b7a74605 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -276,9 +276,12 @@ public class Modules2MTBDD ((NondetModel)model).setTransSynch(transSynch); } - // if required, we also store info about action labels + // If required, we also store info about action labels if (storeTransActions) { + // Note: one of these will be null, depending on model type + // but this is fine: null = none stored. model.setTransActions(transActions); + model.setTransPerAction(transPerAction); } // do reachability (or not) @@ -863,10 +866,13 @@ public class Modules2MTBDD // (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) { + // Initialise storage to null so we know what we have used + transActions = null; + transPerAction = null; switch (modelType) { case MDP: transActions = JDD.Constant(0); - // Don't need to store info for independent (action-less) transitions + // 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); @@ -879,8 +885,15 @@ public class Modules2MTBDD break; case DTMC: case CTMC: - // not implemented yet - // TODO: base on code for transInd and transSynch above + // Just reference DDs and copy them to new array + transPerAction = new JDDNode[numSynchs + 1]; + JDD.Ref(sysDDs.ind.trans); + transPerAction[0] = sysDDs.ind.trans; + for (i = 0; i < numSynchs; i++) { + JDD.Ref(sysDDs.synchs[i].trans); + transPerAction[i + 1] = sysDDs.synchs[i].trans; + } + break; } } diff --git a/prism/src/prism/NondetModel.java b/prism/src/prism/NondetModel.java index 0d4258dc..43d3f1a8 100644 --- a/prism/src/prism/NondetModel.java +++ b/prism/src/prism/NondetModel.java @@ -233,6 +233,8 @@ public class NondetModel extends ProbModel // (also update transInd (if necessary) at same time) // (note: we don't need to update transActions since // action-less transitions are encoded as 0 anyway) + // (note: would need to update transPerAction[0] + // but this is not stored for MDPs) JDD.Ref(deadlocks); tmp = JDD.SetVectorElement(JDD.Constant(0), allDDNondetVars, 0, 1); tmp = JDD.And(tmp, JDD.Identity(allDDRowVars, allDDColVars)); @@ -330,6 +332,7 @@ public class NondetModel extends ProbModel log.print(JDD.GetNumNodes(transActions) + " nodes ("); log.print(JDD.GetNumTerminals(transActions) + " terminal)\n"); } + // Don't need to print info for transPerAction (not stored for MDPs) } // export transition matrix to a file diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java index 38ec3894..a494c920 100644 --- a/prism/src/prism/ProbModel.java +++ b/prism/src/prism/ProbModel.java @@ -73,7 +73,8 @@ public class ProbModel implements Model protected JDDNode fixdl; // fixed deadlock states dd protected JDDNode stateRewards[]; // state rewards dds protected JDDNode transRewards[]; // transition rewards dds - protected JDDNode transActions; // dd for transition action labels + protected JDDNode transActions; // dd for transition action labels (MDPs) + protected JDDNode transPerAction[]; // dds for transition action labels (D/CTMCs) // dd vars protected JDDVars[] varDDRowVars; // dd vars for each module variable (rows) @@ -294,6 +295,11 @@ public class ProbModel implements Model return transActions; } + public JDDNode[] getTransPerAction() + { + return transPerAction; + } + // dd vars public JDDVars[] getVarDDRowVars() { @@ -411,6 +417,7 @@ public class ProbModel implements Model // action label info (optional) is initially null transActions = null; + transPerAction = null; // compute numbers for globalToLocal converter gtol = new long[numVars]; @@ -505,13 +512,21 @@ public class ProbModel implements Model } /** - * Set the DD used to store transitoin action label indices. + * Set the DD used to store transition action label indices (MDPs). */ public void setTransActions(JDDNode transActions) { this.transActions = transActions; } + /** + * Set the DDs used to store transition action label indices (D/CTMCs). + */ + public void setTransPerAction(JDDNode[] transPerAction) + { + this.transPerAction = transPerAction; + } + // remove non-reachable states from various dds // (and calculate num transitions) @@ -545,12 +560,22 @@ public class ProbModel implements Model transRewards[i] = JDD.Apply(JDD.TIMES, tmp, transRewards[i]); } - // Action label indices matrix - // (just filter rows here; subclasses, e.g. CTMCs, may do more subsequently) + // Action label index info if (transActions != null) { + // transActions just stored per state so only filter rows JDD.Ref(reach); transActions = JDD.Apply(JDD.TIMES, reach, transActions); } + if (transPerAction != null) { + // transPerAction stored as matrix so filter both rows/cols + for (i = 0; i < numSynchs + 1; i++) { + JDD.Ref(reach); + transPerAction[i] = JDD.Apply(JDD.TIMES, reach, transPerAction[i]); + JDD.Ref(reach); + tmp = JDD.PermuteVariables(reach, allDDRowVars, allDDColVars); + transPerAction[i] = JDD.Apply(JDD.TIMES, tmp, transPerAction[i]); + } + } // filter start states, work out number of initial states JDD.Ref(reach); @@ -582,11 +607,18 @@ public class ProbModel implements Model if (!deadlocks.equals(JDD.ZERO)) { // remove deadlocks by adding self-loops + // also update transPerAction info, if present JDD.Ref(deadlocks); tmp = JDD.And(deadlocks, JDD.Identity(allDDRowVars, allDDColVars)); JDD.Ref(tmp); trans = JDD.Apply(JDD.PLUS, trans, tmp); + JDD.Ref(tmp); trans01 = JDD.Apply(JDD.PLUS, trans01, tmp); + if (transPerAction != null) { + JDD.Ref(tmp); + transPerAction[0] = JDD.Apply(JDD.PLUS, transPerAction[0], tmp); + } + JDD.Deref(tmp); // update lists of deadlocks JDD.Deref(fixdl); fixdl = deadlocks; @@ -668,6 +700,14 @@ public class ProbModel implements Model log.print(JDD.GetNumNodes(transActions) + " nodes ("); log.print(JDD.GetNumTerminals(transActions) + " terminal)\n"); } + if (transPerAction != null) { + for (i = 0; i < numSynchs + 1; i++) { + log.print("Action label info ("); + log.print((i == 0 ? "" : synchs.get(i - 1)) + "): "); + log.print(JDD.GetNumNodes(transPerAction[i]) + " nodes ("); + log.print(JDD.GetNumTerminals(transPerAction[i]) + " terminal)\n"); + } + } } // export transition matrix to a file @@ -845,5 +885,10 @@ public class ProbModel implements Model JDD.Deref(transRewards[i]); } if (transActions != null) JDD.Deref(transActions); + if (transPerAction != null) { + for (int i = 0; i < numSynchs + 1; i++) { + JDD.Deref(transPerAction[i]); + } + } } } diff --git a/prism/src/prism/StochModel.java b/prism/src/prism/StochModel.java index 1f19dfcf..a15fad48 100644 --- a/prism/src/prism/StochModel.java +++ b/prism/src/prism/StochModel.java @@ -61,22 +61,4 @@ public class StochModel extends ProbModel { super(tr, s, sr, trr, rsn, arv, acv, ddvn, nm, mn, mrv, mcv, nv, vl, vrv, vcv, cv); } - - /** - * Remove non-reachable states from various DDs. - * Most of the work is done in the superclass (ProbModel); - * just a few extra things to do here. - */ - public void filterReachableStates() - { - super.filterReachableStates(); - - // If required, also filter columns of action label indices matrix - // (for the superclass - DTMCs - we only store info per state). - if (transActions != null) { - JDD.Ref(reach); - JDDNode tmp = JDD.PermuteVariables(reach, allDDRowVars, allDDColVars); - transActions = JDD.Apply(JDD.TIMES, tmp, transActions); - } - } }