diff --git a/prism/src/explicit/AccumulationProductRegular.java b/prism/src/explicit/AccumulationProductRegular.java index a3609342..a5214a74 100644 --- a/prism/src/explicit/AccumulationProductRegular.java +++ b/prism/src/explicit/AccumulationProductRegular.java @@ -101,7 +101,9 @@ public class AccumulationProductRegular extends AccumulationPro final AccumulationProductRegular result = new AccumulationProductRegular(graph); // Create auxiliary data + mc.getLog().println(" [AP] generating aux data..."); result.createAuxData(graph, accexp, rewards, mc); + mc.getLog().println(" done."); class AccumulationMDPProductOperator implements MDPProductOperator { @@ -240,7 +242,6 @@ public class AccumulationProductRegular extends AccumulationPro * @throws PrismException */ public void createAuxData(final Model graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc) throws PrismException { - mc.getLog().println(" [AP] generating aux data for " + graph + "\n and " + accexp); // Build labels and DFA AccumulationModelChecker accMc = new AccumulationModelChecker(); ExpressionRegular reg = (ExpressionRegular)accMc.checkMaximalStateFormulas(mc, graph, accexp.getRegularExpression(), labels); @@ -261,8 +262,6 @@ public class AccumulationProductRegular extends AccumulationPro } numberOfTracks = automaton.getLongestPathLength()+1; - mc.getLog().println(" [AP] tracks: " + numberOfTracks); numberOfWeights= rewards.size(); - mc.getLog().println(" [AP] weights: " + numberOfWeights); } } diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java index 2ba07edd..143d5701 100644 --- a/prism/src/explicit/AccumulationTransformation.java +++ b/prism/src/explicit/AccumulationTransformation.java @@ -124,6 +124,7 @@ public class AccumulationTransformation implements ModelExpress } // Transform the model + mc.getLog().println(" [AT] getting the good states..."); BitSet goodStates = product.getGoodStates(); String label = gensymLabel("good", product.getTransformedModel()); @@ -132,6 +133,7 @@ public class AccumulationTransformation implements ModelExpress //System.out.println("Good states " + goodStates); // Transform the expression + mc.getLog().println(" [AT] replacing the formula..."); ReplaceAccumulationExpression replace = new ReplaceAccumulationExpression(accexp, label, product.getNumberOfTracks()-1); transformedExpression = (Expression)transformedExpression.accept(replace); mc.getLog().println(" [AT] " + originalExpression.toString() + "\n" +