diff --git a/src/test/storm/builder/DdJaniModelBuilderTest.cpp b/src/test/storm/builder/DdJaniModelBuilderTest.cpp index 6cce536b4..7f2afa3d6 100644 --- a/src/test/storm/builder/DdJaniModelBuilderTest.cpp +++ b/src/test/storm/builder/DdJaniModelBuilderTest.cpp @@ -292,20 +292,6 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(59ul, mdp->getNumberOfChoices()); } -TEST(DdJaniModelBuilderTest_Cudd, IllegalSynchronizingWrites) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2-illegalSynchronizingWrite.nm"); - storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); - storm::builder::DdJaniModelBuilder builder; - EXPECT_THROW(std::shared_ptr> model = builder.build(janiModel), storm::exceptions::WrongFormatException); -} - -TEST(DdJaniModelBuilderTest_Sylvan, IllegalSynchronizingWrites) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2-illegalSynchronizingWrite.nm"); - storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); - storm::builder::DdJaniModelBuilder builder; - EXPECT_THROW(std::shared_ptr> model = builder.build(janiModel), storm::exceptions::WrongFormatException); -} - TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) { storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/SmallPrismTest.nm"); storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); diff --git a/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp b/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp index f98834a20..e6dfffcd7 100644 --- a/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp +++ b/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp @@ -147,14 +147,3 @@ TEST(ExplicitJaniModelBuilderTest, FailComposition) { ASSERT_THROW(storm::builder::ExplicitModelBuilder(janiModel).build(), storm::exceptions::WrongFormatException); } - -TEST(ExplicitJaniModelBuilderTest, IllegalSynchronizingWrites) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2-illegalSynchronizingWrite.nm"); - storm::jani::Model janiModel = program.toJani().substituteConstantsFunctions(); - storm::generator::NextStateGeneratorOptions options; - options.setExplorationChecks(true); - std::shared_ptr> nextStateGenerator = std::make_shared>(janiModel, options); - - ASSERT_THROW(storm::builder::ExplicitModelBuilder(nextStateGenerator).build(), storm::exceptions::WrongFormatException); -} - diff --git a/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp b/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp index d8a0c403d..0e6cf08c9 100644 --- a/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp +++ b/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp @@ -148,13 +148,3 @@ TEST(ExplicitJitJaniModelBuilderTest, FailComposition) { ASSERT_THROW(storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();, storm::exceptions::WrongFormatException); } - -TEST(ExplicitJitJaniModelBuilderTest, IllegalSynchronizingWrites) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2-illegalSynchronizingWrite.nm"); - storm::jani::Model janiModel = program.toJani().substituteConstantsFunctions(); - storm::builder::BuilderOptions options; - options.setExplorationChecks(true); - - ASSERT_THROW(storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel, options).build(), storm::exceptions::WrongFormatException); -} - diff --git a/src/test/storm/parser/PrismParserTest.cpp b/src/test/storm/parser/PrismParserTest.cpp index 4fe5735f5..62c970ba1 100644 --- a/src/test/storm/parser/PrismParserTest.cpp +++ b/src/test/storm/parser/PrismParserTest.cpp @@ -219,3 +219,8 @@ TEST(PrismParser, IllegalInputTest) { EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException); } + +TEST(PrismParser, IllegalSynchronizedWriteTest) { + EXPECT_THROW(storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2-illegalSynchronizingWrite.nm"), storm::exceptions::WrongFormatException); +} +