Browse Source

Added PathFullInfo interface.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3466 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 15 years ago
parent
commit
6706b44a3e
  1. 8
      prism/src/simulator/PathFull.java
  2. 114
      prism/src/simulator/PathFullInfo.java

8
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.

114
prism/src/simulator/PathFullInfo.java

@ -0,0 +1,114 @@
//==============================================================================
//
// Copyright (c) 2002-
// Authors:
// * Dave Parker <david.parker@comlab.ox.ac.uk> (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();
}
Loading…
Cancel
Save