From 436f9a1c5a6005a25cae308b1ac41e1cec37d0c6 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:24:42 +0200 Subject: [PATCH] imported patch ex-dtmc-weights-rewards-has-positive-negative.patch --- prism/src/explicit/DTMCModelChecker.java | 12 ++++++ prism/src/explicit/ZeroRewardECQuotient.java | 12 ++++++ .../rewards/MCRewardsFromMDPRewards.java | 13 ++++++ .../explicit/rewards/MDPRewardsSimple.java | 35 ++++++++++++++++ prism/src/explicit/rewards/Rewards.java | 19 +++++++++ .../explicit/rewards/STPGRewardsSimple.java | 1 + .../explicit/rewards/StateRewardsArray.java | 41 +++++++++++++++++-- .../rewards/StateRewardsConstant.java | 12 ++++++ .../explicit/rewards/StateRewardsSimple.java | 33 +++++++++++++++ 9 files changed, 175 insertions(+), 3 deletions(-) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index f96f0af3..640a9b5b 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -1405,6 +1405,18 @@ public class DTMCModelChecker extends ProbModelChecker { return false; } + + @Override + public boolean hasPositiveRewards() + { + return true; + } + + @Override + public boolean hasNegativeRewards() + { + return false; + } }; upperBound = DijkstraSweepMPI.computeUpperBound(this, mdp, mdpRewards, target, unknown); method = "Dijkstra Sweep MPI"; diff --git a/prism/src/explicit/ZeroRewardECQuotient.java b/prism/src/explicit/ZeroRewardECQuotient.java index 80a3234a..b5e330b2 100644 --- a/prism/src/explicit/ZeroRewardECQuotient.java +++ b/prism/src/explicit/ZeroRewardECQuotient.java @@ -165,6 +165,18 @@ public class ZeroRewardECQuotient { return rewards.hasTransitionRewards(); } + + @Override + public boolean hasPositiveRewards() + { + return rewards.hasPositiveRewards(); + } + + @Override + public boolean hasNegativeRewards() + { + return rewards.hasNegativeRewards(); + } }; if (debug) { diff --git a/prism/src/explicit/rewards/MCRewardsFromMDPRewards.java b/prism/src/explicit/rewards/MCRewardsFromMDPRewards.java index 4628de5c..9aef2074 100644 --- a/prism/src/explicit/rewards/MCRewardsFromMDPRewards.java +++ b/prism/src/explicit/rewards/MCRewardsFromMDPRewards.java @@ -71,4 +71,17 @@ public class MCRewardsFromMDPRewards implements MCRewards // only state rewards return false; } + + @Override + public boolean hasPositiveRewards() + { + return mdpRewards.hasPositiveRewards(); + } + + @Override + public boolean hasNegativeRewards() + { + return mdpRewards.hasNegativeRewards(); + } + } diff --git a/prism/src/explicit/rewards/MDPRewardsSimple.java b/prism/src/explicit/rewards/MDPRewardsSimple.java index d5d8c5cc..84159709 100644 --- a/prism/src/explicit/rewards/MDPRewardsSimple.java +++ b/prism/src/explicit/rewards/MDPRewardsSimple.java @@ -45,6 +45,11 @@ public class MDPRewardsSimple implements MDPRewards /** Transition rewards */ protected List> transRewards; + /** Flag: has positive rewards */ + protected boolean hasPositiveRewards = false; + /** Flag: has negative rewards */ + protected boolean hasNegativeRewards = false; + /** * Constructor: all zero rewards. * @param numStates Number of states @@ -90,6 +95,8 @@ public class MDPRewardsSimple implements MDPRewards } } } + this.hasPositiveRewards = rews.hasPositiveRewards; + this.hasNegativeRewards = rews.hasNegativeRewards; } // Mutators @@ -107,6 +114,7 @@ public class MDPRewardsSimple implements MDPRewards } // Set reward stateRewards.set(s, r); + updateFlags(r); } /** @@ -145,6 +153,7 @@ public class MDPRewardsSimple implements MDPRewards } // Set reward list.set(i, r); + updateFlags(r); } /** @@ -165,6 +174,19 @@ public class MDPRewardsSimple implements MDPRewards transRewards.set(s, null); } } + + /** + * Update the flags for positive / negative rewards by taking + * value r into account. + */ + protected void updateFlags(double r) + { + if (r > 0) { + hasPositiveRewards = true; + } else if (r < 0) { + hasNegativeRewards = true; + } + } // Accessors @@ -225,4 +247,17 @@ public class MDPRewardsSimple implements MDPRewards { return transRewards != null; } + + @Override + public boolean hasPositiveRewards() + { + return hasPositiveRewards; + } + + @Override + public boolean hasNegativeRewards() + { + return hasNegativeRewards; + } + } diff --git a/prism/src/explicit/rewards/Rewards.java b/prism/src/explicit/rewards/Rewards.java index f8d07ae4..0160aca9 100644 --- a/prism/src/explicit/rewards/Rewards.java +++ b/prism/src/explicit/rewards/Rewards.java @@ -43,4 +43,23 @@ public interface Rewards /** Returns true if this reward structure has transition rewards */ public boolean hasTransitionRewards(); + + /** + * Returns true if this reward structure has positive (>0) rewards. + *
+ * Note: This information is best-effort. E.g., a reward structure that + * contained a positive reward at some time, which was later on overwritten + * may still return true. + */ + public boolean hasPositiveRewards(); + + /** + * Returns true if this reward structure has negative (<0) rewards. + *
+ * Note: This information is best-effort. E.g., a reward structure that + * contained a positive reward at some time, which was later on overwritten + * may still return true. + */ + public boolean hasNegativeRewards(); + } diff --git a/prism/src/explicit/rewards/STPGRewardsSimple.java b/prism/src/explicit/rewards/STPGRewardsSimple.java index 4acc520b..ae721721 100644 --- a/prism/src/explicit/rewards/STPGRewardsSimple.java +++ b/prism/src/explicit/rewards/STPGRewardsSimple.java @@ -108,6 +108,7 @@ public class STPGRewardsSimple extends MDPRewardsSimple implements STPGRewards } // Set reward list2.set(j, r); + updateFlags(r); } /** diff --git a/prism/src/explicit/rewards/StateRewardsArray.java b/prism/src/explicit/rewards/StateRewardsArray.java index bc360788..7794f96d 100644 --- a/prism/src/explicit/rewards/StateRewardsArray.java +++ b/prism/src/explicit/rewards/StateRewardsArray.java @@ -37,6 +37,11 @@ public class StateRewardsArray extends StateRewards /** Array of state rewards **/ protected double stateRewards[] = null; + /** Flag: has positive rewards */ + protected boolean hasPositiveRewards = false; + /** Flag: has negative rewards */ + protected boolean hasNegativeRewards = false; + /** * Constructor: all zero rewards. * @param numStates Number of states @@ -60,6 +65,8 @@ public class StateRewardsArray extends StateRewards for (int i = 0; i < numStates; i++) { stateRewards[i] = rews.stateRewards[i]; } + hasPositiveRewards = rews.hasPositiveRewards; + hasNegativeRewards = rews.hasNegativeRewards; } // Mutators @@ -70,6 +77,7 @@ public class StateRewardsArray extends StateRewards public void setStateReward(int s, double r) { stateRewards[s] = r; + updateFlags(r); } /** @@ -77,9 +85,24 @@ public class StateRewardsArray extends StateRewards */ public void addToStateReward(int s, double r) { - stateRewards[s] += r; + double v; + v = stateRewards[s] += r; + updateFlags(v); } - + + /** + * Update the flags for positive / negative rewards by taking + * value r into account. + */ + private void updateFlags(double r) + { + if (r > 0) { + hasPositiveRewards = true; + } else if (r < 0) { + hasNegativeRewards = true; + } + } + // Accessors @Override @@ -87,7 +110,19 @@ public class StateRewardsArray extends StateRewards { return stateRewards[s]; } - + + @Override + public boolean hasPositiveRewards() + { + return hasPositiveRewards; + } + + @Override + public boolean hasNegativeRewards() + { + return hasNegativeRewards; + } + // Converters @Override diff --git a/prism/src/explicit/rewards/StateRewardsConstant.java b/prism/src/explicit/rewards/StateRewardsConstant.java index 76fee3b5..1cdb7968 100644 --- a/prism/src/explicit/rewards/StateRewardsConstant.java +++ b/prism/src/explicit/rewards/StateRewardsConstant.java @@ -67,4 +67,16 @@ public class StateRewardsConstant extends StateRewards { return new StateRewardsConstant(stateReward); } + + @Override + public boolean hasPositiveRewards() + { + return stateReward > 0; + } + + @Override + public boolean hasNegativeRewards() + { + return stateReward < 0; + } } diff --git a/prism/src/explicit/rewards/StateRewardsSimple.java b/prism/src/explicit/rewards/StateRewardsSimple.java index 5d3d7739..c8fd0361 100644 --- a/prism/src/explicit/rewards/StateRewardsSimple.java +++ b/prism/src/explicit/rewards/StateRewardsSimple.java @@ -39,6 +39,11 @@ public class StateRewardsSimple extends StateRewards /** Arraylist of state rewards **/ protected ArrayList stateRewards; + /** Flag: has positive rewards */ + protected boolean hasPositiveRewards = false; + /** Flag: has negative rewards */ + protected boolean hasNegativeRewards = false; + /** * Constructor: all zero rewards. */ @@ -62,6 +67,8 @@ public class StateRewardsSimple extends StateRewards stateRewards.add(rews.stateRewards.get(i)); } } + hasPositiveRewards = rews.hasPositiveRewards; + hasNegativeRewards = rews.hasNegativeRewards; } // Mutators @@ -82,6 +89,20 @@ public class StateRewardsSimple extends StateRewards } // Set reward stateRewards.set(s, r); + updateFlags(r); + } + + /** + * Update the flags for positive / negative rewards by taking + * value r into account. + */ + private void updateFlags(double r) + { + if (r > 0) { + hasPositiveRewards = true; + } else if (r < 0) { + hasNegativeRewards = true; + } } // Accessors @@ -96,6 +117,18 @@ public class StateRewardsSimple extends StateRewards } } + @Override + public boolean hasPositiveRewards() + { + return hasPositiveRewards; + } + + @Override + public boolean hasNegativeRewards() + { + return hasNegativeRewards; + } + // Converters @Override