imported patch MT-states-of-interest.patch

prism/src/explicit/BasicModelTransformation.java

@@ -49,6 +49,7 @@ public class BasicModelTransformation<OM extends Model, TM extends Model> implem
 
 	protected final OM originalModel;
 	protected final TM transformedModel;
+	protected BitSet transformedStatesOfInterest;
 	protected final IntFunction<Integer> mapToTransformedModel;
 
 	protected final int numberOfStates;
@@ -56,19 +57,26 @@ public class BasicModelTransformation<OM extends Model, TM extends Model> implem
 	/** Constructor for a model transformation that maps states one-on-one. */
 	public BasicModelTransformation(final OM originalModel, final TM transformedModel)
 	{
-		this(originalModel, transformedModel, IDENTITY);
+		this(originalModel, transformedModel, null);
+	}
+
+	public BasicModelTransformation(final OM originalModel, final TM transformedModel, final BitSet transformedStatesOfInterest)
+	{
+		this(originalModel, transformedModel, transformedStatesOfInterest, IDENTITY);
 	}
 
 	/**
 	 * Constructor for a model transformation where the state mapping is given
 	 * by a function
 	 */
-	public BasicModelTransformation(final OM originalModel, final TM transformedModel, final IntFunction<Integer> mapToTransformedModel)
+	public BasicModelTransformation(final OM originalModel, final TM transformedModel, final BitSet transformedStatesOfInterest, final IntFunction<Integer> mapToTransformedModel)
 	{
 		this.originalModel               = originalModel;
 		this.transformedModel            = transformedModel;
 		this.numberOfStates              = originalModel.getNumStates();
 		this.mapToTransformedModel       = mapToTransformedModel;
+		setTransformedStatesOfInterest(transformedStatesOfInterest);
+
 	}
 
 	@Override
@@ -83,6 +91,21 @@ public class BasicModelTransformation<OM extends Model, TM extends Model> implem
 		return transformedModel;
 	}
 
+	@Override
+	public BitSet getTransformedStatesOfInterest()
+	{
+		return transformedStatesOfInterest;
+	}
+
+	public BasicModelTransformation<OM, TM> setTransformedStatesOfInterest(BitSet transformedStatesOfInterest)
+	{
+		if (transformedStatesOfInterest != null && transformedStatesOfInterest.length() > transformedModel.getNumStates()) {
+			throw new IndexOutOfBoundsException("State set must be subset of transformed model's state space");
+		}
+		this.transformedStatesOfInterest = transformedStatesOfInterest;
+		return this;
+	}
+
 	@Override
 	public StateValues projectToOriginalModel(final StateValues sv) throws PrismException
 	{

prism/src/explicit/ModelTransformation.java

@@ -26,6 +26,8 @@
 
 package explicit;
 
+import java.util.BitSet;
+
 import prism.PrismException;
 
 /**
@@ -46,4 +48,9 @@ public interface ModelTransformation<OriginalModel extends Model, TransformedMod
 	 * @return a corresponding {@code StateValues} object for the original model.
 	 **/
 	public StateValues projectToOriginalModel(StateValues svTransformedModel) throws PrismException;
+
+	/**
+	 * Get the transformed set of states of interest.
+	 **/
+	public BitSet getTransformedStatesOfInterest();
 }

prism/src/explicit/ModelTransformationNested.java

@@ -27,6 +27,8 @@
 
 package explicit;
 
+import java.util.BitSet;
+
 import prism.PrismException;
 
 /**
@@ -69,6 +71,12 @@ public class ModelTransformationNested<OriginalModel extends Model,
 		return outerTransformation.getTransformedModel();
 	}
 
+	@Override
+	public BitSet getTransformedStatesOfInterest()
+	{
+		return outerTransformation.getTransformedStatesOfInterest();
+	}
+
 	@Override
 	public StateValues projectToOriginalModel(final StateValues svTransformedModel) throws PrismException
 	{

prism/src/explicit/Product.java

@@ -39,9 +39,15 @@ import prism.PrismNotSupportedException;
  * Base class for the results of a product operation between a model and
  * an automaton. Provides infrastructure for converting information on the
  * states between the original model, the automaton and the product model.
- *
+ * <br>
  * The mapping between product states and the constituent parts is
  * specified via the (abstract) functions getModelState() and getAutomatonState().
+ * <br>
+ * By default it is assumed that each initial state in the product corresponds
+ * to exactly one lifted state of interest in the original model,
+ * allowing a mapping between product and original model state values.
+ * If this assumption is not correct, overload {@code projectToOriginalModel} and
+ * {@code getTransformedStatesOfInterest}.
  *
  * @param <M> The type of the product model, e.g, DTMC, MDP, ...
  */
@@ -212,4 +218,13 @@ public abstract class Product<M extends Model> implements ModelTransformation<M,
 		return result;
 	}
 
+	@Override
+	public BitSet getTransformedStatesOfInterest()
+	{
+		BitSet productStatesOfInterest = new BitSet();
+		for (int initial : productModel.getInitialStates()) {
+			productStatesOfInterest.set(initial);
+		}
+		return productStatesOfInterest;
+	}
 }