diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 9a2546eae..0a2d172d8 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -171,7 +171,7 @@ void processOptions() { // All events are relevant additionalRelevantEventNames = {"all"}; } - std::set relevantEvents = storm::api::computeRelevantEvents(*dft, props, additionalRelevantEventNames); + storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents(*dft, props, additionalRelevantEventNames, faultTreeSettings.isAllowDCForRelevantEvents()); // Analyze DFT @@ -183,9 +183,7 @@ void processOptions() { if (faultTreeSettings.isApproximationErrorSet()) { approximationError = faultTreeSettings.getApproximationError(); } - storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, - faultTreeSettings.isAllowDCForRelevantEvents(), approximationError, faultTreeSettings.getApproximationHeuristic(), - transformationSettings.isChainEliminationSet(), transformationSettings.getLabelBehavior(), true); + storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, approximationError, faultTreeSettings.getApproximationHeuristic(), transformationSettings.isChainEliminationSet(), transformationSettings.getLabelBehavior(), true); } } diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index a14d7d2c7..0535cf280 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -125,13 +125,14 @@ namespace storm { * @param dft DFT. * @param properties List of properties. All events occurring in a property are relevant. * @param additionalRelevantEventNames List of names of additional relevant events. - * @return Set of relevant event ids. + * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events. + * @return Relevant events. */ template - std::set computeRelevantEvents(storm::storage::DFT const& dft, std::vector> const& properties, std::vector const additionalRelevantEventNames) { - std::vector relevantNames = storm::utility::getRelevantEventNames(dft, properties); - relevantNames.insert(relevantNames.end(), additionalRelevantEventNames.begin(), additionalRelevantEventNames.end()); - return storm::utility::getRelevantEvents(dft, relevantNames); + storm::utility::RelevantEvents computeRelevantEvents(storm::storage::DFT const& dft, std::vector> const& properties, std::vector const& additionalRelevantEventNames, bool allowDCForRelevant) { + storm::utility::RelevantEvents events(additionalRelevantEventNames, allowDCForRelevant); + events.addNamesFromProperty(properties); + return events; } /*! @@ -142,8 +143,7 @@ namespace storm { * @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 relevantEvents List of relevant events which should be observed. - * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events. + * @param relevantEvents Relevant events which should be observed. * @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. @@ -153,14 +153,11 @@ namespace storm { */ template 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, + analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred = true, bool allowModularisation = true, storm::utility::RelevantEvents const& relevantEvents = storm::utility::RelevantEvents(), + double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool eliminateChains = 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, labelBehavior); + typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents, approximationError, approximationHeuristic, eliminateChains, labelBehavior); if (printOutput) { modelChecker.printTimings(); modelChecker.printResults(results); diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index 956805544..13628a7ff 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -5,7 +5,6 @@ #include #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/UnexpectedException.h" -#include "storm/logic/AtomicLabelFormula.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/Ctmc.h" #include "storm/utility/bitoperations.h" @@ -530,6 +529,9 @@ namespace storm { if (this->uniqueFailedState) { // Unique failed state has label 0 modelComponents.stateLabeling.addLabelToState("failed", 0); + std::shared_ptr const> element = dft.getElement(dft.getTopLevelIndex()); + STORM_LOG_ASSERT(element->isRelevant(), "TLE should be relevant if unique failed state is used."); + modelComponents.stateLabeling.addLabelToState(element->name() + "_failed", 0); } for (auto const& stateIdPair : stateStorage.stateToId) { storm::storage::BitVector state = stateIdPair.first; diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index fb52401d6..503f05207 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -21,12 +21,10 @@ namespace storm { namespace modelchecker { template - typename DFTModelChecker::dft_results DFTModelChecker::check(storm::storage::DFT const& origDft, - std::vector> const& properties, bool symred, - bool allowModularisation, std::set const& relevantEvents, - bool allowDCForRelevantEvents, double approximationError, - storm::builder::ApproximationHeuristic approximationHeuristic, bool eliminateChains, - storm::transformer::EliminationLabelBehavior labelBehavior) { + typename DFTModelChecker::dft_results DFTModelChecker::check(storm::storage::DFT const& origDft, std::vector> const& properties, + bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents, + double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic, + bool eliminateChains, storm::transformer::EliminationLabelBehavior labelBehavior) { totalTimer.start(); dft_results results; @@ -50,8 +48,7 @@ namespace storm { results.push_back(result); } } else { - results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevantEvents, approximationError, approximationHeuristic, - eliminateChains, labelBehavior); + results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, approximationError, approximationHeuristic, eliminateChains, labelBehavior); } totalTimer.stop(); return results; @@ -59,9 +56,8 @@ namespace storm { template typename DFTModelChecker::dft_results DFTModelChecker::checkHelper(storm::storage::DFT const& dft, property_vector const& properties, - bool symred, bool allowModularisation, std::set const& relevantEvents, - bool allowDCForRelevantEvents, double approximationError, - storm::builder::ApproximationHeuristic approximationHeuristic, + bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents, + double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic, bool eliminateChains, storm::transformer::EliminationLabelBehavior labelBehavior) { STORM_LOG_TRACE("Check helper called"); std::vector> dfts; @@ -118,8 +114,7 @@ namespace storm { std::vector res; for (auto const ft : dfts) { // TODO: allow approximation in modularisation - dft_results ftResults = checkHelper(ft, {property}, symred, true, relevantEvents, - allowDCForRelevantEvents, 0.0); + dft_results ftResults = checkHelper(ft, {property}, symred, true, relevantEvents, 0.0); STORM_LOG_ASSERT(ftResults.size() == 1, "Wrong number of results"); res.push_back(boost::get(ftResults[0])); } @@ -157,18 +152,13 @@ namespace storm { return results; } else { // No modularisation was possible - return checkDFT(dft, properties, symred, relevantEvents, allowDCForRelevantEvents, approximationError, - approximationHeuristic, eliminateChains, labelBehavior); + return checkDFT(dft, properties, symred, relevantEvents, approximationError, approximationHeuristic, eliminateChains, labelBehavior); } } template std::shared_ptr> - DFTModelChecker::buildModelViaComposition(storm::storage::DFT const &dft, - property_vector const &properties, bool symred, - bool allowModularisation, - std::set const &relevantEvents, - bool allowDCForRelevantEvents) { + DFTModelChecker::buildModelViaComposition(storm::storage::DFT const &dft, property_vector const &properties, bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents) { // TODO: use approximation? STORM_LOG_TRACE("Build model via composition"); std::vector> dfts; @@ -207,7 +197,7 @@ namespace storm { STORM_LOG_DEBUG("Building Model via parallel composition..."); explorationTimer.start(); - ft.setRelevantEvents(relevantEvents, allowDCForRelevantEvents); + ft.setRelevantEvents(relevantEvents); // Find symmetries std::map>> emptySymmetry; storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); @@ -269,7 +259,7 @@ namespace storm { // No composition was possible explorationTimer.start(); - dft.setRelevantEvents(relevantEvents, allowDCForRelevantEvents); + dft.setRelevantEvents(relevantEvents); // Find symmetries std::map>> emptySymmetry; @@ -299,17 +289,13 @@ namespace storm { template typename DFTModelChecker::dft_results - DFTModelChecker::checkDFT(storm::storage::DFT const &dft, - property_vector const &properties, bool symred, - std::set const &relevantEvents, bool allowDCForRelevantEvents, - double approximationError, - storm::builder::ApproximationHeuristic approximationHeuristic, - bool eliminateChains, storm::transformer::EliminationLabelBehavior labelBehavior) { + DFTModelChecker::checkDFT(storm::storage::DFT const &dft, property_vector const &properties, bool symred, storm::utility::RelevantEvents const& relevantEvents, + double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic, bool eliminateChains, storm::transformer::EliminationLabelBehavior labelBehavior) { explorationTimer.start(); auto ioSettings = storm::settings::getModule(); auto dftIOSettings = storm::settings::getModule(); - dft.setRelevantEvents(relevantEvents, allowDCForRelevantEvents); + dft.setRelevantEvents(relevantEvents); // Find symmetries std::map>> emptySymmetry; diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h index 068481998..4c61655fa 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -6,6 +6,7 @@ #include "storm/utility/Stopwatch.h" #include "storm-dft/storage/dft/DFT.h" +#include "storm-dft/utility/RelevantEvents.h" namespace storm { @@ -46,17 +47,15 @@ namespace storm { * @param properties Properties to check for. * @param symred Flag whether symmetry reduction should be used. * @param allowModularisation Flag indicating if modularisation is allowed. - * @param relevantEvents List with ids of relevant events which should be observed. - * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events. + * @param relevantEvents Relevant events which should be observed. * @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 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, + dft_results check(storm::storage::DFT const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true, storm::utility::RelevantEvents const& relevantEvents = storm::utility::RelevantEvents(), + double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool eliminateChains = false, storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels); /*! @@ -92,19 +91,16 @@ namespace storm { * @param properties Properties to check for. * @param symred Flag indicating if symmetry reduction should be used. * @param allowModularisation Flag indicating if modularisation is allowed. - * @param relevantEvents List with ids of relevant events which should be observed. - * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events. + * @param relevantEvents Relevant events which should be observed. * @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 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, - storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels); + dft_results checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents, + double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, + bool eliminateChains = false, storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels); /*! * Internal helper for building a CTMC from a DFT via parallel composition. @@ -114,12 +110,9 @@ namespace storm { * @param symred Flag indicating if symmetry reduction should be used. * @param allowModularisation Flag indicating if modularisation is allowed. * @param relevantEvents List with ids of relevant events which should be observed. - * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events. * @return CTMC representing the DFT */ - std::shared_ptr> buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, - bool symred, bool allowModularisation, std::set const& relevantEvents, - bool allowDCForRelevantEvents = true); + std::shared_ptr> buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents); /*! * Check model generated from DFT. @@ -128,7 +121,6 @@ namespace storm { * @param properties Properties to check for. * @param symred Flag indicating if symmetry reduction should be used. * @param relevantEvents List with ids of relevant events which should be observed. - * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events. * @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 @@ -136,11 +128,9 @@ namespace storm { * * @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, - storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels); + dft_results checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, storm::utility::RelevantEvents const& relevantEvents, + double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, + 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-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 570ba9fa5..86a99290c 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -1025,6 +1025,11 @@ namespace storm { return ids; } + template + bool DFT::existsName(std::string const& name) const { + return std::find_if(mElements.begin(), mElements.end(), [&name](DFTElementPointer const& e) { return e->name() == name; }) != mElements.end(); + } + template size_t DFT::getIndex(std::string const& name) const { auto iter = std::find_if(mElements.begin(), mElements.end(), [&name](DFTElementPointer const& e) { return e->name() == name; }); @@ -1033,14 +1038,15 @@ namespace storm { } template - void DFT::setRelevantEvents(std::set const& relevantEvents, bool allowDCForRelevantEvents) const { + void DFT::setRelevantEvents(storm::utility::RelevantEvents const& relevantEvents) const { mRelevantEvents.clear(); + STORM_LOG_THROW(relevantEvents.checkRelevantNames(*this), storm::exceptions::InvalidArgumentException, "One of the relevant elements does not exist."); // Top level element is first element mRelevantEvents.push_back(this->getTopLevelIndex()); - for (auto const& elem : mElements) { - if (relevantEvents.find(elem->id()) != relevantEvents.end() || elem->id() == this->getTopLevelIndex()) { + for (auto& elem : mElements) { + if (relevantEvents.isRelevant(elem->name()) || elem->id() == this->getTopLevelIndex()) { elem->setRelevance(true); - elem->setAllowDC(allowDCForRelevantEvents); + elem->setAllowDC(relevantEvents.isAllowDC()); if (elem->id() != this->getTopLevelIndex()) { // Top level element was already added mRelevantEvents.push_back(elem->id()); diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index 9f5ecdea4..f089c8ae5 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -17,6 +17,7 @@ #include "storm-dft/storage/dft/SymmetricUnits.h" #include "storm-dft/storage/dft/DFTStateGenerationInfo.h" #include "storm-dft/storage/dft/DFTLayoutInfo.h" +#include "storm-dft/utility/RelevantEvents.h" namespace storm { namespace builder { @@ -352,6 +353,13 @@ namespace storm { */ std::set getAllIds() const; + /*! + * Check whether an element with the given name exists. + * @param name Name of element. + * @return True iff element with given name exists. + */ + bool existsName(std::string const& name) const; + /*! * Get id for the given element name. * @param name Name of element. @@ -368,9 +376,8 @@ namespace storm { /*! * Set the relevance flag for all elements according to the given relevant events. * @param relevantEvents All elements which should be to relevant. All elements not occurring are set to irrelevant. - * @param allowDCForRelevantEvents Flag whether Don't Care propagation is allowed even for relevant events. */ - void setRelevantEvents(std::set const& relevantEvents, bool allowDCForRelevantEvents) const; + void setRelevantEvents(storm::utility::RelevantEvents const& relevantEvents) const; /*! * Get a string containing the list of all relevant events. diff --git a/src/storm-dft/utility/RelevantEvents.h b/src/storm-dft/utility/RelevantEvents.h index 127c0849c..f32f348c8 100644 --- a/src/storm-dft/utility/RelevantEvents.h +++ b/src/storm-dft/utility/RelevantEvents.h @@ -1,69 +1,122 @@ #pragma once +#include "storm/exceptions/InvalidArgumentException.h" +#include "storm/logic/AtomicLabelFormula.h" +#include "storm/logic/Formula.h" +#include "storm/settings/SettingsManager.h" + #include "storm-dft/storage/dft/DFT.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" namespace storm { namespace utility { - /*! - * Get relevant event names from labels in properties. - * - * @param dft DFT. - * @param properties List of properties. All events occurring in a property are relevant. - * @return List of relevant event names. - */ - template - std::vector getRelevantEventNames(storm::storage::DFT const& dft, std::vector> const& properties) { - // Get necessary labels from properties - std::vector> atomicLabels; - for (auto property : properties) { - property->gatherAtomicLabelFormulas(atomicLabels); + class RelevantEvents { + public: + + /*! + * Create relevant events from given event names. + * If name 'all' occurs, all elements are stored as relevant. + * + * @param relevantEvents List of relevant event names. + * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events. + */ + RelevantEvents(std::vector const& relevantEvents = {}, bool allowDCForRelevant = false) : names(), allRelevant(false), allowDC(allowDCForRelevant) { + for (auto const& name: relevantEvents) { + if (name == "all") { + this->allRelevant = true; + this->names.clear(); + break; + } else { + this->addEvent(name); + } + } } - // Add relevant event names from properties - std::vector relevantEventNames; - for (auto atomic : atomicLabels) { - std::string label = atomic->getLabel(); - if (label == "failed" or label == "skipped") { - // Ignore as these label will always be added if necessary - } else { - // Get name of event - if (boost::ends_with(label, "_failed")) { - relevantEventNames.push_back(label.substr(0, label.size() - 7)); - } else if (boost::ends_with(label, "_dc")) { - relevantEventNames.push_back(label.substr(0, label.size() - 3)); - } else if (label.find("_claimed_") != std::string::npos) { - STORM_LOG_THROW(storm::settings::getModule().isAddLabelsClaiming(), storm::exceptions::InvalidArgumentException, "Claiming labels will not be exported but are required for label '" << label << "'. Try setting --labels-claiming."); + + /*! + * Add relevant event names required by the labels in properties. + * + * @param properties List of properties. All events occurring in a property are relevant. + */ + void addNamesFromProperty(std::vector> const& properties) { + if (this->allRelevant) { + return; + } + + // Get necessary labels from properties + std::vector> atomicLabels; + for (auto property : properties) { + property->gatherAtomicLabelFormulas(atomicLabels); + } + + // Add relevant event names from properties + for (auto atomic : atomicLabels) { + std::string label = atomic->getLabel(); + if (label == "failed" or label == "skipped") { + // Ignore as these label will always be added if necessary } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Label '" << label << "' not known."); + // Get name of event + if (boost::ends_with(label, "_failed")) { + this->addEvent(label.substr(0, label.size() - 7)); + } else if (boost::ends_with(label, "_dc")) { + this->addEvent(label.substr(0, label.size() - 3)); + } else if (label.find("_claimed_") != std::string::npos) { + STORM_LOG_THROW(storm::settings::getModule().isAddLabelsClaiming(), storm::exceptions::InvalidArgumentException, "Claiming labels will not be exported but are required for label '" << label << "'. Try setting --labels-claiming."); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Label '" << label << "' not known."); + } + } + } + } + + /*! + * Check that the relevant names correspond to existing elements in the DFT. + * + * @param dft DFT. + * @return True iff relevant names are consistent with DFT elements. + */ + template + bool checkRelevantNames(storm::storage::DFT const& dft) const { + for (std::string const& relevantName : this->names) { + if (!dft.existsName(relevantName)) { + return false; } } + return true; } - return relevantEventNames; - } - - /*! - * Get relevant event id from relevant event name. - * - * @param dft DFT. - * @param relevantEventNames Names of relevant events. - * @return Set of relevant event ids. - */ - template - std::set getRelevantEvents(storm::storage::DFT const& dft, std::vector const& relevantEventNames) { - // Set relevant elements - std::set relevantEvents; // Per default no event (except the toplevel event) is relevant - for (std::string const& relevantName : relevantEventNames) { - if (relevantName == "all") { - // All events are relevant - return dft.getAllIds(); + + bool isRelevant(std::string const& name) const { + if (this->allRelevant) { + return true; } else { - // Find and add corresponding event id - relevantEvents.insert(dft.getIndex(relevantName)); + return this->names.find(name) != this->names.end(); } } - return relevantEvents; - } + + bool isAllowDC() const { + return this->allowDC; + } + + private: + + /*! + * Add relevant event. + * + * @param name Name of relevant event. + */ + void addEvent(std::string const& name) { + names.insert(name); + } + + // Names of relevant events. + std::set names; + + // Whether all elements are relevant. + bool allRelevant; + + // Whether to allow Don't Care propagation for relevant events. + bool allowDC; + }; } // namespace utility -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/test/storm-dft/api/DftApproximationTest.cpp b/src/test/storm-dft/api/DftApproximationTest.cpp index ee59b9a15..70778c653 100644 --- a/src/test/storm-dft/api/DftApproximationTest.cpp +++ b/src/test/storm-dft/api/DftApproximationTest.cpp @@ -57,8 +57,7 @@ namespace { EXPECT_TRUE(storm::api::isWellFormed(*dft).first); std::string property = "T=? [F \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); - typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, false, {}, true, errorBound, - config.heuristic, false); + typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, false, storm::utility::RelevantEvents(), errorBound, config.heuristic, false); return boost::get::approximation_result>(results[0]); } @@ -68,8 +67,7 @@ namespace { std::stringstream propertyStream; propertyStream << "P=? [F<=" << timeBound << " \"failed\"]"; std::vector > properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propertyStream.str())); - typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, false, {}, true, errorBound, - config.heuristic, false); + typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, false, storm::utility::RelevantEvents(), errorBound, config.heuristic, false); return boost::get::approximation_result>(results[0]); } diff --git a/src/test/storm-dft/api/DftModelBuildingTest.cpp b/src/test/storm-dft/api/DftModelBuildingTest.cpp index 7837fe793..71c6351e1 100644 --- a/src/test/storm-dft/api/DftModelBuildingTest.cpp +++ b/src/test/storm-dft/api/DftModelBuildingTest.cpp @@ -18,8 +18,8 @@ namespace { storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); // Set relevant events (none) - std::set relevantEvents; - dft->setRelevantEvents(relevantEvents, false); + storm::utility::RelevantEvents relevantEvents({}, false); + dft->setRelevantEvents(relevantEvents); // Build model storm::builder::ExplicitDFTModelBuilder builder(*dft, symmetries); builder.buildModel(0, 0.0); @@ -28,7 +28,8 @@ namespace { EXPECT_EQ(13ul, model->getNumberOfTransitions()); // Set relevant events (all) - dft->setRelevantEvents(dft->getAllIds(), false); + relevantEvents = storm::utility::RelevantEvents({"all"}, false); + dft->setRelevantEvents(relevantEvents); // Build model storm::builder::ExplicitDFTModelBuilder builder2(*dft, symmetries); builder2.buildModel(0, 0.0); @@ -37,9 +38,8 @@ namespace { EXPECT_EQ(2305ul, model->getNumberOfTransitions()); // Set relevant events (H) - relevantEvents.clear(); - relevantEvents.insert(dft->getIndex("H")); - dft->setRelevantEvents(relevantEvents, false); + relevantEvents = storm::utility::RelevantEvents({"H"}, false); + dft->setRelevantEvents(relevantEvents); // Build model storm::builder::ExplicitDFTModelBuilder builder3(*dft, symmetries); builder3.buildModel(0, 0.0); @@ -49,10 +49,8 @@ namespace { // Set relevant events (H, I) - relevantEvents.clear(); - relevantEvents.insert(dft->getIndex("H")); - relevantEvents.insert(dft->getIndex("I")); - dft->setRelevantEvents(relevantEvents, false); + relevantEvents = storm::utility::RelevantEvents({"H", "I"}, false); + dft->setRelevantEvents(relevantEvents); // Build model storm::builder::ExplicitDFTModelBuilder builder4(*dft, symmetries); builder4.buildModel(0, 0.0); @@ -61,8 +59,8 @@ namespace { EXPECT_EQ(33ul, model->getNumberOfTransitions()); // Set relevant events (none) - relevantEvents.clear(); - dft->setRelevantEvents(relevantEvents, true); + relevantEvents = storm::utility::RelevantEvents({}, true); + dft->setRelevantEvents(relevantEvents); // Build model storm::builder::ExplicitDFTModelBuilder builder5(*dft, symmetries); builder5.buildModel(0, 0.0); @@ -71,7 +69,8 @@ namespace { EXPECT_EQ(13ul, model->getNumberOfTransitions()); // Set relevant events (all) - dft->setRelevantEvents(dft->getAllIds(), true); + relevantEvents = storm::utility::RelevantEvents({"all"}, true); + dft->setRelevantEvents(relevantEvents); // Build model storm::builder::ExplicitDFTModelBuilder builder6(*dft, symmetries); builder6.buildModel(0, 0.0); @@ -81,10 +80,8 @@ namespace { // Set relevant events (H, I) - relevantEvents.clear(); - relevantEvents.insert(dft->getIndex("H")); - relevantEvents.insert(dft->getIndex("I")); - dft->setRelevantEvents(relevantEvents, true); + relevantEvents = storm::utility::RelevantEvents({"H", "I"}, true); + dft->setRelevantEvents(relevantEvents); // Build model storm::builder::ExplicitDFTModelBuilder builder7(*dft, symmetries); builder7.buildModel(0, 0.0); diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index 94d6f0775..be93bbf2c 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -12,7 +12,6 @@ namespace { bool useSR; bool useMod; bool useDC; - bool allowDCForRelevantEvents; }; class NoOptimizationsConfig { @@ -20,7 +19,7 @@ namespace { typedef double ValueType; static DftAnalysisConfig createConfig() { - return DftAnalysisConfig{false, false, false, true}; + return DftAnalysisConfig{false, false, false}; } }; @@ -29,7 +28,7 @@ namespace { typedef double ValueType; static DftAnalysisConfig createConfig() { - return DftAnalysisConfig{false, false, true, true}; + return DftAnalysisConfig{false, false, true}; } }; @@ -38,7 +37,7 @@ namespace { typedef double ValueType; static DftAnalysisConfig createConfig() { - return DftAnalysisConfig{false, true, false, true}; + return DftAnalysisConfig{false, true, false}; } }; @@ -47,7 +46,7 @@ namespace { typedef double ValueType; static DftAnalysisConfig createConfig() { - return DftAnalysisConfig{true, false, false, true}; + return DftAnalysisConfig{true, false, false}; } }; @@ -56,7 +55,7 @@ namespace { typedef double ValueType; static DftAnalysisConfig createConfig() { - return DftAnalysisConfig{true, true, true, true}; + return DftAnalysisConfig{true, true, true}; } }; @@ -75,17 +74,18 @@ namespace { double analyzeMTTF(std::string const& file) { storm::transformations::dft::DftTransformator dftTransformator = storm::transformations::dft::DftTransformator(); - std::shared_ptr> dft = dftTransformator.transformBinaryFDEPs( - *(storm::api::loadDFTGalileoFile(file))); + std::shared_ptr> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile(file))); EXPECT_TRUE(storm::api::isWellFormed(*dft).first); std::string property = "Tmin=? [F \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); - std::set relevantEvents; + + std::vector relevantNames; if (!config.useDC) { - relevantEvents = dft->getAllIds(); + relevantNames.push_back("all"); } - typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, config.useMod, - relevantEvents, config.allowDCForRelevantEvents); + 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]); } @@ -94,14 +94,15 @@ namespace { 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::set relevantEvents; + std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); + + std::vector relevantNames; if (!config.useDC) { - relevantEvents = dft->getAllIds(); + relevantNames.push_back("all"); } - typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, config.useMod, - relevantEvents, config.allowDCForRelevantEvents); + 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]); }