From 524dce617fd410ba35b552afffc273993926abbc Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 19 Mar 2021 09:04:36 +0000 Subject: [PATCH] Add a check that clocks in POPTAs are observable. --- prism/src/parser/ast/ModulesFile.java | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 87270c05..c5c06f39 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -1231,6 +1231,17 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato } addObservable(name, obs, obs.getDefinition(), exprVar); } + // For real-time models with partial observability (i.e. POPTAs), check that all clocks are observable + if (getModelType().partiallyObservable() && containsClockVariables()) { + int n = getNumVars(); + for (int i = 0; i < n; i++) { + if (getVarDeclaration(i).getDeclType() instanceof DeclarationClock) { + if (!observableVars.contains(getVarName(i))) { + throw new PrismLangException("All clocks in " + modelType + "s must be observable" , getVarDeclaration(i)); + } + } + } + } } /**