From f518d66c6c7db64c8c2096cd8398c7405e89fb17 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 30 Jun 2016 15:58:48 +0000 Subject: [PATCH] Sampler: fix logic for rejecting co-safety path formulas in reward samplers (fixes previous commit) git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11447 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/simulator/sampler/Sampler.java | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/prism/src/simulator/sampler/Sampler.java b/prism/src/simulator/sampler/Sampler.java index eca8f947..faa4e8fb 100644 --- a/prism/src/simulator/sampler/Sampler.java +++ b/prism/src/simulator/sampler/Sampler.java @@ -235,9 +235,8 @@ public abstract class Sampler throw new PrismException("Invalid reward structure index \"" + rs + "\""); // Construct sampler based on type - if (!(expr.getExpression() instanceof ExpressionTemporal) || - !(expr.isSimplePathFormula())) { - // catch co-safety reward specifications + if (!(expr.getExpression() instanceof ExpressionTemporal)) { + // catch complex co-safety reward specifications throw new PrismException("Can't create sampler for property \"" + expr + "\""); } ExpressionTemporal exprTemp = (ExpressionTemporal) expr.getExpression(); @@ -260,6 +259,12 @@ public abstract class Sampler } case ExpressionTemporal.P_F: // reachability reward + + // catch the case of a complex co-safety path formula + if (!exprTemp.isSimplePathFormula()) { + throw new PrismException("Can't create sampler for property \"" + exprTemp + "\""); + } + return new SamplerRewardReach(exprTemp, rsi); }