Browse Source

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
master
Dave Parker 9 years ago
parent
commit
8f2f9a3d28
  1. 4
      prism/src/prism/ModelGenerator2MTBDD.java

4
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

Loading…
Cancel
Save