From 35786a8b38e315c6b034012f1bb7b004bef95737 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:26:30 +0200 Subject: [PATCH] imported patch NondetModelChecker-cosafety-guard-against-rewards.patch --- prism/src/prism/NondetModelChecker.java | 4 ++++ 1 file changed, 4 insertions(+) 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"); }