From a4659afd034e897f0cc980f813604360332bf6b5 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Sat, 19 Dec 2020 17:50:55 +0000
Subject: [PATCH] Improved model type auto-detect when unspecified
 (MDP/PTA/LTS).

---
 prism/src/parser/ast/ModulesFile.java | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java
index 03fb42bd..0b969a01 100644
--- a/prism/src/parser/ast/ModulesFile.java
+++ b/prism/src/parser/ast/ModulesFile.java
@@ -697,6 +697,17 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		return false;
 	}
 	
+	public boolean containsClockVariables()
+	{
+		int n = getNumVars();
+		for (int i = 0; i < n; i++) {
+			if (getVarDeclaration(i).getDeclType() instanceof DeclarationClock) {
+				return true;
+			}
+		}
+		return false;
+	}
+	
 	/**
 	 * Method to "tidy up" after parsing (must be called)
 	 * (do some checks and extract some information)
@@ -1290,9 +1301,13 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 	{
 		// If unspecified, auto-detect model type
 		if (modelTypeInFile == null) {
+			boolean isRealTime = containsClockVariables();
 			boolean nonProb = isNonProbabilistic();
-			// MDP/LTS depending if probabilistic
-			modelType = nonProb ? ModelType.LTS : ModelType.MDP;
+			if (isRealTime) {
+				modelType = ModelType.PTA;
+			} else {
+				modelType = nonProb ? ModelType.LTS : ModelType.MDP;
+			}
 		}
 		// Otherwise, it's just whatever was specified
 		else {