Browse Source

imported patch NondetModelChecker-cosafety-guard-against-rewards.patch

accumulation-v4.7
Joachim Klein 7 years ago
committed by Joachim Klein
parent
commit
35786a8b38
  1. 4
      prism/src/prism/NondetModelChecker.java

4
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");
}

Loading…
Cancel
Save