prism.StochModel: provide getEmbeddedDTMC()

Allows the direct construction of a ProbModel (DTMC) for
the embedded Markov chain.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12059 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/prism/StochModel.java

@@ -26,6 +26,7 @@
 
 package prism;
 
+import java.util.Map.Entry;
 import java.util.Vector;
 
 import jdd.*;
@@ -61,4 +62,77 @@ public class StochModel extends ProbModel
 	{
 		super(tr, s, sr, trr, rsn, arv, acv, mvdd, nm, mn, mrv, mcv, nv, vl, vrv, vcv, cv);
 	}
+
+	/**
+	 * Get the embedded DTMC for this CTMC.
+	 * <br>
+	 * If parameter {@code log} is non-{@code null}, print some statistics.
+	 * <br>
+	 * If parameter {@code convertRewards} is {@code true}, transforms the rewards as well,
+	 * otherwise the reward structures are stripped.
+	 * <br>[ REFS: <i>result</i>, DEREFS: <i>nothing</i> ]
+	 * @param log the log for printing statistics (may be {@code null})
+	 * @param convertRewards if true, rewards are transformed, otherwise they are stripped
+	 * @return the embedded DTMC
+	 */
+	public ProbModel getEmbeddedDTMC(PrismLog log, boolean convertRewards) throws PrismException
+	{
+		// Compute embedded Markov chain
+		JDDNode diags = JDD.SumAbstract(trans.copy(), allDDColVars);
+		JDDNode embeddedTrans = JDD.Apply(JDD.DIVIDE, trans.copy(), diags.copy());
+		log.println("\nDiagonals vector: " + JDD.GetInfoString(diags, allDDRowVars.n()));
+		log.println("Embedded Markov chain: " + JDD.GetInfoString(embeddedTrans, allDDRowVars.n() * 2));
+
+		// Convert rewards
+		JDDNode[] embStateRewards;
+		JDDNode[] embTransRewards;
+		String[] embRewardStructNames;
+		if (convertRewards) {
+			embStateRewards = new JDDNode[stateRewards.length];
+			embTransRewards = new JDDNode[stateRewards.length];
+			embRewardStructNames = rewardStructNames.clone();
+			for (int i = 0; i < stateRewards.length; i++) {
+				// state rewards are scaled
+				embStateRewards[i] = JDD.Apply(JDD.DIVIDE, stateRewards[i].copy(), diags.copy());
+				// trans rewards are simply copied
+				embTransRewards[i] = transRewards[i].copy();
+			}
+		} else {
+			// strip reward information
+			embStateRewards = new JDDNode[0];
+			embTransRewards = new JDDNode[0];
+			embRewardStructNames = new String[0];
+		}
+
+		JDD.Deref(diags);
+
+		ProbModel result = new ProbModel(embeddedTrans,
+		                                 start.copy(),
+		                                 embStateRewards,
+		                                 embTransRewards,
+		                                 embRewardStructNames,
+		                                 allDDRowVars.copy(),
+		                                 allDDColVars.copy(),
+		                                 modelVariables.copy(),
+		                                 numModules,
+		                                 moduleNames,  // pass by reference, will not be changed
+		                                 JDDVars.copyArray(moduleDDRowVars),
+		                                 JDDVars.copyArray(moduleDDColVars),
+		                                 numModules,
+		                                 varList, // pass by reference, will not be changed
+		                                 JDDVars.copyArray(moduleDDColVars),
+		                                 JDDVars.copyArray(moduleDDColVars),
+		                                 constantValues // pass by reference, will not be changed
+		                                );
+
+		// set reachable states to be the same as for the CTMC
+		result.setReach(getReach().copy());
+
+		// copy labels
+		for (Entry<String, JDDNode> label : labelsDD.entrySet()) {
+			result.addLabelDD(label.getKey(), label.getValue().copy());
+		}
+
+		return result;
+	}
 }