From 2700f52271737146860a55037b60ac9f701c16bf Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 18 May 2020 14:37:29 +0100 Subject: [PATCH] Allow the actual type of a PRISM model to differ from the one specified in the file. For now, this provides a cleaner implementation of the default (unspecified) model type being set to an MDP. Later, this will allow the actual model type to be omitted or partially specified and derived from langage features. --- prism/src/parser/PrismParser.java | 8 ++--- prism/src/parser/PrismParser.jj | 8 ++--- prism/src/parser/ast/ModulesFile.java | 52 +++++++++++++++++++++++++-- prism/src/pta/DigitalClocks.java | 2 +- 4 files changed, 58 insertions(+), 12 deletions(-) diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java index 51c18ffe..3a4508be 100644 --- a/prism/src/parser/PrismParser.java +++ b/prism/src/parser/PrismParser.java @@ -151,7 +151,7 @@ public class PrismParser implements PrismParserConstants { } // Override type of model if requested if (typeOverride != null) { - mf.setModelType(typeOverride); + mf.setModelTypeInFile(typeOverride); } return mf; @@ -371,7 +371,7 @@ public class PrismParser implements PrismParserConstants { // Modules file static final public -ModulesFile ModulesFile() throws ParseException, PrismLangException {ModelType type = ModelType.MDP; +ModulesFile ModulesFile() throws ParseException, PrismLangException {ModelType type = null; int typeCount = 0; Token typeDupe = null; Declaration global; @@ -491,8 +491,8 @@ mf.setInitialStates(init); initCount++; if (initCount == 2) initDupe = init; {if (true) throw new PrismLangException("There were multiple init...endinit constructs", initDupe);} } - // Set model type (note default is MDP) - mf.setModelType(type); + // Set model type (might be null, i.e., unspecified) + mf.setModelTypeInFile(type); // Return completed ModulesFile object mf.setPosition(begin != null? begin: getToken(0), getToken(0)); diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj index e3b5c87e..911bb9e4 100644 --- a/prism/src/parser/PrismParser.jj +++ b/prism/src/parser/PrismParser.jj @@ -183,7 +183,7 @@ public class PrismParser } // Override type of model if requested if (typeOverride != null) { - mf.setModelType(typeOverride); + mf.setModelTypeInFile(typeOverride); } return mf; @@ -531,7 +531,7 @@ TOKEN : ModulesFile ModulesFile() throws PrismLangException : { - ModelType type = ModelType.MDP; + ModelType type = null; int typeCount = 0; Token typeDupe = null; Declaration global; @@ -574,8 +574,8 @@ ModulesFile ModulesFile() throws PrismLangException : throw new PrismLangException("There were multiple init...endinit constructs", initDupe); } - // Set model type (note default is MDP) - mf.setModelType(type); + // Set model type (might be null, i.e., unspecified) + mf.setModelTypeInFile(type); // Return completed ModulesFile object mf.setPosition(begin != null? begin: getToken(0), getToken(0)); diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 0d9c33b8..900496f4 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -44,7 +44,9 @@ import parser.type.*; public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerator { - // Model type (enum) + // Model type, as specified in the model file + private ModelType modelTypeInFile; + // Model type (actual, may differ) private ModelType modelType; // Model components @@ -84,7 +86,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato formulaList = new FormulaList(); labelList = new LabelList(); constantList = new ConstantList(); - modelType = ModelType.MDP; // default type + modelTypeInFile = modelType = null; // Unspecified globals = new Vector(); modules = new Vector(); systemDefns = new ArrayList(); @@ -119,6 +121,22 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato constantList = cl; } + /** + * Set the model type that is specified in the model file. + * Can be null, denoting that it is unspecified. + */ + public void setModelTypeInFile(ModelType t) + { + modelTypeInFile = t; + // As a default, set the actual type to be the same + modelType = modelTypeInFile; + } + + /** + * Set the actual model type, + * which may differ from the type specified in the model file. + * Note: if {@link #tidyUp()} is called, this may be overwritten. + */ public void setModelType(ModelType t) { modelType = t; @@ -273,6 +291,11 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato return constantList; } + public ModelType getModelTypeInFile() + { + return modelTypeInFile; + } + @Override public ModelType getModelType() { @@ -705,6 +728,11 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato // Then identify/check any references to action names findAllActions(synchs); + // Determine actual model type + // (checks/processing below this point can assume that modelType + // is non-null; methods before this point cannot) + finaliseModelType(); + // Various semantic checks doSemanticChecks(); // Type checking @@ -1244,6 +1272,21 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato return new VarList(this); } + /** + * Determine the actual model type + */ + private void finaliseModelType() + { + // Default (if unspecified) is MDP + if (modelTypeInFile == null) { + modelType = ModelType.MDP; + } + // Otherwise, it's just whatever was specified + else { + modelType = modelTypeInFile; + } + } + // Methods required for ASTElement: /** @@ -1262,7 +1305,9 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato String s = "", tmp; int i, n; - s += modelType.toString().toLowerCase() + "\n\n"; + if (modelTypeInFile != null) { + s += modelTypeInFile.toString().toLowerCase() + "\n\n"; + } tmp = "" + formulaList; if (tmp.length() > 0) @@ -1323,6 +1368,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato // Copy ASTElement stuff ret.setPosition(this); // Copy type + ret.setModelTypeInFile(modelTypeInFile); ret.setModelType(modelType); // Deep copy main components ret.setFormulaList((FormulaList) formulaList.deepCopy()); diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java index 0ac0e62d..8989536b 100644 --- a/prism/src/pta/DigitalClocks.java +++ b/prism/src/pta/DigitalClocks.java @@ -172,7 +172,7 @@ public class DigitalClocks prop = (Expression) propertyToCheck.deepCopy(); // Change the model type - mf.setModelType(ModelType.MDP); + mf.setModelTypeInFile(ModelType.MDP); // Change all clock variable declarations to bounded integers mf = (ModulesFile) mf.accept(new ASTTraverseModify()