diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java index 00db25ae..7c236862 100644 --- a/prism/src/explicit/AccumulationTransformation.java +++ b/prism/src/explicit/AccumulationTransformation.java @@ -117,6 +117,7 @@ public class AccumulationTransformation 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,12 +125,11 @@ public class AccumulationTransformation 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); // Transform the expression @@ -142,14 +142,4 @@ public class AccumulationTransformation 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; - } }