From e4e069a98ce1c9c7000f2d9ff1a317ad3cd5b336 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 23 Oct 2019 18:50:21 +0200 Subject: [PATCH] Slight refactoring of transformations --- src/storm-cli-utilities/model-handling.h | 18 ++-- src/storm-dft-cli/storm-dft.cpp | 85 ++++++++----------- src/storm-dft/api/storm-dft.h | 66 +++++++++++--- .../transformations/DftTransformator.cpp | 1 + .../transformations/DftTransformator.h | 2 + src/storm/api/transformation.h | 45 ++++------ .../NonMarkovianChainTransformer.h | 27 +++--- 7 files changed, 132 insertions(+), 112 deletions(-) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 6613030a2..4db5adbed 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -326,12 +326,20 @@ namespace storm { template std::shared_ptr> preprocessSparseMarkovAutomaton(std::shared_ptr> const& model) { + auto transformationSettings = storm::settings::getModule(); + std::shared_ptr> result = model; model->close(); if (model->isConvertibleToCtmc()) { STORM_LOG_WARN_COND(false, "MA is convertible to a CTMC, consider using a CTMC instead."); result = model->convertToCtmc(); } + + if (transformationSettings.isChainEliminationSet() && result->isOfType(storm::models::ModelType::MarkovAutomaton)) { + result = storm::transformer::NonMarkovianChainTransformer::eliminateNonmarkovianStates( + result->template as>(), !transformationSettings.isIgnoreLabelingSet()); + } + return result; } @@ -351,18 +359,12 @@ namespace storm { auto generalSettings = storm::settings::getModule(); auto bisimulationSettings = storm::settings::getModule(); auto ioSettings = storm::settings::getModule(); - auto transformationSettings = storm::settings::getModule(); - + + std::pair>, bool> result = std::make_pair(model, false); if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { result.first = preprocessSparseMarkovAutomaton(result.first->template as>()); - if (transformationSettings.isChainEliminationSet() && - result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { - result.first = storm::transformer::NonMarkovianChainTransformer::eliminateNonmarkovianStates( - result.first->template as>(), - !transformationSettings.isIgnoreLabelingSet()); - } result.second = true; } diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index ebc7a73f8..3f9d302b3 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -14,7 +14,6 @@ #include "storm/utility/initialize.h" #include "storm-cli-utilities/cli.h" #include "storm-parsers/api/storm-parsers.h" -#include "storm-dft/transformations/DftTransformator.h" /*! @@ -25,52 +24,40 @@ 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::IOSettings const& ioSettings = storm::settings::getModule(); - storm::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule(); - storm::settings::modules::TransformationSettings const &transformationSettings = storm::settings::getModule(); - - auto dftTransformator = storm::transformations::dft::DftTransformator(); - - if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model given."); - } + auto const& dftIOSettings = storm::settings::getModule(); + auto const& faultTreeSettings = storm::settings::getModule(); + auto const& ioSettings = storm::settings::getModule(); + auto const& dftGspnSettings = storm::settings::getModule(); + auto const& transformationSettings = storm::settings::getModule(); // Build DFT from given file std::shared_ptr> dft; - if (dftIOSettings.isDftJsonFileSet()) { - STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftJsonFilename()); + if (dftIOSettings.isDftFileSet()) { + STORM_LOG_DEBUG("Loading DFT from Galileo file " << dftIOSettings.getDftFilename()); + dft = storm::api::loadDFTGalileoFile(dftIOSettings.getDftFilename()); + } else if (dftIOSettings.isDftJsonFileSet()) { + STORM_LOG_DEBUG("Loading DFT from Json file " << dftIOSettings.getDftJsonFilename()); dft = storm::api::loadDFTJsonFile(dftIOSettings.getDftJsonFilename()); } else { - STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftFilename()); - dft = storm::api::loadDFTGalileoFile(dftIOSettings.getDftFilename()); + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model given."); } + // DFT statistics if (dftIOSettings.isDisplayStatsSet()) { dft->writeStatsToStream(std::cout); } + // Export to json if (dftIOSettings.isExportToJson()) { - // Export to json storm::api::exportDFTToJsonFile(*dft, dftIOSettings.getExportJsonFilename()); } - // Limit to one constantly failed BE - if (faultTreeSettings.isUniqueFailedBE()) { - dft = dftTransformator.transformUniqueFailedBe(*dft); - } - - // Eliminate non-binary dependencies - if (!dft->getDependencies().empty()) { - dft = dftTransformator.transformBinaryFDEPs(*dft); - } // Check well-formedness of DFT auto wellFormedResult = storm::api::isWellFormed(*dft, false); STORM_LOG_THROW(wellFormedResult.first, storm::exceptions::UnmetRequirementException, "DFT is not well-formed: " << wellFormedResult.second); + // Transformation to GSPN if (dftGspnSettings.isTransformToGspn()) { - // Transform to GSPN std::pair, uint64_t> pair = storm::api::transformToGSPN(*dft); std::shared_ptr gspn = pair.first; uint64_t toplevelFailedPlace = pair.second; @@ -79,13 +66,13 @@ void processOptions() { storm::api::handleGSPNExportSettings(*gspn); // Transform to Jani + // TODO analyse Jani model std::shared_ptr model = storm::api::transformToJani(*gspn, toplevelFailedPlace); return; } - // SMT + // Export to SMT if (dftIOSettings.isExportToSmt()) { - // Export to smtlib2 storm::api::exportDFTToSMT(*dft, dftIOSettings.getExportSmtFilename()); return; } @@ -95,35 +82,35 @@ void processOptions() { #ifdef STORM_HAVE_Z3 if (faultTreeSettings.solveWithSMT()) { useSMT = true; - STORM_PRINT("Use SMT for preprocessing" << std::endl) + STORM_LOG_DEBUG("Use SMT for preprocessing"); } #endif + // Apply transformations + // TODO transform later before actual analysis + dft = storm::api::applyTransformations(*dft, faultTreeSettings.isUniqueFailedBE(), true); + + dft->setDynamicBehaviorInfo(); storm::api::PreprocessingResult preResults; - preResults.lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(*dft, useSMT, - solverTimeout); - preResults.upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, useSMT, - solverTimeout); - STORM_LOG_DEBUG("BE FAILURE BOUNDS" << std::endl << "========================================" << std::endl << + // TODO: always needed? + preResults.lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(*dft, useSMT, solverTimeout); + preResults.upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, useSMT, solverTimeout); + STORM_LOG_DEBUG("BE failure bounds" << std::endl << "========================================" << std::endl << "Lower bound: " << std::to_string(preResults.lowerBEBound) << std::endl << - "Upper bound: " << std::to_string(preResults.upperBEBound) << std::endl); + "Upper bound: " << std::to_string(preResults.upperBEBound)); // TODO: move into API call? preResults.fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, useSMT, solverTimeout); if (preResults.fdepConflicts.empty()) { - STORM_LOG_DEBUG("No FDEP conflicts found" << std::endl); + STORM_LOG_DEBUG("No FDEP conflicts found"); } else { - STORM_LOG_DEBUG("========================================" << std::endl << - "FDEP CONFLICTS" << std::endl << - "========================================" - << std::endl); + STORM_LOG_DEBUG("========================================" << std::endl << "FDEP CONFLICTS" << std::endl << "========================================"); } for (auto pair: preResults.fdepConflicts) { - STORM_LOG_DEBUG("Conflict between " << dft->getElement(pair.first)->name() << " and " - << dft->getElement(pair.second)->name() << std::endl); + STORM_LOG_DEBUG("Conflict between " << dft->getElement(pair.first)->name() << " and " << dft->getElement(pair.second)->name()); } // Set the conflict map of the dft @@ -140,16 +127,16 @@ void processOptions() { #ifdef STORM_HAVE_Z3 - if (faultTreeSettings.solveWithSMT()) { + if (useSMT) { // Solve with SMT - STORM_LOG_DEBUG("Running DFT analysis with use of SMT" << std::endl); + STORM_LOG_DEBUG("Running DFT analysis with use of SMT"); // Set dynamic behavior vector storm::api::analyzeDFTSMT(*dft, true); } #endif - // From now on we analyse DFT via model checking + // From now on we analyse the DFT via model checking // Set min or max std::string optimizationDirection = "min"; @@ -256,10 +243,8 @@ void processOptions() { approximationError = faultTreeSettings.getApproximationError(); } storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, - faultTreeSettings.isAllowDCForRelevantEvents(), approximationError, - faultTreeSettings.getApproximationHeuristic(), - transformationSettings.isChainEliminationSet(), - transformationSettings.isIgnoreLabelingSet(), true); + faultTreeSettings.isAllowDCForRelevantEvents(), approximationError, faultTreeSettings.getApproximationHeuristic(), + transformationSettings.isChainEliminationSet(), transformationSettings.isIgnoreLabelingSet(), true); } } diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index fdeddd7be..5912a3c73 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -9,6 +9,7 @@ #include "storm-dft/modelchecker/dft/DFTModelChecker.h" #include "storm-dft/modelchecker/dft/DFTASFChecker.h" #include "storm-dft/transformations/DftToGspnTransformator.h" +#include "storm-dft/transformations/DftTransformator.h" #include "storm-dft/utility/FDEPConflictFinder.h" #include "storm-dft/utility/FailureBoundFinder.h" @@ -70,6 +71,52 @@ namespace storm { return std::pair(wellFormed, stream.str()); } + /*! + * Apply transformations for DFT. + * + * @param dft DFT. + * @param uniqueBE Flag whether a unique constant failed BE is created. + * @param binaryFDEP Flag whether all dependencies should be binary (only one dependent child). + * @return Transformed DFT. + */ + template + std::shared_ptr> applyTransformations(storm::storage::DFT const& dft, bool uniqueBE, bool binaryFDEP) { + std::shared_ptr> transformedDFT = std::make_shared>(dft); + auto dftTransformator = storm::transformations::dft::DftTransformator(); + if (uniqueBE) { + transformedDFT = dftTransformator.transformUniqueFailedBe(*transformedDFT); + } + if (binaryFDEP && !dft.getDependencies().empty()) { + transformedDFT = dftTransformator.transformBinaryFDEPs(*transformedDFT); + } + return transformedDFT; + } + + template + bool computeDependencyConflicts(storm::storage::DFT const& dft, bool useSMT, double solverTimeout) { + std::vector> fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, useSMT, solverTimeout); + + if (fdepConflicts.empty()) { + return false; + } + for (auto pair: fdepConflicts) { + STORM_LOG_DEBUG("Conflict between " << dft.getElement(pair.first)->name() << " and " << dft.getElement(pair.second)->name()); + } + + // Set the conflict map of the dft + std::set conflict_set; + for (auto conflict : fdepConflicts) { + conflict_set.insert(size_t(conflict.first)); + conflict_set.insert(size_t(conflict.second)); + } + for (size_t depId : dft->getDependencies()) { + if (!conflict_set.count(depId)) { + dft->setDependencyNotInConflict(depId); + } + } + return true; + } + /*! * Compute the exact or approximate analysis result of 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. @@ -82,8 +129,8 @@ namespace storm { * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events. * @param approximationError Allowed approximation error. Value 0 indicates no approximation. * @param approximationHeuristic Heuristic used for state space exploration. - * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA - * @param ignoreLabeling If true, the labeling of states is ignored during state elimination + * @param eliminateChains If true, chains of non-Markovian states are eliminated from the resulting MA. + * @param ignoreLabeling If true, the labeling of states is ignored during state elimination. * @param printOutput If true, model information, timings, results, etc. are printed. * @return Results. */ @@ -91,14 +138,12 @@ namespace storm { typename storm::modelchecker::DFTModelChecker::dft_results analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred = true, bool allowModularisation = true, std::set const& relevantEvents = {}, bool allowDCForRelevantEvents = true, double approximationError = 0.0, - storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, - bool eliminateChains = false, bool ignoreLabeling = false, bool printOutput = false) { + storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool eliminateChains = false, + bool ignoreLabeling = false, bool printOutput = false) { storm::modelchecker::DFTModelChecker modelChecker(printOutput); typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents, - allowDCForRelevantEvents, approximationError, - approximationHeuristic, - eliminateChains, - ignoreLabeling); + allowDCForRelevantEvents, approximationError, approximationHeuristic, + eliminateChains, ignoreLabeling); if (printOutput) { modelChecker.printTimings(); modelChecker.printResults(results); @@ -114,8 +159,7 @@ namespace storm { * @return Result result vector */ template - void - analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput); + void analyzeDFTSMT(storm::storage::DFT const& dft, bool printOutput); /*! * Export DFT to JSON file. @@ -142,7 +186,7 @@ namespace storm { * @param file File. */ template - void exportDFTToSMT(storm::storage::DFT const &dft, std::string const &file); + void exportDFTToSMT(storm::storage::DFT const& dft, std::string const& file); /*! * Transform DFT to GSPN. diff --git a/src/storm-dft/transformations/DftTransformator.cpp b/src/storm-dft/transformations/DftTransformator.cpp index 473f4249b..6dcbdf17c 100644 --- a/src/storm-dft/transformations/DftTransformator.cpp +++ b/src/storm-dft/transformations/DftTransformator.cpp @@ -4,6 +4,7 @@ namespace storm { namespace transformations { namespace dft { + template DftTransformator::DftTransformator() { } diff --git a/src/storm-dft/transformations/DftTransformator.h b/src/storm-dft/transformations/DftTransformator.h index c8e832f1b..5e1c48f13 100644 --- a/src/storm-dft/transformations/DftTransformator.h +++ b/src/storm-dft/transformations/DftTransformator.h @@ -1,3 +1,5 @@ +#pragma once + #include "storm-dft/storage/dft/DFT.h" #include "storm-dft/builder/DFTBuilder.h" #include "storm/utility/macros.h" diff --git a/src/storm/api/transformation.h b/src/storm/api/transformation.h index 521aecb75..3ffbab033 100644 --- a/src/storm/api/transformation.h +++ b/src/storm/api/transformation.h @@ -16,21 +16,11 @@ namespace storm { * Eliminates chains of non-Markovian states from a given Markov Automaton */ template - std::pair>, std::vector>> - eliminateNonMarkovianChains(std::shared_ptr> const &ma, - std::vector> const &formulas, - bool ignoreLabeling) { - - auto newFormulas = storm::transformer::NonMarkovianChainTransformer::checkAndTransformFormulas( - formulas); - STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), - "The state elimination does not preserve all properties."); - STORM_LOG_WARN_COND(!ignoreLabeling, - "Labels are ignored for the state elimination. This may cause incorrect results."); - return std::make_pair( - storm::transformer::NonMarkovianChainTransformer::eliminateNonmarkovianStates(ma, - !ignoreLabeling), - newFormulas); + std::pair>, std::vector>> eliminateNonMarkovianChains(std::shared_ptr> const& ma, std::vector> const& formulas,bool ignoreLabeling) { + auto newFormulas = storm::transformer::NonMarkovianChainTransformer::checkAndTransformFormulas(formulas); + STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "The state elimination does not preserve all properties."); + STORM_LOG_WARN_COND(!ignoreLabeling, "Labels are ignored for the state elimination. This may cause incorrect results."); + return std::make_pair(storm::transformer::NonMarkovianChainTransformer::eliminateNonmarkovianStates(ma, !ignoreLabeling), newFormulas); } @@ -40,17 +30,17 @@ namespace storm { * If such a transformation does not preserve one of the given formulas, a warning is issued. */ template - std::pair>, std::vector>> transformContinuousToDiscreteTimeSparseModel(std::shared_ptr> const& model, std::vector> const& formulas) { - + std::pair>, std::vector>> transformContinuousToDiscreteTimeSparseModel(std::shared_ptr> const& model, std::vector> const& formulas) { + storm::transformer::ContinuousToDiscreteTimeModelTransformer transformer; - + std::string timeRewardName = "_time"; while(model->hasRewardModel(timeRewardName)) { timeRewardName += "_"; } auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName); STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model->getType() << " to a discrete time model does not preserve all properties."); - + if (model->isOfType(storm::models::ModelType::Ctmc)) { return std::make_pair(transformer.transform(*model->template as>(), timeRewardName), newFormulas); } else if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) { @@ -68,16 +58,16 @@ namespace storm { */ template std::pair>, std::vector>> transformContinuousToDiscreteTimeSparseModel(storm::models::sparse::Model&& model, std::vector> const& formulas) { - + storm::transformer::ContinuousToDiscreteTimeModelTransformer transformer; - + std::string timeRewardName = "_time"; while(model.hasRewardModel(timeRewardName)) { timeRewardName += "_"; } auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName); STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model.getType() << " to a discrete time model does not preserve all properties."); - + if (model.isOfType(storm::models::ModelType::Ctmc)) { return std::make_pair(transformer.transform(std::move(*model.template as>()), timeRewardName), newFormulas); } else if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) { @@ -86,9 +76,9 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model.getType() << " to a discrete time model is not supported."); } return std::make_pair(nullptr, newFormulas);; - + } - + template std::shared_ptr checkAndTransformContinuousToDiscreteTimeFormula(storm::logic::Formula const& formula, std::string const& timeRewardName = "_time") { storm::transformer::ContinuousToDiscreteTimeModelTransformer transformer; @@ -99,8 +89,7 @@ namespace storm { } return nullptr; } - - + /*! * Transforms the given symbolic model to a sparse model. */ @@ -118,7 +107,7 @@ namespace storm { } return nullptr; } - + template std::shared_ptr> transformToNondeterministicModel(storm::models::sparse::Model&& model) { storm::storage::sparse::ModelComponents components(std::move(model.getTransitionMatrix()), std::move(model.getStateLabeling()), std::move(model.getRewardModels())); @@ -135,6 +124,6 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot transform model of type " << model.getType() << " to a nondeterministic model."); } } - + } } diff --git a/src/storm/transformer/NonMarkovianChainTransformer.h b/src/storm/transformer/NonMarkovianChainTransformer.h index 317be4b2d..8382f7419 100644 --- a/src/storm/transformer/NonMarkovianChainTransformer.h +++ b/src/storm/transformer/NonMarkovianChainTransformer.h @@ -4,7 +4,7 @@ namespace storm { namespace transformer { /** - * Transformer for eliminating chains of non-Markovian states (instantaneous path fragment leading to the same outcome) from Markov Automata + * Transformer for eliminating chains of non-Markovian states (instantaneous path fragment leading to the same outcome) from Markov automata. */ template> class NonMarkovianChainTransformer { @@ -14,32 +14,29 @@ namespace storm { * Generates a model with the same basic behavior as the input, but eliminates non-Markovian chains. * If no non-determinism occurs, a CTMC is generated. * - * @param ma the input Markov Automaton - * @param preserveLabels if set, the procedure considers the labels of non-Markovian states when eliminating states - * @return a reference to the new Mmodel after eliminating non-Markovian states + * @param ma The input Markov Automaton. + * @param preserveLabels If set, the procedure considers the labels of non-Markovian states when eliminating states. + * @return A reference to the new model after eliminating non-Markovian states. */ - static std::shared_ptr< - models::sparse::Model < ValueType, RewardModelType>> eliminateNonmarkovianStates(std::shared_ptr< - models::sparse::MarkovAutomaton < ValueType, RewardModelType>> ma, - bool preserveLabels = true + static std::shared_ptr> eliminateNonmarkovianStates( + std::shared_ptr> ma, bool preserveLabels = true ); /** * Check if the property specified by the given formula is preserved by the transformation. * - * @param formula the formula to check - * @return true, if the property is preserved + * @param formula The formula to check. + * @return True, if the property is preserved. */ - static bool preservesFormula(storm::logic::Formula const &formula); + static bool preservesFormula(storm::logic::Formula const& formula); /** * Checks for the given formulae if the specified properties are preserved and removes formulae of properties which are not preserved. * - * @param formulas - * @return vector containing all fomulae which are valid for the transformed model + * @param formulas Formulae. + * @return Vector containing all fomulae which are valid for the transformed model. */ - static std::vector> - checkAndTransformFormulas(std::vector> const &formulas); + static std::vector> checkAndTransformFormulas(std::vector> const& formulas); }; } }