From 972371c9a2848c62bf326ab77e6f1af520e888ea Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 5 Apr 2019 19:07:48 +0200 Subject: [PATCH] Started on the notion of 'relevant events' for DFT analysis --- src/storm-dft-cli/storm-dft.cpp | 34 +++++++++--- src/storm-dft/api/storm-dft.h | 49 ++++++----------- .../builder/ExplicitDFTModelBuilder.cpp | 6 +-- .../builder/ExplicitDFTModelBuilder.h | 8 +-- .../generator/DftNextStateGenerator.cpp | 4 +- .../generator/DftNextStateGenerator.h | 6 +-- .../modelchecker/dft/DFTModelChecker.cpp | 24 ++++----- .../modelchecker/dft/DFTModelChecker.h | 25 ++++----- .../settings/modules/FaultTreeSettings.cpp | 25 +++++++-- .../settings/modules/FaultTreeSettings.h | 28 ++++++++-- src/storm-dft/storage/dft/DFT.cpp | 16 ++++++ src/storm-dft/storage/dft/DFT.h | 13 +++++ .../storm-dft/api/DftApproximationTest.cpp | 19 ++++--- .../storm-dft/api/DftModelCheckerTest.cpp | 52 ++++++++++++------- 14 files changed, 198 insertions(+), 111 deletions(-) diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index eb4b1b837..0514e63d0 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -120,16 +120,38 @@ void processOptions() { propString += ";" + properties[i]; } std::vector> 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 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(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), - faultTreeSettings.getApproximationError(), faultTreeSettings.getApproximationHeuristic(), true); - } else { - storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), true); + approximationError = faultTreeSettings.getApproximationError(); } + storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, approximationError, + faultTreeSettings.getApproximationHeuristic(), true); } /*! diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index 6cd701e83..f36bfc3ca 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -53,57 +53,40 @@ namespace storm { return std::make_shared>(parser.parseJsonFromFile(file)); } - template - bool isWellFormed(storm::storage::DFT 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 storm::modelchecker::DFTModelChecker::dft_results - analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, - bool enableDC, bool printOutput) { - storm::modelchecker::DFTModelChecker modelChecker(printOutput); - typename storm::modelchecker::DFTModelChecker::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 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 storm::modelchecker::DFTModelChecker::dft_results - analyzeDFTApprox(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, - bool allowModularisation, bool enableDC, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic, bool printOutput) { + analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred = true, + bool allowModularisation = true, std::set const& relevantEvents = {}, double approximationError = 0.0, + storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool printOutput = false) { storm::modelchecker::DFTModelChecker modelChecker(printOutput); - typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, approximationError, approximationHeuristic); + typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents, + approximationError, approximationHeuristic); if (printOutput) { modelChecker.printTimings(); modelChecker.printResults(results); diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index 8c23c6d6a..aba061935 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -54,11 +54,11 @@ namespace storm { } template - ExplicitDFTModelBuilder::ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : + ExplicitDFTModelBuilder::ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, std::set const& relevantEvents) : dft(dft), stateGenerationInfo(std::make_shared(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) diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h index 379918f9b..ce00eb144 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.h @@ -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 const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC); + ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, std::set const& relevantEvents); /*! * Build model from DFT. @@ -312,8 +312,8 @@ namespace storm { // TODO Matthias: use const reference std::shared_ptr 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 const& relevantEvents; //TODO Matthias: make changeable const bool mergeFailedStates = true; diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index b59e91d52..f0646a0c5 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -10,7 +10,7 @@ namespace storm { namespace generator { template - DftNextStateGenerator::DftNextStateGenerator(storm::storage::DFT const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, bool enableDC, bool mergeFailedStates) : mDft(dft), mStateGenerationInfo(stateGenerationInfo), state(nullptr), enableDC(enableDC), mergeFailedStates(mergeFailedStates) { + DftNextStateGenerator::DftNextStateGenerator(storm::storage::DFT const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, std::set 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); } diff --git a/src/storm-dft/generator/DftNextStateGenerator.h b/src/storm-dft/generator/DftNextStateGenerator.h index 08aa3739e..0574d0266 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.h +++ b/src/storm-dft/generator/DftNextStateGenerator.h @@ -24,7 +24,7 @@ namespace storm { public: typedef std::function StateToIdCallback; - DftNextStateGenerator(storm::storage::DFT const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, bool enableDC, bool mergeFailedStates); + DftNextStateGenerator(storm::storage::DFT const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, std::set const& relevantEvents, bool mergeFailedStates); bool isDeterministicModel() const; std::vector 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 const& relevantEvents; // Flag indication if all failed states should be merged into one. bool mergeFailedStates = true; diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index c76495177..385d0efe4 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -17,7 +17,7 @@ namespace storm { namespace modelchecker { template - typename DFTModelChecker::dft_results DFTModelChecker::check(storm::storage::DFT const& origDft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) { + typename DFTModelChecker::dft_results DFTModelChecker::check(storm::storage::DFT const& origDft, std::vector> const& properties, bool symred, bool allowModularisation, std::set 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> model = buildModelViaComposition(dft, properties, symred, true, enableDC); + std::shared_ptr> model = buildModelViaComposition(dft, properties, symred, true, relevantEvents); // Model checking std::vector 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 DFTModelChecker::dft_results DFTModelChecker::checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) { + typename DFTModelChecker::dft_results DFTModelChecker::checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set const& relevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) { STORM_LOG_TRACE("Check helper called"); std::vector> dfts; bool invResults = false; @@ -98,7 +98,7 @@ namespace storm { std::vector 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(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 - std::shared_ptr> DFTModelChecker::buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC) { + std::shared_ptr> DFTModelChecker::buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set const& relevantEvents) { // TODO Matthias: use approximation? STORM_LOG_TRACE("Build model via composition"); std::vector> dfts; @@ -193,7 +193,7 @@ namespace storm { // Build a single CTMC STORM_LOG_DEBUG("Building Model..."); - storm::builder::ExplicitDFTModelBuilder builder(ft, symmetries, enableDC); + storm::builder::ExplicitDFTModelBuilder builder(ft, symmetries, relevantEvents); typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> model = builder.getModel(); @@ -245,7 +245,7 @@ namespace storm { // Build a single CTMC STORM_LOG_DEBUG("Building Model..."); - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents); typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> model = builder.getModel(); @@ -257,7 +257,7 @@ namespace storm { } template - typename DFTModelChecker::dft_results DFTModelChecker::checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool enableDC, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) { + typename DFTModelChecker::dft_results DFTModelChecker::checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, std::set 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(), storm::utility::zero()); std::shared_ptr> model; std::vector newResult; - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents); typename storm::builder::ExplicitDFTModelBuilder::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_LOG_DEBUG("Building Model..."); - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents); typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties, ioSettings.isExportExplicitSet() || ioSettings.isExportDotSet()); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> model = builder.getModel(); diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h index 7bc07e30e..34568d2f4 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -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 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 const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true, std::set 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 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 const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set 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> buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC); + std::shared_ptr> buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set 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 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 const& dft, property_vector const& properties, bool symred, std::set const& relevantEvents = {}, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH); /*! * Check the given markov model for the given properties. diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.cpp b/src/storm-dft/settings/modules/FaultTreeSettings.cpp index 740c6aa54..fd365a1ea 100644 --- a/src/storm-dft/settings/modules/FaultTreeSettings.cpp +++ b/src/storm-dft/settings/modules/FaultTreeSettings.cpp @@ -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 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 diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.h b/src/storm-dft/settings/modules/FaultTreeSettings.h index 171d5c38e..1e88b48e4 100644 --- a/src/storm-dft/settings/modules/FaultTreeSettings.h +++ b/src/storm-dft/settings/modules/FaultTreeSettings.h @@ -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 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; diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index a9ecb8a5a..6a926e3a3 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -845,6 +845,22 @@ namespace storm { return std::make_tuple(parents, ingoingDeps, outgoingDeps); } + template + std::set DFT::getAllIds() const { + std::set ids; + for (auto const& elem : mElements) { + ids.insert(elem->id()); + } + return ids; + } + + 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; }); + STORM_LOG_THROW(iter != mElements.end(), storm::exceptions::InvalidArgumentException, "Event name '" << name << "' not known."); + return (*iter)->id(); + } + template void DFT::writeStatsToStream(std::ostream& stream) const { // Count individual types of elements diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index 940e8adcf..dfb7c583d 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -305,6 +305,19 @@ namespace storm { void writeStatsToStream(std::ostream& stream) const; + /*! + * Get Ids of all elements. + * @return All element ids. + */ + std::set 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, std::vector> getSortedParentAndDependencyIds(size_t index) const; diff --git a/src/test/storm-dft/api/DftApproximationTest.cpp b/src/test/storm-dft/api/DftApproximationTest.cpp index d00973da1..7718d9218 100644 --- a/src/test/storm-dft/api/DftApproximationTest.cpp +++ b/src/test/storm-dft/api/DftApproximationTest.cpp @@ -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> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); - typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFTApprox(*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, {}, errorBound, + config.heuristic, false); return boost::get::approximation_result>(results[0]); } @@ -62,7 +68,8 @@ 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::analyzeDFTApprox(*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, {}, errorBound, + config.heuristic, false); return boost::get::approximation_result>(results[0]); } @@ -83,7 +90,7 @@ namespace { std::pair 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); } diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index 6da316081..790c29509 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -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> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); - typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, config.useMod, config.useDC, false); + std::set relevantEvents; + if (config.useDC) { + relevantEvents = dft->getAllIds(); + } + typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, config.useMod, + relevantEvents); return boost::get(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()); } } + 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);