From 6706b44a3efd64d18b4deea6cd0f74f9bc12bdbe Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 13 Aug 2011 12:05:17 +0000 Subject: [PATCH] Added PathFullInfo interface. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3466 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/simulator/PathFull.java | 8 +- prism/src/simulator/PathFullInfo.java | 114 ++++++++++++++++++++++++++ 2 files changed, 119 insertions(+), 3 deletions(-) create mode 100644 prism/src/simulator/PathFullInfo.java diff --git a/prism/src/simulator/PathFull.java b/prism/src/simulator/PathFull.java index 5ebf9b35..c6fed9ea 100644 --- a/prism/src/simulator/PathFull.java +++ b/prism/src/simulator/PathFull.java @@ -38,7 +38,7 @@ import prism.PrismLog; * The full path is stored, i.e. all info at all steps. * State objects and arrays are copied for storage. */ -public class PathFull extends Path +public class PathFull extends Path implements PathFullInfo { // Model to which the path corresponds private ModulesFile modulesFile; @@ -204,7 +204,7 @@ public class PathFull extends Path loopDet.removePrecedingStates(this, step); } - // ACCESSORS (for Path) + // ACCESSORS (for Path (and some of PathFullInfo)) @Override public boolean continuousTime() @@ -284,7 +284,7 @@ public class PathFull extends Path return loopDet.loopEnd(); } - // ACCESSORS (additional) + // ACCESSORS (for PathFullInfo) /** * Get the state at a given step of the path. @@ -378,6 +378,8 @@ public class PathFull extends Path return steps.get(step).transitionRewards[rsi]; } + // Other methods + /** * Export path to a file. * @param log PrismLog to which the path should be exported to. diff --git a/prism/src/simulator/PathFullInfo.java b/prism/src/simulator/PathFullInfo.java new file mode 100644 index 00000000..4ec28405 --- /dev/null +++ b/prism/src/simulator/PathFullInfo.java @@ -0,0 +1,114 @@ +//============================================================================== +// +// 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; + +/** + * Interface for classes that provide (read) access to a path through a model. + */ +public interface PathFullInfo +{ + /** + * Get the size of the path (number of steps; or number of states - 1). + */ + public abstract int size(); + + /** + * Get the state at a given step of the path. + * @param step Step index (0 = initial state/step of path) + */ + public abstract State getState(int step); + + /** + * Get a state reward for the state at a given step of the path. + * @param step Step index (0 = initial state/step of path) + * @param rsi Reward structure index + */ + public abstract double getStateReward(int step, int rsi); + + /** + * Get the total time spent up until entering a given step of the path. + * @param step Step index (0 = initial state/step of path) + */ + public abstract double getCumulativeTime(int step); + + /** + * Get the total (state and transition) reward accumulated up until entering a given step of the path. + * @param step Step index (0 = initial state/step of path) + * @param rsi Reward structure index + */ + public abstract double getCumulativeReward(int step, int rsi); + + /** + * Get the time spent in a state at a given step of the path. + * @param step Step index (0 = initial state/step of path) + */ + public abstract double getTime(int step); + + /** + * Get the index of the choice taken for a given step. + * @param step Step index (0 = initial state/step of path) + */ + public abstract int getChoice(int step); + + /** + * Get the index i of the action taken for a given step. + * If i>0, then i-1 is the index of an action label (0-indexed) + * If i<0, then -i-1 is the index of a module (0-indexed) + * @param step Step index (0 = initial state/step of path) + */ + public abstract int getModuleOrActionIndex(int step); + + /** + * Get a string describing the action/module of a given step. + * @param step Step index (0 = initial state/step of path) + */ + public abstract String getModuleOrAction(int step); + + /** + * Get a transition reward associated with a given step. + * @param step Step index (0 = initial state/step of path) + * @param rsi Reward structure index + */ + public abstract double getTransitionReward(int step, int rsi); + + /** + * Does the path contain a deterministic loop? + */ + public abstract boolean isLooping(); + + /** + * What is the step index of the start of the deterministic loop, if it exists? + */ + public abstract int loopStart(); + + /** + * What is the step index of the end of the deterministic loop, if it exists? + */ + public abstract int loopEnd(); +}