From 605546358bc42d2ad5cbb9a64b4a17074fb5817d Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Fri, 15 Nov 2019 10:11:35 +0100 Subject: [PATCH] Added option to merge labels of eliminated states into existing states --- src/storm-cli-utilities/model-handling.h | 2 +- src/storm-dft-cli/storm-dft.cpp | 2 +- src/storm-dft/api/storm-dft.h | 6 +- .../modelchecker/dft/DFTModelChecker.cpp | 13 ++--- .../modelchecker/dft/DFTModelChecker.h | 14 +++-- src/storm-pars-cli/storm-pars.cpp | 2 +- src/storm/api/transformation.h | 9 ++- .../modules/TransformationSettings.cpp | 30 ++++++++-- .../settings/modules/TransformationSettings.h | 9 +-- .../NonMarkovianChainTransformer.cpp | 55 +++++++++++++++---- .../NonMarkovianChainTransformer.h | 9 ++- 11 files changed, 108 insertions(+), 43 deletions(-) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 060f87dcd..a70ddf981 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -341,7 +341,7 @@ namespace storm { if (transformationSettings.isChainEliminationSet() && result->isOfType(storm::models::ModelType::MarkovAutomaton)) { result = storm::transformer::NonMarkovianChainTransformer::eliminateNonmarkovianStates( - result->template as>(), !transformationSettings.isIgnoreLabelingSet()); + result->template as>(), transformationSettings.getLabelBehavior()); } return result; diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 3f9d302b3..130e32765 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -244,7 +244,7 @@ void processOptions() { } storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, faultTreeSettings.isAllowDCForRelevantEvents(), approximationError, faultTreeSettings.getApproximationHeuristic(), - transformationSettings.isChainEliminationSet(), transformationSettings.isIgnoreLabelingSet(), true); + transformationSettings.isChainEliminationSet(), transformationSettings.getLabelBehavior(), true); } } diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index 5912a3c73..22f7152ef 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -130,7 +130,7 @@ namespace storm { * @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 eliminated from the resulting MA. - * @param ignoreLabeling If true, the labeling of states is ignored during state elimination. + * @param labelBehavior Behavior of labels of eliminated states * @param printOutput If true, model information, timings, results, etc. are printed. * @return Results. */ @@ -139,11 +139,11 @@ namespace storm { 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::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels, 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); + eliminateChains, labelBehavior); if (printOutput) { modelChecker.printTimings(); modelChecker.printResults(results); diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 83887c503..3fbf9cdd0 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -25,7 +25,7 @@ namespace storm { bool allowModularisation, std::set const& relevantEvents, bool allowDCForRelevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic, bool eliminateChains, - bool ignoreLabeling) { + storm::transformer::EliminationLabelBehavior labelBehavior) { totalTimer.start(); dft_results results; @@ -50,7 +50,7 @@ namespace storm { } } else { results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevantEvents, approximationError, approximationHeuristic, - eliminateChains, ignoreLabeling); + eliminateChains, labelBehavior); } totalTimer.stop(); return results; @@ -61,7 +61,7 @@ namespace storm { bool symred, bool allowModularisation, std::set const& relevantEvents, bool allowDCForRelevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic, - bool eliminateChains, bool ignoreLabeling) { + bool eliminateChains, storm::transformer::EliminationLabelBehavior labelBehavior) { STORM_LOG_TRACE("Check helper called"); std::vector> dfts; bool invResults = false; @@ -160,7 +160,7 @@ namespace storm { } else { // No modularisation was possible return checkDFT(dft, properties, symred, relevantEvents, allowDCForRelevantEvents, approximationError, - approximationHeuristic, eliminateChains, ignoreLabeling); + approximationHeuristic, eliminateChains, labelBehavior); } } @@ -299,7 +299,7 @@ namespace storm { std::set const &relevantEvents, bool allowDCForRelevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic, - bool eliminateChains, bool ignoreLabeling) { + bool eliminateChains, storm::transformer::EliminationLabelBehavior labelBehavior) { explorationTimer.start(); // Find symmetries @@ -406,8 +406,7 @@ namespace storm { std::shared_ptr> model = builder.getModel(); if (eliminateChains && model->isOfType(storm::models::ModelType::MarkovAutomaton)) { auto ma = std::static_pointer_cast>(model); - model = storm::transformer::NonMarkovianChainTransformer::eliminateNonmarkovianStates(ma, - !ignoreLabeling); + model = storm::transformer::NonMarkovianChainTransformer::eliminateNonmarkovianStates(ma, labelBehavior); } explorationTimer.stop(); diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h index 9b898725a..d40d1488f 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -56,13 +56,13 @@ namespace storm { * @param approximationError Error allowed for approximation. 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 labelBehavior Behavior of labels of eliminated states * @return Model checking results for the given properties.. */ dft_results check(storm::storage::DFT const& origDft, property_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 eliminateChains = false, storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels); /*! * Print timings of all operations to stream. @@ -102,13 +102,14 @@ namespace storm { * @param approximationError Error allowed for approximation. Value 0 indicates no approximation. * @param approximationHeuristic Heuristic used for approximation. * @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 labelBehavior Behavior of labels of eliminated states * @return Model checking results (or in case of approximation two results for lower and upper bound) */ dft_results checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, 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 eliminateChains = false, + storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels); /*! * Internal helper for building a CTMC from a DFT via parallel composition. @@ -136,14 +137,15 @@ namespace storm { * @param approximationError Error allowed for approximation. Value 0 indicates no approximation. * @param approximationHeuristic Heuristic used for approximation. * @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 labelBehavior Behavior of labels of eliminated states * * @return Model checking result */ dft_results checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, 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 eliminateChains = false, + storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels); /*! * Check the given markov model for the given properties. diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index de8542e25..d290dd47c 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -181,7 +181,7 @@ namespace storm { auto eliminationResult = storm::api::eliminateNonMarkovianChains( result.model->template as>(), storm::api::extractFormulasFromProperties(input.properties), - transformationSettings.isIgnoreLabelingSet()); + transformationSettings.getLabelBehavior()); result.model = eliminationResult.first; // Set transformed properties as new properties in input result.formulas = eliminationResult.second; diff --git a/src/storm/api/transformation.h b/src/storm/api/transformation.h index 3ffbab033..9aa99aa01 100644 --- a/src/storm/api/transformation.h +++ b/src/storm/api/transformation.h @@ -16,11 +16,14 @@ 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) { + std::pair>, std::vector>> + eliminateNonMarkovianChains(std::shared_ptr> const &ma, + std::vector> const &formulas, storm::transformer::EliminationLabelBehavior labelBehavior) { 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); + STORM_LOG_WARN_COND(!(labelBehavior == storm::transformer::EliminationLabelBehavior::KeepLabels), + "Labels are not preserved by the state elimination. This may cause incorrect results."); + return std::make_pair(storm::transformer::NonMarkovianChainTransformer::eliminateNonmarkovianStates(ma, labelBehavior), newFormulas); } diff --git a/src/storm/settings/modules/TransformationSettings.cpp b/src/storm/settings/modules/TransformationSettings.cpp index 4b0d50ae0..ed9b0252c 100644 --- a/src/storm/settings/modules/TransformationSettings.cpp +++ b/src/storm/settings/modules/TransformationSettings.cpp @@ -2,7 +2,9 @@ #include "storm/settings/Option.h" #include "storm/settings/OptionBuilder.h" +#include "storm/settings/ArgumentBuilder.h" #include "storm/exceptions/InvalidSettingsException.h" +#include "storm/exceptions/IllegalArgumentValueException.h" namespace storm { namespace settings { @@ -11,7 +13,7 @@ namespace storm { const std::string TransformationSettings::moduleName = "transformation"; const std::string TransformationSettings::chainEliminationOptionName = "eliminate-chains"; - const std::string TransformationSettings::ignoreLabelingOptionName = "ec-ignore-labeling"; + const std::string TransformationSettings::labelBehaviorOptionName = "ec-label-behavior"; const std::string TransformationSettings::toNondetOptionName = "to-nondet"; const std::string TransformationSettings::toDiscreteTimeOptionName = "to-discrete"; @@ -19,8 +21,15 @@ namespace storm { TransformationSettings::TransformationSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, chainEliminationOptionName, false, "If set, chains of non-Markovian states are eliminated if the resulting model is a Markov Automaton.").setIsAdvanced().build()); - this->addOption(storm::settings::OptionBuilder(moduleName, ignoreLabelingOptionName, false, - "If set, the elimination of chains ignores the labels for all non-Markovian states. This may cause wrong results.").setIsAdvanced().build()); + std::vector labelBehavior; + labelBehavior.push_back("keep"); + labelBehavior.push_back("merge"); + labelBehavior.push_back("delete"); + this->addOption(storm::settings::OptionBuilder(moduleName, labelBehaviorOptionName, false, + "Sets the behavior of labels for all non-Markovian states. Some options may cause wrong results.").setIsAdvanced().addArgument( + storm::settings::ArgumentBuilder::createStringArgument("behavior", + "The behavior how the transformer handles labels of non-Markovian states").setDefaultValueString( + "keep").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(labelBehavior)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, toNondetOptionName, false, "If set, DTMCs/CTMCs are converted to MDPs/MAs (without actual nondeterminism) before model checking.").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, toDiscreteTimeOptionName, false, "If set, CTMCs/MAs are converted to DTMCs/MDPs (which might or might not preserve the provided properties).").setIsAdvanced().build()); } @@ -29,8 +38,17 @@ namespace storm { return this->getOption(chainEliminationOptionName).getHasOptionBeenSet(); } - bool TransformationSettings::isIgnoreLabelingSet() const { - return this->getOption(ignoreLabelingOptionName).getHasOptionBeenSet(); + storm::transformer::EliminationLabelBehavior TransformationSettings::getLabelBehavior() const { + std::string labelBehaviorAsString = this->getOption(labelBehaviorOptionName).getArgumentByName("behavior").getValueAsString(); + if (labelBehaviorAsString == "keep") { + return storm::transformer::EliminationLabelBehavior::KeepLabels; + } else if (labelBehaviorAsString == "merge") { + return storm::transformer::EliminationLabelBehavior::MergeLabels; + } else if (labelBehaviorAsString == "delete") { + return storm::transformer::EliminationLabelBehavior::DeleteLabels; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, + "Illegal value '" << labelBehaviorAsString << "' set as label behavior for the elimination."); } bool TransformationSettings::isToNondeterministicModelSet() const { @@ -43,7 +61,7 @@ namespace storm { bool TransformationSettings::check() const { // Ensure that labeling preservation is only set if chain elimination is set - STORM_LOG_THROW(isChainEliminationSet() || !isIgnoreLabelingSet(), + STORM_LOG_THROW(isChainEliminationSet() || !this->getOption(labelBehaviorOptionName).getHasOptionBeenSet(), storm::exceptions::InvalidSettingsException, "Label preservation can only be chosen if chain elimination is applied."); diff --git a/src/storm/settings/modules/TransformationSettings.h b/src/storm/settings/modules/TransformationSettings.h index 00642e5fb..8603893a5 100644 --- a/src/storm/settings/modules/TransformationSettings.h +++ b/src/storm/settings/modules/TransformationSettings.h @@ -3,6 +3,7 @@ #include "storm-config.h" #include "storm/settings/modules/ModuleSettings.h" +#include "storm/api/transformation.h" namespace storm { namespace settings { @@ -28,11 +29,11 @@ namespace storm { /*! - * Retrieves whether the preserve-labeling option for jani was set. + * Retrieves how the transformer should deal with labels when non-Markovian states are eliminated * - * @return True if the preserve-labeling option was set. + * @return the label behavior */ - bool isIgnoreLabelingSet() const; + storm::transformer::EliminationLabelBehavior getLabelBehavior() const; /*! * Retrieves whether a DTMC/CTMC should be converted to an MDP/MA @@ -54,7 +55,7 @@ namespace storm { private: // Define the string names of the options as constants. static const std::string chainEliminationOptionName; - static const std::string ignoreLabelingOptionName; + static const std::string labelBehaviorOptionName; static const std::string toNondetOptionName; static const std::string toDiscreteTimeOptionName; diff --git a/src/storm/transformer/NonMarkovianChainTransformer.cpp b/src/storm/transformer/NonMarkovianChainTransformer.cpp index be5e57858..2b77b69dc 100644 --- a/src/storm/transformer/NonMarkovianChainTransformer.cpp +++ b/src/storm/transformer/NonMarkovianChainTransformer.cpp @@ -21,10 +21,16 @@ namespace storm { std::shared_ptr> NonMarkovianChainTransformer::eliminateNonmarkovianStates( std::shared_ptr> ma, - bool preserveLabels) { + EliminationLabelBehavior labelBehavior) { // TODO reward models - STORM_LOG_WARN_COND(preserveLabels, "Labels are not preserved! Results may be incorrect."); + STORM_LOG_WARN_COND(labelBehavior == EliminationLabelBehavior::KeepLabels, "Labels are not preserved! Results may be incorrect. Continue at your own caution."); + if (labelBehavior == EliminationLabelBehavior::DeleteLabels) { + STORM_PRINT("Use Label Deletion" << std::endl) + } + if (labelBehavior == EliminationLabelBehavior::MergeLabels) { + STORM_PRINT("Use Label Merging" << std::endl) + } STORM_LOG_WARN("Reward Models and Choice Labelings are ignored!"); if (ma->isClosed() && ma->getMarkovianStates().full()) { storm::storage::sparse::ModelComponents components( @@ -69,7 +75,8 @@ namespace storm { entryIt != entryIte; ++entryIt) { uint_fast64_t predecessor = entryIt->getColumn(); if (!ma->isMarkovianState(predecessor) && !statesToKeep.count(predecessor)) { - if (!preserveLabels || currLabels == ma->getLabelsOfState(predecessor)) { + if (labelBehavior == EliminationLabelBehavior::DeleteLabels || labelBehavior == EliminationLabelBehavior::MergeLabels || + currLabels == ma->getLabelsOfState(predecessor)) { // If labels are not to be preserved or states are labeled the same if (!eliminationMapping.count(predecessor)) { eliminationMapping[predecessor] = base_state; @@ -111,7 +118,8 @@ namespace storm { entryIt != entryIte; ++entryIt) { uint_fast64_t predecessor = entryIt->getColumn(); if (!ma->isMarkovianState(predecessor) && !statesToKeep.count(predecessor)) { - if (!preserveLabels || currLabels == ma->getLabelsOfState(predecessor)) { + if (labelBehavior == EliminationLabelBehavior::DeleteLabels || labelBehavior == EliminationLabelBehavior::MergeLabels || + currLabels == ma->getLabelsOfState(predecessor)) { // If labels are not to be preserved or states are labeled the same if (!eliminationMapping.count(predecessor)) { eliminationMapping[predecessor] = base_state; @@ -146,6 +154,10 @@ namespace storm { // TODO explore if one can construct elimination mapping and state remapping in one step + uint64_t newStateCount = ma->getNumberOfStates() - eliminationMapping.size(); + + std::vector> labelMap(newStateCount, std::set()); + // Construct a mapping of old state space to new one std::vector stateRemapping(ma->getNumberOfStates(), -1); uint_fast64_t currentNewState = 0; @@ -159,14 +171,26 @@ namespace storm { } else { stateRemapping[state] = stateRemapping[eliminationMapping[state]]; } - } else if (stateRemapping[state] == uint_fast64_t(-1)) { - stateRemapping[state] = currentNewState; - queue.push(state); - ++currentNewState; + if (labelBehavior == EliminationLabelBehavior::MergeLabels) { + //add all labels to the label set for the representative + for (auto const &label : ma->getLabelsOfState(state)) { + labelMap[stateRemapping[eliminationMapping[state]]].insert(label); + } + } + } else { + if (stateRemapping[state] == uint_fast64_t(-1)) { + stateRemapping[state] = currentNewState; + queue.push(state); + ++currentNewState; + } + if (labelBehavior == EliminationLabelBehavior::MergeLabels) { + for (auto const &label : ma->getLabelsOfState(state)) { + labelMap[stateRemapping[state]].insert(label); + } + } } } - uint64_t newStateCount = ma->getNumberOfStates() - eliminationMapping.size(); // Build the new MA storm::storage::SparseMatrix newTransitionMatrix; storm::models::sparse::StateLabeling newStateLabeling( @@ -180,13 +204,24 @@ namespace storm { // Initialize the matrix builder and helper variables storm::storage::SparseMatrixBuilder matrixBuilder = storm::storage::SparseMatrixBuilder( 0, 0, 0, false, true, 0); + + for (auto const &label : ma->getStateLabeling()) { + if (!newStateLabeling.containsLabel(label)) { + newStateLabeling.addLabel(label); + } + } uint_fast64_t currentRow = 0; uint_fast64_t state = 0; while (!queue.empty()) { state = queue.front(); queue.pop(); - for (auto const &label : ma->getLabelsOfState(state)) { + std::set labelSet = ma->getLabelsOfState(state); + if (labelBehavior == EliminationLabelBehavior::MergeLabels) { + labelSet = labelMap[stateRemapping[state]]; + } + + for (auto const &label : labelSet) { if (!newStateLabeling.containsLabel(label)) { newStateLabeling.addLabel(label); } diff --git a/src/storm/transformer/NonMarkovianChainTransformer.h b/src/storm/transformer/NonMarkovianChainTransformer.h index 8382f7419..691fcc9ee 100644 --- a/src/storm/transformer/NonMarkovianChainTransformer.h +++ b/src/storm/transformer/NonMarkovianChainTransformer.h @@ -3,6 +3,12 @@ namespace storm { namespace transformer { + enum EliminationLabelBehavior { + KeepLabels, + MergeLabels, + DeleteLabels + }; + /** * Transformer for eliminating chains of non-Markovian states (instantaneous path fragment leading to the same outcome) from Markov automata. */ @@ -19,7 +25,8 @@ namespace storm { * @return A reference to the new model after eliminating non-Markovian states. */ static std::shared_ptr> eliminateNonmarkovianStates( - std::shared_ptr> ma, bool preserveLabels = true + std::shared_ptr> ma, + EliminationLabelBehavior labelBehavior = EliminationLabelBehavior::KeepLabels ); /**