diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 61cb768c..a5492480 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -849,7 +849,7 @@ public class ProbModelChecker extends NonProbModelChecker MinMax minMax = opInfo.getMinMax(model.getModelType(), forAll); // Build rewards - RewardStruct rewStruct = expr.getRewardStructByIndexObject(modulesFile, constantValues); + RewardStruct rewStruct = expr.getRewardStructByIndexObject(modelInfo, constantValues); mainLog.println("Building reward structure..."); Rewards rewards = constructRewards(model, rewStruct); diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 73a8eae8..f4944946 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -61,6 +61,7 @@ import parser.type.TypeDouble; import parser.type.TypeInt; import parser.visitor.ASTTraverseModify; import prism.Filter; +import prism.ModelInfo; import prism.ModelType; import prism.Prism; import prism.PrismComponent; @@ -107,8 +108,9 @@ public class StateModelChecker extends PrismComponent // Do bisimulation minimisation before model checking? protected boolean doBisim = false; - // Model file (for reward structures, etc.) + // Model info (for reward structures, etc.) protected ModulesFile modulesFile = null; + protected ModelInfo modelInfo = null; // Properties file (for labels, constants, etc.) protected PropertiesFile propertiesFile = null; @@ -186,7 +188,7 @@ public class StateModelChecker extends PrismComponent */ public void inheritSettings(StateModelChecker other) { - setModulesFileAndPropertiesFile(other.modulesFile, other.propertiesFile); + setModulesFileAndPropertiesFile(other.modelInfo, other.propertiesFile); setLog(other.getLog()); setVerbosity(other.getVerbosity()); setExportTarget(other.getExportTarget()); @@ -345,14 +347,17 @@ public class StateModelChecker extends PrismComponent * Set the attached model file (for e.g. reward structures when model checking) * and the attached properties file (for e.g. constants/labels when model checking) */ - public void setModulesFileAndPropertiesFile(ModulesFile modulesFile, PropertiesFile propertiesFile) + public void setModulesFileAndPropertiesFile(ModelInfo modelInfo, PropertiesFile propertiesFile) { - this.modulesFile = modulesFile; + this.modelInfo = modelInfo; + if (modelInfo instanceof ModulesFile) { + this.modulesFile = (ModulesFile) modelInfo; + } this.propertiesFile = propertiesFile; // Get combined constant values from model/properties constantValues = new Values(); - if (modulesFile != null) - constantValues.addValues(modulesFile.getConstantValues()); + if (modelInfo != null) + constantValues.addValues(modelInfo.getConstantValues()); if (propertiesFile != null) constantValues.addValues(propertiesFile.getConstantValues()); } diff --git a/prism/src/parser/ast/ExpressionReward.java b/prism/src/parser/ast/ExpressionReward.java index 192c8fe2..93b975d9 100644 --- a/prism/src/parser/ast/ExpressionReward.java +++ b/prism/src/parser/ast/ExpressionReward.java @@ -29,6 +29,7 @@ package parser.ast; import parser.EvaluateContext; import parser.Values; import parser.visitor.ASTVisitor; +import prism.ModelInfo; import prism.OpRelOpBound; import prism.PrismException; import prism.PrismLangException; @@ -110,15 +111,15 @@ public class ExpressionReward extends ExpressionQuant * Throws an exception (with explanatory message) if it cannot be found. * This means that, the method always returns a valid index if it finishes. */ - public int getRewardStructIndexByIndexObject(ModulesFile modulesFile, Values constantValues) throws PrismException + public int getRewardStructIndexByIndexObject(ModelInfo modelInfo, Values constantValues) throws PrismException { int rewStruct = -1; Object rsi = rewardStructIndex; // Recall: the index is an Object which is either an Integer, denoting the index (starting from 0) directly, // or an expression, which can be evaluated (possibly using the passed in constants) to an index. - if (modulesFile == null) - throw new PrismException("No model file to obtain reward structures"); - if (modulesFile.getNumRewardStructs() == 0) + if (modelInfo == null) + throw new PrismException("No model info to obtain reward structures"); + if (modelInfo.getNumRewardStructs() == 0) throw new PrismException("Model has no rewards specified"); // No index specified - use the first one if (rsi == null) { @@ -132,7 +133,7 @@ public class ExpressionReward extends ExpressionQuant } // String - name of reward structure else if (rsi instanceof String) { - rewStruct = modulesFile.getRewardStructIndex((String) rsi); + rewStruct = modelInfo.getRewardStructIndex((String) rsi); } if (rewStruct == -1) { throw new PrismException("Invalid reward structure index \"" + rsi + "\""); @@ -144,10 +145,10 @@ public class ExpressionReward extends ExpressionQuant * Get the reward structure (from a model) corresponding to the index of this R operator. * Throws an exception (with explanatory message) if it cannot be found. */ - public RewardStruct getRewardStructByIndexObject(ModulesFile modulesFile, Values constantValues) throws PrismException + public RewardStruct getRewardStructByIndexObject(ModelInfo modelInfo, Values constantValues) throws PrismException { - int rewardStructIndex = getRewardStructIndexByIndexObject(modulesFile, constantValues); - return modulesFile.getRewardStruct(rewardStructIndex); + int rewardStructIndex = getRewardStructIndexByIndexObject(modelInfo, constantValues); + return modelInfo.getRewardStruct(rewardStructIndex); } /** diff --git a/prism/src/prism/DefaultModelGenerator.java b/prism/src/prism/DefaultModelGenerator.java index 339752e6..02156a0a 100644 --- a/prism/src/prism/DefaultModelGenerator.java +++ b/prism/src/prism/DefaultModelGenerator.java @@ -32,6 +32,7 @@ import java.util.List; import parser.State; import parser.Values; +import parser.ast.RewardStruct; import parser.type.Type; /** @@ -44,12 +45,6 @@ public abstract class DefaultModelGenerator implements ModelGenerator @Override public abstract ModelType getModelType(); - @Override - public boolean containsUnboundedVariables() - { - return false; - } - @Override public void setSomeUndefinedConstants(Values someValues) throws PrismException { @@ -64,6 +59,12 @@ public abstract class DefaultModelGenerator implements ModelGenerator return new Values(); } + @Override + public boolean containsUnboundedVariables() + { + return false; + } + @Override public abstract int getNumVars(); @@ -90,6 +91,24 @@ public abstract class DefaultModelGenerator implements ModelGenerator return -1; } + @Override + public int getNumRewardStructs() + { + return 0; + } + + @Override + public int getRewardStructIndex(String name) + { + return -1; + } + + @Override + public RewardStruct getRewardStruct(int i) + { + return null; + } + // Methods for ModelGenerator interface public boolean hasSingleInitialState() throws PrismException diff --git a/prism/src/prism/ModelGenerator.java b/prism/src/prism/ModelGenerator.java index 25086fc0..3b037f38 100644 --- a/prism/src/prism/ModelGenerator.java +++ b/prism/src/prism/ModelGenerator.java @@ -30,7 +30,6 @@ package prism; import java.util.List; import parser.State; -import parser.Values; import parser.VarList; /** @@ -40,21 +39,6 @@ import parser.VarList; */ public interface ModelGenerator extends ModelInfo { - /** - * Set values for *some* undefined constants. - * If there are no undefined constants, {@code someValues} can be null. - * 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; - - /** - * 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(); - /** * Does the model have a single initial state? */ diff --git a/prism/src/prism/ModelInfo.java b/prism/src/prism/ModelInfo.java index 793a7b58..51015461 100644 --- a/prism/src/prism/ModelInfo.java +++ b/prism/src/prism/ModelInfo.java @@ -29,6 +29,8 @@ package prism; import java.util.List; +import parser.Values; +import parser.ast.RewardStruct; import parser.type.Type; /** @@ -41,6 +43,21 @@ public interface ModelInfo */ public ModelType getModelType(); + /** + * Set values for *some* undefined constants. + * If there are no undefined constants, {@code someValues} can be null. + * 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; + + /** + * 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(); + /** * Does the model contain unbounded variables? */ @@ -85,4 +102,23 @@ public interface ModelInfo * Get the index of the label with name {@code label}. Returns -1 if none exists. */ public int getLabelIndex(String label); + + /** + * Get the number of reward structures in the model. + */ + public int getNumRewardStructs(); + + /** + * 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); + + /** + * 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); } diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 98f82aa5..66556888 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -3636,7 +3636,11 @@ public class Prism extends PrismComponent implements PrismSettingsListener { // Create model checker explicit.StateModelChecker mc = explicit.StateModelChecker.createModelChecker(currentModelType, this); - mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile); + if (currentModulesFile != null) { + mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile); + } else { + mc.setModulesFileAndPropertiesFile(currentModelGenerator, propertiesFile); + } // Pass any additional local settings mc.setExportTarget(exportTarget); mc.setExportTargetFilename(exportTargetFilename); diff --git a/prism/src/simulator/ModulesFileModelGenerator.java b/prism/src/simulator/ModulesFileModelGenerator.java index 499f79f9..753d74c9 100644 --- a/prism/src/simulator/ModulesFileModelGenerator.java +++ b/prism/src/simulator/ModulesFileModelGenerator.java @@ -105,12 +105,6 @@ public class ModulesFileModelGenerator extends DefaultModelGenerator return modelType; } - @Override - public boolean containsUnboundedVariables() - { - return modulesFile.containsUnboundedVariables(); - } - @Override public void setSomeUndefinedConstants(Values someValues) throws PrismException { @@ -125,6 +119,12 @@ public class ModulesFileModelGenerator extends DefaultModelGenerator return mfConstants; } + @Override + public boolean containsUnboundedVariables() + { + return modulesFile.containsUnboundedVariables(); + } + @Override public int getNumVars() { @@ -167,12 +167,24 @@ public class ModulesFileModelGenerator extends DefaultModelGenerator return varList; } - //@Override + @Override public int getNumRewardStructs() { return modulesFile.getNumRewardStructs(); } + @Override + public int getRewardStructIndex(String name) + { + return modulesFile.getRewardStructIndex(name); + } + + @Override + public RewardStruct getRewardStruct(int i) + { + return modulesFile.getRewardStruct(i); + } + @Override public boolean hasSingleInitialState() throws PrismException {