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

Started on the notion of 'relevant events' for DFT analysis

tempestpy_adaptions
Matthias Volk 6 years ago
parent
26366e43cf
commit
99651bdc71
14 changed files with 198 additions and 111 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. 34
      src/storm-dft-cli/storm-dft.cpp
  2. 49
      src/storm-dft/api/storm-dft.h
  3. 6
      src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
  4. 8
      src/storm-dft/builder/ExplicitDFTModelBuilder.h
  5. 4
      src/storm-dft/generator/DftNextStateGenerator.cpp
  6. 6
      src/storm-dft/generator/DftNextStateGenerator.h
  7. 24
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
  8. 25
      src/storm-dft/modelchecker/dft/DFTModelChecker.h
  9. 25
      src/storm-dft/settings/modules/FaultTreeSettings.cpp
  10. 28
      src/storm-dft/settings/modules/FaultTreeSettings.h
  11. 16
      src/storm-dft/storage/dft/DFT.cpp
  12. 13
      src/storm-dft/storage/dft/DFT.h
  13. 19
      src/test/storm-dft/api/DftApproximationTest.cpp
  14. 52
      src/test/storm-dft/api/DftModelCheckerTest.cpp

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

@ -120,16 +120,38 @@ void processOptions() {
propString += ";" + properties[i];
}
std::vector<std::shared_ptr<storm::logic::Formula const>> props = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propString));
STORM_LOG_ASSERT(props.size() > 0, "No properties found.");
// Set relevant elements
// TODO: also incorporate events from properties
std::set<size_t> relevantEvents; // Per default only the toplevel event is relevant
// Possible clash of relevantEvents and disableDC was already considered in FaultTreeSettings::check().
if (faultTreeSettings.areRelevantEventsSet()) {
for (std::string const& relevantName : faultTreeSettings.getRelevantEvents()) {
if (relevantName == "none") {
// Only toplevel event is relevant
relevantEvents = {};
break;
} else if (relevantName == "all") {
// All events are relevant
relevantEvents = dft->getAllIds();
break;
} else {
// Find corresponding id
relevantEvents.insert(dft->getIndex(relevantName));
}
}
} else if (faultTreeSettings.isDisableDC()) {
// All events are relevant
relevantEvents = dft->getAllIds();
}
// Carry out the actual analysis
double approximationError = 0.0;
if (faultTreeSettings.isApproximationErrorSet()) {
// Approximate analysis
storm::api::analyzeDFTApprox<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(),
faultTreeSettings.getApproximationError(), faultTreeSettings.getApproximationHeuristic(), true);
} else {
storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), true);
approximationError = faultTreeSettings.getApproximationError();
}
storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, approximationError,
faultTreeSettings.getApproximationHeuristic(), true);
}
/*!

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

@ -53,57 +53,40 @@ namespace storm {
return std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJsonFromFile(file));
}
template<typename ValueType>
bool isWellFormed(storm::storage::DFT<ValueType> const& dft) {
std::stringstream stream;
return dft.checkWellFormedness(stream);
}
/*!
* Analyse 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.
* Check whether the DFT is well-formed.
*
* @param dft DFT.
* @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 enableDC Flag whether Don't Care propagation should be used.
*
* @return Result.
* @return True iff the DFT is well-formed.
*/
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, bool allowModularisation,
bool enableDC, bool printOutput) {
storm::modelchecker::DFTModelChecker<ValueType> modelChecker(printOutput);
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, 0.0);
if (printOutput) {
modelChecker.printTimings();
modelChecker.printResults(results);
}
return results;
bool isWellFormed(storm::storage::DFT<ValueType> const& dft) {
std::stringstream stream;
return dft.checkWellFormedness(stream);
}
/*!
* Approximate the analysis result of the given DFT according to the given properties.
* 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.
*
* @param dft DFT.
* @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 enableDC Flag whether Don't Care propagation should be used.
* @param approximationError Allowed approximation error.
*
* @return Result.
* @param relevantEvents List of 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 printOutput If true, model information, timings, results, etc. are printed.
* @return Results.
*/
template<typename ValueType>
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results
analyzeDFTApprox(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred,
bool allowModularisation, bool enableDC, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic, bool printOutput) {
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 = {}, double approximationError = 0.0,
storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool printOutput = false) {
storm::modelchecker::DFTModelChecker<ValueType> modelChecker(printOutput);
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, approximationError, approximationHeuristic);
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents,
approximationError, approximationHeuristic);
if (printOutput) {
modelChecker.printTimings();
modelChecker.printResults(results);

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

@ -54,11 +54,11 @@ namespace storm {
}
template<typename ValueType, typename StateType>
ExplicitDFTModelBuilder<ValueType, StateType>::ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) :
ExplicitDFTModelBuilder<ValueType, StateType>::ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, std::set<size_t> const& relevantEvents) :
dft(dft),
stateGenerationInfo(std::make_shared<storm::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries))),
enableDC(enableDC),
generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates),
relevantEvents(relevantEvents),
generator(dft, *stateGenerationInfo, relevantEvents, mergeFailedStates),
matrixBuilder(!generator.isDeterministicModel()),
stateStorage(dft.stateBitVectorSize()),
explorationQueue(1, 0, 0.9, false)

