diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index cef8717b2..2d2e24b8e 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -1,163 +1,65 @@ -#include "storm-dft/settings/DftSettings.h" +#include "storm-dft/api/storm-dft.h" +#include "storm-dft/settings/DftSettings.h" #include "storm-dft/settings/modules/DftIOSettings.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" #include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/ResourceSettings.h" #include "storm/utility/initialize.h" -#include "storm/api/storm.h" #include "storm-cli-utilities/cli.h" -#include "storm-dft/parser/DFTGalileoParser.h" -#include "storm-dft/parser/DFTJsonParser.h" -#include "storm-dft/modelchecker/dft/DFTModelChecker.h" -#include "storm-dft/modelchecker/dft/DFTASFChecker.h" -#include "storm-dft/transformations/DftToGspnTransformator.h" -#include "storm-dft/storage/dft/DftJsonExporter.h" - -#include "storm-gspn/storage/gspn/GSPN.h" -#include "storm-gspn/storm-gspn.h" - -#include -#include - -template -std::shared_ptr> loadDFT() { - storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule(); - std::shared_ptr> dft; - // Build DFT from given file. - if (dftIOSettings.isDftJsonFileSet()) { - storm::parser::DFTJsonParser parser; - STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftJsonFilename()); - dft = std::make_shared>(parser.parseJson(dftIOSettings.getDftJsonFilename())); - } else { - STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftFilename()); - dft = std::make_shared>(storm::parser::DFTGalileoParser::parseDFT(dftIOSettings.getDftFilename())); - } - - if (dftIOSettings.isDisplayStatsSet()) { - std::cout << "=============DFT Statistics==============" << std::endl; - dft->writeStatsToStream(std::cout); - std::cout << "=========================================" << std::endl; - } - return dft; -} - -/*! - * Analyse the given DFT according to the given properties. - * We first load the DFT from the given file, then build the corresponding model and last check against the given properties. - * - * @param properties PCTL formulas capturing the properties to check. - * @param symred Flag whether symmetry reduction should be used. - * @param allowModularisation Flag whether modularisation should be applied if possible. - * @param enableDC Flag whether Don't Care propagation should be used. - * @param approximationError Allowed approximation error. - */ -template -void analyzeDFT(std::vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { - std::shared_ptr> dft = loadDFT(); - - // Build properties - std::string propString = properties[0]; - for (size_t i = 1; i < properties.size(); ++i) { - propString += ";" + properties[i]; - } - std::vector> props = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propString)); - STORM_LOG_ASSERT(props.size() > 0, "No properties found."); - - // Check model - storm::modelchecker::DFTModelChecker modelChecker; - modelChecker.check(*dft, props, symred, allowModularisation, enableDC, approximationError); - modelChecker.printTimings(); - modelChecker.printResults(); -} - /*! - * Analyze the DFT with use of SMT solving. - * - * @param filename Path to DFT file in Galileo format. + * Process commandline options and start computations. */ template -void analyzeWithSMT(std::shared_ptr> dft) { - STORM_LOG_DEBUG("Running DFT analysis with use of SMT"); - storm::modelchecker::DFTASFChecker asfChecker(*dft); - asfChecker.convert(); - asfChecker.toFile("test.smt2"); - //bool sat = dftSmtBuilder.check(); - //std::cout << "SMT result: " << sat << std::endl; -} - void processOptions() { // Start by setting some urgent options (log levels, resources, etc.) storm::cli::setUrgentOptions(); storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule(); storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule(); - storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::getModule(); storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule(); + if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } + // Build DFT from given file + std::shared_ptr> dft; + if (dftIOSettings.isDftJsonFileSet()) { + STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftJsonFilename()); + dft = storm::api::loadDFTJson(dftIOSettings.getDftJsonFilename()); + } else { + STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftFilename()); + dft = storm::api::loadDFTGalileo(dftIOSettings.getDftFilename()); + } + + if (dftIOSettings.isDisplayStatsSet()) { + std::cout << "=============DFT Statistics==============" << std::endl; + dft->writeStatsToStream(std::cout); + std::cout << "=========================================" << std::endl; + } + if (dftIOSettings.isExportToJson()) { - STORM_LOG_THROW(dftIOSettings.isDftFileSet(), storm::exceptions::InvalidSettingsException, "No input model in Galileo format given."); - std::shared_ptr> dft = loadDFT(); // Export to json - storm::storage::DftJsonExporter::toFile(*dft, dftIOSettings.getExportJsonFilename()); + storm::api::exportDFTToJson(*dft, dftIOSettings.getExportJsonFilename()); return; } - if (dftIOSettings.isTransformToGspn()) { - std::shared_ptr> dft = loadDFT(); // Transform to GSPN - storm::transformations::dft::DftToGspnTransformator gspnTransformator(*dft); - bool smart = true; - gspnTransformator.transform(smart); - storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN(); - uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId(); - - storm::handleGSPNExportSettings(*gspn); - - std::shared_ptr const& exprManager = gspn->getExpressionManager(); - storm::builder::JaniGSPNBuilder builder(*gspn); - storm::jani::Model* model = builder.build(); - storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace); - - storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression(); - auto evtlFormula = std::make_shared(targetExpression); - auto tbFormula = std::make_shared(std::make_shared(true), evtlFormula, storm::logic::TimeBound(false, exprManager->integer(0)), storm::logic::TimeBound(false, exprManager->integer(10)), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time)); - auto tbUntil = std::make_shared(tbFormula); - - auto evFormula = std::make_shared(evtlFormula, storm::logic::FormulaContext::Time); - auto rewFormula = std::make_shared(evFormula, storm::logic::OperatorInformation(), storm::logic::RewardMeasureType::Expectation); - - storm::settings::modules::JaniExportSettings const& janiSettings = storm::settings::getModule(); - if (janiSettings.isJaniFileSet()) { - storm::api::exportJaniModel(*model, {storm::jani::Property("time-bounded", tbUntil), storm::jani::Property("mttf", rewFormula)}, janiSettings.getJaniFilename()); - } - - delete model; - delete gspn; + storm::api::transformToGSPN(*dft); return; } - bool parametric = false; -#ifdef STORM_HAVE_CARL - parametric = generalSettings.isParametricSet(); -#endif - + #ifdef STORM_HAVE_Z3 if (faultTreeSettings.solveWithSMT()) { // Solve with SMT - if (parametric) { - // std::shared_ptr> dft = loadDFT(); - // analyzeWithSMT(dftSettings.getDftFilename()); - } else { - std::shared_ptr> dft = loadDFT(); - analyzeWithSMT(dft); - } + STORM_LOG_DEBUG("Running DFT analysis with use of SMT"); + storm::api::exportDFTToSMT(*dft, "test.smt2"); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only exported to SMT file 'test.smt2' but analysis is not supported."); return; } #endif @@ -169,9 +71,8 @@ void processOptions() { optimizationDirection = "max"; } - // Construct properties to check for + // Construct properties to analyse std::vector properties; - if (ioSettings.isPropertySet()) { properties.push_back(ioSettings.getProperty()); } @@ -194,38 +95,32 @@ void processOptions() { } } - if (properties.empty()) { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No property given."); - } - // Set possible approximation error double approximationError = 0.0; if (faultTreeSettings.isApproximationErrorSet()) { approximationError = faultTreeSettings.getApproximationError(); } - // From this point on we are ready to carry out the actual computations. - if (parametric) { -#ifdef STORM_HAVE_CARL - analyzeDFT(properties, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), approximationError); -#else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build."); -#endif - } else { - analyzeDFT(properties, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), approximationError); + // Build properties + STORM_LOG_THROW(!properties.empty(), storm::exceptions::InvalidSettingsException, "No property given."); + std::string propString = properties[0]; + for (size_t i = 1; i < properties.size(); ++i) { + propString += ";" + properties[i]; } + std::vector> props = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propString)); + STORM_LOG_ASSERT(props.size() > 0, "No properties found."); + + // Carry out the actual analysis + storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), approximationError); } /*! - * Entry point for the DyFTeE backend. + * Entry point for Storm-DFT. * * @param argc The argc argument of main(). * @param argv The argv argument of main(). * @return Return code, 0 if successfull, not 0 otherwise. */ -/*! - * Main entry point of the executable storm-pars. - */ int main(const int argc, const char** argv) { try { storm::utility::setUp(); @@ -237,7 +132,12 @@ int main(const int argc, const char** argv) { return -1; } - processOptions(); + storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::getModule(); + if (generalSettings.isParametricSet()) { + processOptions(); + } else { + processOptions(); + } totalTimer.stop(); if (storm::settings::getModule().isPrintTimeAndMemorySet()) { @@ -248,10 +148,10 @@ int main(const int argc, const char** argv) { storm::utility::cleanUp(); return 0; } catch (storm::exceptions::BaseException const& exception) { - STORM_LOG_ERROR("An exception caused Storm-DyFTeE to terminate. The message of the exception is: " << exception.what()); + STORM_LOG_ERROR("An exception caused Storm-DFT to terminate. The message of the exception is: " << exception.what()); return 1; } catch (std::exception const& exception) { - STORM_LOG_ERROR("An unexpected exception occurred and caused Storm-DyFTeE to terminate. The message of this exception is: " << exception.what()); + STORM_LOG_ERROR("An unexpected exception occurred and caused Storm-DFT to terminate. The message of this exception is: " << exception.what()); return 2; } } diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h new file mode 100644 index 000000000..fc88fe792 --- /dev/null +++ b/src/storm-dft/api/storm-dft.h @@ -0,0 +1,159 @@ +#pragma once + +#include + +#include "storm-dft/parser/DFTGalileoParser.h" +#include "storm-dft/parser/DFTJsonParser.h" +#include "storm-dft/storage/dft/DftJsonExporter.h" + +#include "storm-dft/modelchecker/dft/DFTModelChecker.h" +#include "storm-dft/modelchecker/dft/DFTASFChecker.h" + +#include "storm-dft/transformations/DftToGspnTransformator.h" +#include "storm-gspn/storage/gspn/GSPN.h" +#include "storm-gspn/storm-gspn.h" + +namespace storm { + namespace api { + + /*! + * Load DFT from Galileo file. + * + * @param file File containing DFT description in Galileo format. + * + * @return DFT. + */ + template + std::shared_ptr> loadDFTGalileo(std::string const& file) { + return std::make_shared>(storm::parser::DFTGalileoParser::parseDFT(file)); + } + + /*! + * Load DFT from JSON file. + * + * @param file File containing DFT description in JSON format. + * + * @return DFT. + */ + template + std::shared_ptr> loadDFTJson(std::string const& file) { + storm::parser::DFTJsonParser parser; + return std::make_shared>(parser.parseJson(file)); + } + + /*! + * 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. + * + * @param dft DFT. + * @param properties PCTL formulas capturing the properties to check. + * @param symred Flag whether symmetry reduction should be used. + * @param allowModularisation Flag whether modularisation should be applied if possible. + * @param enableDC Flag whether Don't Care propagation should be used. + * @param approximationError Allowed approximation error, 0 indicates no approximation. + */ + template + void analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { + storm::modelchecker::DFTModelChecker modelChecker; + modelChecker.check(dft, properties, symred, allowModularisation, enableDC, approximationError); + modelChecker.printTimings(); + modelChecker.printResults(); + } + + + /*! + * Export DFT to JSON file. + * + * @param dft DFT. + * @param file File. + */ + template + typename std::enable_if::value, void>::type exportDFTToJson(storm::storage::DFT const& dft, std::string const& file) { + storm::storage::DftJsonExporter::toFile(dft, file); + } + + /*! + * Export DFT to JSON file. + * + * @param dft DFT. + * @param file File. + */ + template + typename std::enable_if::value, void>::type exportDFTToJson(storm::storage::DFT const& dft, std::string const& file) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export to JSON not supported for this data type."); + } + + /*! + * Export DFT to SMT encoding. + * + * @param dft DFT. + * @param file File. + */ + template + typename std::enable_if::value, void>::type exportDFTToSMT(storm::storage::DFT const& dft, std::string const& file) { + storm::modelchecker::DFTASFChecker asfChecker(dft); + asfChecker.convert(); + asfChecker.toFile(file); + } + + /*! + * Export DFT to SMT encoding. + * + * @param dft DFT. + * @param file File. + */ + template + typename std::enable_if::value, void>::type exportDFTToSMT(storm::storage::DFT const& dft, std::string const& file) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export to SMT does not support this data type."); + } + + /*! + * Transform DFT to GSPN. + * + * @param dft DFT. + */ + template + typename std::enable_if::value, void>::type transformToGSPN(storm::storage::DFT const& dft) { + // Transform to GSPN + storm::transformations::dft::DftToGspnTransformator gspnTransformator(dft); + bool smart = true; + gspnTransformator.transform(smart); + storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN(); + uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId(); + + storm::handleGSPNExportSettings(*gspn); + + std::shared_ptr const& exprManager = gspn->getExpressionManager(); + storm::builder::JaniGSPNBuilder builder(*gspn); + storm::jani::Model* model = builder.build(); + storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace); + + storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression(); + auto evtlFormula = std::make_shared(targetExpression); + auto tbFormula = std::make_shared(std::make_shared(true), evtlFormula, storm::logic::TimeBound(false, exprManager->integer(0)), storm::logic::TimeBound(false, exprManager->integer(10)), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time)); + auto tbUntil = std::make_shared(tbFormula); + + auto evFormula = std::make_shared(evtlFormula, storm::logic::FormulaContext::Time); + auto rewFormula = std::make_shared(evFormula, storm::logic::OperatorInformation(), storm::logic::RewardMeasureType::Expectation); + + storm::settings::modules::JaniExportSettings const& janiSettings = storm::settings::getModule(); + if (janiSettings.isJaniFileSet()) { + storm::api::exportJaniModel(*model, {storm::jani::Property("time-bounded", tbUntil), storm::jani::Property("mttf", rewFormula)}, janiSettings.getJaniFilename()); + } + + delete model; + delete gspn; + } + + /*! + * Transform DFT to GSPN. + * + * @param dft DFT. + */ + template + typename std::enable_if::value, void>::type transformToGSPN(storm::storage::DFT const& dft) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation to GSPN not supported for this data type."); + } + + } +}