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

Move methods from DefaultModelGenerator into default implementations within ModelGenerator interface.

master
Dave Parker 9 years ago
parent
675cb324dc
commit
4add8e1244
7 changed files with 152 additions and 363 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. 208
      prism/src/prism/DefaultModelGenerator.java
  2. 60
      prism/src/prism/ModelGenerator.java
  3. 124
      prism/src/prism/ModelGeneratorSymbolic.java
  4. 114
      prism/src/prism/ModelInfo.java
  5. 2
      prism/src/prism/TestModelGenerator.java
  6. 4
      prism/src/simulator/ModulesFileModelGenerator.java
  7. 3
      prism/src/simulator/ModulesFileModelGeneratorSymbolic.java

208
prism/src/prism/DefaultModelGenerator.java
View File

@ -27,213 +27,11 @@
package prism;
import java.util.ArrayList;
import java.util.Collections;
import java.util.List;
import parser.State;
import parser.Values;
import parser.ast.RewardStruct;
import parser.type.Type;
/**
* Default implementation of the {@link ModelGenerator} interface
* Default implementation of the {@link ModelGenerator} interface.
* Basically redundant since that interface now has default method implementations.
* Retained just for backwards compatibility.
*/
public abstract class DefaultModelGenerator implements ModelGenerator
{
// Methods for ModelInfo interface
@Override
public abstract ModelType getModelType();
@Override
public void setSomeUndefinedConstants(Values someValues) throws PrismException
{
if (someValues != null && someValues.getNumValues() > 0)
throw new PrismException("This model has no constants to set");
}
@Override
public Values getConstantValues()
{
// Empty values
return new Values();
}
@Override
public boolean containsUnboundedVariables()
{
return false;
}
@Override
public abstract int getNumVars();
@Override
public abstract List<String> getVarNames();
@Override
public int getVarIndex(String name)
{
return getVarNames().indexOf(name);
}
@Override
public String getVarName(int i)
{
return getVarNames().get(i);
}
@Override
public abstract List<Type> getVarTypes();
@Override
public int getNumLabels()
{
return 0;
}
@Override
public abstract List<String> getLabelNames();
@Override
public int getLabelIndex(String name)
{
return getLabelNames().indexOf(name);
}
@Override
public String getLabelName(int i) throws PrismException
{
try {
return getLabelNames().get(i);
} catch (IndexOutOfBoundsException e) {
throw new PrismException("Label number \"" + i + "\" not defined");
}
}
@Override
public int getNumRewardStructs()
{
return getRewardStructNames().size();
}
@Override
public List<String> getRewardStructNames()
{
// No reward structures by default
return Collections.emptyList();
}
@Override
public int getRewardStructIndex(String name)
{
return getRewardStructNames().indexOf(name);
}
@Override
public RewardStruct getRewardStruct(int i)
{
// No reward structures by default
return null;
}
@Override
public boolean rewardStructHasTransitionRewards(int i)
{
// By default, assume that any reward structures that do exist may have transition rewards
return true;
}
// Methods for ModelGenerator interface
public boolean hasSingleInitialState() throws PrismException
{
// Default to the case of a single initial state
return true;
}
@Override
public List<State> getInitialStates() throws PrismException
{
// Default to the case of a single initial state
ArrayList<State> initStates = new ArrayList<State>();
initStates.add(getInitialState());
return initStates;
}
@Override
public abstract State getInitialState() throws PrismException;
@Override
public abstract void exploreState(State exploreState) throws PrismException;
@Override
public abstract State getExploreState();
@Override
public abstract int getNumChoices() throws PrismException;
@Override
public int getNumTransitions() throws PrismException
{
// Default implementation
int tot = 0;
int n = getNumChoices();
for (int i = 0; i < n; i++) {
tot += getNumTransitions(i);
}
return tot;
}
@Override
public abstract int getNumTransitions(int i) throws PrismException;
@Override
public abstract Object getTransitionAction(int i) throws PrismException;
@Override
public abstract Object getTransitionAction(int i, int offset) throws PrismException;
@Override
public Object getChoiceAction(int i) throws PrismException
{
return getTransitionAction(i, 0);
}
@Override
public abstract double getTransitionProbability(int i, int offset) throws PrismException;
@Override
public abstract State computeTransitionTarget(int i, int offset) throws PrismException;
@Override
public boolean isLabelTrue(String label) throws PrismException
{
// Look up label and then check by index
int i = getLabelIndex(label);
if (i == -1) {
throw new PrismException("Label \"" + label + "\" not defined");
} else {
return isLabelTrue(i);
}
}
@Override
public boolean isLabelTrue(int i) throws PrismException
{
throw new PrismException("Label number \"" + i + "\" not defined");
}
@Override
public double getStateReward(int index, State state) throws PrismException
{
return 0.0;
}
@Override
public double getStateActionReward(int r, State state, Object action) throws PrismException
{
return 0.0;
}
}

