Browse Source

Make RelevantEvents independent of std::vector

Instead use a flexible iterator based api
tempestpy_adaptions
Daniel Basgöze 4 years ago
committed by Matthias Volk
parent
commit
7cd2394078
  1. 6
      src/storm-dft/api/storm-dft.h
  2. 2
      src/storm-dft/modelchecker/dft/DFTModelChecker.h
  3. 100
      src/storm-dft/utility/RelevantEvents.h

6
src/storm-dft/api/storm-dft.h

@ -129,8 +129,8 @@ namespace storm {
*/
template<typename ValueType>
storm::utility::RelevantEvents computeRelevantEvents(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, std::vector<std::string> const& additionalRelevantEventNames) {
storm::utility::RelevantEvents events(additionalRelevantEventNames);
events.addNamesFromProperty(properties);
storm::utility::RelevantEvents events(additionalRelevantEventNames.begin(), additionalRelevantEventNames.end());
events.insertNamesFromProperties(properties.begin(), properties.end());
return events;
}
@ -153,7 +153,7 @@ namespace storm {
*/
template<typename ValueType>
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results
analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred = true, bool allowModularisation = true, storm::utility::RelevantEvents const& relevantEvents = storm::utility::RelevantEvents(), bool allowDCForRelevant = false,
analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred = true, bool allowModularisation = true, storm::utility::RelevantEvents const& relevantEvents = {}, bool allowDCForRelevant = false,
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<ValueType> modelChecker(printOutput);

2
src/storm-dft/modelchecker/dft/DFTModelChecker.h

@ -56,7 +56,7 @@ namespace storm {
* @return Model checking results for the given properties..
*/
dft_results check(storm::storage::DFT<ValueType> const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true,
storm::utility::RelevantEvents const& relevantEvents = storm::utility::RelevantEvents(), bool allowDCForRelevant = false,
storm::utility::RelevantEvents const& relevantEvents = {}, bool allowDCForRelevant = false,
double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH,
bool eliminateChains = false, storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels);

100
src/storm-dft/utility/RelevantEvents.h

@ -7,6 +7,7 @@
#include "storm-dft/storage/dft/DFT.h"
#include "storm-dft/settings/modules/FaultTreeSettings.h"
#include <initializer_list>
namespace storm {
namespace utility {
@ -15,19 +16,35 @@ namespace storm {
public:
/*!
* Create relevant events from given event names.
* Constructs empty RelevantEvents object
*/
RelevantEvents() = default;
/*!
* Create relevant events from given event names in an initializer list.
* If name 'all' occurs, all elements are stored as relevant.
*
* @param relevantEvents List of relevant event names.
* Allows syntactic sugar like:
* RelevantEvents e = {};
* and
* RelevantEvents e{"a"};
*
* @param init The initializer list.
*/
RelevantEvents(std::vector<std::string> const& relevantEvents = {}) {
// check if the name "all" occurs
if (std::any_of(relevantEvents.begin(), relevantEvents.end(),
[](auto const& name) { return name == "all"; })) {
this->allRelevant = true;
} else {
this->names.insert(relevantEvents.begin(), relevantEvents.end());
}
RelevantEvents(std::initializer_list<std::string> init) {
insert(init.begin(), init.end());
}
/*!
* Create relevant events from given event names in a range.
* If name 'all' occurs, all elements are stored as relevant.
*
* @param first Iterator pointing to the start of a range of names.
* @param last Iterator pointing to the end of a range of names.
*/
template <typename ForwardIt>
RelevantEvents(ForwardIt first, ForwardIt last) {
insert(first, last);
}
bool operator==(RelevantEvents const& rhs) {
@ -39,23 +56,25 @@ namespace storm {
}
/*!
* Add relevant event names required by the labels in properties.
* Add relevant event names required by the labels in properties of a range.
*
* @param properties List of properties. All events occurring in a property are relevant.
* @param first Iterator pointing to the start of a std::shared_ptr<storm::logic::Formula const> range.
* @param last Iterator pointing to the end of a std::shared_ptr<storm::logic::Formula const> range.
*/
void addNamesFromProperty(std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties) {
template <typename ForwardIt>
void insertNamesFromProperties(ForwardIt first, ForwardIt last) {
if (this->allRelevant) {
return;
}
// Get necessary labels from properties
std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabels;
for (auto property : properties) {
property->gatherAtomicLabelFormulas(atomicLabels);
}
std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabels{};
std::for_each(first, last, [&atomicLabels](auto const& property){
property->gatherAtomicLabelFormulas(atomicLabels);
});
// Add relevant event names from properties
for (auto atomic : atomicLabels) {
for (auto const& atomic : atomicLabels) {
std::string label = atomic->getLabel();
if (label == "failed" or label == "skipped") {
// Ignore as these label will always be added if necessary
@ -63,10 +82,10 @@ namespace storm {
// Get name of event
if (boost::ends_with(label, "_failed")) {
// length of "_failed" = 7
this->addEvent(label.substr(0, label.size() - 7));
this->names.insert(label.substr(0, label.size() - 7));
} else if (boost::ends_with(label, "_dc")) {
// length of "_dc" = 3
this->addEvent(label.substr(0, label.size() - 3));
this->names.insert(label.substr(0, label.size() - 3));
} else if (label.find("_claimed_") != std::string::npos) {
STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().isAddLabelsClaiming(), storm::exceptions::InvalidArgumentException, "Claiming labels will not be exported but are required for label '" << label << "'. Try setting --labels-claiming.");
} else {
@ -76,6 +95,36 @@ namespace storm {
}
}
/*!
* Add relevant event.
* If name 'all' occurs, all elements are stored as relevant.
*
* @param name Name of relevant event.
*/
void insert(std::string const& name) {
if(name == "all") {
setAllRelevant();
}
names.insert(name);
}
/*!
* Add relevant event names from a range.
* If name 'all' occurs, all elements are stored as relevant.
*
* @param first Iterator pointing to the start of a range of names.
* @param last Iterator pointing to the end of a range of names.
*/
template <typename ForwardIt>
void insert(ForwardIt first, ForwardIt last) {
// check if the name "all" occurs
if (std::any_of(first, last, [](auto const& name) { return name == "all"; })) {
setAllRelevant();
} else {
this->names.insert(first, last);
}
}
/*!
* Check that the relevant names correspond to existing elements in the DFT.
*
@ -104,14 +153,9 @@ namespace storm {
}
private:
/*!
* Add relevant event.
*
* @param name Name of relevant event.
*/
void addEvent(std::string const& name) {
names.insert(name);
void setAllRelevant() {
this->allRelevant = true;
this->names.clear();
}
// Names of relevant events.

Loading…
Cancel
Save