ConvertForJltl2ba: catch translation of temporal operators with bounds

Normally, that should be caught before, defense in depth.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12063 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/parser/visitor/ConvertForJltl2ba.java

@@ -124,6 +124,9 @@ public class ConvertForJltl2ba
 		Expression until;
 		if (e.getOperand1() != null) ltl1 = convert(e.getOperand1());
 		if (e.getOperand2() != null) ltl2 = convert(e.getOperand2());
+		if (e.hasBounds()) {
+			throw new PrismLangException("Can not convert expression with temporal bounds to SimpleLTL: " + e);
+		}
 		switch (e.getOperator()) {
 		case ExpressionTemporal.P_X:
 			res = new SimpleLTL(SimpleLTL.LTLType.NEXT, ltl2);