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

@@ -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);
 

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());
 	}

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);
 	}
 	
 	/**

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

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?
 	 */

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);
 }

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);

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
 	{