From 0f2bbbc7b6b773dd502e372a922975e6fa14eafa Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 7 Dec 2015 09:54:19 +0000 Subject: [PATCH] Add some (syntactic) reward info to the ModelInfo interface and use this where possible in explicit model checking. Can now use ModulesFileModelGenerator for reward property model checking. Also push constant info from ModelGenerator up to ModelInfo. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11006 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/ProbModelChecker.java | 2 +- prism/src/explicit/StateModelChecker.java | 17 +++++---- prism/src/parser/ast/ExpressionReward.java | 17 ++++----- prism/src/prism/DefaultModelGenerator.java | 31 ++++++++++++---- prism/src/prism/ModelGenerator.java | 16 --------- prism/src/prism/ModelInfo.java | 36 +++++++++++++++++++ prism/src/prism/Prism.java | 6 +++- .../simulator/ModulesFileModelGenerator.java | 26 ++++++++++---- 8 files changed, 106 insertions(+), 45 deletions(-) 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 {