From 43b22d170bb9cae079a46bca9b7b69bf92a2c78c Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Sun, 12 May 2019 15:53:49 +0200 Subject: [PATCH] CTMC steady explicit: Fix regression introduced by #116 PR #116 (in particular 5c33a555ac85465393c30609e0f253cfd1b839aa) moved the post-processing of the BSCC steady state probabilities (weighing by the exit rates of the CTMC) into computeSteadyStateProbsForBSCC(). This introduced a regression, leading to wrong results, as the post-processing would be applied on the solution vector that was returned by the method, but not necessarily on the values passed back out via the result argument vector. We fix this by moving the post-processing up, before the copy and adding a note of caution. Failure e.g. for prism prism-tests/papers/Par02/Par02-3.3.3.sm prism-tests/papers/Par02/Par02-3.3.3.sm.props -explicit -testall --- prism/src/explicit/DTMCModelChecker.java | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 5df7221e..41d2fbd1 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -2553,6 +2553,11 @@ public class DTMCModelChecker extends ProbModelChecker iterationsExport.close(); } + // Apply post processing on soln + if (bsccPostProcessor != null) { + bsccPostProcessor.apply(soln, states); + } + if (result != null && result != soln) { // If result vector was passed in as method argument, // it can be the case that result does not point to the current soln vector (most recent values) @@ -2563,6 +2568,10 @@ public class DTMCModelChecker extends ProbModelChecker result[state] = soln[state]; } } + // + // NOTE: from here on, don't change the values of result/soln, + // as the values may have already been copied to the result vector above + // // store only one result vector, free temporary vectors result = soln; soln = soln2 = null; @@ -2574,11 +2583,6 @@ public class DTMCModelChecker extends ProbModelChecker throw new PrismException(msg); } - // Apply post processing - if (bsccPostProcessor != null) { - bsccPostProcessor.apply(result, states); - } - // Return results ModelCheckerResult res = new ModelCheckerResult(); res.soln = result;