From 7fcf31d1d0f489f29aee0aecb41a808f8da1f7d9 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 7 Dec 2010 23:12:00 +0000 Subject: [PATCH] Bug fix: do not allow <0 time bound for CSL on CTMCs. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2324 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/StochModelChecker.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/prism/src/prism/StochModelChecker.java b/prism/src/prism/StochModelChecker.java index 5192af9c..a5cfb416 100644 --- a/prism/src/prism/StochModelChecker.java +++ b/prism/src/prism/StochModelChecker.java @@ -110,8 +110,9 @@ public class StochModelChecker extends ProbModelChecker exprTmp = expr.getUpperBound(); if (exprTmp != null) { uTime = exprTmp.evaluateDouble(constantValues, null); - if (uTime < 0) { - throw new PrismException("Invalid upper bound " + uTime + " in time-bounded until formula"); + if (uTime < 0 || (uTime == 0 && expr.upperBoundIsStrict())) { + String bound = (expr.upperBoundIsStrict() ? "<" : "<=") + uTime; + throw new PrismException("Invalid upper bound " + bound + " in time-bounded until formula"); } if (uTime < lTime) { throw new PrismException("Upper bound must exceed lower bound in time-bounded until formula");