Browse Source

Property information output

tempestpy_adaptions
TimQu 7 years ago
parent
commit
e3a506ecc6
  1. 14
      src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
  2. 11
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

14
src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp

@ -50,13 +50,17 @@ namespace storm {
auto epochOrder = rewardUnfolding.getEpochComputationOrder(initEpoch);
EpochCheckingData cachedData;
ValueType precision = storm::utility::convertNumber<ValueType>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
uint64_t epochCount = 0;
for (uint64_t dim = 0; dim < rewardUnfolding.getEpochManager().getDimensionCount(); ++dim) {
epochCount += rewardUnfolding.getEpochManager().getDimensionOfEpoch(initEpoch, dim) + 1;
}
if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isSoundSet()) {
uint64_t denom = 0;
for (uint64_t dim = 0; dim < rewardUnfolding.getEpochManager().getDimensionCount(); ++dim) {
denom += rewardUnfolding.getEpochManager().getDimensionOfEpoch(initEpoch, dim) + 1;
}
precision = precision / storm::utility::convertNumber<ValueType>(denom);
precision = precision / storm::utility::convertNumber<ValueType>(epochCount);
}
if (numChecks == 1) {
STORM_PRINT_AND_LOG("Objective/Dimension/Epoch count is: " << 1 << "/" << rewardUnfolding.getEpochManager().getDimensionCount() << "/" << epochCount << "." << std::endl);
}
for (auto const& epoch : epochOrder) {
computeEpochSolution(epoch, weightVector, cachedData, precision);

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

@ -91,13 +91,14 @@ namespace storm {
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> minMaxSolver;
ValueType precision = storm::utility::convertNumber<ValueType>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
uint64_t epochCount = 0;
for (uint64_t dim = 0; dim < rewardUnfolding.getEpochManager().getDimensionCount(); ++dim) {
epochCount += rewardUnfolding.getEpochManager().getDimensionOfEpoch(initEpoch, dim) + 1;
}
if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isSoundSet()) {
uint64_t denom = 0;
for (uint64_t dim = 0; dim < rewardUnfolding.getEpochManager().getDimensionCount(); ++dim) {
denom += rewardUnfolding.getEpochManager().getDimensionOfEpoch(initEpoch, dim) + 1;
}
precision = precision / storm::utility::convertNumber<ValueType>(denom);
precision = precision / storm::utility::convertNumber<ValueType>(epochCount);
}
STORM_PRINT_AND_LOG("Objective/Dimension/Epoch count is: " << 1 << "/" << rewardUnfolding.getEpochManager().getDimensionCount() << "/" << epochCount << "." << std::endl);
for (auto const& epoch : epochOrder) {
swBuild.start();

Loading…
Cancel
Save