From 9fc0899fb5108cb3fb818a8ff29d23cfa0e975fe Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Wed, 19 Jul 2017 12:32:51 +0000
Subject: [PATCH] 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 | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/prism/src/parser/visitor/ConvertForJltl2ba.java b/prism/src/parser/visitor/ConvertForJltl2ba.java
index 7c667191..7f967b24 100644
--- a/prism/src/parser/visitor/ConvertForJltl2ba.java
+++ b/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);