diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 90f1b931..dd4542f6 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1579,6 +1579,10 @@ public class NondetModelChecker extends NonProbModelChecker throw new PrismException("Model checking for \"dfa\" specifications not supported yet"); } + if (Expression.containsTemporalRewardBounds(expr)) { + throw new PrismException("Can not handle reward bounds via deterministic automata."); + } + if (Expression.isHOA(expr)) { throw new PrismNotSupportedException("Co-safety rewards with HOA automata not supported yet"); }