accumulation: deduplicate gensym

prism/src/explicit/AccumulationTransformation.java

@@ -117,6 +117,7 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
 			} else {
 				throw new PrismException("Accumulation Expression has no valid monitor!");
 			}
+			mc.getLog().println(" [AT] finished product construction: " + product.getTransformedModel().getNumStates());
 			
 			break;
 		default:
@@ -124,11 +125,10 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
 		}
 		
 		// Transform the model
-		mc.getLog().println(" [AT] getting the good states...");
+		mc.getLog().print(" [AT] getting the good states: ");
 		BitSet goodStates = product.getGoodStates();
-		String label = gensymLabel("good", product.getTransformedModel());
-		
-		((ModelExplicit)product.getTransformedModel()).addLabel(label, goodStates);
+		String label = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("good", goodStates, product.getTransformedModel().getLabels());
+		mc.getLog().println(goodStates.cardinality() + " | " + label);
 
 		//System.out.println("Good states " + goodStates);
 		
@@ -142,14 +142,4 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
 			product.exportToDotFile("DEBUG-product.dot");
 		}
 	}
-	
-	public String gensymLabel(String prefix, Model model) {
-		int suffix = 0;
-		String label = prefix + "_" + suffix;
-		while(product.getTransformedModel().getLabels().contains(label)) {
-			suffix++;
-			label = prefix + "_" + suffix;
-		}
-		return label;
-	}
 }