diff --git a/src/test/storm-pomdp/CMakeLists.txt b/src/test/storm-pomdp/CMakeLists.txt index 6c96497e3..4b3f060d7 100644 --- a/src/test/storm-pomdp/CMakeLists.txt +++ b/src/test/storm-pomdp/CMakeLists.txt @@ -9,7 +9,7 @@ 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) +foreach (testsuite transformation 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) diff --git a/src/test/storm-pomdp/transformation/MakeCanonicTest.cpp b/src/test/storm-pomdp/transformation/MakeCanonicTest.cpp new file mode 100644 index 000000000..f2d159a48 --- /dev/null +++ b/src/test/storm-pomdp/transformation/MakeCanonicTest.cpp @@ -0,0 +1,19 @@ +#include "test/storm_gtest.h" +#include "storm-config.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm/builder/ExplicitModelBuilder.h" +#include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" +#include "storm-pomdp/analysis/FormulaInformation.h" +#include "storm-pomdp/analysis/QualitativeAnalysisOnGraphs.h" +#include "storm-pomdp/transformer/MakePOMDPCanonic.h" + +TEST(MakeCanonic, Simple) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism"); + program = storm::utility::prism::preprocess(program, "slippery=0.4"); + std::shared_ptr formula = storm::api::parsePropertiesForPrismProgram("Pmax=? [F \"goal\" ]", program).front().getRawFormula(); + std::shared_ptr> pomdp = storm::api::buildSparseModel(program, {formula})->as>(); + storm::transformer::MakePOMDPCanonic makeCanonic(*pomdp); + pomdp = makeCanonic.transform(); +}