From c9be4ac33feeed22afb7bfcdd09b8d6e690ed0a2 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 29 Dec 2020 18:26:36 +0000 Subject: [PATCH] Model type auto-detection: MDPs are considered to be PTAs if they have clocks. Also re-factor finaliseModelType() to allow similar checks to be added. --- prism/src/parser/ast/ModulesFile.java | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 0b969a01..4d2a8c5e 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -1299,20 +1299,24 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato */ private void finaliseModelType() { - // If unspecified, auto-detect model type + // First, fix a "base" model type + // If unspecified, auto-detect if (modelTypeInFile == null) { - boolean isRealTime = containsClockVariables(); - boolean nonProb = isNonProbabilistic(); - if (isRealTime) { - modelType = ModelType.PTA; - } else { - modelType = nonProb ? ModelType.LTS : ModelType.MDP; - } + boolean isNonProb = isNonProbabilistic(); + modelType = isNonProb ? ModelType.LTS : ModelType.MDP; } // Otherwise, it's just whatever was specified else { modelType = modelTypeInFile; } + // Then, even if already specified, update the model type + // based on the existence of certain features + boolean isRealTime = containsClockVariables(); + if (isRealTime) { + if (modelType == ModelType.MDP || modelType == ModelType.LTS) { + modelType = ModelType.PTA; + } + } } /**