From 6cce20c5ed8956c72fad65454cc6d0e6c43f073a Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 12 Oct 2018 14:25:37 +0200
Subject: [PATCH] imported patch
 prod-with-productstates-rely-on-product-for-soi.patch

---
 prism/src/explicit/ProductWithProductStates.java | 13 +++----------
 1 file changed, 3 insertions(+), 10 deletions(-)

diff --git a/prism/src/explicit/ProductWithProductStates.java b/prism/src/explicit/ProductWithProductStates.java
index c0fb839f..b6d55764 100644
--- a/prism/src/explicit/ProductWithProductStates.java
+++ b/prism/src/explicit/ProductWithProductStates.java
@@ -43,14 +43,15 @@ import prism.PrismException;
 /**
  * Provides functionality for generating a Product via a
  * DTMCProductOperator / MDPProductOperator.
+ * <br>
+ * The initial states in the product correspond to the lifted
+ * states of interest in the original model.
  *
  * @param <M> the model type
  */
 public class ProductWithProductStates<M extends Model> extends Product<M> {
 	/** Mapping index to ProductState */
 	protected Vector<ProductState> prod_states = new Vector<ProductState>();
-	/** States of interest in the product */
-	protected BitSet statesOfInterestInProduct = new BitSet();
 
 	/** Constructor */
 	protected ProductWithProductStates(M originalModel)
@@ -76,12 +77,6 @@ public class ProductWithProductStates<M extends Model> extends Product<M> {
 		return getState(productState).getSecondState();
 	}
 
-	@Override
-	public BitSet getTransformedStatesOfInterest()
-	{
-		return statesOfInterestInProduct;
-	}
-
 	/**
 	 * Generates the DTMC for a {@code ProductWithProductStates<DTMC>}
 	 * using the operator {@code op}, storing the result in
@@ -128,7 +123,6 @@ public class ProductWithProductStates<M extends Model> extends Product<M> {
 			Integer s = mapping.findOrAdd(prod_initial);
 			todo.add(prod_initial);
 			dtmcProduct.addInitialState(s);
-			product.statesOfInterestInProduct.set(s);
 		}
 
 		while (!todo.isEmpty()) {
@@ -215,7 +209,6 @@ public class ProductWithProductStates<M extends Model> extends Product<M> {
 			Integer s = mapping.findOrAdd(prod_initial);
 			todo.add(prod_initial);
 			mdpProduct.addInitialState(s);
-			product.statesOfInterestInProduct.set(s);
 		}
 
 		while (!todo.isEmpty()) {