diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index e595e28d..2c424535 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1580,6 +1580,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"); }