From 4add8e124480471c2be8815b2f6f20af27b97556 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 17 Dec 2017 16:22:15 +0000 Subject: [PATCH] Move methods from DefaultModelGenerator into default implementations within ModelGenerator interface. --- prism/src/prism/DefaultModelGenerator.java | 208 +----------------- prism/src/prism/ModelGenerator.java | 60 ++++- prism/src/prism/ModelGeneratorSymbolic.java | 124 +---------- prism/src/prism/ModelInfo.java | 114 ++++++++-- prism/src/prism/TestModelGenerator.java | 2 +- .../simulator/ModulesFileModelGenerator.java | 4 +- .../ModulesFileModelGeneratorSymbolic.java | 3 +- 7 files changed, 152 insertions(+), 363 deletions(-) diff --git a/prism/src/prism/DefaultModelGenerator.java b/prism/src/prism/DefaultModelGenerator.java index bfb7705b..83dafcb5 100644 --- a/prism/src/prism/DefaultModelGenerator.java +++ b/prism/src/prism/DefaultModelGenerator.java @@ -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 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 getVarTypes(); - - @Override - public int getNumLabels() - { - return 0; - } - - @Override - public abstract List 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 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 getInitialStates() throws PrismException - { - // Default to the case of a single initial state - ArrayList initStates = new ArrayList(); - 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; - } } diff --git a/prism/src/prism/ModelGenerator.java b/prism/src/prism/ModelGenerator.java index 7d341300..3829cd25 100644 --- a/prism/src/prism/ModelGenerator.java +++ b/prism/src/prism/ModelGenerator.java @@ -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 getInitialStates() throws PrismException; + public default List 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; + } } diff --git a/prism/src/prism/ModelGeneratorSymbolic.java b/prism/src/prism/ModelGeneratorSymbolic.java index 85d45cc7..ab81d808 100644 --- a/prism/src/prism/ModelGeneratorSymbolic.java +++ b/prism/src/prism/ModelGeneratorSymbolic.java @@ -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 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 diff --git a/prism/src/prism/ModelInfo.java b/prism/src/prism/ModelInfo.java index ba9a9565..aab27378 100644 --- a/prism/src/prism/ModelInfo.java +++ b/prism/src/prism/ModelInfo.java @@ -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 getVarNames(); - /** - * Get the types of all the variables in the model. - */ - public List 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 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 getLabelNames(); + public default List 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 getRewardStructNames(); + public default List 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; diff --git a/prism/src/prism/TestModelGenerator.java b/prism/src/prism/TestModelGenerator.java index 692909b6..391dec77 100644 --- a/prism/src/prism/TestModelGenerator.java +++ b/prism/src/prism/TestModelGenerator.java @@ -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; diff --git a/prism/src/simulator/ModulesFileModelGenerator.java b/prism/src/simulator/ModulesFileModelGenerator.java index 3dc753b8..4e70b8a7 100644 --- a/prism/src/simulator/ModulesFileModelGenerator.java +++ b/prism/src/simulator/ModulesFileModelGenerator.java @@ -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; diff --git a/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java b/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java index 718e81a0..d8da5ca1 100644 --- a/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java +++ b/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java @@ -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;