sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Revised relevant events

tempestpy_adaptions
Matthias Volk 4 years ago
parent
4c7b069212
commit
a99be1bb06
No known key found for this signature in database GPG Key ID: 83A57678F739FCD3
11 changed files with 200 additions and 165 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 6
      src/storm-dft-cli/storm-dft.cpp
  2. 23
      src/storm-dft/api/storm-dft.h
  3. 4
      src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
  4. 44
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
  5. 34
      src/storm-dft/modelchecker/dft/DFTModelChecker.h
  6. 14
      src/storm-dft/storage/dft/DFT.cpp
  7. 11
      src/storm-dft/storage/dft/DFT.h
  8. 97
      src/storm-dft/utility/RelevantEvents.h
  9. 6
      src/test/storm-dft/api/DftApproximationTest.cpp
  10. 31
      src/test/storm-dft/api/DftModelBuildingTest.cpp
  11. 37
      src/test/storm-dft/api/DftModelCheckerTest.cpp

6
src/storm-dft-cli/storm-dft.cpp
View File

@ -171,7 +171,7 @@ void processOptions() {
// All events are relevant
additionalRelevantEventNames = {"all"};
}
std::set<size_t> relevantEvents = storm::api::computeRelevantEvents<ValueType>(*dft, props, additionalRelevantEventNames);
storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<ValueType>(*dft, props, additionalRelevantEventNames, faultTreeSettings.isAllowDCForRelevantEvents());
// Analyze DFT
@ -183,9 +183,7 @@ void processOptions() {
if (faultTreeSettings.isApproximationErrorSet()) {
approximationError = faultTreeSettings.getApproximationError();
}
storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents,
faultTreeSettings.isAllowDCForRelevantEvents(), approximationError, faultTreeSettings.getApproximationHeuristic(),
transformationSettings.isChainEliminationSet(), transformationSettings.getLabelBehavior(), true);
storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, approximationError, faultTreeSettings.getApproximationHeuristic(), transformationSettings.isChainEliminationSet(), transformationSettings.getLabelBehavior(), true);
}
}

23
src/storm-dft/api/storm-dft.h
View File

