Browse Source

somewhat improved counting of winning region sizes

tempestpy_adaptions
Sebastian Junges 5 years ago
parent
commit
c9ef222a7f
  1. 12
      src/storm-pomdp/analysis/WinningRegion.cpp

12
src/storm-pomdp/analysis/WinningRegion.cpp

@ -226,7 +226,7 @@ namespace pomdp {
std::vector<storm::storage::BitVector> useIntersects; std::vector<storm::storage::BitVector> useIntersects;
std::vector<storm::storage::BitVector> useInfo; std::vector<storm::storage::BitVector> useInfo;
for(uint64_t i = 0; i < intersects.size(); ++i) { for(uint64_t i = 0; i < intersects.size(); ++i) {
if (upperBoundElements > 1000 && intersects[i].getNumberOfSetBits() < intersectSetSkip - 2) {
if (upperBoundElements > 10000 && intersects[i].getNumberOfSetBits() < intersectSetSkip - 3) {
skipped += (carl::pow(two, intersects[i].getNumberOfSetBits()) * origSets.size()); skipped += (carl::pow(two, intersects[i].getNumberOfSetBits()) * origSets.size());
STORM_LOG_DEBUG("Skipped " << skipped); STORM_LOG_DEBUG("Skipped " << skipped);
} else { } else {
@ -243,7 +243,7 @@ namespace pomdp {
std::vector<storm::storage::BitVector> newInfo; std::vector<storm::storage::BitVector> newInfo;
for (uint64_t i = 0; i < origSets.size(); ++i) { for (uint64_t i = 0; i < origSets.size(); ++i) {
if (upperBoundElements > 1000 && origSets[i].getNumberOfSetBits() < origSetSkip - 2) {
if (upperBoundElements > 20000 && origSets[i].getNumberOfSetBits() < origSetSkip - 3) {
skipped += (carl::pow(two, origSets[i].getNumberOfSetBits()) * useIntersects.size()); skipped += (carl::pow(two, origSets[i].getNumberOfSetBits()) * useIntersects.size());
STORM_LOG_DEBUG("Skipped " << skipped); STORM_LOG_DEBUG("Skipped " << skipped);
continue; continue;
@ -273,9 +273,11 @@ namespace pomdp {
auto res = count(origSets, newIntersects, newInfo, newVal, !plus, remdepth - 1); auto res = count(origSets, newIntersects, newInfo, newVal, !plus, remdepth - 1);
if (plus) { if (plus) {
return std::make_pair(res.first - skipped, res.second);
storm::RationalNumber tmp = res.first - skipped;
return std::make_pair(storm::utility::max(tmp, val), res.second);
} else { } else {
return std::make_pair(res.first, res.second + skipped);
storm::RationalNumber tmp = res.second + skipped;
return std::make_pair(res.first, storm::utility::min(tmp, val));
} }
} }
} }
@ -294,7 +296,7 @@ namespace pomdp {
entry.set(i); entry.set(i);
info.push_back(entry); info.push_back(entry);
} }
auto res = count(winningSets, winningSets, info, totalForObs, true, 6);
auto res = count(winningSets, winningSets, info, totalForObs, true, 40);
lower += res.first; lower += res.first;
upper += res.second; upper += res.second;
} }

Loading…
Cancel
Save