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

@@ -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