Tests: Illegal synchronized writes are now detected already during parsing.

The corresponding test case has thus been moved.

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<storm::dd::DdType::CUDD, double> builder;
-    EXPECT_THROW(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> 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<storm::dd::DdType::Sylvan, double> builder;
-    EXPECT_THROW(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> 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();

src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp

@@ -147,14 +147,3 @@ TEST(ExplicitJaniModelBuilderTest, FailComposition) {
 
     ASSERT_THROW(storm::builder::ExplicitModelBuilder<double>(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<storm::generator::NextStateGenerator<double, uint32_t>> nextStateGenerator = std::make_shared<storm::generator::JaniNextStateGenerator<double, uint32_t>>(janiModel, options);
-    
-    ASSERT_THROW(storm::builder::ExplicitModelBuilder<double>(nextStateGenerator).build(), storm::exceptions::WrongFormatException);
-}
-

src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp

@@ -148,13 +148,3 @@ TEST(ExplicitJitJaniModelBuilderTest, FailComposition) {
     
     ASSERT_THROW(storm::builder::jit::ExplicitJitJaniModelBuilder<double>(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<double>(janiModel, options).build(), storm::exceptions::WrongFormatException);
-}
-

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);
+}
+