symbolic: add ProbModelTransformationOperator and ProbModel.getTransformed()

By specifying a ProbModelTransformationOperator, we can easily transform
a given symbolic ProbModel (DTMC/CTMC) to a transformed model. The necessary
handling of the meta-information is done in ProbModel.getTransformed.


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

prism/src/prism/ProbModel.java

@@ -34,6 +34,9 @@ import jdd.*;
 import odd.*;
 import mtbdd.*;
 import parser.*;
+import parser.ast.Declaration;
+import parser.ast.DeclarationInt;
+import parser.ast.Expression;
 import sparse.*;
 
 /*
@@ -942,6 +945,180 @@ public class ProbModel implements Model
 		return (int) (x + varList.getLow(numVars - 1));
 	}
 
+	/**
+	 * Apply the given model transformation operator to this model
+	 * and return the resulting, transformed model.
+	 * @param transformation the transformation operator
+	 * @return the transformed model (needs to be cleared after use)
+	 */
+	public ProbModel getTransformed(ProbModelTransformationOperator transformation) throws PrismException
+	{
+		// New (transformed) model - dds, vars, etc.
+		JDDNode newTrans, newStart;
+		JDDVars newVarDDRowVars[], newVarDDColVars[];
+		JDDVars newAllDDRowVars, newAllDDColVars;
+		JDDNode newStateRewards[], newTransRewards[];
+		ModelVariablesDD newModelVariables;
+		VarList newVarList;
+		String extraVar;
+		// DRA stuff
+		JDDVars extraDDRowVars, extraDDColVars;
+		// Misc
+		int i, n;
+		boolean before;
+
+		// Create a (new, unique) name for the variable that will represent the extra states
+		extraVar = transformation.getExtraStateVariableName();
+		while (varList.getIndex(extraVar) != -1) {
+			extraVar = "_" + extraVar;
+		}
+
+		newModelVariables = this.getModelVariables().copy();
+
+		// See how many new dd vars will be needed for the extra variables
+		// and whether there is room to put them before rather than after the existing vars
+		n = transformation.getExtraStateVariableCount();
+		before = newModelVariables.canPrependExtraStateVariable(n);
+
+		extraDDRowVars = new JDDVars();
+		extraDDColVars = new JDDVars();
+		// Create the new dd state variables
+		JDDVars draVars = newModelVariables.allocateExtraStateVariable(n, extraVar, before);
+
+		for (i = 0; i < n; i++) {
+			extraDDRowVars.addVar(draVars.getVar(2*i));
+			extraDDColVars.addVar(draVars.getVar(2*i+1));
+		}
+
+		// notify the transformation operator about the allocated state variables
+		transformation.hookExtraStateVariableAllocation(extraDDRowVars.copy(), extraDDColVars.copy());
+
+		// Create/populate new state variable lists
+		if (n==0) {
+			// no additional state vars, we can just copy everything
+			newVarDDRowVars = JDDVars.copyArray(varDDRowVars);
+			newVarDDColVars = JDDVars.copyArray(varDDColVars);
+			newAllDDRowVars = allDDRowVars.copy();
+			newAllDDColVars = allDDColVars.copy();
+			newVarList = (VarList) varList.clone();
+		} else {
+			// insert new variable either before or after the other variables
+			newVarDDRowVars = new JDDVars[varDDRowVars.length + 1];
+			newVarDDColVars = new JDDVars[varDDRowVars.length + 1];
+			newVarDDRowVars[before ? 0 : varDDRowVars.length] = extraDDRowVars.copy();
+			newVarDDColVars[before ? 0 : varDDColVars.length] = extraDDColVars.copy();
+			for (i = 0; i < varDDRowVars.length; i++) {
+				newVarDDRowVars[before ? i + 1 : i] = varDDRowVars[i].copy();
+				newVarDDColVars[before ? i + 1 : i] = varDDColVars[i].copy();
+			}
+			if (before) {
+				newAllDDRowVars = extraDDRowVars.copy();
+				newAllDDColVars = extraDDColVars.copy();
+				newAllDDRowVars.copyVarsFrom(allDDRowVars);
+				newAllDDColVars.copyVarsFrom(allDDColVars);
+			} else {
+				newAllDDRowVars = allDDRowVars.copy();
+				newAllDDColVars = allDDColVars.copy();
+				newAllDDRowVars.copyVarsFrom(extraDDRowVars);
+				newAllDDColVars.copyVarsFrom(extraDDColVars);
+			}
+			newVarList = (VarList) varList.clone();
+			Declaration decl = new Declaration(extraVar, new DeclarationInt(Expression.Int(0), Expression.Int((1 << n) - 1)));
+			newVarList.addVar(before ? 0 : varList.getNumVars(), decl, 1, this.getConstantValues());
+		}
+
+		// Build transition matrix for transformed model
+		newTrans = transformation.getTransformedTrans();
+
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsDDOverVars(newTrans, newAllDDRowVars, newAllDDColVars);
+		}
+
+		// Build set of initial states for transformed model
+		newStart = transformation.getTransformedStart();
+
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsStateSet(newStart, newAllDDRowVars);
+		}
+
+
+		// Build transformed reward information
+		newStateRewards = new JDDNode[stateRewards.length];
+		for (i=0; i < stateRewards.length; i++) {
+			newStateRewards[i] = transformation.getTransformedStateReward(stateRewards[i]);
+
+			if (SanityJDD.enabled) {
+				SanityJDD.checkIsDDOverVars(newStateRewards[i], newAllDDRowVars);
+			}
+		}
+
+		newTransRewards = new JDDNode[transRewards.length];
+		for (i=0; i < transRewards.length; i++) {
+			newTransRewards[i] = transformation.getTransformedTransReward(transRewards[i]);
+
+			if (SanityJDD.enabled) {
+				SanityJDD.checkIsDDOverVars(newTransRewards[i], newAllDDRowVars, newAllDDColVars);
+			}
+		}
+
+
+		// Create a new model model object to store the transformed model
+		ProbModel result = new ProbModel(
+				// New transition matrix/start state
+				newTrans, newStart,
+				// New reward information
+				newStateRewards,
+				newTransRewards,
+				this.rewardStructNames.clone(),
+				// New list of all row/col vars
+				newAllDDRowVars, newAllDDColVars,
+				// New model variables
+				newModelVariables,
+				// Module info (unchanged)
+				this.getNumModules(),
+				this.getModuleNames(),
+				JDDVars.copyArray(this.getModuleDDRowVars()),
+				JDDVars.copyArray(this.getModuleDDColVars()),
+				// New var info
+				newVarList.getNumVars(), newVarList, newVarDDRowVars, newVarDDColVars,
+				// Constants (no change)
+				this.getConstantValues());
+
+		// Do reachability/etc. for the new model
+		JDDNode S;
+		if ( (S = transformation.getReachableStates()) != null) {
+			// the transformation operator knows the reachable state set
+			result.setReach(S);
+		} else if ( (S = transformation.getReachableStateSeed()) != null ) {
+			// the transformation operator knows a seed for the reachability computation
+			result.doReachability(S);
+		} else {
+			// otherwise: do standard reachability
+			result.doReachability();
+		}
+		result.filterReachableStates();
+
+		if (!transformation.deadlocksAreFine()) {
+			result.findDeadlocks(false);
+			if (result.getDeadlockStates().size() > 0) {
+				// Assuming original model has no deadlocks, neither should the transformed model
+				throw new PrismException("Transformed model has deadlock states");
+			}
+		}
+
+		// lift labels attached to the model
+		for (Entry<String, JDDNode> entry : labelsDD.entrySet()) {
+			JDDNode labelStates = entry.getValue();
+			JDDNode transformedLabelStates = transformation.getTransformedLabelStates(labelStates, result.getReach());
+			result.labelsDD.put(entry.getKey(), transformedLabelStates);
+		}
+
+		extraDDRowVars.derefAll();
+		extraDDColVars.derefAll();
+
+		return result;
+	}
+
 	/**
 	 * Convert a BDD (over model row variables) representing a single state to a State object. 
 	 */

