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

@@ -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?
 

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();

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;
 			}
 		}
 		

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

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]);
+			}
+		}
 	}
 }

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);
-		}
-	}
 }