symbolic: add NondetModelTransformationOperator and NondetModel.getTransformed()

By specifying a NondetModelTransformationOperator, we can easily transform
a given symbolic NondetModel (MDP) to a transformed model. The necessary
handling of the meta-information is done in NondetModelModel.getTransformed.


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

prism/src/prism/NondetModel.java

@@ -27,11 +27,16 @@
 package prism;
 
 import java.io.*;
+import java.util.ArrayList;
+import java.util.Map.Entry;
 
 import jdd.*;
 import odd.*;
 import mtbdd.*;
 import parser.*;
+import parser.ast.Declaration;
+import parser.ast.DeclarationInt;
+import parser.ast.Expression;
 import sparse.*;
 
 /*
@@ -482,6 +487,216 @@ public class NondetModel extends ProbModel
 			JDD.Deref(transReln);
 	}
 
+	/**
+	 * Apply the given model transformation operator to this model
+	 * and return the resulting, transformed model.
+	 * @param transformation the information about the transformation
+	 * @return the transformed model (needs to be cleared after use)
+	 */
+	public NondetModel getTransformed(NondetModelTransformationOperator transformation) throws PrismException
+	{
+		// New (transformed) model - dds, vars, etc.
+		JDDNode newTrans, newStart;
+		JDDVars newVarDDRowVars[], newVarDDColVars[];
+		JDDVars newAllDDRowVars, newAllDDColVars;
+		JDDVars newAllDDChoiceVars, newAllDDNondetVars;
+		JDDNode newStateRewards[], newTransRewards[];
+		ModelVariablesDD newModelVariables;
+		VarList newVarList;
+		String extraStateVar, extraActionVar;
+		// extra variable stuff
+		JDDVars extraDDRowVars, extraDDColVars, extraActionVars;
+		// Misc
+		int i, nStateVars, nActionVars;
+		boolean before;
+
+		// Create a (new, unique) name for the variable that will represent extra states
+		extraStateVar = transformation.getExtraStateVariableName();
+		while (varList.getIndex(extraStateVar) != -1) {
+			extraStateVar = "_" + extraStateVar;
+		}
+
+		// Create a (new, unique) name for the variable that will represent extra actions
+		extraActionVar = transformation.getExtraActionVariableName();
+		while (varList.getIndex(extraActionVar) != -1) {
+			extraActionVar = "_" + extraActionVar;
+		}
+
+		newModelVariables = this.getModelVariables().copy();
+
+		// See how many new dd vars will be needed for extra state variables
+		// and whether there is room to put them before rather than after the existing vars
+		nStateVars = transformation.getExtraStateVariableCount();
+		before = newModelVariables.canPrependExtraStateVariable(nStateVars);
+
+		extraDDRowVars = new JDDVars();
+		extraDDColVars = new JDDVars();
+		// Create the new dd state variables
+		JDDVars extraStateVars = newModelVariables.allocateExtraStateVariable(nStateVars, extraStateVar, before);
+
+		for (i = 0; i < nStateVars; i++) {
+			extraDDRowVars.addVar(extraStateVars.getVar(2*i));
+			extraDDColVars.addVar(extraStateVars.getVar(2*i+1));
+		}
+
+		// notify the transformation about the allocated state variables
+		transformation.hookExtraStateVariableAllocation(extraDDRowVars.copy(), extraDDColVars.copy());
+
+		// allocate action vars
+		nActionVars = transformation.getExtraActionVariableCount();
+		extraActionVars = newModelVariables.allocateExtraActionVariable(nActionVars, extraActionVar);
+
+		// notify the transformation about the allocated action variables
+		transformation.hookExtraActionVariableAllocation(extraActionVars.copy());
+
+		// Generate new allDDChoiceVars and newAllDDNondetVars
+		newAllDDChoiceVars = new JDDVars();
+		newAllDDChoiceVars.copyVarsFrom(extraActionVars);
+		newAllDDChoiceVars.copyVarsFrom(this.allDDChoiceVars);
+
+		newAllDDNondetVars = new JDDVars();
+		newAllDDNondetVars.copyVarsFrom(extraActionVars);
+		newAllDDNondetVars.copyVarsFrom(this.allDDNondetVars);
+
+
+		// Create/populate new state variable lists
+		if (nStateVars == 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(extraStateVar, new DeclarationInt(Expression.Int(0), Expression.Int((1 << nStateVars) - 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, newAllDDNondetVars);
+		}
+
+		// 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, newAllDDNondetVars);
+			}
+		}
+
+		// Create a new model model object to store the product model
+		NondetModel result = new NondetModel(
+		// New transition matrix/start state
+				newTrans, newStart,
+				// New reward information
+				newStateRewards,
+				newTransRewards,
+				this.rewardStructNames.clone(),
+				// New list of all row/col vars
+				newAllDDRowVars, newAllDDColVars,
+				// Nondet variables (unchanged)
+				this.getAllDDSchedVars().copy(),
+				this.getAllDDSynchVars().copy(),
+				newAllDDChoiceVars,
+				newAllDDNondetVars,
+				// 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());
+
+		// Set new transActions
+		result.setTransActions(transformation.getTransformedTransActions());
+
+		// Also need to copy set of action label strings
+		result.setSynchs(new ArrayList<String>(this.getSynchs()));
+
+
+		// 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();
+		extraActionVars.derefAll();
+
+		return result;
+	}
+
 }
 
 //------------------------------------------------------------------------------

prism/src/prism/NondetModelTransformationOperator.java

@@ -0,0 +1,238 @@
+//==============================================================================
+//	
+//	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 NondetModel (MDP).
+ * The transformation can request the allocation of extra state and action variables,
+ * and specify new transition matrix, initial states and reward information.
+ * <br>
+ * After use, the transformation should be cleared by calling {@code clear()}.
+ */
+public abstract class NondetModelTransformationOperator
+{
+	/** The original model */
+	protected NondetModel originalModel;
+	/** The extra state variables (rows) */
+	protected JDDVars extraRowVars;
+	/** The extra state variables (columns) */
+	protected JDDVars extraColVars;
+	/** The extra action (non-deterministic choice) variables */
+	protected JDDVars extraActionVars;
+
+	/**
+	 * 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 NondetModelTransformationOperator(NondetModel model)
+	{
+		originalModel = model;
+	}
+
+	/**
+	 * Clear the transformation.
+	 */
+	public void clear()
+	{
+		if (extraRowVars != null) {
+			extraRowVars.derefAll();
+		}
+		if (extraColVars != null) {
+			extraColVars.derefAll();
+		}
+		if (extraActionVars != null) {
+			extraActionVars.derefAll();
+		}
+	}
+
+	/**
+	 * Return the name (prefix) to use for any new extra state variables.
+	 * Default implementation: Return "extra".
+	 */
+	public String getExtraStateVariableName()
+	{
+		return "extra";
+	}
+
+	/**
+	 * Return the name (prefix) to use for any new extra action variable.
+	 * Default implementation: Return "tau".
+	 */
+	public String getExtraActionVariableName()
+	{
+		return "tau";
+	}
+
+	/**
+	 * 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();
+
+	/**
+	 * Get the number of needed extra action variables for this transformation.
+	 * This will result in the allocation of n additional non-deterministic choice variables.
+	 */
+	public abstract int getExtraActionVariableCount();
+
+	/**
+	 * 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;
+	}
+
+	/**
+	 * This method is called to notify the transformation about the action variables
+	 * that were allocated.
+	 * <br>
+	 * The extraActionsVars are copies, i.e., this method is responsible
+	 * to ensure that they will be derefed eventually.
+	 * <br>
+	 * Default implementation: store in extraActionVars field.
+	 * <br>[ STORES: extraActionVars ]
+	 */
+	public void hookExtraActionVariableAllocation(JDDVars extraActionVars)
+	{
+		this.extraActionVars = extraActionVars;
+	}
+
+	/**
+	 * Get the transformed transition function.
+	 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+	 */
+	public abstract	JDDNode getTransformedTrans() throws PrismException;
+
+	/**
+	 * Get the transformed start function.
+	 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+	 */
+	public abstract JDDNode getTransformedStart() throws PrismException;
+
+	/**
+	 * 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) throws PrismException
+	{
+		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) throws PrismException
+	{
+		return oldReward.copy();
+	}
+
+	/**
+	 * Get the transformed trans actions relation,
+	 * mapping (state,action) to action index.
+	 * Action index 0 indicates unnamed action.
+	 * <br>
+	 * Default implementation: The old trans action relation is returned.
+	 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+	 */
+	public JDDNode getTransformedTransActions() throws PrismException
+	{
+		if (originalModel.getTransActions() == null)
+			return null;
+		return originalModel.getTransActions().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;
+	}
+
+}