From 967dcef326388ba29f0058a1d2e15d1151eb5727 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 13 Jul 2010 19:47:38 +0000 Subject: [PATCH] Yet another fix for adversary generation: previous fix was only for max (prob or exp reach) so now split into 2 cases for min/max. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1983 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/sparse/PS_NondetReachReward.cc | 22 ++++++++++++---------- prism/src/sparse/PS_NondetUntil.cc | 22 ++++++++++++---------- 2 files changed, 24 insertions(+), 20 deletions(-) diff --git a/prism/src/sparse/PS_NondetReachReward.cc b/prism/src/sparse/PS_NondetReachReward.cc index 71f3253c..e4aa9f95 100644 --- a/prism/src/sparse/PS_NondetReachReward.cc +++ b/prism/src/sparse/PS_NondetReachReward.cc @@ -297,13 +297,19 @@ jboolean min // min or max probabilities (true = min, false = max) // see if this value is the min/max so far if (first || (min&&(d2d1))) { d1 = d2; - // if adversary generation is enabled, remember new (strictly) better choices + // if adversary generation is enabled, remember optimal choice if (export_adv_enabled != EXPORT_ADV_NONE) { - if (adv[i] == -1 || (min&&(d1soln[i]))) { - // NB: don't overwrite adv[i] yet, just make a note that we need to update it - // (want to remember if is -1: this is necessary for (at least) min rewards) - adv_j = j; - adv_new = true; + // for max, only remember strictly better choices + // (this resolves problems with end components) + if (!min) { + if (adv[i] == -1 || (d1>soln[i])) { + adv[i] = j; + } + } + // for min, this is straightforward + // (in fact, could do it at the end of value iteration, but we don't) + else { + adv[i] = j; } } } @@ -312,10 +318,6 @@ jboolean min // min or max probabilities (true = min, false = max) // set vector element // (if there were no choices from this state, reward is zero/infinity) soln2[i] = (h1 > l1) ? d1 : inf_vec[i] > 0 ? HUGE_VAL : 0; - // store adversary choice (if required) - if (export_adv_enabled != EXPORT_ADV_NONE && adv_new) { - adv[i] = adv_j; - } } // check convergence diff --git a/prism/src/sparse/PS_NondetUntil.cc b/prism/src/sparse/PS_NondetUntil.cc index bf35e8b2..1c1b0576 100644 --- a/prism/src/sparse/PS_NondetUntil.cc +++ b/prism/src/sparse/PS_NondetUntil.cc @@ -250,13 +250,19 @@ jboolean min // min or max probabilities (true = min, false = max) } if (first || (min&&(d2d1))) { d1 = d2; - // if adversary generation is enabled, remember new (strictly) better choices + // if adversary generation is enabled, remember optimal choice if (export_adv_enabled != EXPORT_ADV_NONE) { - if (adv[i] == -1 || (min&&(d1soln[i]))) { - // NB: don't overwrite adv[i] yet, just make a note that we need to update it - // (want to remember if is -1: this is necessary for (at least) min rewards) - adv_j = j; - adv_new = true; + // for max, only remember strictly better choices + // (this resolves problems with end components) + if (!min) { + if (adv[i] == -1 || (d1>soln[i])) { + adv[i] = j; + } + } + // for min, this is straightforward + // (in fact, could do it at the end of value iteration, but we don't) + else { + adv[i] = j; } } } @@ -265,10 +271,6 @@ jboolean min // min or max probabilities (true = min, false = max) // set vector element // (if no choices, use value of yes) soln2[i] = (h1 > l1) ? d1 : yes_vec[i]; - // store adversary choice (if required) - if (export_adv_enabled != EXPORT_ADV_NONE && adv_new) { - adv[i] = adv_j; - } } // check convergence