diff --git a/resources/examples/testfiles/mdp/unbounded.nm b/resources/examples/testfiles/mdp/unbounded.nm new file mode 100644 index 000000000..235caa982 --- /dev/null +++ b/resources/examples/testfiles/mdp/unbounded.nm @@ -0,0 +1,8 @@ +mdp +const int N; +module main + x : int; + [] x<=0 -> (x'=x+1); + [] x>0 -> (x'=N*x); +endmodule + diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index 79c7fb8a3..6a879d9ba 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -541,7 +541,7 @@ namespace storm { template bool DdPrismModelBuilder::canHandle(storm::prism::Program const& program) { - return program.getModelType() != storm::prism::Program::ModelType::PTA; + return !program.hasUnboundedVariables() && (program.getModelType() != storm::prism::Program::ModelType::PTA); } template @@ -1311,6 +1311,7 @@ namespace storm { stream << "."; STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str()); } + STORM_LOG_THROW(!program.hasUnboundedVariables(), storm::exceptions::InvalidArgumentException, "Program contains unbounded variables which is not supported by the DD engine."); STORM_LOG_TRACE("Building representation of program:" << std::endl << program << std::endl); diff --git a/src/test/storm/builder/DdPrismModelBuilderTest.cpp b/src/test/storm/builder/DdPrismModelBuilderTest.cpp index fef10b9a3..b64e2d277 100644 --- a/src/test/storm/builder/DdPrismModelBuilderTest.cpp +++ b/src/test/storm/builder/DdPrismModelBuilderTest.cpp @@ -319,3 +319,14 @@ TEST(DdPrismModelBuilderTest_Cudd, Composition) { EXPECT_EQ(21ul, mdp->getNumberOfChoices()); } +TEST(UnboundedTest_Sylvan, Mdp) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm"); + storm::prism::Program program = modelDescription.preprocess("N=1").asPrismProgram(); + EXPECT_FALSE(storm::builder::DdPrismModelBuilder().canHandle(program)); +} + +TEST(UnboundedTest_Cudd, Mdp) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm"); + storm::prism::Program program = modelDescription.preprocess("N=1").asPrismProgram(); + EXPECT_FALSE(storm::builder::DdPrismModelBuilder().canHandle(program)); +} \ No newline at end of file