From 8f2f9a3d28472ac78e45497b0f39dd5451f2214e Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 25 Jul 2017 20:45:43 +0000 Subject: [PATCH] Bug fix in prism.ModelGenerator2MTBDD: action names were not being read properly. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12167 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/ModelGenerator2MTBDD.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/prism/src/prism/ModelGenerator2MTBDD.java b/prism/src/prism/ModelGenerator2MTBDD.java index febcfa87..bc7ff3b9 100644 --- a/prism/src/prism/ModelGenerator2MTBDD.java +++ b/prism/src/prism/ModelGenerator2MTBDD.java @@ -484,8 +484,8 @@ public class ModelGenerator2MTBDD /// ...for mdps... else { tmp = JDD.ThereExists(elem.copy(), allDDColVars); - // use max here because we see multiple transitions for a sinlge choice - transActions = JDD.Apply(JDD.MAX, transActions, JDD.Apply(JDD.TIMES, JDD.Constant(j), tmp)); + // use max here because we see multiple transitions for a single choice + transActions = JDD.Apply(JDD.MAX, transActions, JDD.Apply(JDD.TIMES, JDD.Constant(k), tmp)); } // Add action rewards