Browse Source

Added an exception for the case when -lp is used for multi-objective, and there is a finite step bound. Up until now no warning was given and the step bound was ignored (treated as infinite)

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11074 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Vojtech Forejt 10 years ago
parent
commit
f4961ba4ed
  1. 5
      prism/src/prism/MultiObjModelChecker.java

5
prism/src/prism/MultiObjModelChecker.java

@ -666,6 +666,11 @@ public class MultiObjModelChecker extends PrismComponent
// Do computation
// Linear programming
if (method == Prism.MDP_MULTI_LP) {
if (opsAndBounds.numberOfStepBounded() > 0) {
throw new PrismNotSupportedException("Step-bounded objectives are not currently supported with linear programming");
}
if (opsAndBounds.rewardSize() > 0) {
if (hasconflictobjectives) {
value = PrismSparse.NondetMultiReachReward1(model.getTrans(), model.getTransActions(), model.getSynchs(), model.getODD(),

Loading…
Cancel
Save