From b270d9b9848ddf32a0a6b71bce6a5797415178ed Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 29 Dec 2020 00:22:45 +0000 Subject: [PATCH] Add check that POMDP observables are valid variable references. Also fix a few test cases (with erroneous extra observables). --- prism/src/explicit/ConstructModel.java | 5 +++++ prism/tests/poptas/pump_popta.prism | 2 +- prism/tests/poptas/pump_popta_deadline.prism | 2 +- 3 files changed, 7 insertions(+), 2 deletions(-) diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java index ad061b66..6ed25a0c 100644 --- a/prism/src/explicit/ConstructModel.java +++ b/prism/src/explicit/ConstructModel.java @@ -236,6 +236,11 @@ public class ConstructModel extends PrismComponent if (!justReach && modelType.partiallyObservable()) { List allVars = modelGen.getVarNames(); observableVars = modelGen.getObservableVars(); + for (String obsVar : observableVars) { + if (!allVars.contains(obsVar)) { + throw new PrismException("Observable " + obsVar + " is not a variable"); + } + } unobservableVars = new ArrayList<>(); for (String varName : allVars) { if (!observableVars.contains(varName)) { diff --git a/prism/tests/poptas/pump_popta.prism b/prism/tests/poptas/pump_popta.prism index c9e05b22..9cafbff5 100644 --- a/prism/tests/poptas/pump_popta.prism +++ b/prism/tests/poptas/pump_popta.prism @@ -13,7 +13,7 @@ popta // can see the state of the pump and its local variables and all clocks observables - p, messages, l, m, guess, correct, x, y + p, l, m, guess, correct, x, y endobservables // delays for high sending 0 and 1 (both need to be >1) diff --git a/prism/tests/poptas/pump_popta_deadline.prism b/prism/tests/poptas/pump_popta_deadline.prism index bf9d90dd..dab5f8a2 100644 --- a/prism/tests/poptas/pump_popta_deadline.prism +++ b/prism/tests/poptas/pump_popta_deadline.prism @@ -2,7 +2,7 @@ pomdp // can see the state of the pump and its local variables and all clocks observables - p, messages, l, m, guess, correct, x, y, t + p, l, m, guess, correct, x, y, t endobservables label "invariants" = (p=0=>true)&(p=1=>y<=1)&(p=2=>y<=0)&(l=0=>x<=0)&(l=1=>x<=Tout)&(l=2=>x<=0)&(l=3=>true);