|
@ -72,38 +72,35 @@ namespace { |
|
|
return config; |
|
|
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<double> dftTransformator = storm::transformations::dft::DftTransformator<double>(); |
|
|
storm::transformations::dft::DftTransformator<double> dftTransformator = storm::transformations::dft::DftTransformator<double>(); |
|
|
std::shared_ptr<storm::storage::DFT<double>> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile<double>(file))); |
|
|
std::shared_ptr<storm::storage::DFT<double>> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile<double>(file))); |
|
|
EXPECT_TRUE(storm::api::isWellFormed(*dft).first); |
|
|
EXPECT_TRUE(storm::api::isWellFormed(*dft).first); |
|
|
std::string property = "Tmin=? [F \"failed\"]"; |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
// Create property
|
|
|
std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); |
|
|
std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); |
|
|
|
|
|
|
|
|
|
|
|
// Create relevant names
|
|
|
std::vector<std::string> relevantNames; |
|
|
std::vector<std::string> relevantNames; |
|
|
if (!config.useDC) { |
|
|
if (!config.useDC) { |
|
|
relevantNames.push_back("all"); |
|
|
relevantNames.push_back("all"); |
|
|
} |
|
|
} |
|
|
storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<ValueType>(*dft, properties, relevantNames, false); |
|
|
storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<ValueType>(*dft, properties, relevantNames, false); |
|
|
|
|
|
|
|
|
|
|
|
// Perform model checking
|
|
|
typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod, relevantEvents); |
|
|
typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod, relevantEvents); |
|
|
return boost::get<double>(results[0]); |
|
|
return boost::get<double>(results[0]); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
double analyzeReliability(std::string const &file, double bound) { |
|
|
|
|
|
storm::transformations::dft::DftTransformator<double> dftTransformator = storm::transformations::dft::DftTransformator<double>(); |
|
|
|
|
|
std::shared_ptr<storm::storage::DFT<double>> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile<double>(file))); |
|
|
|
|
|
EXPECT_TRUE(storm::api::isWellFormed(*dft).first); |
|
|
|
|
|
std::string property = "Pmin=? [F<=" + std::to_string(bound) + " \"failed\"]"; |
|
|
|
|
|
std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); |
|
|
|
|
|
|
|
|
|
|
|
std::vector<std::string> relevantNames; |
|
|
|
|
|
if (!config.useDC) { |
|
|
|
|
|
relevantNames.push_back("all"); |
|
|
|
|
|
|
|
|
double analyzeMTTF(std::string const& file) { |
|
|
|
|
|
std::string property = "Tmin=? [F \"failed\"]"; |
|
|
|
|
|
return analyze(file, property); |
|
|
} |
|
|
} |
|
|
storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<ValueType>(*dft, properties, relevantNames, false); |
|
|
|
|
|
|
|
|
|
|
|
typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod, relevantEvents); |
|
|
|
|
|
return boost::get<double>(results[0]); |
|
|
|
|
|
|
|
|
double analyzeReliability(std::string const &file, double bound) { |
|
|
|
|
|
std::string property = "Pmin=? [F<=" + std::to_string(bound) + " \"failed\"]"; |
|
|
|
|
|
return analyze(file, property); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
private: |
|
|
private: |
|
|