prism/src/prism/ProbModelTransformationOperator.java

@@ -0,0 +1,190 @@
+//==============================================================================
+//	
+//	Copyright (c) 2015-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	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
+//	
+//==============================================================================
+
+package prism;
+
+import jdd.JDDNode;
+import jdd.JDDVars;
+
+/**
+ * Description of a transformation operation for a ProbModel (DTMC/CTMC).
+ * The transformation can request the allocation of extra state variables,
+ * and specify new transition matrix, initial states and reward information.
+ * <br>
+ * After use, the transformation should be cleared by calling {@code clear()}.
+ * <br>
+ * Use ProbModel.getTransformed() to obtain a transformed model.
+ */
+public abstract class ProbModelTransformationOperator
+{
+	/** The original model */
+	protected ProbModel originalModel;
+	/** The extra state variables (rows) */
+	protected JDDVars extraRowVars;
+	/** The extra state variables (columns) */
+	protected JDDVars extraColVars;
+
+	/**
+	 * Constructor with the original model that is to be transformed.
+	 * The original model is not changed and will not be cleared when
+	 * {@code clear()} is called.
+ 	 */
+	public ProbModelTransformationOperator(ProbModel model)
+	{
+		originalModel = model;
+	}
+
+	/**
+	 * Clear the transformation.
+	 */
+	public void clear()
+	{
+		if (extraRowVars != null) {
+			extraRowVars.derefAll();
+		}
+		if (extraColVars != null) {
+			extraColVars.derefAll();
+		}
+	}
+
+	/**
+	 * Return the name (prefix) to use for any new extra state variables.
+	 * Default implementation: Return "extra".
+	 */
+	public String getExtraStateVariableName()
+	{
+		return "extra";
+	}
+
+	/**
+	 * Get the number of extra state variables needed for this transformation.
+	 * This is the number n of state variables and will lead to the allocation of
+	 * 2*n variables, n row and n column variables (interleaved).
+	 */
+	public abstract int getExtraStateVariableCount();
+
+	/**
+	 * This method is called to notify the transformation operator
+	 * about the state variables that were allocated.
+	 * <br>
+	 * The extraRowVars and extraColVars are copies, i.e., this method is responsible
+	 * to ensure that they will be derefed eventually.
+	 * <br>
+	 * Default implementation: Store in extraRowVars and extraColVars fields.
+	 * <br>[ STORES: extraRowVars, extraColVars ]
+	 */
+	public void hookExtraStateVariableAllocation(JDDVars extraRowVars, JDDVars extraColVars)
+	{
+		this.extraRowVars = extraRowVars;
+		this.extraColVars = extraColVars;
+	}
+
+	/**
+	 * Get the transformed transition function.
+	 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+	 */
+	public abstract	JDDNode getTransformedTrans();
+
+	/**
+	 * Get the transformed start function.
+	 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+	 */
+	public abstract JDDNode getTransformedStart();
+
+	/**
+	 * Get the transformed state reward relation, given the old reward relation.
+	 * <br>
+	 * Default implementation: Return the old reward relation, unchanged.
+	 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+	 */
+	public JDDNode getTransformedStateReward(JDDNode oldReward)
+	{
+		return oldReward.copy();
+	}
+
+	/**
+	 * Get the transformed transition reward relation, given the old reward relation.
+	 * <br>
+	 * Default implementation: Return the old reward relation, unchanged.
+	 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+	 */
+	public JDDNode getTransformedTransReward(JDDNode oldReward)
+	{
+		return oldReward.copy();
+	}
+
+	/**
+	 * Get the transformed (lifted) state set corresponding to a label in the original model.
+	 * As a convenience, the reachable states in the transformed model are provided as well.
+	 * <br>
+	 * Default implementation: Return the old state set, i.e.,
+	 * assume don't cares for the extra state variables.
+	 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+	 */
+	public JDDNode getTransformedLabelStates(JDDNode oldLabelStates, JDDNode transformedReach)
+	{
+		return oldLabelStates.copy();
+	}
+
+	/**
+	 * Directly provide the set of reachable states in the transformed model (optional).
+	 * If the set of reachable states is not known, this function should return {@code null}
+	 * and normal reachability computations will be performed.
+	 * <br/>
+	 * Default implementation: return {@code null}
+	 * <br>[ REFS: <i>result</i> ]
+	 */
+	public JDDNode getReachableStates() throws PrismException {
+		return null;
+	}
+
+	/**
+	 * Provide a set of states in the transformed model that is known to be reachable,
+	 * which is then used as a seed in the subsequent reachability computation (speed-up).
+	 * <br>
+	 * If this transformation operator does not want to provide this information,
+	 * this function should return {@code null} and normal reachability computations
+	 * will be performed (from the start states).
+	 * <br/>
+	 * Default implementation: return {@code null}
+	 * <br>[ REFS: <i>result</i> ]
+	 */
+	public JDDNode getReachableStateSeed() throws PrismException {
+		return null;
+	}
+
+	/**
+	 * If true, this transformation may produce deadlock states and the normal
+	 * deadlock check should not be invoked for the transformed model.
+	 * <br>
+	 * Default implementation: return {@code false}
+	 */
+	public boolean deadlocksAreFine()
+	{
+		return false;
+	}
+
+}