Added well-formedness check for DFTs

src/storm-dft-cli/storm-dft.cpp

@@ -51,6 +51,12 @@ void processOptions() {
         return;
     }
 
+    // Check well-formedness of DFT
+    std::stringstream stream;
+    if (!dft->checkWellFormedness(stream)) {
+        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "DFT is not well-formed: " << stream.str());
+    }
+
     if (dftGspnSettings.isTransformToGspn()) {
         // Transform to GSPN
         std::pair<std::shared_ptr<storm::gspn::GSPN>, uint64_t> pair = storm::api::transformToGSPN(*dft);

src/storm-dft/api/storm-dft.h

@@ -53,6 +53,13 @@ namespace storm {
                 return std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJsonFromFile(file));
         }
 
+        template<typename ValueType>
+        bool isWellFormed(storm::storage::DFT<ValueType> const& dft) {
+            std::stringstream stream;
+            return dft.checkWellFormedness(stream);
+        }
+
+
         /*!
          * Analyse the given DFT according to the given properties.
          * First the Markov model is built from the DFT and then this model is checked against the given properties.

src/storm-dft/storage/dft/DFT.cpp

@@ -48,17 +48,6 @@ namespace storm {
                 }
             }
 
-            // Check independence of spare modules
-            // TODO: comparing one element of each spare module sufficient?
-            for (auto module1 = mSpareModules.begin() ; module1 != mSpareModules.end() ; ++module1) {
-                size_t firstElement = module1->second.front();
-                for (auto module2 = std::next(module1) ; module2 != mSpareModules.end() ; ++module2) {
-                    if (std::find(module2->second.begin(), module2->second.end(), firstElement) != module2->second.end()) {
-                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Spare modules of '" << getElement(module1->first)->name() << "' and '" << getElement(module2->first)->name() << "' should not overlap.");
-                    }
-                }
-            }
-
             // For the top module, we assume, contrary to [Jun15], that we have all spare gates and basic elements which are not in another module.
             std::set<size_t> topModuleSet;
             // Initialize with all ids.
@@ -617,6 +606,26 @@ namespace storm {
             return !getDependencies().empty();
         }
 
+        template<typename ValueType>
+        bool DFT<ValueType>::checkWellFormedness(std::ostream& stream) const {
+            bool wellformed = true;
+            // Check independence of spare modules
+            // TODO: comparing one element of each spare module sufficient?
+            for (auto module1 = mSpareModules.begin() ; module1 != mSpareModules.end() ; ++module1) {
+                size_t firstElement = module1->second.front();
+                for (auto module2 = std::next(module1); module2 != mSpareModules.end(); ++module2) {
+                    if (std::find(module2->second.begin(), module2->second.end(), firstElement) != module2->second.end()) {
+                        if (!wellformed) {
+                            stream << std::endl;
+                        }
+                        stream << "Spare modules of '" << getElement(module1->first)->name() << "' and '" << getElement(module2->first)->name() << "' should not overlap.";
+                        wellformed = false;
+                    }
+                }
+            }
+            return wellformed;
+        }
+
         template<typename ValueType>
         DFTColouring<ValueType> DFT<ValueType>::colourDFT() const {
             return DFTColouring<ValueType>(*this);

src/storm-dft/storage/dft/DFT.h

@@ -205,7 +205,14 @@ namespace storm {
             }
 
             bool canHaveNondeterminism() const;
-            
+
+            /*!
+             * Check if the DFT is well-formed.
+             * @param stream Output stream where warnings about non-well-formed parts are written.
+             * @return True iff the DFT is well-formed.
+             */
+            bool checkWellFormedness(std::ostream& stream) const;
+
             uint64_t maxRank() const;
             
             std::vector<DFT<ValueType>> topModularisation() const;

src/test/storm-dft/api/DftModelCheckerTest.cpp

@@ -64,6 +64,7 @@ namespace {
 
         double analyzeMTTF(std::string const& file) {
             std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
+            EXPECT_TRUE(storm::api::isWellFormed(*dft));
             std::string property = "Tmin=? [F \"failed\"]";
             std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
             typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod, config.useDC, false);

src/test/storm-dft/api/DftParserTest.cpp

@@ -10,6 +10,7 @@ namespace {
         std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
         EXPECT_EQ(3ul, dft->nrElements());
         EXPECT_EQ(2ul, dft->nrBasicElements());
+        EXPECT_TRUE(storm::api::isWellFormed(*dft));
     }
 
     TEST(DftParserTest, LoadFromJsonFile) {
@@ -17,5 +18,6 @@ namespace {
         std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTJsonFile<double>(file);
         EXPECT_EQ(3ul, dft->nrElements());
         EXPECT_EQ(2ul, dft->nrBasicElements());
+        EXPECT_TRUE(storm::api::isWellFormed(*dft));
     }
 }