From 07ad85ac252764ef9a71c77289f158c1ffd08277 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 17 Mar 2010 10:10:18 +0000 Subject: [PATCH] Optimisation in MDP until - remove prob 1 self-loops for max (also fixes some simple adv gen problems). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1810 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/sparse/PS_NondetUntil.cc | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/prism/src/sparse/PS_NondetUntil.cc b/prism/src/sparse/PS_NondetUntil.cc index 5ea3fe2d..f84e9b23 100644 --- a/prism/src/sparse/PS_NondetUntil.cc +++ b/prism/src/sparse/PS_NondetUntil.cc @@ -107,6 +107,18 @@ jboolean min // min or max probabilities (true = min, false = max) Cudd_Ref(maybe); a = DD_Apply(ddman, APPLY_TIMES, trans, maybe); + // When computing maximum reachability probabilities, + // we can safely remove any probability 1 self-loops for efficiency. + // This might leave some states with no choices (only if no precomp done) + // but this is not a problem, for value iteration. + // This is also motivated by the fact that this fixes some simple problem + // cases for adversary generation. + if (!min) { + Cudd_Ref(a); + tmp = DD_And(ddman, DD_Equals(ddman, a, 1.0), DD_Identity(ddman, rvars, cvars, num_rvars)); + a = DD_ITE(ddman, tmp, DD_Constant(ddman, 0), a); + } + // get number of states n = odd->eoff + odd->toff;