@ -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<typename ValueType>
std::set<size_t> computeRelevantEvents(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, std::vector<std::string> const additionalRelevantEventNames) {
std::vector<std::string> relevantNames = storm::utility::getRelevantEventNames<ValueType>(dft, properties);
relevantNames.insert(relevantNames.end(), additionalRelevantEventNames.begin(), additionalRelevantEventNames.end());
return storm::utility::getRelevantEvents<ValueType>(dft, relevantNames);
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, 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 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, std::set<size_t> const& relevantEvents = {}, bool allowDCForRelevantEvents = true, double approximationError = 0.0,
storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool eliminateChains = 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 = 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<ValueType> modelChecker(printOutput);
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents,
allowDCForRelevantEvents, approximationError, approximationHeuristic,
eliminateChains, labelBehavior);
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents, approximationError, approximationHeuristic, eliminateChains, labelBehavior);
if (printOutput) {
modelChecker.printTimings();
modelChecker.printResults(results);

4
src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
View File

@ -5,7 +5,6 @@
#include <storm/exceptions/IllegalArgumentException.h>
#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<storage::DFTElement<ValueType> 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;

44
src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
View File

@ -21,12 +21,10 @@ namespace storm {
namespace modelchecker {
template<typename ValueType>
typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::check(storm::storage::DFT<ValueType> const& origDft,
std::vector<std::shared_ptr<const storm::logic::Formula>> const& properties, bool symred,
bool allowModularisation, std::set<size_t> const& relevantEvents,
bool allowDCForRelevantEvents, double approximationError,
storm::builder::ApproximationHeuristic approximationHeuristic, bool eliminateChains,
storm::transformer::EliminationLabelBehavior labelBehavior) {
typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::check(storm::storage::DFT<ValueType> const& origDft, std::vector<std::shared_ptr<const storm::logic::Formula>> 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 ValueType>
typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::checkHelper(storm::storage::DFT<ValueType> const& dft, property_vector const& properties,
bool symred, bool allowModularisation, std::set<size_t> 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<storm::storage::DFT<ValueType>> dfts;
@ -118,8 +114,7 @@ namespace storm {
std::vector<ValueType> 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<ValueType>(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<typename ValueType>
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>>
DFTModelChecker<ValueType>::buildModelViaComposition(storm::storage::DFT<ValueType> const &dft,
property_vector const &properties, bool symred,
bool allowModularisation,
std::set<size_t> const &relevantEvents,
bool allowDCForRelevantEvents) {
DFTModelChecker<ValueType>::buildModelViaComposition(storm::storage::DFT<ValueType> 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<storm::storage::DFT<ValueType>> 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<size_t, std::vector<std::vector<size_t>>> 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<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
@ -299,17 +289,13 @@ namespace storm {
template<typename ValueType>
typename DFTModelChecker<ValueType>::dft_results
DFTModelChecker<ValueType>::checkDFT(storm::storage::DFT<ValueType> const &dft,
property_vector const &properties, bool symred,
std::set<size_t> const &relevantEvents, bool allowDCForRelevantEvents,
double approximationError,
storm::builder::ApproximationHeuristic approximationHeuristic,
bool eliminateChains, storm::transformer::EliminationLabelBehavior labelBehavior) {
DFTModelChecker<ValueType>::checkDFT(storm::storage::DFT<ValueType> 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<storm::settings::modules::IOSettings>();
auto dftIOSettings = storm::settings::getModule<storm::settings::modules::DftIOSettings>();
dft.setRelevantEvents(relevantEvents, allowDCForRelevantEvents);
dft.setRelevantEvents(relevantEvents);
// Find symmetries
std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;

34
src/storm-dft/modelchecker/dft/DFTModelChecker.h
View File

@ -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<ValueType> const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true,
std::set<size_t> const& relevantEvents = {}, bool allowDCForRelevantEvents = true, double approximationError = 0.0,
storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH,
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(),
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<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation,
std::set<size_t> 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<ValueType> 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<storm::models::sparse::Ctmc<ValueType>> buildModelViaComposition(storm::storage::DFT<ValueType> const& dft, property_vector const& properties,
bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents,
bool allowDCForRelevantEvents = true);
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> buildModelViaComposition(storm::storage::DFT<ValueType> 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<ValueType> const& dft, property_vector const& properties, bool symred, std::set<size_t> 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<ValueType> 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.

14
src/storm-dft/storage/dft/DFT.cpp
View File

@ -1025,6 +1025,11 @@ namespace storm {
return ids;
}
template<typename ValueType>
bool DFT<ValueType>::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<typename ValueType>
size_t DFT<ValueType>::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<typename ValueType>
void DFT<ValueType>::setRelevantEvents(std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents) const {
void DFT<ValueType>::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());

11
src/storm-dft/storage/dft/DFT.h
View File

@ -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<size_t> 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<size_t> const& relevantEvents, bool allowDCForRelevantEvents) const;
void setRelevantEvents(storm::utility::RelevantEvents const& relevantEvents) const;
/*!
* Get a string containing the list of all relevant events.

97
src/storm-dft/utility/RelevantEvents.h
View File

@ -1,27 +1,55 @@
#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 {
class RelevantEvents {
public:
/*!
* Get relevant event names from labels in properties.
* 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<std::string> 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 required by the 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 <typename ValueType>
std::vector<std::string> getRelevantEventNames(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties) {
void addNamesFromProperty(std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties) {
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);
}
// Add relevant event names from properties
std::vector<std::string> relevantEventNames;
for (auto atomic : atomicLabels) {
std::string label = atomic->getLabel();
if (label == "failed" or label == "skipped") {
@ -29,9 +57,9 @@ namespace storm {
} else {
// Get name of event
if (boost::ends_with(label, "_failed")) {
relevantEventNames.push_back(label.substr(0, label.size() - 7));
this->addEvent(label.substr(0, label.size() - 7));
} else if (boost::ends_with(label, "_dc")) {
relevantEventNames.push_back(label.substr(0, label.size() - 3));
this->addEvent(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 {
@ -39,31 +67,56 @@ namespace storm {
}
}
}
return relevantEventNames;
}
/*!
* Get relevant event id from relevant event name.
* Check that the relevant names correspond to existing elements in the DFT.
*
* @param dft DFT.
* @param relevantEventNames Names of relevant events.
* @return Set of relevant event ids.
* @return True iff relevant names are consistent with DFT elements.
*/
template <typename ValueType>
std::set<size_t> getRelevantEvents(storm::storage::DFT<ValueType> const& dft, std::vector<std::string> const& relevantEventNames) {
// Set relevant elements
std::set<size_t> 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 checkRelevantNames(storm::storage::DFT<ValueType> const& dft) const {
for (std::string const& relevantName : this->names) {
if (!dft.existsName(relevantName)) {
return false;
}
}
return true;
}
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<std::string> names;
// Whether all elements are relevant.
bool allRelevant;
// Whether to allow Don't Care propagation for relevant events.
bool allowDC;
};
} // namespace utility
} // namespace storm

6
src/test/storm-dft/api/DftApproximationTest.cpp
View File

@ -57,8 +57,7 @@ namespace {
EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
std::string property = "T=? [F \"failed\"]";
std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, false, {}, true, errorBound,
config.heuristic, false);
typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, false, storm::utility::RelevantEvents(), errorBound, config.heuristic, false);
return boost::get<storm::modelchecker::DFTModelChecker<double>::approximation_result>(results[0]);
}
@ -68,8 +67,7 @@ namespace {
std::stringstream propertyStream;
propertyStream << "P=? [F<=" << timeBound << " \"failed\"]";
std::vector <std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propertyStream.str()));
typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, false, {}, true, errorBound,
config.heuristic, false);
typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, false, storm::utility::RelevantEvents(), errorBound, config.heuristic, false);
return boost::get<storm::modelchecker::DFTModelChecker<double>::approximation_result>(results[0]);
}

31
src/test/storm-dft/api/DftModelBuildingTest.cpp
View File

@ -18,8 +18,8 @@ namespace {
storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
// Set relevant events (none)
std::set<size_t> relevantEvents;
dft->setRelevantEvents(relevantEvents, false);
storm::utility::RelevantEvents relevantEvents({}, false);
dft->setRelevantEvents(relevantEvents);
// Build model
storm::builder::ExplicitDFTModelBuilder<double> 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<double> 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<double> 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<double> 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<double> 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<double> 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<double> builder7(*dft, symmetries);
builder7.buildModel(0, 0.0);

37
src/test/storm-dft/api/DftModelCheckerTest.cpp
View File

@ -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<double> dftTransformator = storm::transformations::dft::DftTransformator<double>();
std::shared_ptr<storm::storage::DFT<double>> dft = dftTransformator.transformBinaryFDEPs(
*(storm::api::loadDFTGalileoFile<double>(file)));
std::shared_ptr<storm::storage::DFT<double>> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile<double>(file)));
EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
std::string property = "Tmin=? [F \"failed\"]";
std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
std::set<size_t> relevantEvents;
std::vector<std::string> relevantNames;
if (!config.useDC) {
relevantEvents = dft->getAllIds();
relevantNames.push_back("all");
}
typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod,
relevantEvents, config.allowDCForRelevantEvents);
storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<ValueType>(*dft, properties, relevantNames, false);
typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod, relevantEvents);
return boost::get<double>(results[0]);
}
@ -94,14 +94,15 @@ namespace {
std::shared_ptr<storm::storage::DFT<double>> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile<double>(file)));
EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
std::string property = "Pmin=? [F<=" + std::to_string(bound) + " \"failed\"]";
std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(
storm::api::parseProperties(property));
std::set<size_t> relevantEvents;
std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
std::vector<std::string> relevantNames;
if (!config.useDC) {
relevantEvents = dft->getAllIds();
relevantNames.push_back("all");
}
typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod,
relevantEvents, config.allowDCForRelevantEvents);
storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<ValueType>(*dft, properties, relevantNames, false);
typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod, relevantEvents);
return boost::get<double>(results[0]);
}

Write Preview
Loading…
Cancel
Save