From 107358f933f7e8441fb843824c5e62d53f6bee47 Mon Sep 17 00:00:00 2001 From: Sascha Wunderlich Date: Thu, 20 Dec 2018 13:09:55 +0100 Subject: [PATCH] accumulation: bail out of past operators when complex is forced --- .../src/explicit/AccumulationTransformation.java | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java index 3817f8f1..bb4dc2da 100644 --- a/prism/src/explicit/AccumulationTransformation.java +++ b/prism/src/explicit/AccumulationTransformation.java @@ -97,12 +97,19 @@ public class AccumulationTransformation implements ModelExpress } // Figure out if we need a complex or a simple trafo... - boolean isComplex = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_COMPLEX) || accexp.hasFireOn() || !accexp.isNullary(); - if(isComplex) { - mc.getLog().println(" ... which is complex!"); + boolean isComplex = accexp.hasFireOn() || !accexp.isNullary(); + boolean isPast = accexp.getSymbol().isMinus(); + boolean forceComplex = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_COMPLEX); + + if(forceComplex && isPast) { + throw new PrismException("Unable to handle <->/[-] with -accforcecomplex. Bailing."); + } + + if(isComplex || forceComplex) { + mc.getLog().println(" ... using complex!"); doTransformationComplex(accexp, rewards); } else { - mc.getLog().println(" ... which is simple!"); + mc.getLog().println(" ... using simple!"); doTransformationSimple(accexp, rewards); } }