Renamed ApproximatePOMDPModelchecker to BeliefExplorationPomdpModelChecker

src/storm-pomdp-cli/settings/modules/BeliefExplorationSettings.cpp

@@ -8,7 +8,7 @@
 
 #include "storm/utility/NumberTraits.h"
 #include "storm/adapters/RationalNumberAdapter.h"
-#include "storm-pomdp/modelchecker/ApproximatePOMDPModelCheckerOptions.h"
+#include "storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerOptions.h"
 
 #include "storm/exceptions/InvalidArgumentException.h"
 
@@ -134,7 +134,7 @@ namespace storm {
             }
             
             template<typename ValueType>
-            void BeliefExplorationSettings::setValuesInOptionsStruct(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<ValueType>& options) const {
+            void BeliefExplorationSettings::setValuesInOptionsStruct(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) const {
                 options.refine = isRefineSet();
                 options.refinePrecision = storm::utility::convertNumber<ValueType>(getRefinePrecision());
                 if (isRefineStepLimitSet()) {
@@ -170,8 +170,8 @@ namespace storm {
                 options.dynamicTriangulation = isDynamicTriangulationModeSet();
             }
             
-            template void BeliefExplorationSettings::setValuesInOptionsStruct<double>(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<double>& options) const;
-            template void BeliefExplorationSettings::setValuesInOptionsStruct<storm::RationalNumber>(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<storm::RationalNumber>& options) const;
+            template void BeliefExplorationSettings::setValuesInOptionsStruct<double>(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<double>& options) const;
+            template void BeliefExplorationSettings::setValuesInOptionsStruct<storm::RationalNumber>(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<storm::RationalNumber>& options) const;
 
             
             

src/storm-pomdp-cli/settings/modules/BeliefExplorationSettings.h

@@ -7,7 +7,7 @@ namespace storm {
     namespace pomdp {
         namespace modelchecker {
             template<typename ValueType>
-            struct ApproximatePOMDPModelCheckerOptions;
+            struct BeliefExplorationPomdpModelCheckerOptions;
         }
     }
     
@@ -62,7 +62,7 @@ namespace storm {
                 bool isStaticTriangulationModeSet() const;
     
                 template<typename ValueType>
-                void setValuesInOptionsStruct(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<ValueType>& options) const;
+                void setValuesInOptionsStruct(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) const;
                 
                 // The name of the module.
                 static const std::string moduleName;

src/storm-pomdp-cli/storm-pomdp.cpp

@@ -22,7 +22,7 @@
 #include "storm-pomdp/transformer/MakePOMDPCanonic.h"
 #include "storm-pomdp/analysis/UniqueObservationStates.h"
 #include "storm-pomdp/analysis/QualitativeAnalysisOnGraphs.h"
-#include "storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.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"
@@ -226,10 +226,10 @@ namespace storm {
                 bool analysisPerformed = false;
                 if (pomdpSettings.isBeliefExplorationSet()) {
                     STORM_PRINT_AND_LOG("Exploring the belief MDP... ");
-                    auto options = storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<ValueType>(pomdpSettings.isBeliefExplorationDiscretizeSet(), pomdpSettings.isBeliefExplorationUnfoldSet());
+                    auto options = storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>(pomdpSettings.isBeliefExplorationDiscretizeSet(), pomdpSettings.isBeliefExplorationUnfoldSet());
                     auto const& beliefExplorationSettings = storm::settings::getModule<storm::settings::modules::BeliefExplorationSettings>();
                     beliefExplorationSettings.setValuesInOptionsStruct(options);
-                    storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<storm::models::sparse::Pomdp<ValueType>> checker(pomdp, options);
+                    storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(pomdp, options);
                     auto result = checker.check(formula);
                     checker.printStatisticsToStream(std::cout);
                     if (storm::utility::resources::isTerminate()) {

src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp → src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.cpp

@@ -1,4 +1,4 @@
-#include "ApproximatePOMDPModelchecker.h"
+#include "BeliefExplorationPomdpModelChecker.h"
 
 #include <tuple>
 
@@ -31,13 +31,13 @@ namespace storm {
         namespace modelchecker {
             
             template<typename PomdpModelType, typename BeliefValueType>
-            ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::Result::Result(ValueType lower, ValueType upper) : lowerBound(lower), upperBound(upper) {
+            BeliefExplorationPomdpModelChecker<PomdpModelType, BeliefValueType>::Result::Result(ValueType lower, ValueType upper) : lowerBound(lower), upperBound(upper) {
                 // Intentionally left empty
             }
             
             template<typename PomdpModelType, typename BeliefValueType>
-            typename ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::ValueType
-            ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::Result::diff(bool relative) const {
+            typename BeliefExplorationPomdpModelChecker<PomdpModelType, BeliefValueType>::ValueType
+            BeliefExplorationPomdpModelChecker<PomdpModelType, BeliefValueType>::Result::diff(bool relative) const {
                 ValueType diff = upperBound - lowerBound;
                 if (diff < storm::utility::zero<ValueType>()) {
                     STORM_LOG_WARN_COND(diff >= storm::utility::convertNumber<ValueType>(1e-6), "Upper bound '" << upperBound << "' is smaller than lower bound '" << lowerBound << "': Difference is " << diff << ".");
@@ -50,7 +50,7 @@ namespace storm {
             }
             
             template<typename PomdpModelType, typename BeliefValueType>
-            bool ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::Result::updateLowerBound(ValueType const& value) {
+            bool BeliefExplorationPomdpModelChecker<PomdpModelType, BeliefValueType>::Result::updateLowerBound(ValueType const& value) {
                 if (value > lowerBound) {
                     lowerBound = value;
                     return true;
@@ -59,7 +59,7 @@ namespace storm {
             }
             
             template<typename PomdpModelType, typename BeliefValueType>
-            bool ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::Result::updateUpperBound(ValueType const& value) {
+            bool BeliefExplorationPomdpModelChecker<PomdpModelType, BeliefValueType>::Result::updateUpperBound(ValueType const& value) {
                 if (value < upperBound) {
                     upperBound = value;
                     return true;
@@ -68,12 +68,12 @@ namespace storm {
             }
             
             template<typename PomdpModelType, typename BeliefValueType>
-            ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::Statistics::Statistics() :  overApproximationBuildAborted(false), underApproximationBuildAborted(false), aborted(false) {
+            BeliefExplorationPomdpModelChecker<PomdpModelType, BeliefValueType>::Statistics::Statistics() :  overApproximationBuildAborted(false), underApproximationBuildAborted(false), aborted(false) {
                 // intentionally left empty;
             }
             
             template<typename PomdpModelType, typename BeliefValueType>
-            ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::ApproximatePOMDPModelchecker(std::shared_ptr<PomdpModelType> pomdp, Options options) : inputPomdp(pomdp), options(options) {
+            BeliefExplorationPomdpModelChecker<PomdpModelType, BeliefValueType>::BeliefExplorationPomdpModelChecker(std::shared_ptr<PomdpModelType> pomdp, Options options) : inputPomdp(pomdp), options(options) {
                 STORM_LOG_ASSERT(inputPomdp, "The given POMDP is not initialized.");
                 STORM_LOG_ERROR_COND(inputPomdp->isCanonic(), "Input Pomdp is not known to be canonic. This might lead to unexpected verification results.");
 
@@ -81,7 +81,7 @@ namespace storm {
             }
 
             template<typename PomdpModelType, typename BeliefValueType>
-            typename ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::Result ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::check(storm::logic::Formula const& formula) {
+            typename BeliefExplorationPomdpModelChecker<PomdpModelType, BeliefValueType>::Result BeliefExplorationPomdpModelChecker<PomdpModelType, BeliefValueType>::check(storm::logic::Formula const& formula) {
                 STORM_LOG_ASSERT(options.unfold || options.discretize, "Invoked belief exploration but no task (unfold or discretize) given.");
                 
                 // Potentially reset preprocessed model from previous call
@@ -147,7 +147,7 @@ namespace storm {
             }
             
             template<typename PomdpModelType, typename BeliefValueType>
-            void ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::printStatisticsToStream(std::ostream& stream) const {
+            void BeliefExplorationPomdpModelChecker<PomdpModelType, BeliefValueType>::printStatisticsToStream(std::ostream& stream) const {
                 stream << "##### Grid Approximation Statistics ######" << std::endl;
                 stream << "# Input model: " << std::endl;
                 pomdp().printModelInformationToStream(stream);
@@ -202,7 +202,7 @@ namespace storm {
             }
             
             template<typename PomdpModelType, typename BeliefValueType>
-            void ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::computeReachabilityOTF(std::set<uint32_t> const &targetObservations, bool min, boost::optional<std::string> rewardModelName, storm::pomdp::modelchecker::TrivialPomdpValueBounds<ValueType> const& pomdpValueBounds, Result& result) {
+            void BeliefExplorationPomdpModelChecker<PomdpModelType, BeliefValueType>::computeReachabilityOTF(std::set<uint32_t> const &targetObservations, bool min, boost::optional<std::string> rewardModelName, storm::pomdp::modelchecker::TrivialPomdpValueBounds<ValueType> const& pomdpValueBounds, Result& result) {
                 
                 if (options.discretize) {
                     std::vector<BeliefValueType> observationResolutionVector(pomdp().getNrObservations(), storm::utility::convertNumber<BeliefValueType>(options.resolutionInit));
@@ -254,7 +254,7 @@ namespace storm {
             }
             
             template<typename PomdpModelType, typename BeliefValueType>
-            void ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::refineReachability(std::set<uint32_t> const &targetObservations, bool min, boost::optional<std::string> rewardModelName, storm::pomdp::modelchecker::TrivialPomdpValueBounds<ValueType> const& pomdpValueBounds, Result& result) {
+            void BeliefExplorationPomdpModelChecker<PomdpModelType, BeliefValueType>::refineReachability(std::set<uint32_t> const &targetObservations, bool min, boost::optional<std::string> rewardModelName, storm::pomdp::modelchecker::TrivialPomdpValueBounds<ValueType> const& pomdpValueBounds, Result& result) {
                 statistics.refinementSteps = 0;
 
                 // Set up exploration data
@@ -418,7 +418,7 @@ namespace storm {
              * Here, 0 means a bad approximation and 1 means a good approximation.
              */
             template<typename PomdpModelType, typename BeliefValueType>
-            BeliefValueType ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::rateObservation(typename ExplorerType::SuccessorObservationInformation const& info, BeliefValueType const& observationResolution, BeliefValueType const& maxResolution) {
+            BeliefValueType BeliefExplorationPomdpModelChecker<PomdpModelType, BeliefValueType>::rateObservation(typename ExplorerType::SuccessorObservationInformation const& info, BeliefValueType const& observationResolution, BeliefValueType const& maxResolution) {
                 auto n = storm::utility::convertNumber<BeliefValueType, uint64_t>(info.support.size());
                 auto one = storm::utility::one<BeliefValueType>();
                 if (storm::utility::isOne(n)) {
@@ -439,7 +439,7 @@ namespace storm {
             }
             
             template<typename PomdpModelType, typename BeliefValueType>
-            std::vector<BeliefValueType> ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::getObservationRatings(std::shared_ptr<ExplorerType> const& overApproximation, std::vector<BeliefValueType> const& observationResolutionVector) {
+            std::vector<BeliefValueType> BeliefExplorationPomdpModelChecker<PomdpModelType, BeliefValueType>::getObservationRatings(std::shared_ptr<ExplorerType> const& overApproximation, std::vector<BeliefValueType> const& observationResolutionVector) {
                 uint64_t numMdpStates = overApproximation->getExploredMdp()->getNumberOfStates();
                 auto const& choiceIndices = overApproximation->getExploredMdp()->getNondeterministicChoiceIndices();
                 BeliefValueType maxResolution = *std::max_element(observationResolutionVector.begin(), observationResolutionVector.end());
@@ -491,7 +491,7 @@ namespace storm {
             }
             
             template<typename PomdpModelType, typename BeliefValueType>
-            bool ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::buildOverApproximation(std::set<uint32_t> const &targetObservations, bool min, bool computeRewards, bool refine, HeuristicParameters const& heuristicParameters, std::vector<BeliefValueType>& observationResolutionVector, std::shared_ptr<BeliefManagerType>& beliefManager, std::shared_ptr<ExplorerType>& overApproximation) {
+            bool BeliefExplorationPomdpModelChecker<PomdpModelType, BeliefValueType>::buildOverApproximation(std::set<uint32_t> const &targetObservations, bool min, bool computeRewards, bool refine, HeuristicParameters const& heuristicParameters, std::vector<BeliefValueType>& observationResolutionVector, std::shared_ptr<BeliefManagerType>& beliefManager, std::shared_ptr<ExplorerType>& overApproximation) {
                 
                 // Detect whether the refinement reached a fixpoint.
                 bool fixPoint = true;
@@ -726,7 +726,7 @@ namespace storm {
             }
 
             template<typename PomdpModelType, typename BeliefValueType>
-            bool ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::buildUnderApproximation(std::set<uint32_t> const &targetObservations, bool min, bool computeRewards, bool refine, HeuristicParameters const& heuristicParameters, std::shared_ptr<BeliefManagerType>& beliefManager, std::shared_ptr<ExplorerType>& underApproximation) {
+            bool BeliefExplorationPomdpModelChecker<PomdpModelType, BeliefValueType>::buildUnderApproximation(std::set<uint32_t> const &targetObservations, bool min, bool computeRewards, bool refine, HeuristicParameters const& heuristicParameters, std::shared_ptr<BeliefManagerType>& beliefManager, std::shared_ptr<ExplorerType>& underApproximation) {
                 statistics.underApproximationBuildTime.start();
                 bool fixPoint = true;
                 if (heuristicParameters.sizeThreshold != std::numeric_limits<uint64_t>::max()) {
@@ -846,7 +846,7 @@ namespace storm {
             }
             
             template<typename PomdpModelType, typename BeliefValueType>
-            PomdpModelType const& ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::pomdp() const {
+            PomdpModelType const& BeliefExplorationPomdpModelChecker<PomdpModelType, BeliefValueType>::pomdp() const {
                 if (preprocessedPomdp) {
                     return *preprocessedPomdp;
                 } else {
@@ -854,8 +854,8 @@ namespace storm {
                 }
             }
 
-            template class ApproximatePOMDPModelchecker<storm::models::sparse::Pomdp<double>>;
-            template class ApproximatePOMDPModelchecker<storm::models::sparse::Pomdp<storm::RationalNumber>>;
+            template class BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<double>>;
+            template class BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<storm::RationalNumber>>;
 
         }
     }

src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h → src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.h

@@ -3,7 +3,7 @@
 #include "storm/utility/logging.h"
 #include "storm-pomdp/storage/Belief.h"
 #include "storm-pomdp/storage/BeliefManager.h"
-#include "storm-pomdp/modelchecker/ApproximatePOMDPModelCheckerOptions.h"
+#include "storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerOptions.h"
 #include "storm-pomdp/builder/BeliefMdpExplorer.h"
 
 #include "storm/storage/jani/Property.h"
@@ -20,13 +20,13 @@ namespace storm {
             struct TrivialPomdpValueBounds;
             
             template<typename PomdpModelType, typename BeliefValueType = typename PomdpModelType::ValueType>
-            class ApproximatePOMDPModelchecker {
+            class BeliefExplorationPomdpModelChecker {
             public:
                 typedef typename PomdpModelType::ValueType ValueType;
                 typedef typename PomdpModelType::RewardModelType RewardModelType;
                 typedef storm::storage::BeliefManager<PomdpModelType, BeliefValueType> BeliefManagerType;
                 typedef storm::builder::BeliefMdpExplorer<PomdpModelType, BeliefValueType> ExplorerType;
-                typedef ApproximatePOMDPModelCheckerOptions<ValueType> Options;
+                typedef BeliefExplorationPomdpModelCheckerOptions<ValueType> Options;
                 
                 struct Result {
                     Result(ValueType lower, ValueType upper);
@@ -37,7 +37,7 @@ namespace storm {
                     bool updateUpperBound(ValueType const& value);
                 };
                 
-                ApproximatePOMDPModelchecker(std::shared_ptr<PomdpModelType> pomdp, Options options = Options());
+                BeliefExplorationPomdpModelChecker(std::shared_ptr<PomdpModelType> pomdp, Options options = Options());
                 
                 Result check(storm::logic::Formula const& formula);
 

src/storm-pomdp/modelchecker/ApproximatePOMDPModelCheckerOptions.h → src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerOptions.h

@@ -8,8 +8,8 @@ namespace storm {
     namespace pomdp {
         namespace modelchecker {
             template<typename ValueType>
-            struct ApproximatePOMDPModelCheckerOptions {
-                ApproximatePOMDPModelCheckerOptions(bool discretize, bool unfold) : discretize(discretize), unfold(unfold) {
+            struct BeliefExplorationPomdpModelCheckerOptions {
+                BeliefExplorationPomdpModelCheckerOptions(bool discretize, bool unfold) : discretize(discretize), unfold(unfold) {
                     // Intentionally left empty
                 }
                 

src/test/storm-pomdp/modelchecker/ApproximatePOMDPModelcheckerTest.cpp → src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp

@@ -1,7 +1,7 @@
 #include "test/storm_gtest.h"
 #include "storm-config.h"
 
-#include "storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h"
+#include "storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.h"
 #include "storm-pomdp/transformer/MakePOMDPCanonic.h"
 #include "storm/api/storm.h"
 #include "storm-parsers/api/storm-parsers.h"
@@ -20,7 +20,7 @@ namespace {
             env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
             return env;
         }
-        static void adaptOptions(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<ValueType>& options) {}  // TODO
+        static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) {}  // TODO
         static PreprocessingType const preprocessingType = PreprocessingType::None;
     };
     
@@ -33,7 +33,7 @@ namespace {
             env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
             return env;
         }
-        static void adaptOptions(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<ValueType>&) { /* intentionally left empty */ }
+        static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>&) { /* intentionally left empty */ }
         static PreprocessingType const preprocessingType = PreprocessingType::None;
     };
     
@@ -46,7 +46,7 @@ namespace {
             env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
             return env;
         }
-        static void adaptOptions(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<ValueType>& options) { /* intentionally left empty */ }
+        static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) { /* intentionally left empty */ }
         static PreprocessingType const preprocessingType = PreprocessingType::None; // TODO
     };
 
@@ -59,7 +59,7 @@ namespace {
             env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
             return env;
         }
-        static void adaptOptions(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<ValueType>& options) {}  // TODO
+        static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) {}  // TODO
         static PreprocessingType const preprocessingType = PreprocessingType::None;
     };
 
@@ -72,7 +72,7 @@ namespace {
             env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
             return env;
         }
-        static void adaptOptions(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<ValueType>& options) {}  // TODO
+        static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) {}  // TODO
         static PreprocessingType const preprocessingType = PreprocessingType::None;
     };
     
@@ -86,7 +86,7 @@ namespace {
             env.solver().setForceSoundness(true);
             return env;
         }
-        static void adaptOptions(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<ValueType>& options) { /* intentionally left empty */ }
+        static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) { /* intentionally left empty */ }
         static PreprocessingType const preprocessingType = PreprocessingType::None;
     };
     
@@ -99,7 +99,7 @@ namespace {
             env.solver().setForceExact(true);
             return env;
         }
-        static void adaptOptions(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<ValueType>& options) { /* intentionally left empty */ }
+        static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) { /* intentionally left empty */ }
         static PreprocessingType const preprocessingType = PreprocessingType::None;
     };
     
@@ -112,7 +112,7 @@ namespace {
             env.solver().setForceExact(true);
             return env;
         }
-        static void adaptOptions(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<ValueType>& options) { /* intentionally left empty */ }
+        static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) { /* intentionally left empty */ }
         static PreprocessingType const preprocessingType = PreprocessingType::None; // TODO
     };
     
@@ -122,8 +122,8 @@ namespace {
         typedef typename TestType::ValueType ValueType;
         BeliefExplorationTest() : _environment(TestType::createEnvironment()) {}
         storm::Environment const& env() const { return _environment; }
-        storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<ValueType> options() const {
-            storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<ValueType> opt(true, true); // Always compute both bounds (lower and upper)
+        storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType> options() const {
+            storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType> opt(true, true); // Always compute both bounds (lower and upper)
             TestType::adaptOptions(opt);
             return opt;
         }
@@ -177,7 +177,7 @@ namespace {
         typedef typename TestFixture::ValueType ValueType;
 
         auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0");
-        storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
+        storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
         auto result = checker.check(*data.formula);
         
         EXPECT_LE(result.lowerBound, this->parseNumber("7/10"));