Browse Source

fixed min prob computation for single objective case

tempestpy_adaptions
TimQu 7 years ago
parent
commit
5c1de03d14
  1. 14
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

14
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@ -128,9 +128,19 @@ namespace storm {
choiceValue += *stepSolutionIt; choiceValue += *stepSolutionIt;
} }
if (isFirstChoice || choiceValue > bestValue) {
if (isFirstChoice) {
bestValue = std::move(choiceValue); bestValue = std::move(choiceValue);
isFirstChoice = false; isFirstChoice = false;
} else {
if (storm::solver::minimize(dir)) {
if (choiceValue < bestValue) {
bestValue = std::move(choiceValue);
}
} else {
if (choiceValue > bestValue) {
bestValue = std::move(choiceValue);
}
}
} }
} }
// Insert the solution w.r.t. this choice // Insert the solution w.r.t. this choice
@ -196,7 +206,7 @@ namespace storm {
std::cout << " #checked epochs: " << epochOrder.size() << "." << std::endl; std::cout << " #checked epochs: " << epochOrder.size() << "." << std::endl;
std::cout << " overall Time: " << swAll << "." << std::endl; std::cout << " overall Time: " << swAll << "." << std::endl;
std::cout << "Epoch Model building Time: " << swBuild << "." << std::endl; std::cout << "Epoch Model building Time: " << swBuild << "." << std::endl;
std::cout << "Epoch Model checking Time: " << swBuild << "." << std::endl;
std::cout << "Epoch Model checking Time: " << swCheck << "." << std::endl;
std::cout << "---------------------------------" << std::endl; std::cout << "---------------------------------" << std::endl;
return result; return result;

Loading…
Cancel
Save