From 85e6a903ba74a6e6fc209cfbc30c04e669da1d97 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 21 Dec 2015 16:14:15 +0000 Subject: [PATCH] Bug fix: Value iteration multi-objective was removing self-loops in situations where it should not be. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11061 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/MultiObjModelChecker.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index e89b8abf..10d32de2 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/prism/src/prism/MultiObjModelChecker.java @@ -1087,7 +1087,7 @@ public class MultiObjModelChecker extends PrismComponent //create a sparse matrix for transitions JDDNode a = JDD.Apply(JDD.TIMES, modelProduct.getTrans(), modelProduct.getReach()); - if (!min) { + if (!min && dimReward == 0) { JDD.Ref(a); JDDNode tmp = JDD.And(JDD.Equals(a, 1.0), JDD.Identity(modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars())); a = JDD.ITE(tmp, JDD.Constant(0), a);