diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index 8c6bab4a8..9eb7145ea 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -72,38 +72,35 @@ namespace { return config; } - double analyzeMTTF(std::string const& file) { + double analyze(std::string const& file, std::string const& property) { + // Load, build and prepare DFT storm::transformations::dft::DftTransformator dftTransformator = storm::transformations::dft::DftTransformator(); std::shared_ptr> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile(file))); EXPECT_TRUE(storm::api::isWellFormed(*dft).first); - std::string property = "Tmin=? [F \"failed\"]"; + + // Create property std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); + // Create relevant names std::vector relevantNames; if (!config.useDC) { relevantNames.push_back("all"); } storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents(*dft, properties, relevantNames, false); + // Perform model checking typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, config.useMod, relevantEvents); return boost::get(results[0]); } + double analyzeMTTF(std::string const& file) { + std::string property = "Tmin=? [F \"failed\"]"; + return analyze(file, property); + } + double analyzeReliability(std::string const &file, double bound) { - storm::transformations::dft::DftTransformator dftTransformator = storm::transformations::dft::DftTransformator(); - std::shared_ptr> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile(file))); - EXPECT_TRUE(storm::api::isWellFormed(*dft).first); std::string property = "Pmin=? [F<=" + std::to_string(bound) + " \"failed\"]"; - std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); - - std::vector relevantNames; - if (!config.useDC) { - relevantNames.push_back("all"); - } - storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents(*dft, properties, relevantNames, false); - - typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, config.useMod, relevantEvents); - return boost::get(results[0]); + return analyze(file, property); } private: