Remove un-needed check for LTL formula inside time-bounded until.

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

prism/src/explicit/CTMCModelChecker.java

@@ -56,12 +56,6 @@ public class CTMCModelChecker extends DTMCModelChecker
 		StateValues probs = null;
 		ModelCheckerResult tmpRes = null, res = null;
 
-		// check not LTL
-		if (!(expr.getOperand1().getType() instanceof TypeBool))
-			throw new PrismException("Invalid path formula");
-		if (!(expr.getOperand2().getType() instanceof TypeBool))
-			throw new PrismException("Invalid path formula");
-
 		// get info from bounded until
 
 		// lower bound is 0 if not specified

prism/src/prism/StochModelChecker.java

@@ -86,12 +86,6 @@ public class StochModelChecker extends ProbModelChecker
 		JDDNode b1, b2, tmp;
 		StateValues tmpProbs = null, probs = null;
 
-		// check not LTL
-		if (!(expr.getOperand1().getType() instanceof TypeBool))
-			throw new PrismException("Invalid path formula");
-		if (!(expr.getOperand2().getType() instanceof TypeBool))
-			throw new PrismException("Invalid path formula");
-
 		// get info from bounded until
 
 		// lower bound is 0 if not specified