From 8889db5a2ac882fd970715b8778e48e4d5fdc4d3 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 11 Feb 2016 12:02:29 +0000 Subject: [PATCH] explicit.CTMCModelChecker: reject LTL with time bounds This is currently caught elsewhere as well, but provides defense-in-depth for the situation that time bounds in LTL are supported later on. Bounds on temporal operators don't have the same semantics in CTMCs as for discrete-time models. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11178 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/CTMCModelChecker.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index ea0ebbd0..f2f1093a 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -54,6 +54,10 @@ public class CTMCModelChecker extends ProbModelChecker @Override protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax, BitSet statesOfInterest) throws PrismException { + if (Expression.containsTemporalTimeBounds(expr)) { + throw new PrismNotSupportedException("LTL formulas with time bounds not supported for CTMCs"); + } + if (!(model instanceof ModelExplicit)) { // needs a ModelExplicit to allow attaching labels in the handleMaximalStateFormulas step throw new PrismNotSupportedException("Need CTMC with ModelExplicit for LTL checking"); @@ -72,6 +76,10 @@ public class CTMCModelChecker extends ProbModelChecker @Override protected StateValues checkRewardCoSafeLTL(Model model, Rewards modelRewards, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { + if (Expression.containsTemporalTimeBounds(expr)) { + throw new PrismNotSupportedException("LTL formulas with time bounds not supported for CTMCs"); + } + if (!(model instanceof ModelExplicit)) { // needs a ModelExplicit to allow attaching labels in the handleMaximalStateFormulas step throw new PrismNotSupportedException("Need CTMC with ModelExplicit for cosafety LTL reward checking");