// ResourceBound: composition program enforcing a resource budget B on
// the shortest-path relaxation chain.  rho[j] is the total resource
// consumed along the chain that established G[j]; the constraint is
// rho[j] <= B.  Composed onto LLP-Dijkstra via predicate conjunction:
//   [ LLP-Dijkstra-Res(s, w, r, G, rho) && ResourceBound(rho, B) ].

class ResourceBound {
  int[] ResourceBound(int[] rho, int B, int[] G) {
    forbidden (j) : rho[j] > B =>
      advance : return null;
    return G;
  }
}