60
prism/src/prism/ModelGenerator.java
View File

@ -27,6 +27,7 @@
package prism;
import java.util.Collections;
import java.util.List;
import parser.State;
@ -41,13 +42,21 @@ public interface ModelGenerator extends ModelInfo
/**
* Does the model have a single initial state?
*/
public boolean hasSingleInitialState() throws PrismException;
public default boolean hasSingleInitialState() throws PrismException
{
// Default to the case of a single initial state
return true;
}
/**
* 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;
public default List<State> getInitialStates() throws PrismException
{
// Default to the case of a single initial state
return Collections.singletonList(getInitialState());
}
/**
* Get the initial state of the model, if there is just one,
@ -78,7 +87,16 @@ public interface ModelGenerator extends ModelInfo
/**
* Get the total number of transitions in the current state.
*/
public int getNumTransitions() throws PrismException;
public default int getNumTransitions() throws PrismException
{
// Default implementation just extracts from getNumChoices() and getNumTransitions(i)
int tot = 0;
int n = getNumChoices();
for (int i = 0; i < n; i++) {
tot += getNumTransitions(i);
}
return tot;
}
/**
* Get the number of transitions in the {@code i}th nondeterministic choice.
@ -113,7 +131,11 @@ public interface ModelGenerator extends ModelInfo
* (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;
public default Object getChoiceAction(int i) throws PrismException
{
// Default implementation
return getTransitionAction(i, 0);
}
/**
* Get the probability/rate of a transition within a choice, specified by its index/offset.
@ -133,13 +155,26 @@ public interface ModelGenerator extends ModelInfo
* 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;
public default boolean isLabelTrue(String label) throws PrismException
{
// Default implementation: Look up label and then check by index
int i = getLabelIndex(label);
if (i == -1) {
throw new PrismException("Label \"" + label + "\" not defined");
} else {
return isLabelTrue(i);
}
}
/**
* 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;
public default boolean isLabelTrue(int i) throws PrismException
{
// No labels by default
throw new PrismException("Label number \"" + i + "\" not defined");
}
/**
* Get the state reward of the {@code r}th reward structure for state {@code state}
@ -147,7 +182,12 @@ public interface ModelGenerator extends ModelInfo
* @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;
public default double getStateReward(int r, State state) throws PrismException
{
// Default reward to 0 (no reward structures by default anyway)
return 0.0;
}
/**
* Get the state-action reward of the {@code r}th reward structure for state {@code state} and action {@code action}
@ -159,5 +199,9 @@ public interface ModelGenerator extends ModelInfo
* @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;
public default double getStateActionReward(int r, State state, Object action) throws PrismException
{
// Default reward to 0 (no reward structures by default anyway)
return 0.0;
}
}

124
prism/src/prism/ModelGeneratorSymbolic.java
View File

@ -27,12 +27,9 @@
package prism;
import java.util.List;
import param.Function;
import param.FunctionFactory;
import param.ModelBuilder;
import parser.State;
import parser.ast.Expression;
/**
@ -40,127 +37,8 @@ import parser.ast.Expression;
* 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
public interface ModelGeneratorSymbolic extends ModelGenerator
{
/**
* 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

114
prism/src/prism/ModelInfo.java
View File

@ -27,6 +27,7 @@
package prism;
import java.util.Collections;
import java.util.List;
import parser.Values;
@ -50,19 +51,32 @@ public interface ModelInfo
* Undefined constants can be subsequently redefined to different values with the same method.
* The current constant values (if set) are available via {@link #getConstantValues()}.
*/
public void setSomeUndefinedConstants(Values someValues) throws PrismException;
public default void setSomeUndefinedConstants(Values someValues) throws PrismException
{
// By default, assume there are no constants to define
if (someValues != null && someValues.getNumValues() > 0)
throw new PrismException("This model has no constants to set");
}
/**
* Get access to the values for all constants in the model, including the
* undefined constants set previously via the method {@link #setUndefinedConstants(Values)}.
* Until they are set for the first time, this method returns null.
*/
public Values getConstantValues();
public default Values getConstantValues()
{
// By default, assume there are no constants to define
return new Values();
}
/**
* Does the model contain unbounded variables?
*/
public boolean containsUnboundedVariables();
public default boolean containsUnboundedVariables()
{
// By default, assume all variables are finite-ranging
return false;
}
/**
* Get the number of variables in the model.
@ -74,70 +88,122 @@ public interface ModelInfo
*/
public List<String> getVarNames();
/**
* Get the types of all the variables in the model.
*/
public List<Type> getVarTypes();
/**
* Look up the index of a variable in the model by name.
* Returns -1 if there is no such variable.
*/
public int getVarIndex(String name);
public default int getVarIndex(String name)
{
// Default implementation just extracts from getVarNames()
return getVarNames().indexOf(name);
}
/**
* Get the name of the {@code i}th variable in the model.
* {@code i} should always be between 0 and getNumVars() - 1.
*/
public String getVarName(int i);
public default String getVarName(int i)
{
// Default implementation just extracts from getVarNames()
return getVarNames().get(i);
}
/**
* Get the types of all the variables in the model.
*/
public List<Type> getVarTypes();
/**
* Get the type of the {@code i}th variable in the model.
* {@code i} should always be between 0 and getNumVars() - 1.
*/
//public Type getVarType(int i) throws PrismException;
public default Type getVarType(int i) throws PrismException
{
// Default implementation just extracts from getVarTypes()
return getVarTypes().get(i);
}
/**
* Get the number of labels (atomic propositions) defined for the model.
*/
public int getNumLabels();
public default int getNumLabels()
{
// Default implementation just extracts from getLabelNames()
return getLabelNames().size();
}
/**
* Get the names of all the labels in the model.
*/
public List<String> getLabelNames();
public default List<String> getLabelNames()
{
// No labels by default
return Collections.emptyList();
}
/**
* Get the name of the {@code i}th label of the model.
*/
public String getLabelName(int i) throws PrismException;
* {@code i} should always be between 0 and getNumLabels() - 1.
*/
public default String getLabelName(int i) throws PrismException
{
// Default implementation just extracts from getLabelNames()
try {
return getLabelNames().get(i);
} catch (IndexOutOfBoundsException e) {
throw new PrismException("Label number " + i + " not defined");
}
}
/**
* Get the index of the label with name {@code label}. Returns -1 if none exists.
* Get the index of the label with name {@code name}.
* Indexed from 0. Returns -1 if label of that name does not exist.
*/
public int getLabelIndex(String label);
public default int getLabelIndex(String name)
{
// Default implementation just extracts from getLabelNames()
return getLabelNames().indexOf(name);
}
/**
* Get the number of reward structures in the model.
*/
public int getNumRewardStructs();
public default int getNumRewardStructs()
{
// Default implementation just extracts from getRewardStructNames()
return getRewardStructNames().size();
}
/**
* Get a list of the names of the reward structures in the model.
*/
public List<String> getRewardStructNames();
public default List<String> getRewardStructNames()
{
// No reward structures by default
return Collections.emptyList();
}
/**
* Get the index of a module by its name
* (indexed from 0, not from 1 like at the user (property language) level).
* Returns -1 if name does not exist.
*/
public int getRewardStructIndex(String name);
public default int getRewardStructIndex(String name)
{
// Default implementation just extracts from getRewardStructNames()
return getRewardStructNames().indexOf(name);
}
/**
* Get a reward structure by its index
* (indexed from 0, not from 1 like at the user (property language) level).
* Returns null if index is out of range.
*/
public RewardStruct getRewardStruct(int i);
public default RewardStruct getRewardStruct(int i)
{
// No reward structures by default
return null;
}
/**
* Returns true if the reward structure with index i defines transition rewards.
@ -146,7 +212,11 @@ public interface ModelInfo
* If using an algorithm or implementation that does not support transition rewards,
* you may need to return false here (as well as not defining transition rewards).
*/
public boolean rewardStructHasTransitionRewards(int i);
public default boolean rewardStructHasTransitionRewards(int i)
{
// By default, assume that any reward structures that do exist may have transition rewards
return true;
}
// TODO: can we remove this?
public VarList createVarList() throws PrismException;

2
prism/src/prism/TestModelGenerator.java
View File

@ -42,7 +42,7 @@ import parser.type.TypeInt;
import explicit.ConstructModel;
import explicit.DTMCModelChecker;
public class TestModelGenerator extends DefaultModelGenerator
public class TestModelGenerator implements ModelGenerator
{
protected State exploreState;
protected int x;

4
prism/src/simulator/ModulesFileModelGenerator.java
View File

@ -11,13 +11,13 @@ import parser.ast.LabelList;
import parser.ast.ModulesFile;
import parser.ast.RewardStruct;
import parser.type.Type;
import prism.DefaultModelGenerator;
import prism.ModelGenerator;
import prism.ModelType;
import prism.PrismComponent;
import prism.PrismException;
import prism.PrismLangException;
public class ModulesFileModelGenerator extends DefaultModelGenerator
public class ModulesFileModelGenerator implements ModelGenerator
{
// Parent PrismComponent (logs, settings etc.)
protected PrismComponent parent;

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

@ -16,14 +16,13 @@ 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
public class ModulesFileModelGeneratorSymbolic implements ModelGeneratorSymbolic
{
// Parent PrismComponent (logs, settings etc.)
protected PrismComponent parent;

Write Preview
Loading…
Cancel
Save