Browse Source
Refactor parametric model construction to use an extension of ModelGenerator instead of reading specifically from a ModulesFile. Needs further refactoring.
Refactor parametric model construction to use an extension of ModelGenerator instead of reading specifically from a ModulesFile. Needs further refactoring.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11793 bbc10eb1-c90d-0410-af57-cb519fbb1720master
Dave Parker
9 years ago
6 changed files with 698 additions and 59 deletions
-
2prism/src/param/FunctionFactory.java
-
102prism/src/param/ModelBuilder.java
-
10prism/src/param/TransitionList.java
-
173prism/src/prism/ModelGeneratorSymbolic.java
-
5prism/src/prism/Prism.java
-
465prism/src/simulator/ModulesFileModelGeneratorSymbolic.java
@ -0,0 +1,173 @@ |
|||||
|
//============================================================================== |
||||
|
// |
||||
|
// Copyright (c) 2002- |
||||
|
// Authors: |
||||
|
// * Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford) |
||||
|
// * Nishan Kamaleson <nxk249@bham.ac.uk> (University of Birmingham) |
||||
|
// |
||||
|
//------------------------------------------------------------------------------ |
||||
|
// |
||||
|
// 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 prism; |
||||
|
|
||||
|
import java.util.List; |
||||
|
|
||||
|
import param.Function; |
||||
|
import param.FunctionFactory; |
||||
|
import param.ModelBuilder; |
||||
|
import parser.State; |
||||
|
import parser.ast.Expression; |
||||
|
|
||||
|
/** |
||||
|
* Interface for classes that generate a probabilistic model: |
||||
|
* given a particular model state (represented as a State object), |
||||
|
* they provide information about the outgoing transitions from that state. |
||||
|
*/ |
||||
|
public interface ModelGeneratorSymbolic extends ModelInfo |
||||
|
{ |
||||
|
/** |
||||
|
* Does the model have a single initial state? |
||||
|
*/ |
||||
|
public boolean hasSingleInitialState() throws PrismException; |
||||
|
|
||||
|
/** |
||||
|
* Get the initial states of the model. |
||||
|
* The returned list should contain fresh State objects that can be kept/modified. |
||||
|
*/ |
||||
|
public List<State> getInitialStates() throws PrismException; |
||||
|
|
||||
|
/** |
||||
|
* Get the initial state of the model, if there is just one, |
||||
|
* or the first of the initial states if there are more than one. |
||||
|
* The returned State object should be fresh, i.e. can be kept/modified. |
||||
|
*/ |
||||
|
public State getInitialState() throws PrismException; |
||||
|
|
||||
|
/** |
||||
|
* Explore a given state of the model. After a call to this method, |
||||
|
* the class should be able to respond to the various methods that are |
||||
|
* available to query the outgoing transitions from the current state. |
||||
|
* @param exploreState State to explore (generate transition information for) |
||||
|
*/ |
||||
|
public void exploreState(State exploreState) throws PrismException; |
||||
|
|
||||
|
/** |
||||
|
* Get the state that is currently being explored, i.e. the last one for which |
||||
|
* {@link #exploreState(State)} was called. Can return null if there is no such state. |
||||
|
*/ |
||||
|
public State getExploreState(); |
||||
|
|
||||
|
/** |
||||
|
* Get the number of nondeterministic choices in the current state. |
||||
|
*/ |
||||
|
public int getNumChoices() throws PrismException; |
||||
|
|
||||
|
/** |
||||
|
* Get the total number of transitions in the current state. |
||||
|
*/ |
||||
|
public int getNumTransitions() throws PrismException; |
||||
|
|
||||
|
/** |
||||
|
* Get the number of transitions in the {@code i}th nondeterministic choice. |
||||
|
* @param i Index of the nondeterministic choice |
||||
|
*/ |
||||
|
public int getNumTransitions(int i) throws PrismException; |
||||
|
|
||||
|
/** |
||||
|
* Get the action label of a transition, specified by its index. |
||||
|
* The label can be any Object, but will often be treated as a string, so it should at least |
||||
|
* have a meaningful toString() method implemented. Absence of an action label is denoted by null. |
||||
|
* Note: For most types of models, the action label will be the same for all transitions within |
||||
|
* the same nondeterministic choice, so it is better to query the action by choice, not transition. |
||||
|
*/ |
||||
|
public Object getTransitionAction(int i) throws PrismException; |
||||
|
|
||||
|
/** |
||||
|
* Get the action label of a transition within a choice, specified by its index/offset. |
||||
|
* The label can be any Object, but will often be treated as a string, so it should at least |
||||
|
* have a meaningful toString() method implemented. Absence of an action label is denoted by null. |
||||
|
* Note: For most types of models, the action label will be the same for all transitions within |
||||
|
* the same nondeterministic choice (i.e. for each different value of {@code offset}), |
||||
|
* but for Markov chains this may not necessarily be the case. |
||||
|
*/ |
||||
|
public Object getTransitionAction(int i, int offset) throws PrismException; |
||||
|
|
||||
|
/** |
||||
|
* Get the action label of a choice, specified by its index. |
||||
|
* The label can be any Object, but will often be treated as a string, so it should at least |
||||
|
* have a meaningful toString() method implemented. Absence of an action label is denoted by null. |
||||
|
* Note: If the model has different actions for different transitions within a choice |
||||
|
* (as can be the case for Markov chains), this method returns the action for the first transition. |
||||
|
* So, this method is essentially equivalent to {@code getTransitionAction(i, 0)}. |
||||
|
*/ |
||||
|
public Object getChoiceAction(int i) throws PrismException; |
||||
|
|
||||
|
/** |
||||
|
* Get the probability/rate of a transition within a choice, specified by its index/offset. |
||||
|
* @param i Index of the nondeterministic choice |
||||
|
* @param offset Index of the transition within the choice |
||||
|
*/ |
||||
|
public double getTransitionProbability(int i, int offset) throws PrismException; |
||||
|
|
||||
|
/** |
||||
|
* Get the target (as a new State object) of a transition within a choice, specified by its index/offset. |
||||
|
* @param i Index of the nondeterministic choice |
||||
|
* @param offset Index of the transition within the choice |
||||
|
*/ |
||||
|
public State computeTransitionTarget(int i, int offset) throws PrismException; |
||||
|
|
||||
|
/** |
||||
|
* Is label {@code label} true in the state currently being explored? |
||||
|
* @param label The name of the label to check |
||||
|
*/ |
||||
|
public boolean isLabelTrue(String label) throws PrismException; |
||||
|
|
||||
|
/** |
||||
|
* Is the {@code i}th label of the model true in the state currently being explored? |
||||
|
* @param i The index of the label to check |
||||
|
*/ |
||||
|
public boolean isLabelTrue(int i) throws PrismException; |
||||
|
|
||||
|
/** |
||||
|
* Get the state reward of the {@code r}th reward structure for state {@code state}. |
||||
|
* @param r The index of the reward structure to use |
||||
|
* @param state The state in which to evaluate the rewards |
||||
|
*/ |
||||
|
public double getStateReward(int r, State state) throws PrismException; |
||||
|
|
||||
|
/** |
||||
|
* Get the state-action reward of the {@code r}th reward structure for state {@code state} |
||||
|
* and action {@code action{. |
||||
|
* @param r The index of the reward structure to use |
||||
|
* @param state The state in which to evaluate the rewards |
||||
|
* @param action The outgoing action label |
||||
|
*/ |
||||
|
public double getStateActionReward(int r, State state, Object action) throws PrismException; |
||||
|
|
||||
|
// Extra methods for symbolic interface (bit of a hack for now: |
||||
|
// we assume some methods do not need to be implemented, e.g. getTransitionProbability, |
||||
|
// and and some new ones to replace them, e.g. getTransitionProbabilityFunction |
||||
|
|
||||
|
public void setSymbolic(ModelBuilder modelBuilder, FunctionFactory functionFactory); |
||||
|
|
||||
|
public Expression getUnknownConstantDefinition(String name) throws PrismException; |
||||
|
|
||||
|
public Function getTransitionProbabilityFunction(int i, int offset) throws PrismException; |
||||
|
} |
||||
@ -0,0 +1,465 @@ |
|||||
|
package simulator; |
||||
|
|
||||
|
import java.util.ArrayList; |
||||
|
import java.util.List; |
||||
|
|
||||
|
import param.Function; |
||||
|
import param.FunctionFactory; |
||||
|
import param.ModelBuilder; |
||||
|
import param.SymbolicEngine; |
||||
|
import parser.State; |
||||
|
import parser.Values; |
||||
|
import parser.VarList; |
||||
|
import parser.ast.ConstantList; |
||||
|
import parser.ast.Expression; |
||||
|
import parser.ast.LabelList; |
||||
|
import parser.ast.ModulesFile; |
||||
|
import parser.ast.RewardStruct; |
||||
|
import parser.type.Type; |
||||
|
import prism.DefaultModelGenerator; |
||||
|
import prism.ModelGeneratorSymbolic; |
||||
|
import prism.ModelType; |
||||
|
import prism.PrismComponent; |
||||
|
import prism.PrismException; |
||||
|
import prism.PrismLangException; |
||||
|
|
||||
|
public class ModulesFileModelGeneratorSymbolic extends DefaultModelGenerator implements ModelGeneratorSymbolic |
||||
|
{ |
||||
|
// Parent PrismComponent (logs, settings etc.) |
||||
|
protected PrismComponent parent; |
||||
|
|
||||
|
// PRISM model info |
||||
|
/** The original modules file (might have unresolved constants) */ |
||||
|
private ModulesFile originalModulesFile; |
||||
|
/** The modules file used for generating (has no unresolved constants after {@code initialise}) */ |
||||
|
private ModulesFile modulesFile; |
||||
|
private ModelType modelType; |
||||
|
private Values mfConstants; |
||||
|
private VarList varList; |
||||
|
private LabelList labelList; |
||||
|
private List<String> labelNames; |
||||
|
|
||||
|
// Model exploration info |
||||
|
|
||||
|
// State currently being explored |
||||
|
private State exploreState; |
||||
|
// Updater object for model |
||||
|
//protected Updater updater; |
||||
|
protected SymbolicEngine engine; |
||||
|
// List of currently available transitions |
||||
|
protected param.TransitionList transitionList; |
||||
|
// Has the transition list been built? |
||||
|
protected boolean transitionListBuilt; |
||||
|
|
||||
|
// Symbolic stuff |
||||
|
boolean symbolic = false; |
||||
|
protected ModelBuilder modelBuilder; |
||||
|
protected FunctionFactory functionFactory; |
||||
|
|
||||
|
/** |
||||
|
* Build a ModulesFileModelGenerator for a particular PRISM model, represented by a ModuleFile instance. |
||||
|
* @param modulesFile The PRISM model |
||||
|
*/ |
||||
|
public ModulesFileModelGeneratorSymbolic(ModulesFile modulesFile) throws PrismException |
||||
|
{ |
||||
|
this(modulesFile, null); |
||||
|
} |
||||
|
|
||||
|
/** |
||||
|
* Build a ModulesFileModelGenerator for a particular PRISM model, represented by a ModuleFile instance. |
||||
|
* @param modulesFile The PRISM model |
||||
|
*/ |
||||
|
public ModulesFileModelGeneratorSymbolic(ModulesFile modulesFile, PrismComponent parent) throws PrismException |
||||
|
{ |
||||
|
this.parent = parent; |
||||
|
|
||||
|
// No support for PTAs yet |
||||
|
if (modulesFile.getModelType() == ModelType.PTA) { |
||||
|
throw new PrismException("Sorry - the simulator does not currently support PTAs"); |
||||
|
} |
||||
|
// No support for system...endsystem yet |
||||
|
if (modulesFile.getSystemDefn() != null) { |
||||
|
throw new PrismException("Sorry - the simulator does not currently handle the system...endsystem construct"); |
||||
|
} |
||||
|
|
||||
|
// Store basic model info |
||||
|
this.modulesFile = modulesFile; |
||||
|
this.originalModulesFile = modulesFile; |
||||
|
modelType = modulesFile.getModelType(); |
||||
|
|
||||
|
// If there are no constants to define, go ahead and initialise; |
||||
|
// Otherwise, setSomeUndefinedConstants needs to be called when the values are available |
||||
|
mfConstants = modulesFile.getConstantValues(); |
||||
|
if (mfConstants != null) { |
||||
|
initialise(); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
/** |
||||
|
* (Re-)Initialise the class ready for model exploration |
||||
|
* (can only be done once any constants needed have been provided) |
||||
|
*/ |
||||
|
private void initialise() throws PrismLangException |
||||
|
{ |
||||
|
// Evaluate constants on (a copy) of the modules file, insert constant values |
||||
|
// Note that we don't optimise expressions since this can create some round-off issues |
||||
|
modulesFile = (ModulesFile) modulesFile.deepCopy().replaceConstants(mfConstants); |
||||
|
|
||||
|
// Get info |
||||
|
varList = modulesFile.createVarList(); |
||||
|
labelList = modulesFile.getLabelList(); |
||||
|
labelNames = labelList.getLabelNames(); |
||||
|
|
||||
|
// Create data structures for exploring model |
||||
|
//updater = new Updater(modulesFile, varList, parent); |
||||
|
//transitionList = new TransitionList(); |
||||
|
engine = new SymbolicEngine(modulesFile, modelBuilder, functionFactory); |
||||
|
transitionListBuilt = false; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public void setSymbolic(ModelBuilder modelBuilder, FunctionFactory functionFactory) |
||||
|
{ |
||||
|
symbolic = true; |
||||
|
this.modelBuilder = modelBuilder; |
||||
|
this.functionFactory = functionFactory; |
||||
|
//updater.setSymbolic(modelBuilder, functionFactory); |
||||
|
// TODO: created twice |
||||
|
engine = new SymbolicEngine(modulesFile, modelBuilder, functionFactory); |
||||
|
} |
||||
|
|
||||
|
// Methods for ModelInfo interface |
||||
|
|
||||
|
@Override |
||||
|
public ModelType getModelType() |
||||
|
{ |
||||
|
return modelType; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public void setSomeUndefinedConstants(Values someValues) throws PrismException |
||||
|
{ |
||||
|
// We start again with a copy of the original modules file |
||||
|
// and set the constants in the copy. |
||||
|
// As {@code initialise()} can replace references to constants |
||||
|
// with the concrete values in modulesFile, this ensures that we |
||||
|
// start again at a place where references to constants have not |
||||
|
// yet been replaced. |
||||
|
modulesFile = (ModulesFile) originalModulesFile.deepCopy(); |
||||
|
modulesFile.setSomeUndefinedConstants(someValues); |
||||
|
mfConstants = modulesFile.getConstantValues(); |
||||
|
initialise(); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public Values getConstantValues() |
||||
|
{ |
||||
|
return mfConstants; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public boolean containsUnboundedVariables() |
||||
|
{ |
||||
|
return modulesFile.containsUnboundedVariables(); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public int getNumVars() |
||||
|
{ |
||||
|
return modulesFile.getNumVars(); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public List<String> getVarNames() |
||||
|
{ |
||||
|
return modulesFile.getVarNames(); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public List<Type> getVarTypes() |
||||
|
{ |
||||
|
return modulesFile.getVarTypes(); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public int getNumLabels() |
||||
|
{ |
||||
|
return labelList.size(); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public List<String> getLabelNames() |
||||
|
{ |
||||
|
return labelNames; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public String getLabelName(int i) throws PrismException |
||||
|
{ |
||||
|
return labelList.getLabelName(i); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public int getLabelIndex(String label) |
||||
|
{ |
||||
|
return labelList.getLabelIndex(label); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public int getNumRewardStructs() |
||||
|
{ |
||||
|
return modulesFile.getNumRewardStructs(); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public List<String> getRewardStructNames() |
||||
|
{ |
||||
|
return modulesFile.getRewardStructNames(); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public int getRewardStructIndex(String name) |
||||
|
{ |
||||
|
return modulesFile.getRewardStructIndex(name); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public RewardStruct getRewardStruct(int i) |
||||
|
{ |
||||
|
return modulesFile.getRewardStruct(i); |
||||
|
} |
||||
|
|
||||
|
// Methods for ModelGenerator interface |
||||
|
|
||||
|
@Override |
||||
|
public boolean hasSingleInitialState() throws PrismException |
||||
|
{ |
||||
|
return modulesFile.getInitialStates() == null; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public State getInitialState() throws PrismException |
||||
|
{ |
||||
|
if (modulesFile.getInitialStates() == null) { |
||||
|
return modulesFile.getDefaultInitialState(); |
||||
|
} else { |
||||
|
// Inefficient but probably won't be called |
||||
|
return getInitialStates().get(0); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public List<State> getInitialStates() throws PrismException |
||||
|
{ |
||||
|
List<State> initStates = new ArrayList<State>(); |
||||
|
// Easy (normal) case: just one initial state |
||||
|
if (modulesFile.getInitialStates() == null) { |
||||
|
State state = modulesFile.getDefaultInitialState(); |
||||
|
initStates.add(state); |
||||
|
} |
||||
|
// Otherwise, there may be multiple initial states |
||||
|
// For now, we handle this is in a very inefficient way |
||||
|
else { |
||||
|
Expression init = modulesFile.getInitialStates(); |
||||
|
List<State> allPossStates = varList.getAllStates(); |
||||
|
for (State possState : allPossStates) { |
||||
|
if (init.evaluateBoolean(modulesFile.getConstantValues(), possState)) { |
||||
|
initStates.add(possState); |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
return initStates; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public void exploreState(State exploreState) throws PrismException |
||||
|
{ |
||||
|
this.exploreState = exploreState; |
||||
|
transitionListBuilt = false; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public State getExploreState() |
||||
|
{ |
||||
|
return exploreState; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public int getNumChoices() throws PrismException |
||||
|
{ |
||||
|
return getTransitionList().getNumChoices(); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public int getNumTransitions() throws PrismException |
||||
|
{ |
||||
|
return getTransitionList().getNumTransitions(); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public int getNumTransitions(int index) throws PrismException |
||||
|
{ |
||||
|
return getTransitionList().getChoice(index).size(); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public String getTransitionAction(int index) throws PrismException |
||||
|
{ |
||||
|
int a = getTransitionList().getTransitionModuleOrActionIndex(index); |
||||
|
return a < 0 ? null : modulesFile.getSynch(a - 1); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public String getTransitionAction(int index, int offset) throws PrismException |
||||
|
{ |
||||
|
param.TransitionList transitions = getTransitionList(); |
||||
|
int a = transitions.getTransitionModuleOrActionIndex(transitions.getTotalIndexOfTransition(index, offset)); |
||||
|
return a < 0 ? null : modulesFile.getSynch(a - 1); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public String getChoiceAction(int index) throws PrismException |
||||
|
{ |
||||
|
param.TransitionList transitions = getTransitionList(); |
||||
|
int a = transitions.getChoiceModuleOrActionIndex(index); |
||||
|
return a < 0 ? null : modulesFile.getSynch(a - 1); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public double getTransitionProbability(int index, int offset) throws PrismException |
||||
|
{ |
||||
|
throw new UnsupportedOperationException(); |
||||
|
/*param.TransitionList transitions = getTransitionList(); |
||||
|
return transitions.getChoice(index).getProbability(offset);*/ |
||||
|
} |
||||
|
|
||||
|
//@Override |
||||
|
public double getTransitionProbability(int index) throws PrismException |
||||
|
{ |
||||
|
throw new UnsupportedOperationException(); |
||||
|
/*param.TransitionList transitions = getTransitionList(); |
||||
|
return transitions.getTransitionProbability(index);*/ |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public Function getTransitionProbabilityFunction(int index, int offset) throws PrismException |
||||
|
{ |
||||
|
param.TransitionList transitions = getTransitionList(); |
||||
|
return transitions.getChoice(index).getProbability(offset); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public State computeTransitionTarget(int index, int offset) throws PrismException |
||||
|
{ |
||||
|
return getTransitionList().getChoice(index).computeTarget(offset, exploreState); |
||||
|
} |
||||
|
|
||||
|
//@Override |
||||
|
public State computeTransitionTarget(int index) throws PrismException |
||||
|
{ |
||||
|
return getTransitionList().computeTransitionTarget(index, exploreState); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public boolean isLabelTrue(int i) throws PrismException |
||||
|
{ |
||||
|
Expression expr = labelList.getLabel(i); |
||||
|
return expr.evaluateBoolean(exploreState); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public double getStateReward(int r, State state) throws PrismException |
||||
|
{ |
||||
|
RewardStruct rewStr = modulesFile.getRewardStruct(r); |
||||
|
int n = rewStr.getNumItems(); |
||||
|
double d = 0; |
||||
|
for (int i = 0; i < n; i++) { |
||||
|
if (!rewStr.getRewardStructItem(i).isTransitionReward()) { |
||||
|
Expression guard = rewStr.getStates(i); |
||||
|
if (guard.evaluateBoolean(modulesFile.getConstantValues(), state)) { |
||||
|
double rew = rewStr.getReward(i).evaluateDouble(modulesFile.getConstantValues(), state); |
||||
|
if (Double.isNaN(rew)) |
||||
|
throw new PrismLangException("Reward structure evaluates to NaN at state " + state, rewStr.getReward(i)); |
||||
|
d += rew; |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
return d; |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public double getStateActionReward(int r, State state, Object action) throws PrismException |
||||
|
{ |
||||
|
RewardStruct rewStr = modulesFile.getRewardStruct(r); |
||||
|
int n = rewStr.getNumItems(); |
||||
|
double d = 0; |
||||
|
for (int i = 0; i < n; i++) { |
||||
|
if (rewStr.getRewardStructItem(i).isTransitionReward()) { |
||||
|
Expression guard = rewStr.getStates(i); |
||||
|
String cmdAction = rewStr.getSynch(i); |
||||
|
if (action == null ? (cmdAction.isEmpty()) : action.equals(cmdAction)) { |
||||
|
if (guard.evaluateBoolean(modulesFile.getConstantValues(), state)) { |
||||
|
double rew = rewStr.getReward(i).evaluateDouble(modulesFile.getConstantValues(), state); |
||||
|
if (Double.isNaN(rew)) |
||||
|
throw new PrismLangException("Reward structure evaluates to NaN at state " + state, rewStr.getReward(i)); |
||||
|
d += rew; |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
return d; |
||||
|
} |
||||
|
|
||||
|
//@Override |
||||
|
public void calculateStateRewards(State state, double[] store) throws PrismLangException |
||||
|
{ |
||||
|
// TODO updater.calculateStateRewards(state, store); |
||||
|
} |
||||
|
|
||||
|
@Override |
||||
|
public VarList createVarList() |
||||
|
{ |
||||
|
return varList; |
||||
|
} |
||||
|
|
||||
|
// Miscellaneous (unused?) methods |
||||
|
|
||||
|
//@Override |
||||
|
public void getRandomInitialState(RandomNumberGenerator rng, State initialState) throws PrismException |
||||
|
{ |
||||
|
if (modulesFile.getInitialStates() == null) { |
||||
|
initialState.copy(modulesFile.getDefaultInitialState()); |
||||
|
} else { |
||||
|
throw new PrismException("Random choice of multiple initial states not yet supported"); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
// Local utility methods |
||||
|
|
||||
|
/** |
||||
|
* Returns the current list of available transitions, generating it first if this has not yet been done. |
||||
|
*/ |
||||
|
private param.TransitionList getTransitionList() throws PrismException |
||||
|
{ |
||||
|
// Compute the current transition list, if required |
||||
|
if (!transitionListBuilt) { |
||||
|
//updater.calculateTransitions(exploreState, transitionList); |
||||
|
transitionList = engine.calculateTransitions(exploreState, true); |
||||
|
transitionListBuilt = true; |
||||
|
} |
||||
|
return transitionList; |
||||
|
} |
||||
|
|
||||
|
// ModelGeneratorSymbolic |
||||
|
|
||||
|
@Override |
||||
|
public Expression getUnknownConstantDefinition(String name) throws PrismException |
||||
|
{ |
||||
|
ConstantList constantList = modulesFile.getConstantList(); |
||||
|
int i = constantList.getConstantIndex(name); |
||||
|
if (i == -1) { |
||||
|
throw new PrismException("Unknown constant " + name); |
||||
|
} |
||||
|
return constantList.getConstant(i); |
||||
|
} |
||||
|
} |
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue