From 759d588ae32516ce59b8958317dd62158612d460 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Tue, 24 Jul 2018 11:10:44 +0200 Subject: [PATCH] param/exact: Transitions that fix a deadlock don't earn transition rewards Same fix as in the explicit engine (eeb801618474323bc4002353eaf35c15caa82850), for issue #29. This change can currently not be detected by any of the properties supported by the exact/parametric engine. --- prism/src/param/ParamModelChecker.java | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index f0791acf..fda74d59 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/prism/src/param/ParamModelChecker.java @@ -1124,6 +1124,12 @@ final public class ParamModelChecker extends PrismComponent String action = rewStruct.getSynch(rewItem); boolean isTransitionReward = rewStruct.getRewardStructItem(rewItem).isTransitionReward(); for (int state = 0; state < numStates; state++) { + if (isTransitionReward && model.isDeadlockState(state)) { + // As state is a deadlock state, any outgoing transition + // was added to "fix" the deadlock and thus does not get a reward. + // Skip to next state + continue; + } if (guard.evaluateExact(constantValues, statesList.get(state)).toBoolean()) { int[] varMap = new int[statesList.get(0).varValues.length]; for (int i = 0; i < varMap.length; i++) {