diff --git a/prism/src/simulator/Path.java b/prism/src/simulator/Path.java new file mode 100644 index 00000000..2d6c0e53 --- /dev/null +++ b/prism/src/simulator/Path.java @@ -0,0 +1,107 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package simulator; + +import parser.State; + +/** + * Classes that store and manipulate a path though a model. + */ +public abstract class Path +{ + // MUTATORS + + /** + * Initialise the path with an initial state and rewards. + */ + public abstract void initialise(State initialState, double[] initialStateRewards); + + /** + * Add a step to the path. + */ + public abstract void addStep(int choice, String action, double[] transRewards, State newState, double[] newStateRewards); + + /** + * Add a timed step to the path. + */ + public abstract void addStep(double time, int choice, String action, double[] transRewards, State newState, double[] newStateRewards); + + // ACCESSORS + + /** + * Get the size of the path (number of steps; or number of states - 1). + */ + public abstract int size(); + + /** + * Get the previous state, i.e. the penultimate state of the current path. + */ + public abstract State getPreviousState(); + + /** + * Get the current state, i.e. the current final state of the path. + */ + public abstract State getCurrentState(); + + /** + * For paths with continuous-time info, get the total time elapsed so far + * (where zero time has been spent in the current (final) state). + */ + public abstract double getTimeSoFar(); + + /** + * For paths with continuous-time info, get the time spent in the previous state. + */ + public abstract double getTimeInPreviousState(); + + /** + * Get the total reward accumulated so far + * (includes reward for previous transition but no state reward for current (final) state). + * @param index Reward structure index + */ + public abstract double getRewardCumulatedSoFar(int index); + + /** + * Get the state reward for the previous state. + * (For continuous-time models, need to multiply this by time spent in the state.) + * @param index Reward structure index + */ + public abstract double getPreviousStateReward(int index); + + /** + * Get the transition reward for the transition between the previous and current states. + * @param index Reward structure index + */ + public abstract double getPreviousTransitionReward(int index); + + /** + * Get the state reward for the current state. + * (For continuous-time models, need to multiply this by time spent in the state.) + * @param index Reward structure index + */ + public abstract double getCurrentStateReward(int index); +} diff --git a/prism/src/simulator/sampler/SamplerBoundedUntilCont.java b/prism/src/simulator/sampler/SamplerBoundedUntilCont.java index ea2f31a7..870b2987 100644 --- a/prism/src/simulator/sampler/SamplerBoundedUntilCont.java +++ b/prism/src/simulator/sampler/SamplerBoundedUntilCont.java @@ -66,12 +66,13 @@ public class SamplerBoundedUntilCont extends SamplerBoolean public void update(Path path) throws PrismLangException { if (path.size() > 0) { - double time_so_far = path.getTimeSoFar(); - if (time_so_far > ub) { + double timeSoFar = path.getTimeSoFar(); + // As soon as upper time bound exceeded, we can decide + if (timeSoFar > ub) { // must take into account the possibility of missing lower bound // could have missed out evaluation of right - if (time_so_far - path.getTimeInPreviousState() <= lb) { + if (timeSoFar - path.getTimeInPreviousState() <= lb) { if (right.evaluateBoolean(path.getPreviousState())) { valueKnown = true; value = true; @@ -83,7 +84,7 @@ public class SamplerBoundedUntilCont extends SamplerBoolean valueKnown = true; value = false; } - } else if (time_so_far <= lb) { + } else if (timeSoFar <= lb) { if (!left.evaluateBoolean(path.getCurrentState())) { valueKnown = true; value = false; diff --git a/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java b/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java index ed64c5ec..5d0b4f90 100644 --- a/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java +++ b/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java @@ -62,23 +62,33 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean public void update(Path path) throws PrismLangException { int pathSize = path.size(); + // Upper bound exceeded if (pathSize > ub) { valueKnown = true; value = false; - } else if (pathSize < lb) { + } + // Lower bound not yet exceeded but LHS of until violated + // (no need to check RHS because too early) + else if (pathSize < lb) { if (!left.evaluateBoolean(path.getCurrentState())) { valueKnown = true; value = false; } - } else { + } + // Current time is between lower/upper bounds... + else { State currentState = path.getCurrentState(); + // Have we reached the target (i.e. RHS of until)? if (right.evaluateBoolean(currentState)) { valueKnown = true; value = true; - } else if (!left.evaluateBoolean(currentState)) { + } + // Or, if not, have we violated the LJS of the until? + else if (!left.evaluateBoolean(currentState)) { valueKnown = true; value = false; } + // Otherwise, don't know } } } diff --git a/prism/src/simulator/sampler/SamplerNext.java b/prism/src/simulator/sampler/SamplerNext.java index 472aeaca..fdcdd174 100644 --- a/prism/src/simulator/sampler/SamplerNext.java +++ b/prism/src/simulator/sampler/SamplerNext.java @@ -28,7 +28,6 @@ package simulator.sampler; import simulator.*; import prism.*; -import parser.*; import parser.ast.*; public class SamplerNext extends SamplerBoolean diff --git a/prism/src/simulator/sampler/SamplerUntil.java b/prism/src/simulator/sampler/SamplerUntil.java index ad5b6f92..dfcdc7bd 100644 --- a/prism/src/simulator/sampler/SamplerUntil.java +++ b/prism/src/simulator/sampler/SamplerUntil.java @@ -70,5 +70,6 @@ public class SamplerUntil extends SamplerBoolean valueKnown = true; value = false; } + // Otherwise, don't know } }