From 8ee81bfd4d5197bbd2cb99fc5ee79d13ba00fdea Mon Sep 17 00:00:00 2001 From: Sascha Wunderlich Date: Fri, 21 Dec 2018 16:26:32 +0100 Subject: [PATCH] fix corner case: forcemulti and simple --- prism/src/explicit/AccumulationTransformation.java | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java index 24738ba9..f635d82c 100644 --- a/prism/src/explicit/AccumulationTransformation.java +++ b/prism/src/explicit/AccumulationTransformation.java @@ -85,10 +85,10 @@ public class AccumulationTransformation implements Mode // Get the first ExpressionAccumulation mc.getLog().println("Looking for an accumulation formula..."); - boolean singleTrack = true; + boolean isSingleTrack = true; ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpressionWithoutTemporal(); if(accexp == null || mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_MULTI)) { - singleTrack = false; + isSingleTrack = false; accexp = transformedExpression.getFirstAccumulationExpression(); } @@ -120,15 +120,20 @@ public class AccumulationTransformation implements Mode boolean isSimple = !accexp.hasFireOn() && accexp.isNullary(); boolean isPast = accexp.getSymbol().isMinus(); boolean forceComplex = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_COMPLEX); + boolean forceMulti = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_MULTI); if(forceComplex && isPast) { throw new PrismException("Unable to handle <->/[-] with -accforcecomplex. Bailing."); } + if(forceMulti && isSimple) { + mc.getLog().println("WARNING: accforcemulti set, but cannot be used with simple method. Using complex one."); + } + // Build the AccumulationContext AccumulationContext ctx = new AccumulationContext(accexp, rewards, mc); - ctx.singleTrack = singleTrack; - ctx.simpleMethod = isSimple && !forceComplex; + ctx.singleTrack = isSingleTrack && !forceMulti; + ctx.simpleMethod = isSimple && !forceComplex && !forceMulti; // Build the product clock.start("accumulation product construction");