From 9729c78b3ef2b186f70924b25f56af16377be5e6 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 19 May 2015 09:38:59 +0000 Subject: [PATCH] Inefficiency in precomputatino routines in explicit engine (spotted by Steffen Marcker). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9850 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/MDPSimple.java | 12 ++++++------ prism/src/explicit/MDPSparse.java | 18 +++++++++--------- 2 files changed, 15 insertions(+), 15 deletions(-) diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index 97d1bf32..0fb287a1 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -588,12 +588,12 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple if (forall) { if (!b2) { b1 = false; - continue; + break; } } else { if (b2) { b1 = true; - continue; + break; } } } @@ -610,7 +610,7 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple for (Distribution distr : trans.get(i)) { if (!(distr.isSubsetOf(u) && distr.containsOneOf(v))) { b1 = false; - continue; + break; } } result.set(i, b1); @@ -631,7 +631,7 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple // If strategy generation is enabled, remember optimal choice if (strat != null) stratCh = j; - continue; + break; } j++; } @@ -656,12 +656,12 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple if (forall) { if (!b2) { b1 = false; - continue; + break; } } else { if (b2) { b1 = true; - continue; + break; } } } diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index a137bc2a..278a3231 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -628,18 +628,18 @@ public class MDPSparse extends MDPExplicit // Assume that only non-zero entries are stored if (u.get(cols[k])) { some = true; - continue; + break; } } if (forall) { if (!some) { b1 = false; - continue; + break; } } else { if (some) { b1 = true; - continue; + break; } } } @@ -665,7 +665,7 @@ public class MDPSparse extends MDPExplicit // Assume that only non-zero entries are stored if (!u.get(cols[k])) { all = false; - continue; // Stop early (already know b1 will be set to false) + break; // Stop early (already know b1 will be set to false) } if (v.get(cols[k])) { some = true; @@ -673,7 +673,7 @@ public class MDPSparse extends MDPExplicit } if (!(some && all)) { b1 = false; - continue; + break; } } result.set(i, b1); @@ -698,7 +698,7 @@ public class MDPSparse extends MDPExplicit // Assume that only non-zero entries are stored if (!u.get(cols[k])) { all = false; - continue; // Stop early (already know b1 will not be set to true) + break; // Stop early (already know b1 will not be set to true) } if (v.get(cols[k])) { some = true; @@ -709,7 +709,7 @@ public class MDPSparse extends MDPExplicit // If strategy generation is enabled, remember optimal choice if (strat != null) stratCh = j - l1; - continue; + break; } } // If strategy generation is enabled, store optimal choice @@ -748,12 +748,12 @@ public class MDPSparse extends MDPExplicit if (forall) { if (!(some && all)) { b1 = false; - continue; + break; } } else { if (some && all) { b1 = true; - continue; + break; } } }