From ac1ea31b4ffa47aae81a420a0fcb0f154ede9083 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 21 Jun 2021 21:51:05 +0200 Subject: [PATCH] accumulation: Fix reward construction UNTESTED --- prism/src/explicit/AccumulationTransformation.java | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java index 4c339e89..9d0c78ae 100644 --- a/prism/src/explicit/AccumulationTransformation.java +++ b/prism/src/explicit/AccumulationTransformation.java @@ -116,11 +116,8 @@ public class AccumulationTransformation implements Mode for (int i=0; i < accexp.getFunctions().size(); i++) { Object rewardIndex = accexp.getFunctions().get(i).getRewardIndex(); - RewardStruct rewStruct = ExpressionReward.getRewardStructByIndexObject(rewardIndex, mc.modulesFile, originalModel.getConstantValues()); - ConstructRewards constructRewards = new ConstructRewards(); - constructRewards.allowNegativeRewards(); - - Rewards reward = constructRewards.buildRewardStructure(originalModel, rewStruct, mc.getConstantValues()); + int rewStructIndex = ExpressionReward.getRewardStructIndexByIndexObject(rewardIndex, mc.modulesFile, originalModel.getConstantValues()); + Rewards reward = ((ProbModelChecker)mc).constructRewards(originalModel, rewStructIndex, true /* allow negative rewards */); rewards.put(rewardIndex,reward); }