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