diff --git a/prism/src/simulator/ChoiceList.java b/prism/src/simulator/ChoiceList.java index 7db04ff4..0b1712ca 100644 --- a/prism/src/simulator/ChoiceList.java +++ b/prism/src/simulator/ChoiceList.java @@ -92,6 +92,16 @@ public class ChoiceList implements Choice // Get methods + public int getModuleOrActionIndex() + { + return 0; // TODO + } + + public String getModuleOrAction() + { + return null; // TODO + } + public String getAction() { return action; diff --git a/prism/src/simulator/ChoiceSingleton.java b/prism/src/simulator/ChoiceSingleton.java index 178bbac3..6862a41a 100644 --- a/prism/src/simulator/ChoiceSingleton.java +++ b/prism/src/simulator/ChoiceSingleton.java @@ -65,6 +65,16 @@ public class ChoiceSingleton implements Choice // Get methods + public int getModuleOrActionIndex() + { + return 0; // TODO + } + + public String getModuleOrAction() + { + return null; // TODO + } + public int size() { return 1; diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index a4bc1b55..7a8c62f1 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -863,8 +863,7 @@ public class SimulatorEngine private void updateSamplers() throws PrismLangException { for (Sampler sampler : propertySamplers) { - if (!sampler.isCurrentValueKnown()) - sampler.update(path); + sampler.update(path); } } @@ -881,8 +880,7 @@ public class SimulatorEngine for (i = 0; i <= n; i++) { prefix.setPrefixLength(i); for (Sampler sampler : propertySamplers) { - if (!sampler.isCurrentValueKnown()) - sampler.update(prefix); + sampler.update(prefix); } } } diff --git a/prism/src/simulator/sampler/Sampler.java b/prism/src/simulator/sampler/Sampler.java index 49e1faed..ed1adde8 100644 --- a/prism/src/simulator/sampler/Sampler.java +++ b/prism/src/simulator/sampler/Sampler.java @@ -59,9 +59,9 @@ public abstract class Sampler /** * Update the current value of the sampler based on the current simulation path. * It is assumed that this is called at every step of the path. - * It is also assumed that this is not called after the value becomes known. + * This returns true if the sampler's value becomes (or is already) known. */ - public abstract void update(Path path) throws PrismLangException; + public abstract boolean update(Path path) throws PrismLangException; /** * Update the statistics for the sampler, assuming that the current path is finished. diff --git a/prism/src/simulator/sampler/SamplerBoolean.java b/prism/src/simulator/sampler/SamplerBoolean.java index a991add4..f7f941a2 100644 --- a/prism/src/simulator/sampler/SamplerBoolean.java +++ b/prism/src/simulator/sampler/SamplerBoolean.java @@ -57,7 +57,7 @@ public abstract class SamplerBoolean extends Sampler } @Override - public abstract void update(Path path) throws PrismLangException; + public abstract boolean update(Path path) throws PrismLangException; @Override public void updateStats() diff --git a/prism/src/simulator/sampler/SamplerBoundedUntilCont.java b/prism/src/simulator/sampler/SamplerBoundedUntilCont.java index a87f0572..28500391 100644 --- a/prism/src/simulator/sampler/SamplerBoundedUntilCont.java +++ b/prism/src/simulator/sampler/SamplerBoundedUntilCont.java @@ -63,8 +63,12 @@ public class SamplerBoundedUntilCont extends SamplerBoolean } @Override - public void update(Path path) throws PrismLangException + public boolean update(Path path) throws PrismLangException { + // If the answer is already known we should do nothing + if (valueKnown) + return true; + // For continuous-time bounded until, we may need to look back at previous state. // So, treat first/subsequent calls to update() differently. @@ -133,5 +137,7 @@ public class SamplerBoundedUntilCont extends SamplerBoolean } } } + + return valueKnown; } } diff --git a/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java b/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java index 5d0b4f90..7eed4f6b 100644 --- a/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java +++ b/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java @@ -59,8 +59,12 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean } @Override - public void update(Path path) throws PrismLangException + public boolean update(Path path) throws PrismLangException { + // If the answer is already known we should do nothing + if (valueKnown) + return true; + int pathSize = path.size(); // Upper bound exceeded if (pathSize > ub) { @@ -90,5 +94,7 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean } // Otherwise, don't know } + + return valueKnown; } } diff --git a/prism/src/simulator/sampler/SamplerDouble.java b/prism/src/simulator/sampler/SamplerDouble.java index aa84bad2..c87db0ee 100644 --- a/prism/src/simulator/sampler/SamplerDouble.java +++ b/prism/src/simulator/sampler/SamplerDouble.java @@ -55,7 +55,7 @@ public abstract class SamplerDouble extends Sampler } @Override - public abstract void update(Path path) throws PrismLangException; + public abstract boolean update(Path path) throws PrismLangException; @Override public void updateStats() diff --git a/prism/src/simulator/sampler/SamplerNext.java b/prism/src/simulator/sampler/SamplerNext.java index fdcdd174..41fd5665 100644 --- a/prism/src/simulator/sampler/SamplerNext.java +++ b/prism/src/simulator/sampler/SamplerNext.java @@ -52,8 +52,12 @@ public class SamplerNext extends SamplerBoolean } @Override - public void update(Path path) throws PrismLangException + public boolean update(Path path) throws PrismLangException { + // If the answer is already known we should do nothing + if (valueKnown) + return true; + // X "target" is true iff state 1 satisfies "target" if (path.size() == 1) { valueKnown = true; @@ -61,5 +65,7 @@ public class SamplerNext extends SamplerBoolean } // Nothing else to do: if path size is 0, can't decide; // if path size > 1 (should never happen), nothing changes + + return valueKnown; } } diff --git a/prism/src/simulator/sampler/SamplerRewardCumulCont.java b/prism/src/simulator/sampler/SamplerRewardCumulCont.java index 003bbff9..b4228a92 100644 --- a/prism/src/simulator/sampler/SamplerRewardCumulCont.java +++ b/prism/src/simulator/sampler/SamplerRewardCumulCont.java @@ -55,8 +55,12 @@ public class SamplerRewardCumulCont extends SamplerDouble } @Override - public void update(Path path) throws PrismLangException + public boolean update(Path path) throws PrismLangException { + // If the answer is already known we should do nothing + if (valueKnown) + return true; + // As soon as time bound exceeded, compute reward total if (path.getTotalTime() >= timeBound) { valueKnown = true; @@ -75,5 +79,7 @@ public class SamplerRewardCumulCont extends SamplerDouble value -= path.getPreviousTransitionReward(rewardStructIndex); } } + + return valueKnown; } } diff --git a/prism/src/simulator/sampler/SamplerRewardCumulDisc.java b/prism/src/simulator/sampler/SamplerRewardCumulDisc.java index 5950ecdf..7088b8df 100644 --- a/prism/src/simulator/sampler/SamplerRewardCumulDisc.java +++ b/prism/src/simulator/sampler/SamplerRewardCumulDisc.java @@ -55,12 +55,18 @@ public class SamplerRewardCumulDisc extends SamplerDouble } @Override - public void update(Path path) throws PrismLangException + public boolean update(Path path) throws PrismLangException { + // If the answer is already known we should do nothing + if (valueKnown) + return true; + // As soon as time bound reached, store current reward total if (path.size() == timeBound) { valueKnown = true; value = path.getTotalCumulativeReward(rewardStructIndex); } + + return valueKnown; } } diff --git a/prism/src/simulator/sampler/SamplerRewardInstCont.java b/prism/src/simulator/sampler/SamplerRewardInstCont.java index 3292601f..c8d7b3c6 100644 --- a/prism/src/simulator/sampler/SamplerRewardInstCont.java +++ b/prism/src/simulator/sampler/SamplerRewardInstCont.java @@ -55,8 +55,12 @@ public class SamplerRewardInstCont extends SamplerDouble } @Override - public void update(Path path) throws PrismLangException + public boolean update(Path path) throws PrismLangException { + // If the answer is already known we should do nothing + if (valueKnown) + return true; + // As soon as time bound exceeded, compute reward if (path.getTotalTime() >= time) { valueKnown = true; @@ -70,5 +74,7 @@ public class SamplerRewardInstCont extends SamplerDouble value = path.getCurrentStateReward(rewardStructIndex); } } + + return valueKnown; } } diff --git a/prism/src/simulator/sampler/SamplerRewardInstDisc.java b/prism/src/simulator/sampler/SamplerRewardInstDisc.java index 1109efb8..d6e67537 100644 --- a/prism/src/simulator/sampler/SamplerRewardInstDisc.java +++ b/prism/src/simulator/sampler/SamplerRewardInstDisc.java @@ -55,12 +55,18 @@ public class SamplerRewardInstDisc extends SamplerDouble } @Override - public void update(Path path) throws PrismLangException + public boolean update(Path path) throws PrismLangException { + // If the answer is already known we should do nothing + if (valueKnown) + return true; + // As soon as time bound reached, store current state reward if (path.size() == time) { valueKnown = true; value = path.getCurrentStateReward(rewardStructIndex); } + + return valueKnown; } } diff --git a/prism/src/simulator/sampler/SamplerRewardReach.java b/prism/src/simulator/sampler/SamplerRewardReach.java index 86c3475d..2fe0408d 100644 --- a/prism/src/simulator/sampler/SamplerRewardReach.java +++ b/prism/src/simulator/sampler/SamplerRewardReach.java @@ -43,6 +43,10 @@ public class SamplerRewardReach extends SamplerDouble */ public SamplerRewardReach(ExpressionTemporal expr, int rewardStructIndex) throws PrismException { + // If the answer is already known we should do nothing + if (valueKnown) + return; + // Make sure expression is of the correct type // Then extract other required info if (expr.getOperator() != ExpressionTemporal.R_F) @@ -55,11 +59,17 @@ public class SamplerRewardReach extends SamplerDouble } @Override - public void update(Path path) throws PrismLangException + public boolean update(Path path) throws PrismLangException { + // If the answer is already known we should do nothing + if (valueKnown) + return true; + if (target.evaluateBoolean(path.getCurrentState())) { valueKnown = true; value = path.getTotalCumulativeReward(rewardStructIndex); } + + return valueKnown; } } diff --git a/prism/src/simulator/sampler/SamplerUntil.java b/prism/src/simulator/sampler/SamplerUntil.java index dfcdc7bd..da77bcc9 100644 --- a/prism/src/simulator/sampler/SamplerUntil.java +++ b/prism/src/simulator/sampler/SamplerUntil.java @@ -57,8 +57,12 @@ public class SamplerUntil extends SamplerBoolean } @Override - public void update(Path path) throws PrismLangException + public boolean update(Path path) throws PrismLangException { + // If the answer is already known we should do nothing + if (valueKnown) + return true; + State currentState = path.getCurrentState(); // Have we reached the target (i.e. RHS of until)? if (right.evaluateBoolean(currentState)) { @@ -71,5 +75,7 @@ public class SamplerUntil extends SamplerBoolean value = false; } // Otherwise, don't know + + return valueKnown; } }