From c7cf09659c5a4befbb8b144028af35b79dd6c0f4 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 29 Dec 2020 23:34:08 +0000
Subject: [PATCH] Model type auto-detection for partially observable models.

MDPs/PTAs are considered to be POMDPs/POPTAs if they have observables.
---
 prism/src/parser/PrismParser.java     | 31 ++++++++++++++-------------
 prism/src/parser/PrismParser.jj       |  2 +-
 prism/src/parser/ast/ModulesFile.java | 29 +++++++++++++++++++++++--
 3 files changed, 44 insertions(+), 18 deletions(-)

diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java
index 1348f5d0..1121d8ec 100644
--- a/prism/src/parser/PrismParser.java
+++ b/prism/src/parser/PrismParser.java
@@ -1389,6 +1389,7 @@ Expression Init() throws ParseException {Expression expr = null;
   static final public 
 void Observables(ModulesFile mf) throws ParseException {String name = null;
     jj_consume_token(OBSERVABLES);
+mf.setHasObservables(true);
     switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
     case REG_IDENT:{
       name = Identifier();
@@ -3765,12 +3766,6 @@ fl.setLHS(s);
     finally { jj_save(17, xla); }
   }
 
-  static private boolean jj_3R_33()
- {
-    if (jj_3R_30()) return true;
-    return false;
-  }
-
   static private boolean jj_3R_164()
  {
     if (jj_scan_token(MAX)) return true;
@@ -4247,15 +4242,6 @@ fl.setLHS(s);
     return false;
   }
 
-  static private boolean jj_3_2()
- {
-    if (jj_scan_token(DQUOTE)) return true;
-    if (jj_3R_30()) return true;
-    if (jj_scan_token(DQUOTE)) return true;
-    if (jj_scan_token(COLON)) return true;
-    return false;
-  }
-
   static private boolean jj_3R_141()
  {
     if (jj_3R_153()) return true;
@@ -4268,6 +4254,15 @@ fl.setLHS(s);
     return false;
   }
 
+  static private boolean jj_3_2()
+ {
+    if (jj_scan_token(DQUOTE)) return true;
+    if (jj_3R_30()) return true;
+    if (jj_scan_token(DQUOTE)) return true;
+    if (jj_scan_token(COLON)) return true;
+    return false;
+  }
+
   static private boolean jj_3R_140()
  {
     if (jj_3R_152()) return true;
@@ -5598,6 +5593,12 @@ fl.setLHS(s);
     return false;
   }
 
+  static private boolean jj_3R_33()
+ {
+    if (jj_3R_30()) return true;
+    return false;
+  }
+
   static private boolean jj_initialized_once = false;
   /** Generated Token Manager. */
   static public PrismParserTokenManager token_source;
diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj
index bf6c6230..2147079e 100644
--- a/prism/src/parser/PrismParser.jj
+++ b/prism/src/parser/PrismParser.jj
@@ -953,7 +953,7 @@ void Observables(ModulesFile mf) :
 	String name = null;
 }
 {
-	(<OBSERVABLES>
+	(<OBSERVABLES> { mf.setHasObservables(true); }
 	( name = Identifier() { mf.addObservableVar(name); }
 	( <COMMA> name = Identifier() { mf.addObservableVar(name); } )* )?
 	<ENDOBSERVABLES>)
diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java
index c30bda2a..7fda7680 100644
--- a/prism/src/parser/ast/ModulesFile.java
+++ b/prism/src/parser/ast/ModulesFile.java
@@ -68,7 +68,8 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 	private ArrayList<RewardStruct> rewardStructs; // Rewards structures
 	private List<String> rewardStructNames; // Names of reward structures
 	private Expression initStates; // Initial states specification
-	private List<String> obsVars; // Observable variables
+	private boolean hasObservables; // Observables info
+	private List<String> obsVars;
 
 	// Lists of all identifiers used and where
 	private HashMap<String, ASTElement> identUsage;
@@ -102,6 +103,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		rewardStructs = new ArrayList<RewardStruct>();
 		rewardStructNames = new ArrayList<String>();
 		initStates = null;
+		hasObservables = false;
 		obsVars = new ArrayList<String>();
 		identUsage = new HashMap<>();
 		varDecls = new Vector<Declaration>();
@@ -258,6 +260,11 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		initStates = e;
 	}
 
+	public void setHasObservables(boolean hasObservables)
+	{
+		this.hasObservables = hasObservables;
+	}
+	
 	public void addObservableVar(String n)
 	{
 		obsVars.add(n);
@@ -543,6 +550,15 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		return initStates;
 	}
 
+	/**
+	 * Does this model have an observables...endobservables block?
+	 * (i.e., is it a partially observable model?)
+	 */
+	public boolean hasObservables()
+	{
+		return hasObservables;
+	}
+	
 	@Override
 	public List<String> getObservableVars()
 	{
@@ -1335,11 +1351,19 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		// Then, even if already specified, update the model type
 		// based on the existence of certain features
 		boolean isRealTime = containsClockVariables();
+		boolean isPartObs = hasObservables();
 		if (isRealTime) {
 			if (modelType == ModelType.MDP || modelType == ModelType.LTS) {
 				modelType = ModelType.PTA;
 			}
 		}
+		if (isPartObs) {
+			if (modelType == ModelType.MDP || modelType == ModelType.LTS) {
+				modelType = ModelType.POMDP;
+			} else if (modelType == ModelType.PTA) {
+				modelType = ModelType.POPTA;
+			}
+		}
 	}
 	
 	/**
@@ -1407,7 +1431,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 			tmp += "\n";
 		s += tmp;
 
-		if (!obsVars.isEmpty()) {
+		if (hasObservables()) {
 			s += "observables " + String.join(",", obsVars) + " endobservables\n\n";
 		}
 
@@ -1479,6 +1503,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		}
 		if (initStates != null)
 			ret.setInitialStates(initStates.deepCopy());
+		ret.hasObservables = hasObservables;
 		for (String ov : obsVars)
 			ret.addObservableVar(ov);
 		// Copy other (generated) info