From fa0077367fabb3b4f4f00e79766f5e48f614d2fa Mon Sep 17 00:00:00 2001 From: Sascha Wunderlich Date: Thu, 20 Dec 2018 17:30:22 +0100 Subject: [PATCH] accumulation: add -accforcemulti to disable single track opt --- prism/src/explicit/AccumulationTransformation.java | 5 +---- prism/src/prism/PrismSettings.java | 10 +++++++++- 2 files changed, 10 insertions(+), 5 deletions(-) diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java index 9c8078d9..db4ce83b 100644 --- a/prism/src/explicit/AccumulationTransformation.java +++ b/prism/src/explicit/AccumulationTransformation.java @@ -72,15 +72,12 @@ public class AccumulationTransformation implements Mode mc.getLog().println("Performing accumulation transformation..."); - // Is this whole thing an ExpressionAccumulation? - //if(transformedExpression.isAccumulationExpression()) { System.out.println("HEYOOOO!!! " + transformedExpression); } - // TODO: WHILE getFirstAccumulationExpression // Get the first ExpressionAccumulation boolean singleTrack = true; ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpressionWithoutTemporal(); - if(accexp == null) { + if(accexp == null || mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_MULTI)) { singleTrack = false; accexp = transformedExpression.getFirstAccumulationExpression(); } diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index 508242cb..ccb08e05 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -161,6 +161,7 @@ public class PrismSettings implements Observer //Accumulation public static final String ACC_GENERATE_DOTS = "accumulation.generateDots"; public static final String ACC_FORCE_COMPLEX = "accumulation.forceComplex"; + public static final String ACC_FORCE_MULTI = "accumulation.forceMulti"; //GUI Model public static final String MODEL_AUTO_PARSE = "model.autoParse"; @@ -416,7 +417,9 @@ public class PrismSettings implements Observer }, { { BOOLEAN_TYPE, ACC_GENERATE_DOTS, "Accumulation: generate DOT files", "4.4", false, "", "Generate DOT files for accumulation monitors and products"}, - { BOOLEAN_TYPE, ACC_FORCE_COMPLEX, "Accumulation: force U-construction", "4.4", false, "", "Force compxe accumulation construction"} + { BOOLEAN_TYPE, ACC_FORCE_COMPLEX, "Accumulation: force U-construction", "4.4", false, "", "Force complex accumulation construction"}, + { BOOLEAN_TYPE, ACC_FORCE_MULTI, "Accumulation: force multiple tracks", "4.4", false, "", "Force multiple accumulation tracks"} + }, { { BOOLEAN_TYPE, MODEL_AUTO_PARSE, "Auto parse", "2.1", new Boolean(true), "", "Parse PRISM models automatically as they are loaded/edited in the text editor." }, @@ -1700,6 +1703,10 @@ public class PrismSettings implements Observer set(ACC_FORCE_COMPLEX, true); } + else if (sw.equals("accforcemulti")) { + set(ACC_FORCE_MULTI, true); + } + // HIDDEN OPTIONS // export property automaton to file (hidden option) @@ -1900,6 +1907,7 @@ public class PrismSettings implements Observer mainLog.println(); mainLog.println("ACCUMULATION MODEL CHECKING OPTIONS:"); mainLog.println("-accforcecomplex ............... Force rewriting into complex until formulae for accumulation"); + mainLog.println("-accforcemulti.. ............... Force multiple accumulation tracks"); mainLog.println("-accgeneratedots ............... Generate DOT files for accumulation automata and products"); }