diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp
index c166f7536..f6a7d3863 100644
--- a/src/storm-dft-cli/storm-dft.cpp
+++ b/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);
diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h
index ca4c7588d..8b4f0ae9c 100644
--- a/src/storm-dft/api/storm-dft.h
+++ b/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.
diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp
index 753f1d23a..5caa0d555 100644
--- a/src/storm-dft/storage/dft/DFT.cpp
+++ b/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);
diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h
index 8999ef6ea..aef5036d8 100644
--- a/src/storm-dft/storage/dft/DFT.h
+++ b/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;
diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp
index 71c440abd..6da316081 100644
--- a/src/test/storm-dft/api/DftModelCheckerTest.cpp
+++ b/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);
diff --git a/src/test/storm-dft/api/DftParserTest.cpp b/src/test/storm-dft/api/DftParserTest.cpp
index 93df569d1..4a19aed08 100644
--- a/src/test/storm-dft/api/DftParserTest.cpp
+++ b/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));
}
}