symbolic models: allow attaching label state sets directly to the model (similar to explicit models)

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

prism/src/prism/Model.java

@@ -51,6 +51,33 @@ public interface Model
 	int getVarRange(int i);
 	Values getConstantValues();
 	List<String> getSynchs();
+
+	/**
+	 * Returns the JDDNode for the state set (over the row variables)
+	 * associated with the given label.
+	 *
+	 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
+	 * @param label the label
+	 * @returns JDDNode for the label, {@code null} if none is stored
+	 */
+	JDDNode getLabelDD(String label);
+
+	/**
+	 * Returns true if a JDDNode state set for the given label
+	 * is stored in the model.
+	 */
+	default boolean hasLabelDD(String label)
+	{
+		return getLabels().contains(label);
+	}
+
+	/**
+	 * Get the (read-only) set of label names
+	 * that are (optionally) stored in the model.
+	 * Returns an empty set if there are none.
+	 */
+	Set<String> getLabels();
+
 	String globalToLocal(long x);
 	int globalToLocal(long x, int l);
 	State convertBddToState(JDDNode dd);
@@ -116,6 +143,22 @@ public interface Model
 	ODDNode getODD();
 
 	void setSynchs(List<String> synchs);
+
+	/**
+	 * Stores a JDDNode state set (over the row variables)
+	 * for the given label.<br>
+	 * If the label already exists, the old state set is dereferenced
+	 * and overwritten.
+	 * <br>
+	 * Note that a stored label takes precedence over the on-the-fly calculation
+	 * of an ExpressionLabel, cf. {@link prism.StateModelChecker#checkExpressionLabel}
+	 *
+	 * <br>[ STORES: labelDD, deref on later call to clear() ]
+	 * @param label the label name
+	 * @param labelDD the JDDNode with the state set for the label
+	*/
+	void addLabelDD(String label, JDDNode labelDD);
+
 	void resetTrans(JDDNode trans);
 	void resetTransRewards(int i, JDDNode transRewards);
 	void doReachability();

prism/src/prism/ProbModel.java

@@ -28,6 +28,7 @@ package prism;
 
 import java.io.*;
 import java.util.*;
+import java.util.Map.Entry;
 
 import jdd.*;
 import odd.*;
@@ -85,6 +86,12 @@ public class ProbModel implements Model
 	// names for all dd vars used
 	protected Vector<String> ddVarNames;
 
+	/**
+	 * A map from label to state set, optionally storing a state set
+	 * for a given label directly in the model.
+	 */
+	protected Map<String, JDDNode> labelsDD = new TreeMap<String, JDDNode>();
+
 	protected ODDNode odd; // odd
 
 	// accessor methods
@@ -353,6 +360,18 @@ public class ProbModel implements Model
 		return allDDColVars;
 	}
 
+	@Override
+	public JDDNode getLabelDD(String label)
+	{
+		return labelsDD.get(label);
+	}
+
+	@Override
+	public Set<String> getLabels()
+	{
+		return Collections.unmodifiableSet(labelsDD.keySet());
+	}
+
 	// additional useful methods to do with dd vars
 	public int getNumDDRowVars()
 	{
@@ -446,6 +465,13 @@ public class ProbModel implements Model
 		this.numSynchs = synchs.size();
 	}
 
+	@Override
+	public void addLabelDD(String label, JDDNode labelDD)
+	{
+		JDDNode old = labelsDD.put(label, labelDD);
+		if (old != null) JDD.Deref(old);
+	}
+
 	/**
 	 * Reset transition matrix DD.
 	 * Note: Update reachable states and call {@code filterReachableStates}
@@ -904,6 +930,11 @@ public class ProbModel implements Model
 	 */
 	public void clear()
 	{
+		for (Entry<String, JDDNode> labelDD : labelsDD.entrySet()) {
+			JDD.Deref(labelDD.getValue());
+		}
+		labelsDD.clear();
+
 		if (varDDRowVars != null)
 			JDDVars.derefAllArray(varDDRowVars);
 		if (varDDColVars != null)
@@ -941,4 +972,5 @@ public class ProbModel implements Model
 			odd = null;
 		}
 	}
+
 }

prism/src/prism/StateModelChecker.java

@@ -982,6 +982,9 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 			dd = start;
 			JDD.Ref(dd);
 			return new StateValuesMTBDD(dd, model);
+		} else if (model.hasLabelDD(expr.getName())) {
+			dd = model.getLabelDD(expr.getName());
+			return new StateValuesMTBDD(dd.copy(), model);
 		} else {
 			// get expression associated with label
 			ll = propertiesFile.getCombinedLabelList();