diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index a693be0a0..83d09cbb9 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -1,3 +1,4 @@ add_subdirectory(storm) add_subdirectory(storm-pars) add_subdirectory(storm-dft) +add_subdirectory(storm-pomdp) diff --git a/src/test/storm-pomdp/CMakeLists.txt b/src/test/storm-pomdp/CMakeLists.txt new file mode 100644 index 000000000..6c96497e3 --- /dev/null +++ b/src/test/storm-pomdp/CMakeLists.txt @@ -0,0 +1,23 @@ +# Base path for test files +set(STORM_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/src/test/storm-pomdp") + +# Test Sources +file(GLOB_RECURSE ALL_FILES ${STORM_TESTS_BASE_PATH}/*.h ${STORM_TESTS_BASE_PATH}/*.cpp) + +register_source_groups_from_filestructure("${ALL_FILES}" test) + +# Note that the tests also need the source files, except for the main file +include_directories(${GTEST_INCLUDE_DIR}) + +foreach (testsuite modelchecker) + + file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp) + add_executable (test-pomdp-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp) + target_link_libraries(test-pomdp-${testsuite} storm-pomdp storm-parsers) + target_link_libraries(test-pomdp-${testsuite} ${STORM_TEST_LINK_LIBRARIES}) + + add_dependencies(test-pomdp-${testsuite} test-resources) + add_test(NAME run-test-pomdp-${testsuite} COMMAND $) + add_dependencies(tests test-pomdp-${testsuite}) + +endforeach () diff --git a/src/test/storm-pomdp/modelchecker/ApproximatePOMDPModelcheckerTest.cpp b/src/test/storm-pomdp/modelchecker/ApproximatePOMDPModelcheckerTest.cpp new file mode 100644 index 000000000..87bd0a83f --- /dev/null +++ b/src/test/storm-pomdp/modelchecker/ApproximatePOMDPModelcheckerTest.cpp @@ -0,0 +1,175 @@ +#include "test/storm_gtest.h" +#include "storm-config.h" + +#include "storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h" +#include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" + +#include "storm/environment/solver/MinMaxSolverEnvironment.h" + + +namespace { + enum class PreprocessingType { None }; + class CoarseDoubleVIEnvironment { + public: + typedef double ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); + return env; + } + static void adaptOptions(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions& options) {} // TODO + static PreprocessingType const preprocessingType = PreprocessingType::None; + }; + + class DefaultDoubleVIEnvironment { + public: + typedef double ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); + return env; + } + static void adaptOptions(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions&) { /* intentionally left empty */ } + static PreprocessingType const preprocessingType = PreprocessingType::None; + }; + + class PreprocessedDefaultDoubleVIEnvironment { + public: + typedef double ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); + return env; + } + static void adaptOptions(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions& options) { /* intentionally left empty */ } + static PreprocessingType const preprocessingType = PreprocessingType::None; // TODO + }; + + class FineDoubleVIEnvironment { + public: + typedef double ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); + return env; + } + static void adaptOptions(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions& options) {} // TODO + static PreprocessingType const preprocessingType = PreprocessingType::None; + }; + + class RefineDoubleVIEnvironment { + public: + typedef double ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); + return env; + } + static void adaptOptions(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions& options) {} // TODO + static PreprocessingType const preprocessingType = PreprocessingType::None; + }; + + class DefaultDoubleOVIEnvironment { + public: + typedef double ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::SoundValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); + env.solver().setForceSoundness(true); + return env; + } + static void adaptOptions(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions& options) { /* intentionally left empty */ } + static PreprocessingType const preprocessingType = PreprocessingType::None; + }; + + class DefaultRationalPIEnvironment { + public: + typedef storm::RationalNumber ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); + env.solver().setForceExact(true); + return env; + } + static void adaptOptions(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions& options) { /* intentionally left empty */ } + static PreprocessingType const preprocessingType = PreprocessingType::None; + }; + + class PreprocessedDefaultRationalPIEnvironment { + public: + typedef storm::RationalNumber ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); + env.solver().setForceExact(true); + return env; + } + static void adaptOptions(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions& options) { /* intentionally left empty */ } + static PreprocessingType const preprocessingType = PreprocessingType::None; // TODO + }; + + template + class BeliefExplorationTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + BeliefExplorationTest() : _environment(TestType::createEnvironment()) {} + storm::Environment const& env() const { return _environment; } + storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions options() const { + storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions opt(true, true); // Always compute both bounds (lower and upper) + TestType::adaptOptions(opt); + return opt; + } + void preprocess(std::shared_ptr>& model, std::shared_ptr& formula) { + switch(TestType::preprocessingType) { + case PreprocessingType::None: + // nothing to do + break; + default: + FAIL() << "Unhandled preprocessing type."; + } + } + private: + storm::Environment _environment; + }; + + typedef ::testing::Types< + CoarseDoubleVIEnvironment, + DefaultDoubleVIEnvironment, + PreprocessedDefaultDoubleVIEnvironment, + FineDoubleVIEnvironment, + RefineDoubleVIEnvironment, + DefaultDoubleOVIEnvironment, + DefaultRationalPIEnvironment, + PreprocessedDefaultRationalPIEnvironment + > TestingTypes; + + TYPED_TEST_SUITE(BeliefExplorationTest, TestingTypes,); + + TYPED_TEST(BeliefExplorationTest, simple) { + typedef typename TestFixture::ValueType ValueType; + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism"; + std::string formulaAsString = "P=? [F \"goal\" ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::shared_ptr formula = storm::api::parsePropertiesForPrismProgram(formulaAsString, program).front().getRawFormula(); + std::shared_ptr> model = storm::api::buildSparseModel(program, {formula})->template as>(); + this->preprocess(model, formula); + + // Invoke model checking + storm::pomdp::modelchecker::ApproximatePOMDPModelchecker> checker(*model, this->options()); + auto result = checker.check(*formula); + std::cout << "[" << result.lowerBound << "," << result.upperBound << std::endl; + + } +} diff --git a/src/test/storm-pomdp/storm-test.cpp b/src/test/storm-pomdp/storm-test.cpp new file mode 100644 index 000000000..704192a79 --- /dev/null +++ b/src/test/storm-pomdp/storm-test.cpp @@ -0,0 +1,9 @@ +#include "test/storm_gtest.h" +#include "storm/settings/SettingsManager.h" + +int main(int argc, char **argv) { + storm::settings::initializeAll("Storm-pomdp (Functional) Testing Suite", "test-pomdp"); + storm::test::initialize(); + ::testing::InitGoogleTest(&argc, argv); + return RUN_ALL_TESTS(); +}