Skip to content
Snippets Groups Projects
Commit 2f20f153 authored by Ben Plummer's avatar Ben Plummer
Browse files

Ensure termination with a max energy bound

parent 9a546a37
No related tags found
No related merge requests found
......@@ -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;
}
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment