From 45466e9f1caf7a45ac616493140acc9b9af95db1 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 23 Aug 2016 16:51:57 +0000 Subject: [PATCH] Minor refactoring (for branch synching). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11695 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCModelChecker.java | 6 ++++-- prism/src/explicit/MDPModelChecker.java | 6 ++++-- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index e6c5b305..70e90811 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -112,7 +112,8 @@ public class DTMCModelChecker extends ProbModelChecker mainLog.println("\nComputing reachability probabilities..."); mcProduct = new DTMCModelChecker(this); mcProduct.inheritSettings(this); - probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs(product.getProductModel(), acc).soln, product.getProductModel()); + ModelCheckerResult res = mcProduct.computeReachProbs(product.getProductModel(), acc); + probsProduct = StateValues.createFromDoubleArray(res.soln, product.getProductModel()); // Output vector over product, if required if (getExportProductVector()) { @@ -183,7 +184,8 @@ public class DTMCModelChecker extends ProbModelChecker mainLog.println("\nComputing reachability probabilities..."); mcProduct = new DTMCModelChecker(this); mcProduct.inheritSettings(this); - rewardsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachRewards(product.getProductModel(), productRewards, acc).soln, product.getProductModel()); + ModelCheckerResult res = mcProduct.computeReachRewards(product.getProductModel(), productRewards, acc); + rewardsProduct = StateValues.createFromDoubleArray(res.soln, product.getProductModel()); // Output vector over product, if required if (getExportProductVector()) { diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 30879e73..517e445c 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -123,7 +123,8 @@ public class MDPModelChecker extends ProbModelChecker mainLog.println("\nComputing reachability probabilities..."); mcProduct = new MDPModelChecker(this); mcProduct.inheritSettings(this); - probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((MDP)product.getProductModel(), acc, false).soln, product.getProductModel()); + ModelCheckerResult res = mcProduct.computeReachProbs((MDP) product.getProductModel(), acc, false); + probsProduct = StateValues.createFromDoubleArray(res.soln, product.getProductModel()); // Subtract from 1 if we're model checking a negated formula for regular Pmin if (minMax.isMin()) { @@ -202,7 +203,8 @@ public class MDPModelChecker extends ProbModelChecker mainLog.println("\nComputing reachability rewards..."); mcProduct = new MDPModelChecker(this); mcProduct.inheritSettings(this); - rewardsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachRewards(product.getProductModel(), productRewards, acc, minMax.isMin()).soln, product.getProductModel()); + ModelCheckerResult res = mcProduct.computeReachRewards(product.getProductModel(), productRewards, acc, minMax.isMin()); + rewardsProduct = StateValues.createFromDoubleArray(res.soln, product.getProductModel()); // Output vector over product, if required if (getExportProductVector()) {