s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Simulator tidies. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1991 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 16 years ago
parent
fcb2d8890a
commit
04b7b65a42
3 changed files with 107 additions and 185 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 3
      prism/src/simulator/Choice.java
  2. 101
      prism/src/simulator/SimulatorEngine.java
  3. 188
      prism/src/simulator/Updater.java

3
prism/src/simulator/Choice.java
View File

@ -27,11 +27,8 @@
package simulator;
import parser.*;
import parser.ast.*;
import prism.*;
import java.util.*;
public interface Choice
{
// public void setAction(String action);

101
prism/src/simulator/SimulatorEngine.java
View File

@ -98,9 +98,6 @@ public class SimulatorEngine
private VarList varList;
private int numVars;
private Map<String, Integer> varIndices;
// Synchronising action info
private Vector<String> synchs;
private int numSynchs;
// Constant definitions from model file
private Values mfConstants;
@ -109,22 +106,18 @@ public class SimulatorEngine
private List<Expression> properties;
private List<Sampler> propertySamplers;
// Current path info
protected Path path;
protected boolean onTheFly;
// TODO: remove these now can get from path?
protected State previousState;
protected State currentState;
// TODO: just temp storage?
// (if so, remove 'current', 'prev' from names?)
protected double currentStateRewards[];
protected double previousTransitionRewards[];
// Temporary storage for manipulating states/rewards
protected State tmpState;
protected double tmpStateRewards[];
protected double tmpTransitionRewards[];
// List of currently available transitions
protected TransitionList transitionList;
// Current path info
protected Path path;
protected boolean onTheFly;
// Updater object for model
protected Updater updater;
@ -205,22 +198,22 @@ public class SimulatorEngine
*/
public void initialisePath(State initialState) throws PrismException
{
// Store a copy of passed in state
// Store a temporary copy of passed in state
if (initialState != null) {
currentState.copy(new State(initialState));
tmpState.copy(new State(initialState));
}
// Or pick a random one
else {
throw new PrismException("Random initial start state not yet supported");
}
updater.calculateStateRewards(currentState, currentStateRewards);
updater.calculateStateRewards(tmpState, tmpStateRewards);
// Initialise stored path if necessary
path.initialise(currentState, currentStateRewards);
path.initialise(tmpState, tmpStateRewards);
// Reset and then update samplers for any loaded properties
resetSamplers();
updateSamplers();
// Generate updates for initial state
updater.calculateTransitions(currentState, transitionList);
updater.calculateTransitions(tmpState, transitionList);
}
/**
@ -269,7 +262,7 @@ public class SimulatorEngine
numChoices = transitionList.getNumChoices();
if (numChoices == 0)
return false;
//throw new PrismException("Deadlock found at state " + currentState.toString(modulesFile));
//throw new PrismException("Deadlock found at state " + path.getCurrentState().toString(modulesFile));
switch (modelType) {
case DTMC:
@ -357,16 +350,10 @@ public class SimulatorEngine
}
// Back track in path
((PathFull) path).backtrack(step);
// Update previous/current state info
if (step == 0)
previousState.clear();
else
previousState.copy(path.getPreviousState());
currentState.copy(path.getCurrentState());
// Recompute samplers for any loaded properties
recomputeSamplers();
// Generate updates for new current state
updater.calculateTransitions(currentState, transitionList);
updater.calculateTransitions(path.getCurrentState(), transitionList);
}
/**
@ -412,10 +399,6 @@ public class SimulatorEngine
}
// Modify path
((PathFull) path).removePrecedingStates(step);
// Update previous state info (if required)
// (No need to update current state info)
if (path.size() == 1)
previousState.clear();
// Recompute samplers for any loaded properties
recomputeSamplers();
// (No need to re-generate updates for new current state)
@ -438,7 +421,7 @@ public class SimulatorEngine
*/
public void computeTransitionsForCurrentState() throws PrismException
{
updater.calculateTransitions(currentState, transitionList);
updater.calculateTransitions(path.getCurrentState(), transitionList);
}
// ------------------------------------------------------------------------------
@ -613,18 +596,13 @@ public class SimulatorEngine
varIndices.put(varList.getName(i), i);
}
// Get list of synchronising actions
synchs = modulesFile.getSynchs();
numSynchs = synchs.size();
// Evaluate constants and optimise (a copy of) modules file for simulation
modulesFile = (ModulesFile) modulesFile.deepCopy().replaceConstants(mfConstants).simplify();
// Create state/transition storage
previousState = new State(numVars);
currentState = new State(numVars);
currentStateRewards = new double[modulesFile.getNumRewardStructs()];
previousTransitionRewards = new double[modulesFile.getNumRewardStructs()];
// Create temporary state/transition storage
tmpState = new State(numVars);
tmpStateRewards = new double[modulesFile.getNumRewardStructs()];
tmpTransitionRewards = new double[modulesFile.getNumRewardStructs()];
transitionList = new TransitionList();
// Create updater for model
@ -652,17 +630,16 @@ public class SimulatorEngine
if (!onTheFly && index == -1)
index = transitionList.getTotalIndexOfTransition(i, offset);
// Compute its transition rewards
updater.calculateTransitionRewards(currentState, choice, previousTransitionRewards);
// Remember last state and compute next one (and its state rewards)
previousState.copy(currentState);
choice.computeTarget(offset, previousState, currentState);
updater.calculateStateRewards(currentState, currentStateRewards);
updater.calculateTransitionRewards(path.getCurrentState(), choice, tmpTransitionRewards);
// Compute next state (and its state rewards)
choice.computeTarget(offset, path.getCurrentState(), tmpState);
updater.calculateStateRewards(tmpState, tmpStateRewards);
// Update path
path.addStep(index, choice.getModuleOrActionIndex(), previousTransitionRewards, currentState, currentStateRewards);
path.addStep(index, choice.getModuleOrActionIndex(), tmpTransitionRewards, tmpState, tmpStateRewards);
// Update samplers for any loaded properties
updateSamplers();
// Generate updates for next state
updater.calculateTransitions(currentState, transitionList);
updater.calculateTransitions(tmpState, transitionList);
}
/**
@ -684,17 +661,16 @@ public class SimulatorEngine
if (!onTheFly && index == -1)
index = transitionList.getTotalIndexOfTransition(i, offset);
// Compute its transition rewards
updater.calculateTransitionRewards(currentState, choice, previousTransitionRewards);
// Remember last state and compute next one (and its state rewards)
previousState.copy(currentState);
choice.computeTarget(offset, previousState, currentState);
updater.calculateStateRewards(currentState, currentStateRewards);
updater.calculateTransitionRewards(path.getCurrentState(), choice, tmpTransitionRewards);
// Compute next state (and its state rewards)
choice.computeTarget(offset, path.getCurrentState(), tmpState);
updater.calculateStateRewards(tmpState, tmpStateRewards);
// Update path
path.addStep(time, index, choice.getModuleOrActionIndex(), previousTransitionRewards, currentState, currentStateRewards);
path.addStep(time, index, choice.getModuleOrActionIndex(), tmpTransitionRewards, tmpState, tmpStateRewards);
// Update samplers for any loaded properties
updateSamplers();
// Generate updates for next state
updater.calculateTransitions(currentState, transitionList);
updater.calculateTransitions(tmpState, transitionList);
}
/**
@ -774,15 +750,6 @@ public class SimulatorEngine
return varList.getIndex(name);
}
/**
* Returns the index of an action name, as stored by the simulator for the current model.
* Returns -1 if the action name does not exist.
*/
public int getIndexOfAction(String name)
{
return synchs.indexOf(name);
}
// ------------------------------------------------------------------------------
// Querying of current state and its available choices/transitions
// ------------------------------------------------------------------------------
@ -860,7 +827,7 @@ public class SimulatorEngine
*/
public State computeTransitionTarget(int i, int offset) throws PrismLangException
{
return transitionList.getChoice(i).computeTarget(offset, currentState);
return transitionList.getChoice(i).computeTarget(offset, path.getCurrentState());
}
/**
@ -868,7 +835,7 @@ public class SimulatorEngine
*/
public State computeTransitionTarget(int index) throws PrismLangException
{
return transitionList.computeTransitionTarget(index, currentState);
return transitionList.computeTransitionTarget(index, path.getCurrentState());
}
// ------------------------------------------------------------------------------

188
prism/src/simulator/Updater.java
View File

@ -195,8 +195,81 @@ public class Updater
//System.out.println(transitionList);
}
/**
* Calculate the state rewards for a given state.
* @param state The state to compute rewards for
* @param store An array in which to store the rewards
*/
public void calculateStateRewards(State state, double[] store) throws PrismLangException
{
int i, j, n;
double d;
RewardStruct rw;
for (i = 0; i < numRewardStructs; i++) {
rw = modulesFile.getRewardStruct(i);
n = rw.getNumItems();
d = 0.0;
for (j = 0; j < n; j++) {
if (!rw.getRewardStructItem(j).isTransitionReward())
if (rw.getStates(j).evaluateBoolean(state))
d += rw.getReward(j).evaluateDouble(state);
}
store[i] = d;
}
}
/**
* Calculate the transition rewards for a given state and outgoing choice.
* @param state The state to compute rewards for
* @param ch The choice from the state to compute rewards for
* @param store An array in which to store the rewards
*/
public void calculateTransitionRewards(State state, Choice ch, double[] store) throws PrismLangException
{
int i, j, n;
double d;
RewardStruct rw;
for (i = 0; i < numRewardStructs; i++) {
rw = modulesFile.getRewardStruct(i);
n = rw.getNumItems();
d = 0.0;
for (j = 0; j < n; j++) {
if (rw.getRewardStructItem(j).isTransitionReward())
if (rw.getRewardStructItem(j).getSynchIndex() == Math.max(0, ch.getModuleOrActionIndex()))
if (rw.getStates(j).evaluateBoolean(state))
d += rw.getReward(j).evaluateDouble(state);
}
store[i] = d;
}
}
// Private helpers
/**
* Determine the enabled updates for the 'm'th module from (global) state 'state'.
* Update information in updateLists, enabledSynchs and enabledModules.
* @param m The module index
* @param state State from which to explore
*/
private void calculateUpdatesForModule(int m, State state) throws PrismLangException
{
Module module;
Command command;
int i, j, n;
module = modulesFile.getModule(m);
n = module.getNumCommands();
for (i = 0; i < n; i++) {
command = module.getCommand(i);
if (command.getGuard().evaluateBoolean(state)) {
j = command.getSynchIndex();
updateLists.get(m).get(j).add(command.getUpdates());
enabledSynchs.set(j);
enabledModules[j].set(m);
}
}
}
/**
* Create a new Choice object (currently ChoiceListFlexi) based on an Updates object
* and a (global) state. If appropriate, check probabilities sum to 1 too.
@ -246,119 +319,4 @@ public class Updater
// Build product with existing
ch.productWith(chNew);
}
/**
* Determine the enabled updates for the 'm'th module from (global) state 'state'.
* Update information in updateLists, enabledSynchs and enabledModules.
* @param m The module index
* @param state State from which to explore
*/
private void calculateUpdatesForModule(int m, State state) throws PrismLangException
{
Module module;
Command command;
int i, j, n;
module = modulesFile.getModule(m);
n = module.getNumCommands();
for (i = 0; i < n; i++) {
command = module.getCommand(i);
if (command.getGuard().evaluateBoolean(state)) {
j = command.getSynchIndex();
updateLists.get(m).get(j).add(command.getUpdates());
enabledSynchs.set(j);
enabledModules[j].set(m);
}
}
}
/*private Choice calculateTransitionsForUpdates(Updates ups, State state) throws PrismLangException
{
int i, n;
State newState;
n = ups.getNumUpdates();
if (n == 1) {
ChoiceSingleton chSingle = null;
chSingle = new ChoiceSingleton();
newState = calculateTransitionsForUpdate(ups.getUpdate(0), state);
chSingle.setTarget(newState);
chSingle.setProbability(ups.getProbabilityInState(0, state));
return chSingle;
} else {
ChoiceList chList;
chList = new ChoiceList(n);
for (i = 0; i < n; i++) {
newState = calculateTransitionsForUpdate(ups.getUpdate(i), state);
chList.addTarget(newState);
chList.addProbability(ups.getProbabilityInState(i, state));
}
return chList;
}
}*/
// TODO: do we really need to evaluate dest State at this point?
// maybe just store pointer to Update object for efficiency
private State calculateTransitionsForUpdate(Update up, State state) throws PrismLangException
{
State newState;
int i, n;
// Copy current state, then apply updates
newState = new State(state);
n = up.getNumElements();
for (i = 0; i < n; i++) {
newState.varValues[up.getVarIndex(i)] = up.getExpression(i).evaluate(state);
}
return newState;
}
/**
* Calculate the state rewards for a given state.
* @param state The state to compute rewards for
* @param store An array in which to store the rewards
*/
public void calculateStateRewards(State state, double[] store) throws PrismLangException
{
int i, j, n;
double d;
RewardStruct rw;
for (i = 0; i < numRewardStructs; i++) {
rw = modulesFile.getRewardStruct(i);
n = rw.getNumItems();
d = 0.0;
for (j = 0; j < n; j++) {
if (!rw.getRewardStructItem(j).isTransitionReward())
if (rw.getStates(j).evaluateBoolean(state))
d += rw.getReward(j).evaluateDouble(state);
}
store[i] = d;
}
}
/**
* Calculate the transition rewards for a given state and outgoing choice.
* @param state The state to compute rewards for
* @param ch The choice from the state to compute rewards for
* @param store An array in which to store the rewards
*/
public void calculateTransitionRewards(State state, Choice ch, double[] store) throws PrismLangException
{
int i, j, n;
double d;
RewardStruct rw;
for (i = 0; i < numRewardStructs; i++) {
rw = modulesFile.getRewardStruct(i);
n = rw.getNumItems();
d = 0.0;
for (j = 0; j < n; j++) {
if (rw.getRewardStructItem(j).isTransitionReward())
if (rw.getRewardStructItem(j).getSynchIndex() == Math.max(0, ch.getModuleOrActionIndex()))
if (rw.getStates(j).evaluateBoolean(state))
d += rw.getReward(j).evaluateDouble(state);
}
store[i] = d;
}
}
}
Write Preview
Loading…
Cancel
Save