From c3b802994ea8044bddcd5a096d21707fa67f3776 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Tue, 23 Feb 2016 16:40:33 +0000 Subject: [PATCH] Modules2PTA: fix handling of probabilities in commands that refer to state variables [bug found by Linda Leuschner] When translating the module state variables to locations, probabilities in commands were not translated. If the probability expression contains a reference to the state variables, e.g., (s=0 ? 0.5 : 0.75) then the variable reference persists, which leads to an exception when updating variable information of the module later on, as the state variable is no longer defined in the translated module. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11215 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/pta/Modules2PTA.java | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/prism/src/pta/Modules2PTA.java b/prism/src/pta/Modules2PTA.java index 572cf4c5..6063c74c 100644 --- a/prism/src/pta/Modules2PTA.java +++ b/prism/src/pta/Modules2PTA.java @@ -606,7 +606,15 @@ public class Modules2PTA extends PrismComponent updateNew.addElement(update.getVarIdent(k), update.getExpression(k)); } } - updatesNew.addUpdate(updates.getProbability(j), updateNew); + // we translate the probability as well, as it may reference states + Expression probNew = updates.getProbability(j); + if (probNew != null) { + // if probability expression is null, it implicitly encodes probability 1, + // so we don't have to change anything + probNew = probNew.deepCopy(); + probNew = (Expression) probNew.evaluatePartially(state, varMap).simplify(); + } + updatesNew.addUpdate(probNew, updateNew); } // Add new stuff to new module commandNew.setUpdates(updatesNew);