From 2f20f1533b33e23e9eeccdd9366145a62207111c Mon Sep 17 00:00:00 2001
From: Ben Plummer <dev@ben-plummer.com>
Date: Thu, 24 Nov 2022 12:37:08 +0000
Subject: [PATCH] Ensure termination with a max energy bound

---
 prism/src/explicit/RBGModelChecker.java | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/prism/src/explicit/RBGModelChecker.java b/prism/src/explicit/RBGModelChecker.java
index ff86a0d8a..9da91cdd5 100644
--- a/prism/src/explicit/RBGModelChecker.java
+++ b/prism/src/explicit/RBGModelChecker.java
@@ -19,6 +19,7 @@ public class RBGModelChecker extends StateModelChecker {
     List<TransList> transitions;
     BitSet accept;
     Rewards rewards;
+    double energyBound;
 
 
     private AcceptanceType[] acceptance = {
@@ -91,6 +92,14 @@ public class RBGModelChecker extends StateModelChecker {
         Rewards modelRewards = constructRewards(model);
         rewards      = modelRewards.liftFromModel(ltlProduct);
 
+        // Calculate energy bound
+        double maxWeight = 0;
+        for (TransList tl : transitions)
+            for (Map.Entry<Integer, Double> t : tl)
+                maxWeight = t.getValue() > maxWeight ? t.getValue() : maxWeight;
+        int numStates = ltlProduct.getProductModel().getNumStates();
+        energyBound = 2 * (numStates - 1) * maxWeight;
+
         List<Decorator> dec = List.of(new ShowRewardDecorator(rewards));
         ltlProduct.getProductModel().exportToDotFile("out/product.dot", /*accept,*/ dec);
         ltlProduct.getOriginalModel().exportToDotFile("out/model.dot", List.of(new ShowRewardDecorator(modelRewards)));
@@ -151,8 +160,9 @@ public class RBGModelChecker extends StateModelChecker {
                     ext[src] = ext[target] + weight - reward;
             }
 
-            // Normalise above 0
+            // Keep extents between 0 and the max energy bound
             if (ext[src] < 0) ext[src] = 0;
+            if (ext[src] > energyBound) ext[src] = Double.POSITIVE_INFINITY;
         }
     }
 
-- 
GitLab