diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 62df69b4c..619754ba1 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -184,56 +184,16 @@ void processOptions() { // Set relevant event names - std::vector relevantEventNames; - //Possible clash of relevantEvents and disableDC was already considered in FaultTreeSettings::check(). + std::vector additionalRelevantEventNames; if (faultTreeSettings.areRelevantEventsSet()) { - relevantEventNames = faultTreeSettings.getRelevantEvents(); + //Possible clash of relevantEvents and disableDC was already considered in FaultTreeSettings::check(). + additionalRelevantEventNames = faultTreeSettings.getRelevantEvents(); } else if (faultTreeSettings.isDisableDC()) { // All events are relevant - relevantEventNames = {"all"}; + additionalRelevantEventNames = {"all"}; } + std::set relevantEvents = storm::api::computeRelevantEvents(*dft, props, additionalRelevantEventNames); - // Events from properties are relevant as well - // Get necessary labels from properties - std::vector> atomicLabels; - for (auto property : props) { - 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 { - // 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(faultTreeSettings.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."); - } - } - } - - // Set relevant elements - std::set relevantEvents; // Per default no event (except the toplevel event) is relevant - for (std::string const& relevantName : relevantEventNames) { - if (relevantName == "none") { - // Only toplevel event is relevant - relevantEvents = {}; - break; - } else if (relevantName == "all") { - // All events are relevant - relevantEvents = dft->getAllIds(); - break; - } else { - // Find and add corresponding event id - relevantEvents.insert(dft->getIndex(relevantName)); - } - } // Analyze DFT // TODO allow building of state space even without properties diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index 22f7152ef..bfe90f37a 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -12,6 +12,7 @@ #include "storm-dft/transformations/DftTransformator.h" #include "storm-dft/utility/FDEPConflictFinder.h" #include "storm-dft/utility/FailureBoundFinder.h" +#include "storm-dft/utility/RelevantEvents.h" #include "storm-gspn/api/storm-gspn.h" @@ -117,6 +118,21 @@ namespace storm { return true; } + /*! + * Get relevant event ids from given relevant event names and labels in properties. + * + * @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. + */ + 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); + } + /*! * 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. diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.cpp b/src/storm-dft/settings/modules/FaultTreeSettings.cpp index a10ebc854..917c2e299 100644 --- a/src/storm-dft/settings/modules/FaultTreeSettings.cpp +++ b/src/storm-dft/settings/modules/FaultTreeSettings.cpp @@ -41,7 +41,7 @@ namespace storm { "Avoid non-determinism by always taking the first possible dependency.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, relevantEventsOptionName, false, "Specifies the relevant events from the DFT.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", - "A comma separated list of names of relevant events. 'all' marks all events as relevant, The default '' or 'none' marks only the top level event as relevant.").setDefaultValueString( + "A comma separated list of names of relevant events. 'all' marks all events as relevant, The default '' marks only the top level event as relevant.").setDefaultValueString( "").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, allowDCRelevantOptionName, false, "Allow Don't Care propagation for relevant events.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, addLabelsClaimingOptionName, false, diff --git a/src/storm-dft/utility/RelevantEvents.h b/src/storm-dft/utility/RelevantEvents.h new file mode 100644 index 000000000..127c0849c --- /dev/null +++ b/src/storm-dft/utility/RelevantEvents.h @@ -0,0 +1,69 @@ +#pragma once + +#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); + } + // 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."); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Label '" << label << "' not known."); + } + } + } + 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(); + } else { + // Find and add corresponding event id + relevantEvents.insert(dft.getIndex(relevantName)); + } + } + return relevantEvents; + } + + } // namespace utility +} // namespace storm \ No newline at end of file