From a9f4c144094245d48318ad6bdb454d24ad808df7 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 27 Jan 2015 13:35:44 +0000 Subject: [PATCH] Don't allow lower time-bounds for weak until (e.g., for a W[l,u] b or a W>=l b) due to unintuitive semantics. [From Joachim Klein; but moved check to higher up] git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9563 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/visitor/CheckValid.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/prism/src/parser/visitor/CheckValid.java b/prism/src/parser/visitor/CheckValid.java index 75c5923a..8b09c460 100644 --- a/prism/src/parser/visitor/CheckValid.java +++ b/prism/src/parser/visitor/CheckValid.java @@ -88,6 +88,10 @@ public class CheckValid extends ASTTraverse + " operator must be integers for PTAs"); } } + // Don't allow lower bounds on weak until - does not have intuitive semantics + if (e.getOperator() == ExpressionTemporal.P_W && e.getLowerBound() != null) { + throw new PrismLangException("The weak until operator (W) with lower bounds is not yet supported"); + } } public void visitPost(ExpressionProb e) throws PrismLangException