diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 1b1a5c895..7cc999ec9 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -24,8 +24,8 @@ #include "storm-pomdp/analysis/QualitativeAnalysisOnGraphs.h" #include "storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.h" #include "storm-pomdp/analysis/FormulaInformation.h" -#include "storm-pomdp/analysis/MemlessStrategySearchQualitative.h" -#include "storm-pomdp/analysis/QualitativeStrategySearchNaive.h" +#include "storm-pomdp/analysis/IterativePolicySearch.h" +#include "storm-pomdp/analysis/OneShotPolicySearch.h" #include "storm/api/storm.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -163,14 +163,14 @@ namespace storm { lookahead = pomdp.getNumberOfStates(); } if (qualSettings.getMemlessSearchMethod() == "one-shot") { - storm::pomdp::QualitativeStrategySearchNaive memlessSearch(pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory); + storm::pomdp::OneShotPolicySearch memlessSearch(pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory); if (qualSettings.isWinningRegionSet()) { STORM_LOG_ERROR("Computing winning regions is not supported by ccd-memless."); } else { memlessSearch.analyzeForInitialStates(lookahead); } } else if (qualSettings.getMemlessSearchMethod() == "iterative") { - storm::pomdp::MemlessStrategySearchQualitative search(pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory, options); + storm::pomdp::IterativePolicySearch search(pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory, options); if (qualSettings.isWinningRegionSet()) { search.computeWinningRegion(lookahead); } else { diff --git a/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp b/src/storm-pomdp/analysis/IterativePolicySearch.cpp similarity index 96% rename from src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp rename to src/storm-pomdp/analysis/IterativePolicySearch.cpp index 1eb9f4c85..719def098 100644 --- a/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp +++ b/src/storm-pomdp/analysis/IterativePolicySearch.cpp @@ -1,7 +1,7 @@ -#include "storm-pomdp/analysis/MemlessStrategySearchQualitative.h" +#include "storm-pomdp/analysis/IterativePolicySearch.h" #include "storm/utility/file.h" -#include "storm-pomdp/analysis/QualitativeStrategySearchNaive.h" +#include "storm-pomdp/analysis/OneShotPolicySearch.h" #include "storm-pomdp/analysis/QualitativeAnalysis.h" #include "storm-pomdp/analysis/QualitativeAnalysisOnGraphs.h" @@ -34,7 +34,7 @@ namespace storm { } template - void MemlessStrategySearchQualitative::Statistics::print() const { + void IterativePolicySearch::Statistics::print() const { STORM_PRINT_AND_LOG("Total time: " << totalTimer); STORM_PRINT_AND_LOG("SAT Calls " << satCalls); STORM_PRINT_AND_LOG("SAT Calls time: " << smtCheckTimer); @@ -48,11 +48,11 @@ namespace storm { } template - MemlessStrategySearchQualitative::MemlessStrategySearchQualitative(storm::models::sparse::Pomdp const& pomdp, - storm::storage::BitVector const& targetStates, - storm::storage::BitVector const& surelyReachSinkStates, - std::shared_ptr& smtSolverFactory, - MemlessSearchOptions const& options) : + IterativePolicySearch::IterativePolicySearch(storm::models::sparse::Pomdp const& pomdp, + storm::storage::BitVector const& targetStates, + storm::storage::BitVector const& surelyReachSinkStates, + std::shared_ptr& smtSolverFactory, + MemlessSearchOptions const& options) : pomdp(pomdp), surelyReachSinkStates(surelyReachSinkStates), targetStates(targetStates), @@ -83,7 +83,7 @@ namespace storm { } template - bool MemlessStrategySearchQualitative::initialize(uint64_t k) { + bool IterativePolicySearch::initialize(uint64_t k) { STORM_LOG_INFO("Start intializing solver..."); bool lookaheadConstraintsRequired; @@ -377,7 +377,7 @@ namespace storm { } template - uint64_t MemlessStrategySearchQualitative::getOffsetFromObservation(uint64_t state, uint64_t observation) const { + uint64_t IterativePolicySearch::getOffsetFromObservation(uint64_t state, uint64_t observation) const { if(!useFindOffset) { STORM_LOG_WARN("This code is slow and should only be used for debugging."); useFindOffset = true; @@ -394,7 +394,7 @@ namespace storm { } template - bool MemlessStrategySearchQualitative::analyze(uint64_t k, storm::storage::BitVector const& oneOfTheseStates, storm::storage::BitVector const& allOfTheseStates) { + bool IterativePolicySearch::analyze(uint64_t k, storm::storage::BitVector const& oneOfTheseStates, storm::storage::BitVector const& allOfTheseStates) { STORM_LOG_DEBUG("Surely reach sink states: " << surelyReachSinkStates); STORM_LOG_DEBUG("Target states " << targetStates); STORM_LOG_DEBUG("Questionmark states " << (~surelyReachSinkStates & ~targetStates)); @@ -897,7 +897,7 @@ namespace storm { template - void MemlessStrategySearchQualitative::printCoveredStates(storm::storage::BitVector const &remaining) const { + void IterativePolicySearch::printCoveredStates(storm::storage::BitVector const &remaining) const { STORM_LOG_DEBUG("states that are okay"); for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) { if (!remaining.get(state)) { @@ -908,22 +908,22 @@ namespace storm { } template - void MemlessStrategySearchQualitative::printScheduler(std::vector const& ) { + void IterativePolicySearch::printScheduler(std::vector const& ) { } template - void MemlessStrategySearchQualitative::finalizeStatistics() { + void IterativePolicySearch::finalizeStatistics() { } template - typename MemlessStrategySearchQualitative::Statistics const& MemlessStrategySearchQualitative::getStatistics() const{ + typename IterativePolicySearch::Statistics const& IterativePolicySearch::getStatistics() const{ return stats; } template - bool MemlessStrategySearchQualitative::smtCheck(uint64_t iteration, std::set const& assumptions) { + bool IterativePolicySearch::smtCheck(uint64_t iteration, std::set const& assumptions) { if(options.isExportSATSet()) { STORM_LOG_DEBUG("Export SMT Solver Call (" <; - template class MemlessStrategySearchQualitative; + template class IterativePolicySearch; + template class IterativePolicySearch; } diff --git a/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.h b/src/storm-pomdp/analysis/IterativePolicySearch.h similarity index 94% rename from src/storm-pomdp/analysis/MemlessStrategySearchQualitative.h rename to src/storm-pomdp/analysis/IterativePolicySearch.h index ec292af1c..b0c172659 100644 --- a/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.h +++ b/src/storm-pomdp/analysis/IterativePolicySearch.h @@ -114,7 +114,7 @@ namespace pomdp { }; template - class MemlessStrategySearchQualitative { + class IterativePolicySearch { // Implements an extension to the Chatterjee, Chmelik, Davies (AAAI-16) paper. public: @@ -162,12 +162,12 @@ namespace pomdp { uint64_t graphBasedAnalysisWinOb = 0; }; - MemlessStrategySearchQualitative(storm::models::sparse::Pomdp const& pomdp, - storm::storage::BitVector const& targetStates, - storm::storage::BitVector const& surelyReachSinkStates, + IterativePolicySearch(storm::models::sparse::Pomdp const& pomdp, + storm::storage::BitVector const& targetStates, + storm::storage::BitVector const& surelyReachSinkStates, - std::shared_ptr& smtSolverFactory, - MemlessSearchOptions const& options); + std::shared_ptr& smtSolverFactory, + MemlessSearchOptions const& options); void analyzeForInitialStates(uint64_t k) { stats.totalTimer.start(); diff --git a/src/storm-pomdp/analysis/QualitativeStrategySearchNaive.cpp b/src/storm-pomdp/analysis/OneShotPolicySearch.cpp similarity index 94% rename from src/storm-pomdp/analysis/QualitativeStrategySearchNaive.cpp rename to src/storm-pomdp/analysis/OneShotPolicySearch.cpp index a959c17f9..a39901eb4 100644 --- a/src/storm-pomdp/analysis/QualitativeStrategySearchNaive.cpp +++ b/src/storm-pomdp/analysis/OneShotPolicySearch.cpp @@ -1,13 +1,13 @@ #include "storm/utility/file.h" -#include "storm-pomdp/analysis/QualitativeStrategySearchNaive.h" +#include "storm-pomdp/analysis/OneShotPolicySearch.h" namespace storm { namespace pomdp { template - void QualitativeStrategySearchNaive::initialize(uint64_t k) { + void OneShotPolicySearch::initialize(uint64_t k) { if (maxK == std::numeric_limits::max()) { // not initialized at all. // Create some data structures. @@ -116,7 +116,7 @@ namespace storm { } template - bool QualitativeStrategySearchNaive::analyze(uint64_t k, storm::storage::BitVector const& oneOfTheseStates, storm::storage::BitVector const& allOfTheseStates) { + bool OneShotPolicySearch::analyze(uint64_t k, storm::storage::BitVector const& oneOfTheseStates, storm::storage::BitVector const& allOfTheseStates) { STORM_LOG_TRACE("Use lookahead of "<; - template class QualitativeStrategySearchNaive; + template class OneShotPolicySearch; + template class OneShotPolicySearch; } } diff --git a/src/storm-pomdp/analysis/QualitativeStrategySearchNaive.h b/src/storm-pomdp/analysis/OneShotPolicySearch.h similarity index 88% rename from src/storm-pomdp/analysis/QualitativeStrategySearchNaive.h rename to src/storm-pomdp/analysis/OneShotPolicySearch.h index 8797dfbe5..fb2b4d5a7 100644 --- a/src/storm-pomdp/analysis/QualitativeStrategySearchNaive.h +++ b/src/storm-pomdp/analysis/OneShotPolicySearch.h @@ -20,7 +20,7 @@ namespace storm { } template - class QualitativeStrategySearchNaive { + class OneShotPolicySearch { // Implements to the Chatterjee, Chmelik, Davies (AAAI-16) paper. class Statistics { public: @@ -32,10 +32,10 @@ namespace storm { }; public: - QualitativeStrategySearchNaive(storm::models::sparse::Pomdp const& pomdp, - storm::storage::BitVector const& targetStates, - storm::storage::BitVector const& surelyReachSinkStates, - std::shared_ptr& smtSolverFactory) : + OneShotPolicySearch(storm::models::sparse::Pomdp const& pomdp, + storm::storage::BitVector const& targetStates, + storm::storage::BitVector const& surelyReachSinkStates, + std::shared_ptr& smtSolverFactory) : pomdp(pomdp), targetObservations(extractObservations(pomdp, targetStates)), targetStates(targetStates),