From 1140d96ba551790e19e65c326a14db162b9ca3b6 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 22 Nov 2018 11:08:07 +0100 Subject: [PATCH] Added well-formedness check for DFTs --- src/storm-dft-cli/storm-dft.cpp | 6 ++++ src/storm-dft/api/storm-dft.h | 7 +++++ src/storm-dft/storage/dft/DFT.cpp | 31 ++++++++++++------- src/storm-dft/storage/dft/DFT.h | 9 +++++- .../storm-dft/api/DftModelCheckerTest.cpp | 1 + src/test/storm-dft/api/DftParserTest.cpp | 2 ++ 6 files changed, 44 insertions(+), 12 deletions(-) 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, 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>(parser.parseJsonFromFile(file)); } + template + bool isWellFormed(storm::storage::DFT 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 topModuleSet; // Initialize with all ids. @@ -617,6 +606,26 @@ namespace storm { return !getDependencies().empty(); } + template + bool DFT::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 DFTColouring DFT::colourDFT() const { return DFTColouring(*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> 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> dft = storm::api::loadDFTGalileoFile(file); + EXPECT_TRUE(storm::api::isWellFormed(*dft)); std::string property = "Tmin=? [F \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*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> dft = storm::api::loadDFTGalileoFile(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> dft = storm::api::loadDFTJsonFile(file); EXPECT_EQ(3ul, dft->nrElements()); EXPECT_EQ(2ul, dft->nrBasicElements()); + EXPECT_TRUE(storm::api::isWellFormed(*dft)); } }