diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index bc4511dc0..e669888d5 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -197,13 +197,14 @@ int main(const int argc, const char** argv) { } storm::cli::setUrgentOptions(); - + typedef double VT; auto const& coreSettings = storm::settings::getModule(); auto const& pomdpSettings = storm::settings::getModule(); auto const &general = storm::settings::getModule(); auto const &debug = storm::settings::getModule(); + if (general.isVerboseSet()) { storm::utility::setLogLevel(l3pp::LogLevel::INFO); } @@ -222,8 +223,8 @@ int main(const int argc, const char** argv) { auto model = storm::cli::buildPreprocessExportModelWithValueTypeAndDdlib(symbolicInput, engine); STORM_LOG_THROW(model && model->getType() == storm::models::ModelType::Pomdp, storm::exceptions::WrongFormatException, "Expected a POMDP."); - std::shared_ptr> pomdp = model->template as>(); - storm::transformer::MakePOMDPCanonic makeCanonic(*pomdp); + std::shared_ptr> pomdp = model->template as>(); + storm::transformer::MakePOMDPCanonic makeCanonic(*pomdp); pomdp = makeCanonic.transform(); std::shared_ptr formula; @@ -235,7 +236,7 @@ int main(const int argc, const char** argv) { if (pomdpSettings.isAnalyzeUniqueObservationsSet()) { STORM_PRINT_AND_LOG("Analyzing states with unique observation ..." << std::endl); - storm::analysis::UniqueObservationStates uniqueAnalysis(*pomdp); + storm::analysis::UniqueObservationStates uniqueAnalysis(*pomdp); std::cout << uniqueAnalysis.analyse() << std::endl; } @@ -261,12 +262,12 @@ int main(const int argc, const char** argv) { if (pomdpSettings.isSelfloopReductionSet() && !storm::solver::minimize(formula->asProbabilityOperatorFormula().getOptimalityType())) { STORM_PRINT_AND_LOG("Eliminating self-loop choices ..."); uint64_t oldChoiceCount = pomdp->getNumberOfChoices(); - storm::transformer::GlobalPOMDPSelfLoopEliminator selfLoopEliminator(*pomdp); + storm::transformer::GlobalPOMDPSelfLoopEliminator selfLoopEliminator(*pomdp); pomdp = selfLoopEliminator.transform(); STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through self-loop elimination." << std::endl); } if (pomdpSettings.isQualitativeReductionSet()) { - storm::analysis::QualitativeAnalysis qualitativeAnalysis(*pomdp); + storm::analysis::QualitativeAnalysis qualitativeAnalysis(*pomdp); STORM_PRINT_AND_LOG("Computing states with probability 0 ..."); prob0States = qualitativeAnalysis.analyseProb0(formula->asProbabilityOperatorFormula()); std::cout << *prob0States << std::endl; @@ -276,15 +277,15 @@ int main(const int argc, const char** argv) { std::cout << *prob1States << std::endl; STORM_PRINT_AND_LOG(" done." << std::endl); //std::cout << "actual reduction not yet implemented..." << std::endl; - storm::pomdp::transformer::KnownProbabilityTransformer kpt = storm::pomdp::transformer::KnownProbabilityTransformer(); + storm::pomdp::transformer::KnownProbabilityTransformer kpt = storm::pomdp::transformer::KnownProbabilityTransformer(); pomdp = kpt.transform(*pomdp, *prob0States, *prob1States); } if (pomdpSettings.isGridApproximationSet()) { - storm::pomdp::modelchecker::ApproximatePOMDPModelchecker checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker(); - auto overRes = storm::utility::one(); - auto underRes = storm::utility::zero(); - std::unique_ptr> result; + storm::pomdp::modelchecker::ApproximatePOMDPModelchecker checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker(); + auto overRes = storm::utility::one(); + auto underRes = storm::utility::zero(); + std::unique_ptr> result; result = checker.refineReachabilityProbability(*pomdp, targetObservationSet, probFormula.getOptimalityType() == storm::OptimizationDirection::Minimize, pomdpSettings.getGridResolution(), pomdpSettings.getExplorationThreshold()); @@ -306,10 +307,10 @@ int main(const int argc, const char** argv) { storm::expressions::ExpressionManager expressionManager; std::shared_ptr smtSolverFactory = std::make_shared(); if (pomdpSettings.getMemlessSearchMethod() == "ccd16memless") { - storm::pomdp::QualitativeStrategySearchNaive memlessSearch(*pomdp, targetObservationSet, targetStates, badStates, smtSolverFactory); + storm::pomdp::QualitativeStrategySearchNaive memlessSearch(*pomdp, targetObservationSet, targetStates, badStates, smtSolverFactory); memlessSearch.findNewStrategyForSomeState(5); } else if (pomdpSettings.getMemlessSearchMethod() == "iterative") { - storm::pomdp::MemlessStrategySearchQualitative memlessSearch(*pomdp, targetObservationSet, targetStates, badStates, smtSolverFactory); + storm::pomdp::MemlessStrategySearchQualitative memlessSearch(*pomdp, targetObservationSet, targetStates, badStates, smtSolverFactory); memlessSearch.findNewStrategyForSomeState(5); } else { STORM_LOG_ERROR("This method is not implemented."); @@ -321,7 +322,7 @@ int main(const int argc, const char** argv) { if (pomdpSettings.isSelfloopReductionSet() && storm::solver::minimize(formula->asRewardOperatorFormula().getOptimalityType())) { STORM_PRINT_AND_LOG("Eliminating self-loop choices ..."); uint64_t oldChoiceCount = pomdp->getNumberOfChoices(); - storm::transformer::GlobalPOMDPSelfLoopEliminator selfLoopEliminator(*pomdp); + storm::transformer::GlobalPOMDPSelfLoopEliminator selfLoopEliminator(*pomdp); pomdp = selfLoopEliminator.transform(); STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through self-loop elimination." << std::endl); } @@ -367,10 +368,10 @@ int main(const int argc, const char** argv) { "The formula is not supported by the grid approximation"); STORM_LOG_ASSERT(!targetObservationSet.empty(), "The set of target observations is empty!"); - storm::pomdp::modelchecker::ApproximatePOMDPModelchecker checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker(); - auto overRes = storm::utility::one(); - auto underRes = storm::utility::zero(); - std::unique_ptr> result; + storm::pomdp::modelchecker::ApproximatePOMDPModelchecker checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker(); + auto overRes = storm::utility::one(); + auto underRes = storm::utility::zero(); + std::unique_ptr> result; result = checker.computeReachabilityReward(*pomdp, targetObservationSet, rewFormula.getOptimalityType() == storm::OptimizationDirection::Minimize, @@ -384,7 +385,7 @@ int main(const int argc, const char** argv) { STORM_PRINT_AND_LOG("Computing the unfolding for memory bound " << pomdpSettings.getMemoryBound() << " and memory pattern '" << storm::storage::toString(pomdpSettings.getMemoryPattern()) << "' ..."); storm::storage::PomdpMemory memory = storm::storage::PomdpMemoryBuilder().build(pomdpSettings.getMemoryPattern(), pomdpSettings.getMemoryBound()); std::cout << memory.toString() << std::endl; - storm::transformer::PomdpMemoryUnfolder memoryUnfolder(*pomdp, memory); + storm::transformer::PomdpMemoryUnfolder memoryUnfolder(*pomdp, memory); pomdp = memoryUnfolder.transform(); STORM_PRINT_AND_LOG(" done." << std::endl); pomdp->printModelInformationToStream(std::cout); @@ -398,7 +399,7 @@ int main(const int argc, const char** argv) { STORM_PRINT_AND_LOG("Eliminating mec choices ..."); // Note: Elimination of mec choices only preserves memoryless schedulers. uint64_t oldChoiceCount = pomdp->getNumberOfChoices(); - storm::transformer::GlobalPomdpMecChoiceEliminator mecChoiceEliminator(*pomdp); + storm::transformer::GlobalPomdpMecChoiceEliminator mecChoiceEliminator(*pomdp); pomdp = mecChoiceEliminator.transform(*formula); STORM_PRINT_AND_LOG(" done." << std::endl); STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through MEC choice elimination." << std::endl); @@ -408,10 +409,10 @@ int main(const int argc, const char** argv) { if (pomdpSettings.isTransformBinarySet() || pomdpSettings.isTransformSimpleSet()) { if (pomdpSettings.isTransformSimpleSet()) { STORM_PRINT_AND_LOG("Transforming the POMDP to a simple POMDP."); - pomdp = storm::transformer::BinaryPomdpTransformer().transform(*pomdp, true); + pomdp = storm::transformer::BinaryPomdpTransformer().transform(*pomdp, true); } else { STORM_PRINT_AND_LOG("Transforming the POMDP to a binary POMDP."); - pomdp = storm::transformer::BinaryPomdpTransformer().transform(*pomdp, false); + pomdp = storm::transformer::BinaryPomdpTransformer().transform(*pomdp, false); } pomdp->printModelInformationToStream(std::cout); STORM_PRINT_AND_LOG(" done." << std::endl); @@ -420,7 +421,7 @@ int main(const int argc, const char** argv) { if (pomdpSettings.isExportToParametricSet()) { STORM_PRINT_AND_LOG("Transforming memoryless POMDP to pMC..."); - storm::transformer::ApplyFiniteSchedulerToPomdp toPMCTransformer(*pomdp); + storm::transformer::ApplyFiniteSchedulerToPomdp toPMCTransformer(*pomdp); std::string transformMode = pomdpSettings.getFscApplicationTypeString(); auto pmc = toPMCTransformer.transform(storm::transformer::parsePomdpFscApplicationMode(transformMode)); STORM_PRINT_AND_LOG(" done." << std::endl);