From a8e412c4a1f57130bb93132fc5b6f5b5b214b4fb Mon Sep 17 00:00:00 2001 From: Sascha Wunderlich Date: Mon, 15 Oct 2018 14:27:07 +0200 Subject: [PATCH] accumulation: deduplicate gensym --- .../explicit/AccumulationTransformation.java | 20 +++++-------------- 1 file changed, 5 insertions(+), 15 deletions(-) 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; - } }