Browse Source

accumulation: don't try to print the model all the time...

accumulation
Sascha Wunderlich 9 years ago
committed by Sascha Wunderlich
parent
commit
43a5a91872
  1. 5
      prism/src/explicit/AccumulationProductRegular.java
  2. 2
      prism/src/explicit/AccumulationTransformation.java

5
prism/src/explicit/AccumulationProductRegular.java

@ -101,7 +101,9 @@ public class AccumulationProductRegular<M extends Model> extends AccumulationPro
final AccumulationProductRegular<MDP> result = new AccumulationProductRegular<MDP>(graph); final AccumulationProductRegular<MDP> result = new AccumulationProductRegular<MDP>(graph);
// Create auxiliary data // Create auxiliary data
mc.getLog().println(" [AP] generating aux data...");
result.createAuxData(graph, accexp, rewards, mc); result.createAuxData(graph, accexp, rewards, mc);
mc.getLog().println(" done.");
class AccumulationMDPProductOperator implements MDPProductOperator class AccumulationMDPProductOperator implements MDPProductOperator
{ {
@ -240,7 +242,6 @@ public class AccumulationProductRegular<M extends Model> extends AccumulationPro
* @throws PrismException * @throws PrismException
*/ */
public void createAuxData(final Model graph, final ExpressionAccumulation accexp, final Vector<? extends Rewards> rewards, final ProbModelChecker mc) throws PrismException { public void createAuxData(final Model graph, final ExpressionAccumulation accexp, final Vector<? extends Rewards> rewards, final ProbModelChecker mc) throws PrismException {
mc.getLog().println(" [AP] generating aux data for " + graph + "\n and " + accexp);
// Build labels and DFA // Build labels and DFA
AccumulationModelChecker accMc = new AccumulationModelChecker(); AccumulationModelChecker accMc = new AccumulationModelChecker();
ExpressionRegular reg = (ExpressionRegular)accMc.checkMaximalStateFormulas(mc, graph, accexp.getRegularExpression(), labels); ExpressionRegular reg = (ExpressionRegular)accMc.checkMaximalStateFormulas(mc, graph, accexp.getRegularExpression(), labels);
@ -261,8 +262,6 @@ public class AccumulationProductRegular<M extends Model> extends AccumulationPro
} }
numberOfTracks = automaton.getLongestPathLength()+1; numberOfTracks = automaton.getLongestPathLength()+1;
mc.getLog().println(" [AP] tracks: " + numberOfTracks);
numberOfWeights= rewards.size(); numberOfWeights= rewards.size();
mc.getLog().println(" [AP] weights: " + numberOfWeights);
} }
} }

2
prism/src/explicit/AccumulationTransformation.java

@ -124,6 +124,7 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
} }
// Transform the model // Transform the model
mc.getLog().println(" [AT] getting the good states...");
BitSet goodStates = product.getGoodStates(); BitSet goodStates = product.getGoodStates();
String label = gensymLabel("good", product.getTransformedModel()); String label = gensymLabel("good", product.getTransformedModel());
@ -132,6 +133,7 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
//System.out.println("Good states " + goodStates); //System.out.println("Good states " + goodStates);
// Transform the expression // Transform the expression
mc.getLog().println(" [AT] replacing the formula...");
ReplaceAccumulationExpression replace = new ReplaceAccumulationExpression(accexp, label, product.getNumberOfTracks()-1); ReplaceAccumulationExpression replace = new ReplaceAccumulationExpression(accexp, label, product.getNumberOfTracks()-1);
transformedExpression = (Expression)transformedExpression.accept(replace); transformedExpression = (Expression)transformedExpression.accept(replace);
mc.getLog().println(" [AT] " + originalExpression.toString() + "\n" + mc.getLog().println(" [AT] " + originalExpression.toString() + "\n" +

Loading…
Cancel
Save