8
src/storm-dft/builder/ExplicitDFTModelBuilder.h
View File

@ -174,9 +174,9 @@ namespace storm {
*
* @param dft DFT.
* @param symmetries Symmetries in the dft.
* @param enableDC Flag indicating if dont care propagation should be used.
* @param relevantEvents List with ids of relevant events which should be observed.
*/
ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC);
ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, std::set<size_t> const& relevantEvents);
/*!
* Build model from DFT.
@ -312,8 +312,8 @@ namespace storm {
// TODO Matthias: use const reference
std::shared_ptr<storm::storage::DFTStateGenerationInfo> stateGenerationInfo;
// Flag indication if dont care propagation should be used.
bool enableDC = true;
// List with ids of relevant events which should be observed.
std::set<size_t> const& relevantEvents;
//TODO Matthias: make changeable
const bool mergeFailedStates = true;

4
src/storm-dft/generator/DftNextStateGenerator.cpp
View File

@ -10,7 +10,7 @@ namespace storm {
namespace generator {
template<typename ValueType, typename StateType>
DftNextStateGenerator<ValueType, StateType>::DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, bool enableDC, bool mergeFailedStates) : mDft(dft), mStateGenerationInfo(stateGenerationInfo), state(nullptr), enableDC(enableDC), mergeFailedStates(mergeFailedStates) {
DftNextStateGenerator<ValueType, StateType>::DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, std::set<size_t> const& relevantEvents, bool mergeFailedStates) : mDft(dft), mStateGenerationInfo(stateGenerationInfo), state(nullptr), relevantEvents(relevantEvents), mergeFailedStates(mergeFailedStates) {
deterministicModel = !mDft.canHaveNondeterminism();
}
@ -144,7 +144,7 @@ namespace storm {
}
// Propagate dont cares
while (enableDC && !queues.dontCarePropagationDone()) {
while (relevantEvents.empty() && !queues.dontCarePropagationDone()) {
DFTElementPointer next = queues.nextDontCarePropagation();
next->checkDontCareAnymore(*newState, queues);
}

6
src/storm-dft/generator/DftNextStateGenerator.h
View File

@ -24,7 +24,7 @@ namespace storm {
public:
typedef std::function<StateType (DFTStatePointer const&)> StateToIdCallback;
DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, bool enableDC, bool mergeFailedStates);
DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, std::set<size_t> const& relevantEvents, bool mergeFailedStates);
bool isDeterministicModel() const;
std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback);
@ -55,8 +55,8 @@ namespace storm {
// Current state
DFTStatePointer state;
// Flag indicating if dont care propagation is enabled.
bool enableDC;
// List with ids of relevant events which should be observed.
std::set<size_t> const& relevantEvents;
// Flag indication if all failed states should be merged into one.
bool mergeFailedStates = true;

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

@ -17,7 +17,7 @@ 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, bool enableDC, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) {
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, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) {
totalTimer.start();
dft_results results;
@ -29,21 +29,21 @@ namespace storm {
// Checking DFT
if (properties[0]->isTimeOperatorFormula() && allowModularisation) {
// Use parallel composition as modularisation approach for expected time
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = buildModelViaComposition(dft, properties, symred, true, enableDC);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = buildModelViaComposition(dft, properties, symred, true, relevantEvents);
// Model checking
std::vector<ValueType> resultsValue = checkModel(model, properties);
for (ValueType result : resultsValue) {
results.push_back(result);
}
} else {
results = checkHelper(dft, properties, symred, allowModularisation, enableDC, approximationError, approximationHeuristic);
results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, approximationError, approximationHeuristic);
}
totalTimer.stop();
return results;
}
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, bool enableDC, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) {
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, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) {
STORM_LOG_TRACE("Check helper called");
std::vector<storm::storage::DFT<ValueType>> dfts;
bool invResults = false;
@ -98,7 +98,7 @@ namespace storm {
std::vector<ValueType> res;
for(auto const ft : dfts) {
// TODO Matthias: allow approximation in modularisation
dft_results ftResults = checkHelper(ft, {property}, symred, true, enableDC, 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]));
}
@ -137,12 +137,12 @@ namespace storm {
return results;
} else {
// No modularisation was possible
return checkDFT(dft, properties, symred, enableDC, approximationError, approximationHeuristic);
return checkDFT(dft, properties, symred, relevantEvents, approximationError, approximationHeuristic);
}
}
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, bool enableDC) {
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) {
// TODO Matthias: use approximation?
STORM_LOG_TRACE("Build model via composition");
std::vector<storm::storage::DFT<ValueType>> dfts;
@ -193,7 +193,7 @@ namespace storm {
// Build a single CTMC
STORM_LOG_DEBUG("Building Model...");
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(ft, symmetries, enableDC);
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(ft, symmetries, relevantEvents);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
@ -245,7 +245,7 @@ namespace storm {
// Build a single CTMC
STORM_LOG_DEBUG("Building Model...");
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, relevantEvents);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
@ -257,7 +257,7 @@ 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, bool enableDC, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) {
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, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) {
explorationTimer.start();
// Find symmetries
@ -277,7 +277,7 @@ namespace storm {
approximation_result approxResult = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
std::vector<ValueType> newResult;
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, relevantEvents);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
// TODO Matthias: compute approximation for all properties simultaneously?
@ -343,7 +343,7 @@ namespace storm {
// Build a single Markov Automaton
auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
STORM_LOG_DEBUG("Building Model...");
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, relevantEvents);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties, ioSettings.isExportExplicitSet() || ioSettings.isExportDotSet());
builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();

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

@ -49,15 +49,14 @@ namespace storm {
*
* @param origDft Original DFT.
* @param properties Properties to check for.
* @param symred Flag indicating if symmetry reduction should be used.
* @param symred Flag whether symmetry reduction should be used.
* @param allowModularisation Flag indicating if modularisation is allowed.
* @param enableDC Flag indicating if Don't Care propagation should be used.
* @param relevantEvents List with ids of relevant events which should be observed.
* @param approximationError Error allowed for approximation. Value 0 indicates no approximation.
* @param approximationHeuristic Heuristic used for approximation.
*
* @return Model checking results for the given properties.
* @param approximationHeuristic Heuristic used for state space exploration.
* @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, bool enableDC = 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, std::set<size_t> const& relevantEvents = {}, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
/*!
* Print timings of all operations to stream.
@ -92,13 +91,12 @@ 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 enableDC Flag indicating if Don't Caree propagation should be used.
* @param relevantEvents List with ids of relevant events which should be observed.
* @param approximationError Error allowed for approximation. Value 0 indicates no approximation.
* @param approximationHeuristic Heuristic used for approximation.
*
* @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, bool enableDC, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
dft_results checkHelper(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
/*!
* Internal helper for building a CTMC from a DFT via parallel composition.
@ -107,11 +105,10 @@ 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 enableDC Flag indicating if Don't Care propagation should be used.
*
* @param relevantEvents List with ids of relevant events which should be observed.
* @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, bool enableDC);
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);
/*!
* Check model generated from DFT.
@ -119,13 +116,13 @@ namespace storm {
* @param dft The DFT.
* @param properties Properties to check for.
* @param symred Flag indicating if symmetry reduction should be used.
* @param enableDC Flag indicating if Don't Care propagation should be used.
* @param relevantEvents List with ids of relevant events which should be observed.
* @param approximationError Error allowed for approximation. Value 0 indicates no approximation.
* @param approximationHeuristic Heuristic used for approximation.
*
* @return Model checking result
*/
dft_results checkDFT(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool enableDC, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
dft_results checkDFT(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, std::set<size_t> const& relevantEvents = {}, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
/*!
* Check the given markov model for the given properties.

25
src/storm-dft/settings/modules/FaultTreeSettings.cpp
View File

@ -7,16 +7,19 @@
#include "storm/settings/ArgumentBuilder.h"
#include "storm/settings/Argument.h"
#include "storm/exceptions/IllegalArgumentValueException.h"
#include "storm/exceptions/InvalidSettingsException.h"
#include "storm/parser/CSVParser.h"
namespace storm {
namespace settings {
namespace modules {
const std::string FaultTreeSettings::moduleName = "dft";
const std::string FaultTreeSettings::symmetryReductionOptionName = "symmetryreduction";
const std::string FaultTreeSettings::symmetryReductionOptionShortName = "symred";
const std::string FaultTreeSettings::modularisationOptionName = "modularisation";
const std::string FaultTreeSettings::disableDCOptionName = "disabledc";
const std::string FaultTreeSettings::relevantEventsOptionName = "relevantevents";
const std::string FaultTreeSettings::approximationErrorOptionName = "approximation";
const std::string FaultTreeSettings::approximationErrorOptionShortName = "approx";
const std::string FaultTreeSettings::approximationHeuristicOptionName = "approximationheuristic";
@ -30,6 +33,8 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build());
this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false, "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 relevant events. 'all' marks all events as relevant, The default '' or 'none' mark only the top level event as relevant.").setDefaultValueString("").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "The name of the heuristic used for approximation.")
@ -43,15 +48,23 @@ namespace storm {
bool FaultTreeSettings::useSymmetryReduction() const {
return this->getOption(symmetryReductionOptionName).getHasOptionBeenSet();
}
bool FaultTreeSettings::useModularisation() const {
return this->getOption(modularisationOptionName).getHasOptionBeenSet();
}
bool FaultTreeSettings::isDisableDC() const {
return this->getOption(disableDCOptionName).getHasOptionBeenSet();
}
bool FaultTreeSettings::areRelevantEventsSet() const {
return this->getOption(relevantEventsOptionName).getHasOptionBeenSet() && (this->getOption(relevantEventsOptionName).getArgumentByName("values").getValueAsString() != "");
}
std::vector<std::string> FaultTreeSettings::getRelevantEvents() const {
return storm::parser::parseCommaSeperatedValues(this->getOption(relevantEventsOptionName).getArgumentByName("values").getValueAsString());
}
bool FaultTreeSettings::isApproximationErrorSet() const {
return this->getOption(approximationErrorOptionName).getHasOptionBeenSet();
}
@ -81,14 +94,16 @@ namespace storm {
return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet();
}
#endif
void FaultTreeSettings::finalize() {
}
bool FaultTreeSettings::check() const {
// Ensure that disableDC and relevantEvents are not set at the same time
STORM_LOG_THROW(!isDisableDC() || !areRelevantEventsSet(), storm::exceptions::InvalidSettingsException, "DisableDC and relevantSets can not both be set.");
return true;
}
} // namespace modules
} // namespace settings
} // namespace storm

28
src/storm-dft/settings/modules/FaultTreeSettings.h
View File

@ -25,14 +25,14 @@ namespace storm {
* @return True iff the option was set.
*/
bool useSymmetryReduction() const;
/*!
* Retrieves whether the option to use modularisation is set.
*
* @return True iff the option was set.
*/
bool useModularisation() const;
/*!
* Retrieves whether the option to disable Dont Care propagation is set.
*
@ -40,6 +40,20 @@ namespace storm {
*/
bool isDisableDC() const;
/*!
* Retrieves whether the option to give relevant events is set.
*
* @return True iff the option was set.
*/
bool areRelevantEventsSet() const;
/*!
* Retrieves the relevant events which should be present throughout the analysis.
*
* @return The list of relevant events.
*/
std::vector<std::string> getRelevantEvents() const;
/*!
* Retrieves whether the option to compute an approximation is set.
*
@ -67,28 +81,32 @@ namespace storm {
* @return True iff the option was set.
*/
bool isTakeFirstDependency() const;
#ifdef STORM_HAVE_Z3
/*!
* Retrieves whether the DFT should be checked via SMT.
*
* @return True iff the option was set.
*/
bool solveWithSMT() const;
#endif
bool check() const override;
void finalize() override;
// The name of the module.
static const std::string moduleName;
private:
// Define the string names of the options as constants.
// Define the string names of the options as constants.
static const std::string symmetryReductionOptionName;
static const std::string symmetryReductionOptionShortName;
static const std::string modularisationOptionName;
static const std::string disableDCOptionName;
static const std::string relevantEventsOptionName;
static const std::string approximationErrorOptionName;
static const std::string approximationErrorOptionShortName;
static const std::string approximationHeuristicOptionName;

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

@ -845,6 +845,22 @@ namespace storm {
return std::make_tuple(parents, ingoingDeps, outgoingDeps);
}
template<typename ValueType>
std::set<size_t> DFT<ValueType>::getAllIds() const {
std::set<size_t> ids;
for (auto const& elem : mElements) {
ids.insert(elem->id());
}
return ids;
}
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; });
STORM_LOG_THROW(iter != mElements.end(), storm::exceptions::InvalidArgumentException, "Event name '" << name << "' not known.");
return (*iter)->id();
}
template<typename ValueType>
void DFT<ValueType>::writeStatsToStream(std::ostream& stream) const {
// Count individual types of elements

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

@ -305,6 +305,19 @@ namespace storm {
void writeStatsToStream(std::ostream& stream) const;
/*!
* Get Ids of all elements.
* @return All element ids.
*/
std::set<size_t> getAllIds() const;
/*!
* Get id for the given element name.
* @param name Name of element.
* @return Index of element.
*/
size_t getIndex(std::string const& name) const;
private:
std::tuple<std::vector<size_t>, std::vector<size_t>, std::vector<size_t>> getSortedParentAndDependencyIds(size_t index) const;

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

@ -15,22 +15,27 @@ namespace {
class ApproxDepthConfig {
public:
typedef double ValueType;
static DftAnalysisConfig createConfig() {
return DftAnalysisConfig {storm::builder::ApproximationHeuristic::DEPTH, false};
return DftAnalysisConfig{storm::builder::ApproximationHeuristic::DEPTH, false};
}
};
class ApproxProbabilityConfig {
public:
typedef double ValueType;
static DftAnalysisConfig createConfig() {
return DftAnalysisConfig {storm::builder::ApproximationHeuristic::PROBABILITY, false};
return DftAnalysisConfig{storm::builder::ApproximationHeuristic::PROBABILITY, false};
}
};
class ApproxBoundDifferenceConfig {
public:
typedef double ValueType;
static DftAnalysisConfig createConfig() {
return DftAnalysisConfig {storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE, false};
return DftAnalysisConfig{storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE, false};
}
};
@ -52,7 +57,8 @@ namespace {
EXPECT_TRUE(storm::api::isWellFormed(*dft));
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::analyzeDFTApprox<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, {}, errorBound,
config.heuristic, false);
return boost::get<storm::modelchecker::DFTModelChecker<double>::approximation_result>(results[0]);
}
@ -62,7 +68,8 @@ 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::analyzeDFTApprox<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, {}, errorBound,
config.heuristic, false);
return boost::get<storm::modelchecker::DFTModelChecker<double>::approximation_result>(results[0]);
}
@ -83,7 +90,7 @@ namespace {
std::pair<double, double> approxResult = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/hecs_3_2_2_np.dft", errorBound);
EXPECT_LE(approxResult.first, 417.9436693);
EXPECT_GE(approxResult.second, 417.9436693);
EXPECT_LE(2*(approxResult.second - approxResult.first) / (approxResult.first + approxResult.second), errorBound);
EXPECT_LE(2 * (approxResult.second - approxResult.first) / (approxResult.first + approxResult.second), errorBound);
// Ensure results are not equal -> not exact values were computed
EXPECT_GE(approxResult.second - approxResult.first, errorBound * approxResult.first / 10);
}

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

