From 4849d6d603bc2637b6c90c548b844a7cf9755c6a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 28 Jan 2015 14:12:53 +0000 Subject: [PATCH] Remove check for lower bounds in path formulas for DTMC, MDP. [Joachim Klein] git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9573 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/visitor/CheckValid.java | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) diff --git a/prism/src/parser/visitor/CheckValid.java b/prism/src/parser/visitor/CheckValid.java index 8b09c460..403abcdb 100644 --- a/prism/src/parser/visitor/CheckValid.java +++ b/prism/src/parser/visitor/CheckValid.java @@ -58,23 +58,16 @@ public class CheckValid extends ASTTraverse throw new PrismLangException("Only reachability (F) reward properties can be used for PTAs"); } } - // Apart from CTMCs, we only support upper time bounds + // PTA only support upper time bounds if (e.getLowerBound() != null) { - if (modelType == ModelType.DTMC) { - throw new PrismLangException("Only upper time bounds are allowed on the " + e.getOperatorSymbol() - + " operator for DTMCs"); - } - if (modelType == ModelType.MDP) { - throw new PrismLangException("Only upper time bounds are allowed on the " + e.getOperatorSymbol() - + " operator for MDPs"); - } if (modelType == ModelType.PTA) { throw new PrismLangException("Only upper time bounds are allowed on the " + e.getOperatorSymbol() + " operator for PTAs"); } } // Apart from CTMCs, we only support integer time bounds - if (e.getUpperBound() != null && !(e.getUpperBound().getType() instanceof TypeInt)) { + if ((e.getUpperBound() != null && !(e.getUpperBound().getType() instanceof TypeInt)) || + (e.getLowerBound() != null && !(e.getLowerBound().getType() instanceof TypeInt))) { if (modelType == ModelType.DTMC) { throw new PrismLangException("Time bounds on the " + e.getOperatorSymbol() + " operator must be integers for DTMCs");