Browse Source

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

tud-infrastructure-2018-10-12
Joachim Klein 7 years ago
parent
commit
da4eda6c5d
  1. 4
      prism/src/prism/NondetModelChecker.java

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

Loading…
Cancel
Save