From 1ff7316aa0eb478d32e349a1df5072c1d81118b3 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 21 Feb 2012 10:47:09 +0000 Subject: [PATCH] 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 | 6 ------ prism/src/prism/StochModelChecker.java | 6 ------ 2 files changed, 12 deletions(-) diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index 2ae0b99e..219c27a2 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/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 diff --git a/prism/src/prism/StochModelChecker.java b/prism/src/prism/StochModelChecker.java index 5ce4aeee..a2e4ac01 100644 --- a/prism/src/prism/StochModelChecker.java +++ b/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