diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index 64e1281e..3fb20a5f 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/prism/src/prism/MultiObjModelChecker.java @@ -606,7 +606,7 @@ public class MultiObjModelChecker extends PrismComponent no = JDD.Constant(0); bottomec = PrismMTBDD.Prob0A(model.getTrans01(), model.getReach(), model.getAllDDRowVars(), model.getAllDDColVars(), model.getAllDDNondetVars(), model.getReach(), yes); - List becs = mcLtl.findBottomEndComponents(model, bottomec); + List becs = mcLtl.findMECStates(model, bottomec); JDD.Deref(bottomec); bottomec = JDD.Constant(0); for (JDDNode ec : becs) diff --git a/prism/src/sparse/PS_NondetMultiReachReward.cc b/prism/src/sparse/PS_NondetMultiReachReward.cc index 35b97894..3bc51c96 100644 --- a/prism/src/sparse/PS_NondetMultiReachReward.cc +++ b/prism/src/sparse/PS_NondetMultiReachReward.cc @@ -170,13 +170,13 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti // Display some info about the rewards PS_PrintToMainLog(env, "\n%d Rewards:\n", num_rewards); - //bool disable_selfloop = true; + bool disable_selfloop = true; for (i = 0; i < num_rewards; i++) { PS_PrintToMainLog(env, "#%d: ", i); switch (relopsReward[i]) { - case 3: PS_PrintToMainLog(env, "Rmax=?\n"); /*disable_selfloop = false;*/ break; + case 3: PS_PrintToMainLog(env, "Rmax=?\n"); disable_selfloop = false; break; case 8: PS_PrintToMainLog(env, "Rmin=?\n"); break; - case 4: PS_PrintToMainLog(env, "R>=%g\n", boundsReward[i]); /*disable_selfloop = false;*/ break; + case 4: PS_PrintToMainLog(env, "R>=%g\n", boundsReward[i]); disable_selfloop = false; break; case 9: PS_PrintToMainLog(env, "R<=%g\n", boundsReward[i]); break; } } @@ -194,11 +194,13 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti // For efficiency, remove any probability 1 self-loops from the model. // For multi-objective, we always do maximum reachability, so these do not matter. - Cudd_Ref(a); - loops = DD_And(ddman, DD_Equals(ddman, a, 1.0), DD_Identity(ddman, rvars, cvars, num_rvars)); - loops = DD_ThereExists(ddman, loops, cvars, num_rvars); - Cudd_Ref(loops); - a = DD_ITE(ddman, loops, DD_Constant(ddman, 0), a); + if (!disable_selfloop) { + Cudd_Ref(a); + loops = DD_And(ddman, DD_Equals(ddman, a, 1.0), DD_Identity(ddman, rvars, cvars, num_rvars)); + loops = DD_ThereExists(ddman, loops, cvars, num_rvars); + Cudd_Ref(loops); + a = DD_ITE(ddman, loops, DD_Constant(ddman, 0), a); + } // Get number of states n = odd->eoff + odd->toff; @@ -589,7 +591,7 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti // Set objective function for LP PS_PrintToMainLog(env, "Setting objective...\n"); isMax = true; - if(relops[0] == 0) { + if(num_targets > 0 && relops[0] == 0) { x = 0; for(i=0; i 0) { diff --git a/prism/src/sparse/PS_NondetMultiReachReward1.cc b/prism/src/sparse/PS_NondetMultiReachReward1.cc index 1050a246..fedc8e9f 100644 --- a/prism/src/sparse/PS_NondetMultiReachReward1.cc +++ b/prism/src/sparse/PS_NondetMultiReachReward1.cc @@ -191,13 +191,13 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti // Display some info about the rewards PS_PrintToMainLog(env, "\n%d Rewards:\n", num_rewards); - //bool disable_selfloop = true; + bool disable_selfloop = true; for (i = 0; i < num_rewards; i++) { PS_PrintToMainLog(env, "#%d: ", i); switch (relopsReward[i]) { - case 3: PS_PrintToMainLog(env, "Rmax=?\n"); /*disable_selfloop = false;*/ break; + case 3: PS_PrintToMainLog(env, "Rmax=?\n"); disable_selfloop = false; break; case 8: PS_PrintToMainLog(env, "Rmin=?\n"); break; - case 4: PS_PrintToMainLog(env, "R>=%g\n", boundsReward[i]); /*disable_selfloop = false;*/ break; + case 4: PS_PrintToMainLog(env, "R>=%g\n", boundsReward[i]); disable_selfloop = false; break; case 9: PS_PrintToMainLog(env, "R<=%g\n", boundsReward[i]); break; } } @@ -219,11 +219,13 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti // For efficiency, remove any probability 1 self-loops from the model. // For multi-objective, we always do maximum reachability, so these do not matter. - Cudd_Ref(a); - loops = DD_And(ddman, DD_Equals(ddman, a, 1.0), DD_Identity(ddman, rvars, cvars, num_rvars)); - loops = DD_ThereExists(ddman, loops, cvars, num_rvars); - Cudd_Ref(loops); - a = DD_ITE(ddman, loops, DD_Constant(ddman, 0), a); + if(!disable_selfloop) { + Cudd_Ref(a); + loops = DD_And(ddman, DD_Equals(ddman, a, 1.0), DD_Identity(ddman, rvars, cvars, num_rvars)); + loops = DD_ThereExists(ddman, loops, cvars, num_rvars); + Cudd_Ref(loops); + a = DD_ITE(ddman, loops, DD_Constant(ddman, 0), a); + } // Get number of states n = odd->eoff + odd->toff; @@ -651,7 +653,7 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti // Set objective function for LP PS_PrintToMainLog(env, "Setting objective...\n"); isMax = true; - if(relops[0] == 0) { + if(num_targets > 0 && relops[0] == 0) { x = 0; for(i=0; i