@ -16,36 +16,45 @@ namespace {
class NoOptimizationsConfig {
public:
typedef double ValueType;
static DftAnalysisConfig createConfig() {
return DftAnalysisConfig {false, false, false};
return DftAnalysisConfig{false, false, false};
}
};
class DontCareConfig {
public:
typedef double ValueType;
static DftAnalysisConfig createConfig() {
return DftAnalysisConfig {false, false, true};
return DftAnalysisConfig{false, false, true};
}
};
class ModularisationConfig {
public:
typedef double ValueType;
static DftAnalysisConfig createConfig() {
return DftAnalysisConfig {false, true, false};
return DftAnalysisConfig{false, true, false};
}
};
class SymmetryReductionConfig {
public:
typedef double ValueType;
static DftAnalysisConfig createConfig() {
return DftAnalysisConfig {true, false, false};
return DftAnalysisConfig{true, false, false};
}
};
class AllOptimizationsConfig {
public:
typedef double ValueType;
static DftAnalysisConfig createConfig() {
return DftAnalysisConfig {true, true, true};
return DftAnalysisConfig{true, true, true};
}
};
@ -67,7 +76,12 @@ namespace {
EXPECT_TRUE(storm::api::isWellFormed(*dft));
std::string property = "Tmin=? [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, config.useMod, config.useDC, false);
std::set<size_t> relevantEvents;
if (config.useDC) {
relevantEvents = dft->getAllIds();
}
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]);
}
@ -97,13 +111,13 @@ namespace {
TYPED_TEST(DftModelCheckerTest, VotingMTTF) {
double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/voting.dft");
EXPECT_FLOAT_EQ(result, 5/3.0);
EXPECT_FLOAT_EQ(result, 5 / 3.0);
result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/voting2.dft");
EXPECT_FLOAT_EQ(result, 10/17.0);
EXPECT_FLOAT_EQ(result, 10 / 17.0);
result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/voting3.dft");
EXPECT_FLOAT_EQ(result, 1.7356173);
result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/voting4.dft");
EXPECT_FLOAT_EQ(result, 5/6.0);
EXPECT_FLOAT_EQ(result, 5 / 6.0);
}
TYPED_TEST(DftModelCheckerTest, PandMTTF) {
@ -127,7 +141,7 @@ namespace {
EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft"), storm::exceptions::NotSupportedException);
} else {
result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep.dft");
EXPECT_FLOAT_EQ(result, 2/3.0);
EXPECT_FLOAT_EQ(result, 2 / 3.0);
result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep4.dft");
EXPECT_FLOAT_EQ(result, 1);
result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft");
@ -137,15 +151,15 @@ namespace {
TYPED_TEST(DftModelCheckerTest, PdepMTTF) {
double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep.dft");
EXPECT_FLOAT_EQ(result, 8/3.0);
EXPECT_FLOAT_EQ(result, 8 / 3.0);
result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep3.dft");
EXPECT_FLOAT_EQ(result, 67/24.0);
EXPECT_FLOAT_EQ(result, 67 / 24.0);
if (this->getConfig().useMod) {
if (!this->getConfig().useDC) {
if (this->getConfig().useDC) {
EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep2.dft"), storm::exceptions::NotSupportedException);
} else {
result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep2.dft");
EXPECT_FLOAT_EQ(result, 38/15.0);
EXPECT_FLOAT_EQ(result, 38 / 15.0);
}
EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft"), storm::exceptions::NotSupportedException);
} else {
@ -153,17 +167,18 @@ namespace {
EXPECT_EQ(result, storm::utility::infinity<double>());
}
}
TYPED_TEST(DftModelCheckerTest, SpareMTTF) {
double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare.dft");
EXPECT_FLOAT_EQ(result, 46/13.0);
EXPECT_FLOAT_EQ(result, 46 / 13.0);
result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare2.dft");
EXPECT_FLOAT_EQ(result, 43/23.0);
EXPECT_FLOAT_EQ(result, 43 / 23.0);
result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare3.dft");
EXPECT_FLOAT_EQ(result, 14/11.0);
EXPECT_FLOAT_EQ(result, 14 / 11.0);
result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare4.dft");
EXPECT_FLOAT_EQ(result, 4.8458967);
result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare5.dft");
EXPECT_FLOAT_EQ(result, 8/3.0);
EXPECT_FLOAT_EQ(result, 8 / 3.0);
result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare6.dft");
EXPECT_FLOAT_EQ(result, 1.4);
result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare7.dft");
@ -171,6 +186,7 @@ namespace {
result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare8.dft");
EXPECT_FLOAT_EQ(result, 4.78846); // DFTCalc has result of 4.33779 due to different semantics of nested spares
}
TYPED_TEST(DftModelCheckerTest, SeqMTTF) {
double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq.dft");
EXPECT_FLOAT_EQ(result, 4);
Write Preview
Loading…
Cancel
Save