From e0d68f8b744ab9b6e1ae932fcbd4ca497835f415 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 8 Aug 2012 15:02:32 +0000 Subject: [PATCH] Bug fix: PTA rewards on digital clocks: forgot to scale by GCD. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5523 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/pta/DigitalClocks.java | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java index 637cb25d..b3f05fc3 100644 --- a/prism/src/pta/DigitalClocks.java +++ b/prism/src/pta/DigitalClocks.java @@ -293,7 +293,12 @@ public class DigitalClocks RewardStructItem rsi = rs.getRewardStructItem(i); // Convert state rewards if (!rsi.isTransitionReward()) { - rsi = new RewardStructItem(timeAction, rsi.getStates().deepCopy(), rsi.getReward().deepCopy()); + // Scale reward by clock GCD + Expression rew = rsi.getReward().deepCopy(); + if (cci.getScaleFactor() > 1) { + rew = Expression.Times(rew, Expression.Int(cci.getScaleFactor())); + } + rsi = new RewardStructItem(timeAction, rsi.getStates().deepCopy(), rew); rs.setRewardStructItem(i, rsi); } }