From b45fcb02b7406dd9354a38b842077c6c1670beb9 Mon Sep 17 00:00:00 2001 From: Sascha Wunderlich Date: Thu, 20 Dec 2018 17:02:48 +0100 Subject: [PATCH] accumulation: support single track mode --- prism/src/explicit/AccumulationProduct.java | 6 ++++- .../explicit/AccumulationProductComplex.java | 11 +++++--- .../AccumulationProductComplexCounting.java | 18 ++++++------- .../AccumulationProductComplexRegular.java | 18 ++++++------- .../explicit/AccumulationProductSimple.java | 10 +++++--- .../AccumulationProductSimpleCounting.java | 18 ++++++------- .../AccumulationProductSimpleRegular.java | 18 ++++++------- .../explicit/AccumulationTransformation.java | 25 ++++++++++++------- prism/src/parser/ast/Expression.java | 25 +++++++++++++++++++ 9 files changed, 95 insertions(+), 54 deletions(-) diff --git a/prism/src/explicit/AccumulationProduct.java b/prism/src/explicit/AccumulationProduct.java index 6252d698..e1a4781e 100644 --- a/prism/src/explicit/AccumulationProduct.java +++ b/prism/src/explicit/AccumulationProduct.java @@ -32,12 +32,16 @@ public abstract class AccumulationProduct extends Pro protected int numberOfTracks; protected int numberOfWeights; - public AccumulationProduct(M originalModel) { + protected boolean singleTrack; + + public AccumulationProduct(M originalModel, boolean singleTrack) { super(originalModel); trackers = new StoragePool<>(); accStates = new StoragePool<>(); labels = new ArrayList(); + + this.singleTrack = singleTrack; } public final int getNumberOfTracks() { diff --git a/prism/src/explicit/AccumulationProductComplex.java b/prism/src/explicit/AccumulationProductComplex.java index df0acd35..bbab68c0 100644 --- a/prism/src/explicit/AccumulationProductComplex.java +++ b/prism/src/explicit/AccumulationProductComplex.java @@ -27,8 +27,8 @@ public abstract class AccumulationProductComplex exte protected final ArrayList runStates; protected final ArrayList goalStates; - public AccumulationProductComplex(M originalModel) { - super(originalModel); + public AccumulationProductComplex(M originalModel, boolean singleTrack) { + super(originalModel, singleTrack); initStates = new ArrayList<>(); runStates = new ArrayList<>(); goalStates = new ArrayList<>(); @@ -165,6 +165,9 @@ public abstract class AccumulationProductComplex exte protected final AccumulationState updateAccumulationState(final int modelFromStateId, final AccumulationState accstate, final ExpressionAccumulation accexp, final double[] weights, final ProbModelChecker mc) throws PrismException { + // If we are in singleTrack mode and the last restart is the numberOfTracks, we can stop... + if(singleTrack && (accstate.lastRestartNr == numberOfTracks-1)) { return accstate; } + // Check if we even need to fire here. if(accexp.hasFireOn()) { @@ -198,12 +201,12 @@ public abstract class AccumulationProductComplex exte AccumulationTrack newTrack; // restart or advance - if(trackNr == newLastRestartNr) { + if(trackNr == newLastRestartNr && !singleTrack) { // If we have a restart, we produce an initial track and let it advance. AccumulationTrack freshTrack = new AccumulationTrack(numberOfWeights, getInitialComponent()); //newTrack = updateTrack(modelFromStateId, freshTrack, accexp, weights, mc); newTrack = freshTrack; - } else if (oldTrack == null) { + } else if (oldTrack == null || (singleTrack && trackNr>0)) { // If the old track is undefined, the new track is as well. newTrack = null; } else { diff --git a/prism/src/explicit/AccumulationProductComplexCounting.java b/prism/src/explicit/AccumulationProductComplexCounting.java index 6486dcb4..301f3788 100644 --- a/prism/src/explicit/AccumulationProductComplexCounting.java +++ b/prism/src/explicit/AccumulationProductComplexCounting.java @@ -23,24 +23,24 @@ import prism.PrismException; public class AccumulationProductComplexCounting extends AccumulationProductComplex { - public AccumulationProductComplexCounting(M originalModel) { - super(originalModel); + public AccumulationProductComplexCounting(M originalModel, boolean singleTrack) { + super(originalModel, singleTrack); } @SuppressWarnings("unchecked") - public static AccumulationProductComplexCounting generate(final Model graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + public static AccumulationProductComplexCounting generate(final Model graph, final ExpressionAccumulation accexp, final Vector rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { switch(graph.getModelType()) { case DTMC: - return (AccumulationProductComplexCounting)generate((DTMC) graph, accexp, (Vector) rewards, mc, statesOfInterest); + return (AccumulationProductComplexCounting)generate((DTMC) graph, accexp, (Vector) rewards, singleTrack, mc, statesOfInterest); case MDP: - return (AccumulationProductComplexCounting)generate((MDP) graph, accexp, (Vector) rewards, mc, statesOfInterest); + return (AccumulationProductComplexCounting)generate((MDP) graph, accexp, (Vector) rewards, singleTrack, mc, statesOfInterest); default: throw new PrismException("Can't handle accumulation product for " + graph.getModelType()); } } - public static AccumulationProductComplexCounting generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { - final AccumulationProductComplexCounting result = new AccumulationProductComplexCounting(graph); + public static AccumulationProductComplexCounting generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + final AccumulationProductComplexCounting result = new AccumulationProductComplexCounting(graph, singleTrack); // Create auxiliary data result.createAuxData(graph, accexp, rewards, mc); @@ -98,9 +98,9 @@ public class AccumulationProductComplexCounting extends Accumul return result; } - public static AccumulationProductComplexCounting generate(final MDP graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + public static AccumulationProductComplexCounting generate(final MDP graph, final ExpressionAccumulation accexp, final Vector rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { // This is basically the same thing as for DTMCs - final AccumulationProductComplexCounting result = new AccumulationProductComplexCounting(graph); + final AccumulationProductComplexCounting result = new AccumulationProductComplexCounting(graph, singleTrack); // Create auxiliary data result.createAuxData(graph, accexp, rewards, mc); diff --git a/prism/src/explicit/AccumulationProductComplexRegular.java b/prism/src/explicit/AccumulationProductComplexRegular.java index b3b5e6e7..0e196aa9 100644 --- a/prism/src/explicit/AccumulationProductComplexRegular.java +++ b/prism/src/explicit/AccumulationProductComplexRegular.java @@ -30,24 +30,24 @@ public class AccumulationProductComplexRegular extends Accumula { protected DeterministicFiniteAutomaton automaton; - public AccumulationProductComplexRegular(M originalModel) { - super(originalModel); + public AccumulationProductComplexRegular(M originalModel, boolean singleTrack) { + super(originalModel, singleTrack); } @SuppressWarnings("unchecked") - public static AccumulationProductComplexRegular generate(final Model graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + public static AccumulationProductComplexRegular generate(final Model graph, final ExpressionAccumulation accexp, final Vector rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { switch(graph.getModelType()) { case DTMC: - return (AccumulationProductComplexRegular)generate((DTMC) graph, accexp, (Vector) rewards, mc, statesOfInterest); + return (AccumulationProductComplexRegular)generate((DTMC) graph, accexp, (Vector) rewards, singleTrack, mc, statesOfInterest); case MDP: - return (AccumulationProductComplexRegular)generate((MDP) graph, accexp, (Vector) rewards, mc, statesOfInterest); + return (AccumulationProductComplexRegular)generate((MDP) graph, accexp, (Vector) rewards, singleTrack, mc, statesOfInterest); default: throw new PrismException("Can't handle accumulation product for " + graph.getModelType()); } } - public static AccumulationProductComplexRegular generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { - final AccumulationProductComplexRegular result = new AccumulationProductComplexRegular(graph); + public static AccumulationProductComplexRegular generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + final AccumulationProductComplexRegular result = new AccumulationProductComplexRegular(graph, singleTrack); // Create auxiliary data result.createAuxData(graph, accexp, rewards, mc); @@ -105,9 +105,9 @@ public class AccumulationProductComplexRegular extends Accumula return result; } - public static AccumulationProductComplexRegular generate(final MDP graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + public static AccumulationProductComplexRegular generate(final MDP graph, final ExpressionAccumulation accexp, final Vector rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { // This is basically the same thing as for DTMCs - final AccumulationProductComplexRegular result = new AccumulationProductComplexRegular(graph); + final AccumulationProductComplexRegular result = new AccumulationProductComplexRegular(graph, singleTrack); // Create auxiliary data result.createAuxData(graph, accexp, rewards, mc); diff --git a/prism/src/explicit/AccumulationProductSimple.java b/prism/src/explicit/AccumulationProductSimple.java index 3c3ec84e..17d4008e 100644 --- a/prism/src/explicit/AccumulationProductSimple.java +++ b/prism/src/explicit/AccumulationProductSimple.java @@ -24,8 +24,8 @@ public abstract class AccumulationProductSimple exten { protected final BitSet goodStates; - public AccumulationProductSimple(M originalModel) { - super(originalModel); + public AccumulationProductSimple(M originalModel, boolean singleTrack) { + super(originalModel, singleTrack); goodStates = new BitSet(); } @@ -152,6 +152,8 @@ public abstract class AccumulationProductSimple exten protected final AccumulationState updateAccumulationState(final int modelFromStateId, final AccumulationState accstate, final ExpressionAccumulation accexp, final double[] weights, final ProbModelChecker mc) throws PrismException { + // If we are in singleTrack mode and the last restart is the numberOfTracks, we can stop... + if(singleTrack && (accstate.lastRestartNr == numberOfTracks-1)) { return accstate; } // Get the old tracker and tracks. AccumulationTracker oldTracker = accstate.getTracker(trackers); @@ -171,14 +173,14 @@ public abstract class AccumulationProductSimple exten AccumulationTrack newTrack; // restart or advance - if(trackNr == newLastRestartNr) { + if(trackNr == newLastRestartNr && !singleTrack) { // If we have a restart, we produce an initial track and let it advance. // The goodness is cleared. AccumulationTrack freshTrack = new AccumulationTrack(numberOfWeights, getInitialComponent()); //newTrack = updateTrack(modelFromStateId, freshTrack, accexp, weights, mc); newTrack = freshTrack; newGoodTracks.clear(trackNr); - } else if (oldTrack == null) { + } else if (oldTrack == null || (singleTrack && trackNr>0)) { // If the old track is undefined, the new track is as well. // Goodness stays! newTrack = null; diff --git a/prism/src/explicit/AccumulationProductSimpleCounting.java b/prism/src/explicit/AccumulationProductSimpleCounting.java index ecf86daa..df8b43fc 100644 --- a/prism/src/explicit/AccumulationProductSimpleCounting.java +++ b/prism/src/explicit/AccumulationProductSimpleCounting.java @@ -23,24 +23,24 @@ import prism.PrismException; public class AccumulationProductSimpleCounting extends AccumulationProductSimple { - public AccumulationProductSimpleCounting(M originalModel) { - super(originalModel); + public AccumulationProductSimpleCounting(M originalModel, boolean singleTrack) { + super(originalModel, singleTrack); } @SuppressWarnings("unchecked") - public static AccumulationProductSimpleCounting generate(final Model graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + public static AccumulationProductSimpleCounting generate(final Model graph, final ExpressionAccumulation accexp, final Vector rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { switch(graph.getModelType()) { case DTMC: - return (AccumulationProductSimpleCounting)generate((DTMC) graph, accexp, (Vector) rewards, mc, statesOfInterest); + return (AccumulationProductSimpleCounting)generate((DTMC) graph, accexp, (Vector) rewards, singleTrack, mc, statesOfInterest); case MDP: - return (AccumulationProductSimpleCounting)generate((MDP) graph, accexp, (Vector) rewards, mc, statesOfInterest); + return (AccumulationProductSimpleCounting)generate((MDP) graph, accexp, (Vector) rewards, singleTrack, mc, statesOfInterest); default: throw new PrismException("Can't handle accumulation product for " + graph.getModelType()); } } - public static AccumulationProductSimpleCounting generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { - final AccumulationProductSimpleCounting result = new AccumulationProductSimpleCounting(graph); + public static AccumulationProductSimpleCounting generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + final AccumulationProductSimpleCounting result = new AccumulationProductSimpleCounting(graph,singleTrack); // Create auxiliary data result.createAuxData(graph, accexp, rewards, mc); @@ -98,9 +98,9 @@ public class AccumulationProductSimpleCounting extends Accumula return result; } - public static AccumulationProductSimpleCounting generate(final MDP graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + public static AccumulationProductSimpleCounting generate(final MDP graph, final ExpressionAccumulation accexp, final Vector rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { // This is basically the same thing as for DTMCs - final AccumulationProductSimpleCounting result = new AccumulationProductSimpleCounting(graph); + final AccumulationProductSimpleCounting result = new AccumulationProductSimpleCounting(graph, singleTrack); // Create auxiliary data result.createAuxData(graph, accexp, rewards, mc); diff --git a/prism/src/explicit/AccumulationProductSimpleRegular.java b/prism/src/explicit/AccumulationProductSimpleRegular.java index 838b9a47..de31f82a 100644 --- a/prism/src/explicit/AccumulationProductSimpleRegular.java +++ b/prism/src/explicit/AccumulationProductSimpleRegular.java @@ -30,24 +30,24 @@ public class AccumulationProductSimpleRegular extends Accumulat { protected DeterministicFiniteAutomaton automaton; - public AccumulationProductSimpleRegular(M originalModel) { - super(originalModel); + public AccumulationProductSimpleRegular(M originalModel, boolean singleTrack) { + super(originalModel, singleTrack); } @SuppressWarnings("unchecked") - public static AccumulationProductSimpleRegular generate(final Model graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + public static AccumulationProductSimpleRegular generate(final Model graph, final ExpressionAccumulation accexp, final Vector rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { switch(graph.getModelType()) { case DTMC: - return (AccumulationProductSimpleRegular)generate((DTMC) graph, accexp, (Vector) rewards, mc, statesOfInterest); + return (AccumulationProductSimpleRegular)generate((DTMC) graph, accexp, (Vector) rewards, singleTrack, mc, statesOfInterest); case MDP: - return (AccumulationProductSimpleRegular)generate((MDP) graph, accexp, (Vector) rewards, mc, statesOfInterest); + return (AccumulationProductSimpleRegular)generate((MDP) graph, accexp, (Vector) rewards, singleTrack, mc, statesOfInterest); default: throw new PrismException("Can't handle accumulation product for " + graph.getModelType()); } } - public static AccumulationProductSimpleRegular generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { - final AccumulationProductSimpleRegular result = new AccumulationProductSimpleRegular(graph); + public static AccumulationProductSimpleRegular generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + final AccumulationProductSimpleRegular result = new AccumulationProductSimpleRegular(graph, singleTrack); // Create auxiliary data result.createAuxData(graph, accexp, rewards, mc); @@ -105,9 +105,9 @@ public class AccumulationProductSimpleRegular extends Accumulat return result; } - public static AccumulationProductSimpleRegular generate(final MDP graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + public static AccumulationProductSimpleRegular generate(final MDP graph, final ExpressionAccumulation accexp, final Vector rewards, final boolean singleTrack, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { // This is basically the same thing as for DTMCs - final AccumulationProductSimpleRegular result = new AccumulationProductSimpleRegular(graph); + final AccumulationProductSimpleRegular result = new AccumulationProductSimpleRegular(graph, singleTrack); // Create auxiliary data result.createAuxData(graph, accexp, rewards, mc); diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java index e5938ca9..9c8078d9 100644 --- a/prism/src/explicit/AccumulationTransformation.java +++ b/prism/src/explicit/AccumulationTransformation.java @@ -78,8 +78,15 @@ public class AccumulationTransformation implements Mode // TODO: WHILE getFirstAccumulationExpression // Get the first ExpressionAccumulation - ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpression(); + boolean singleTrack = true; + ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpressionWithoutTemporal(); + if(accexp == null) { + singleTrack = false; + accexp = transformedExpression.getFirstAccumulationExpression(); + } + mc.getLog().println(" [AT] for " + accexp); + mc.getLog().println(" ... single track? " + singleTrack); // Rewrite it, if it is a BOX if (accexp.getSymbol().isBox()) { @@ -114,24 +121,24 @@ public class AccumulationTransformation implements Mode if(isComplex || forceComplex) { mc.getLog().println(" ... using complex!"); - doTransformationComplex(accexp, rewards); + doTransformationComplex(accexp, rewards, singleTrack); } else { mc.getLog().println(" ... using simple!"); - doTransformationSimple(accexp, rewards); + doTransformationSimple(accexp, rewards, singleTrack); } } @SuppressWarnings("unchecked") - protected void doTransformationComplex(ExpressionAccumulation accexp, Vector rewards) throws PrismException { + protected void doTransformationComplex(ExpressionAccumulation accexp, Vector rewards, boolean singleTrack) throws PrismException { StopWatch clock = new StopWatch(mc.getLog()); // Build the product clock.start("accumulation product construction"); if(accexp.hasRegularExpression()) { - product = (AccumulationProductComplexRegular) AccumulationProductComplexRegular.generate(originalModel, accexp, rewards, mc, statesOfInterest); + product = (AccumulationProductComplexRegular) AccumulationProductComplexRegular.generate(originalModel, accexp, rewards, singleTrack, mc, statesOfInterest); } else if (accexp.hasBoundExpression()) { - product = (AccumulationProductComplexCounting) AccumulationProductComplexCounting.generate(originalModel, accexp, rewards, mc, statesOfInterest); + product = (AccumulationProductComplexCounting) AccumulationProductComplexCounting.generate(originalModel, accexp, rewards, singleTrack, mc, statesOfInterest); } else { throw new PrismException("Accumulation Expression has no valid monitor!"); } @@ -176,7 +183,7 @@ public class AccumulationTransformation implements Mode } @SuppressWarnings("unchecked") - protected void doTransformationSimple(ExpressionAccumulation accexp, Vector rewards) throws PrismException { + protected void doTransformationSimple(ExpressionAccumulation accexp, Vector rewards, boolean singleTrack) throws PrismException { StopWatch clock = new StopWatch(mc.getLog()); // Build the product @@ -184,9 +191,9 @@ public class AccumulationTransformation implements Mode if(accexp.hasRegularExpression()) { //throw new PrismException("I don't know how to do regular things..."); - product = (AccumulationProductSimpleRegular) AccumulationProductSimpleRegular.generate(originalModel, accexp, rewards, mc, statesOfInterest); + product = (AccumulationProductSimpleRegular) AccumulationProductSimpleRegular.generate(originalModel, accexp, rewards, singleTrack, mc, statesOfInterest); } else if (accexp.hasBoundExpression()) { - product = (AccumulationProductSimpleCounting) AccumulationProductSimpleCounting.generate(originalModel, accexp, rewards, mc, statesOfInterest); + product = (AccumulationProductSimpleCounting) AccumulationProductSimpleCounting.generate(originalModel, accexp, rewards, singleTrack, mc, statesOfInterest); } else { throw new PrismException("Accumulation Expression has no valid monitor!"); } diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index 4e33b276..9fff4828 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -1006,6 +1006,31 @@ public abstract class Expression extends ASTElement return null; } + /** + * Get the first Accumulation Subexpression that is not in a Temporal Operator + */ + + public ExpressionAccumulation getFirstAccumulationExpressionWithoutTemporal() + { + try { + ASTTraverse astt = new ASTTraverse() + { + public Object visit(ExpressionTemporal expr) + { + return null; + } + public Object visit(ExpressionAccumulation accexp) throws PrismLangException + { + throw new PrismLangException("Found accumulation here!", accexp); + } + }; + this.accept(astt); + } catch (PrismLangException e) { + return (ExpressionAccumulation)e.getASTElement(); + } + return null; + } + /** * Test if an expression is an LTL formula and is in positive normal form, * i.e. where negation only occurs at the level of state formulae.