sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

ApproximatePomdpModelchecker: Fixed output a little.

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
a187a299af
commit
ddec9ce740
1 changed files with 23 additions and 2 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 25
      src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp

25
src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
View File

@ -266,7 +266,7 @@ namespace storm {
std::shared_ptr<BeliefManagerType> underApproxBeliefManager;
std::shared_ptr<ExplorerType> underApproximation;
HeuristicParameters underApproxHeuristicPar;
if (options.unfold) { // Setup and build first OverApproximation
if (options.unfold) { // Setup and build first UnderApproximation
underApproxBeliefManager = std::make_shared<BeliefManagerType>(pomdp, options.numericPrecision);
if (rewardModelName) {
underApproxBeliefManager->setRewardModel(rewardModelName);
@ -290,6 +290,27 @@ namespace storm {
}
}
// Do some output
STORM_PRINT_AND_LOG("Completed iteration #" << statistics.refinementSteps.get() << ". Current checktime is " << statistics.totalTime << ".");
bool computingLowerBound = false;
bool computingUpperBound = false;
if (options.discretize) {
STORM_PRINT_AND_LOG(" Over-approx MDP has size " << overApproximation->getExploredMdp()->getNumberOfStates() << ".");
(min ? computingLowerBound : computingUpperBound) = true;
}
if (options.unfold) {
STORM_PRINT_AND_LOG(" Under-approx MDP has size " << underApproximation->getExploredMdp()->getNumberOfStates() << ".");
(min ? computingUpperBound : computingLowerBound) = true;
}
if (computingLowerBound && computingUpperBound) {
STORM_PRINT_AND_LOG(" Current result is [" << result.lowerBound << ", " << result.upperBound << "].");
} else if (computingLowerBound) {
STORM_PRINT_AND_LOG(" Current result is ≥" << result.lowerBound << ".");
} else if (computingUpperBound) {
STORM_PRINT_AND_LOG(" Current result is ≤" << result.upperBound << ".");
}
STORM_PRINT_AND_LOG(std::endl);
// Start refinement
STORM_LOG_WARN_COND(options.refineStepLimit.is_initialized() || !storm::utility::isZero(options.refinePrecision), "No termination criterion for refinement given. Consider to specify a steplimit, a non-zero precisionlimit, or a timeout");
STORM_LOG_WARN_COND(storm::utility::isZero(options.refinePrecision) || (options.unfold && options.discretize), "Refinement goal precision is given, but only one bound is going to be refined.");
@ -361,7 +382,7 @@ namespace storm {
STORM_PRINT_AND_LOG(" Current result is ≤" << result.upperBound << ".");
}
STORM_PRINT_AND_LOG(std::endl);
STORM_LOG_WARN_COND(statistics.refinementSteps.get() == 1000, "Refinement requires more than 1000 iterations.");
STORM_LOG_WARN_COND(statistics.refinementSteps.get() < 1000, "Refinement requires more than 1000 iterations.");
}
}
if (overApproxFixPoint && underApproxFixPoint) {

Write Preview
Loading…
Cancel
Save