From f2c902eedb5b0e6a2aecc354cee5fe34d23a1608 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 17 Apr 2019 19:11:34 +0200 Subject: [PATCH] Set labels, dont care propagation and unique failed state according to relevant events --- src/storm-dft-cli/storm-dft.cpp | 16 ++- src/storm-dft/api/storm-dft.h | 8 +- .../builder/ExplicitDFTModelBuilder.cpp | 109 +++++++++--------- .../builder/ExplicitDFTModelBuilder.h | 36 ++---- .../generator/DftNextStateGenerator.cpp | 17 +-- .../generator/DftNextStateGenerator.h | 9 +- .../modelchecker/dft/DFTModelChecker.cpp | 34 +++--- .../modelchecker/dft/DFTModelChecker.h | 20 +++- .../settings/modules/FaultTreeSettings.cpp | 10 +- .../settings/modules/FaultTreeSettings.h | 8 ++ src/storm-dft/storage/dft/DFT.cpp | 4 +- src/storm-dft/storage/dft/DFT.h | 3 +- .../storage/dft/elements/DFTElement.cpp | 3 +- .../storage/dft/elements/DFTElement.h | 11 +- .../storm-dft/api/DftApproximationTest.cpp | 6 +- .../storm-dft/api/DftModelBuildingTest.cpp | 18 ++- .../storm-dft/api/DftModelCheckerTest.cpp | 2 +- 17 files changed, 162 insertions(+), 152 deletions(-) diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 1c036a33d..0db58195b 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -138,11 +138,15 @@ void processOptions() { // Events from properties are relevant as well for (auto atomic : atomicLabels) { std::string label = atomic->getLabel(); - std::size_t foundIndex = label.find("_fail"); - if (foundIndex != std::string::npos) { - relevantEventNames.push_back(label.substr(0, foundIndex)); + if (label == "failed") { + // Ignore as this label will always be added } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Label '" << label << "' not known."); + std::size_t foundIndex = label.find("_fail"); + if (foundIndex != std::string::npos) { + relevantEventNames.push_back(label.substr(0, foundIndex)); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Label '" << label << "' not known."); + } } } @@ -178,8 +182,8 @@ void processOptions() { if (faultTreeSettings.isApproximationErrorSet()) { approximationError = faultTreeSettings.getApproximationError(); } - storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, approximationError, - faultTreeSettings.getApproximationHeuristic(), true); + storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, + faultTreeSettings.isAllowDCForRelevantEvents(), approximationError, faultTreeSettings.getApproximationHeuristic(), true); } } diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index f801b0eda..754bdfc91 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -70,6 +70,7 @@ namespace storm { * @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 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. @@ -78,11 +79,12 @@ namespace storm { template typename storm::modelchecker::DFTModelChecker::dft_results 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) { + bool allowModularisation = true, std::set const& relevantEvents = {}, bool allowDCForRelevantEvents = true, 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, relevantEvents, - approximationError, approximationHeuristic); + allowDCForRelevantEvents, 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 da2100537..9fc882e27 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -31,43 +31,24 @@ namespace storm { } template - ExplicitDFTModelBuilder::LabelOptions::LabelOptions(std::vector> properties, bool buildAllLabels) : buildFailLabel(true), buildFailSafeLabel(false), buildAllLabels(buildAllLabels) { - // Get necessary labels from properties - std::vector> atomicLabels; - for (auto property : properties) { - property->gatherAtomicLabelFormulas(atomicLabels); - } - // Set usage of necessary labels - for (auto atomic : atomicLabels) { - std::string label = atomic->getLabel(); - std::size_t foundIndex = label.find("_fail"); - if (foundIndex != std::string::npos) { - elementLabels.insert(label.substr(0, foundIndex)); - } else if (label.compare("failed") == 0) { - buildFailLabel = true; - } else if (label.compare("failsafe") == 0) { - buildFailSafeLabel = true; - } else { - STORM_LOG_WARN("Label '" << label << "' not known."); - } - } - } - - template - ExplicitDFTModelBuilder::ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, std::set const& relevantEvents) : + ExplicitDFTModelBuilder::ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, std::set const& relevantEvents, bool allowDCForRelevantEvents) : dft(dft), stateGenerationInfo(std::make_shared(dft.buildStateGenerationInfo(symmetries))), relevantEvents(relevantEvents), - generator(dft, *stateGenerationInfo, mergeFailedStates), + generator(dft, *stateGenerationInfo), matrixBuilder(!generator.isDeterministicModel()), stateStorage(dft.stateBitVectorSize()), explorationQueue(1, 0, 0.9, false) { // Set relevant events - this->dft.setRelevantEvents(this->relevantEvents); + this->dft.setRelevantEvents(this->relevantEvents, allowDCForRelevantEvents); // Mark top level element as relevant this->dft.getElement(this->dft.getTopLevelIndex())->setRelevance(true); - + if (this->relevantEvents.empty()) { + // Only interested in top level event -> introduce unique failed state + this->uniqueFailedState = true; + STORM_LOG_DEBUG("Using unique failed state with id 0."); + } // Compute independent subtrees if (dft.topLevelType() == storm::storage::DFTElementType::OR) { @@ -126,10 +107,17 @@ namespace storm { } template - void ExplicitDFTModelBuilder::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold, storm::builder::ApproximationHeuristic approximationHeuristic) { + void ExplicitDFTModelBuilder::buildModel(size_t iteration, double approximationThreshold, storm::builder::ApproximationHeuristic approximationHeuristic) { STORM_LOG_TRACE("Generating DFT state space"); usedHeuristic = approximationHeuristic; + if (approximationThreshold > 0 && !this->uniqueFailedState) { + // Approximation requires unique failed states + // TODO lift this restriction + STORM_LOG_WARN("Approximation requires unique failed state. Forcing use of unique failed state."); + this->uniqueFailedState = true; + } + if (iteration < 1) { // Initialize switch (usedHeuristic) { @@ -147,15 +135,16 @@ namespace storm { } modelComponents.markovianStates = storm::storage::BitVector(INITIAL_BITVECTOR_SIZE); - if(mergeFailedStates) { + if (this->uniqueFailedState) { // Introduce explicit fail state storm::generator::StateBehavior behavior = generator.createMergeFailedState([this] (DFTStatePointer const& state) { - this->failedStateId = newIndex++; + size_t failedStateId = newIndex++; + STORM_LOG_ASSERT(failedStateId == 0, "Unique failed id is not 0."); matrixBuilder.stateRemapping.push_back(0); - return this->failedStateId; + return failedStateId; } ); - matrixBuilder.setRemapping(failedStateId); + matrixBuilder.setRemapping(0); STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty."); matrixBuilder.newRowGroup(); setMarkovian(behavior.begin()->isMarkovian()); @@ -165,7 +154,7 @@ namespace storm { STORM_LOG_ASSERT(behavior.getNumberOfChoices() == 1, "Wrong number of choices for failed state."); STORM_LOG_ASSERT(behavior.begin()->size() == 1, "Wrong number of transitions for failed state."); std::pair stateProbabilityPair = *(behavior.begin()->begin()); - STORM_LOG_ASSERT(stateProbabilityPair.first == failedStateId, "No self loop for failed state."); + STORM_LOG_ASSERT(stateProbabilityPair.first == 0, "No self loop for failed state."); STORM_LOG_ASSERT(storm::utility::isOne(stateProbabilityPair.second), "Probability for failed state != 1."); matrixBuilder.addTransition(stateProbabilityPair.first, stateProbabilityPair.second); matrixBuilder.finishRow(); @@ -214,7 +203,7 @@ namespace storm { } exploreStateSpace(approximationThreshold); - size_t stateSize = stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0); + size_t stateSize = stateStorage.getNumberOfStates() + (this->uniqueFailedState ? 1 : 0); modelComponents.markovianStates.resize(stateSize); modelComponents.deterministicModel = generator.isDeterministicModel(); @@ -237,7 +226,7 @@ namespace storm { STORM_LOG_TRACE("Transition matrix: too big to print"); } - buildLabeling(labelOpts); + buildLabeling(); } template @@ -386,7 +375,8 @@ namespace storm { setMarkovian(true); // Add transition to target state with temporary value 0 // TODO: what to do when there is no unique target state? - matrixBuilder.addTransition(failedStateId, storm::utility::zero()); + STORM_LOG_ASSERT(this->uniqueFailedState, "Approximation only works with unique failed state"); + matrixBuilder.addTransition(0, storm::utility::zero()); // Remember skipped state skippedStates[matrixBuilder.getCurrentRowGroup() - 1] = std::make_pair(currentState, currentExplorationHeuristic); matrixBuilder.finishRow(); @@ -471,47 +461,54 @@ namespace storm { } template - void ExplicitDFTModelBuilder::buildLabeling(LabelOptions const& labelOpts) { + void ExplicitDFTModelBuilder::buildLabeling() { // Build state labeling modelComponents.stateLabeling = storm::models::sparse::StateLabeling(modelComponents.transitionMatrix.getRowGroupCount()); // Initial state modelComponents.stateLabeling.addLabel("init"); STORM_LOG_ASSERT(matrixBuilder.getRemapping(initialStateIndex) == initialStateIndex, "Initial state should not be remapped."); modelComponents.stateLabeling.addLabelToState("init", initialStateIndex); - // Label all states corresponding to their status (failed, failsafe, failed BE) - if(labelOpts.buildFailLabel) { - modelComponents.stateLabeling.addLabel("failed"); - } - if(labelOpts.buildFailSafeLabel) { - modelComponents.stateLabeling.addLabel("failsafe"); - } + // Label all states corresponding to their status (failed, failed/dont care BE) + modelComponents.stateLabeling.addLabel("failed"); // Collect labels for all necessary elements for (size_t id = 0; id < dft.nrElements(); ++id) { std::shared_ptr const> element = dft.getElement(id); - if (labelOpts.buildAllLabels || labelOpts.elementLabels.count(element->name()) > 0) { + if (element->isRelevant()) { modelComponents.stateLabeling.addLabel(element->name() + "_fail"); + modelComponents.stateLabeling.addLabel(element->name() + "_dc"); } } // Set labels to states - if (mergeFailedStates) { - modelComponents.stateLabeling.addLabelToState("failed", failedStateId); + if (this->uniqueFailedState) { + modelComponents.stateLabeling.addLabelToState("failed", 0); } for (auto const& stateIdPair : stateStorage.stateToId) { storm::storage::BitVector state = stateIdPair.first; size_t stateId = matrixBuilder.getRemapping(stateIdPair.second); - if (!mergeFailedStates && labelOpts.buildFailLabel && dft.hasFailed(state, *stateGenerationInfo)) { + if (dft.hasFailed(state, *stateGenerationInfo)) { modelComponents.stateLabeling.addLabelToState("failed", stateId); } - if (labelOpts.buildFailSafeLabel && dft.isFailsafe(state, *stateGenerationInfo)) { - modelComponents.stateLabeling.addLabelToState("failsafe", stateId); - } - // Set fail status for each necessary element + // Set fail/dont care status for each necessary element for (size_t id = 0; id < dft.nrElements(); ++id) { std::shared_ptr const> element = dft.getElement(id); - if ((labelOpts.buildAllLabels || labelOpts.elementLabels.count(element->name()) > 0) && storm::storage::DFTState::hasFailed(state, stateGenerationInfo->getStateIndex(element->id()))) { - modelComponents.stateLabeling.addLabelToState(element->name() + "_fail", stateId); + if (element->isRelevant()){ + storm::storage::DFTElementState elementState = storm::storage::DFTState::getElementState(state, *stateGenerationInfo, element->id()); + switch (elementState) { + case storm::storage::DFTElementState::Failed: + modelComponents.stateLabeling.addLabelToState(element->name() + "_fail", stateId); + break; + case storm::storage::DFTElementState::DontCare: + modelComponents.stateLabeling.addLabelToState(element->name() + "_dc", stateId); + break; + case storm::storage::DFTElementState::Operational: + case storm::storage::DFTElementState::Failsafe: + // do nothing + break; + default: + STORM_LOG_ASSERT(false, "Unknown element state " << elementState); + } } } } @@ -540,7 +537,7 @@ namespace storm { // Set self loop for lower bound for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) { auto matrixEntry = matrix.getRow(it->first, 0).begin(); - STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state."); + STORM_LOG_ASSERT(matrixEntry->getColumn() == 0, "Transition has wrong target state."); STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state."); matrixEntry->setValue(storm::utility::one()); matrixEntry->setColumn(it->first); @@ -658,7 +655,7 @@ namespace storm { // Set lower bound for skipped states for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) { auto matrixEntry = matrix.getRow(it->first, 0).begin(); - STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state."); + STORM_LOG_ASSERT(matrixEntry->getColumn() == 0, "Transition has wrong target state."); STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state."); ExplorationHeuristicPointer heuristic = it->second.second; diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h index 5598ac6ef..46ac973b8 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.h @@ -151,42 +151,24 @@ namespace storm { }; public: - // A structure holding the labeling options. - struct LabelOptions { - // Constructor - LabelOptions(std::vector> properties, bool buildAllLabels = false); - - // Flag indicating if the general fail label should be included. - bool buildFailLabel; - - // Flag indicating if the general failsafe label should be included. - bool buildFailSafeLabel; - - // Flag indicating if all possible labels should be included. - bool buildAllLabels; - - // Set of element names whose fail label to include. - std::set elementLabels; - }; - /*! * Constructor. * * @param dft DFT. * @param symmetries Symmetries in the dft. * @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. */ - ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, std::set const& relevantEvents); + ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, std::set const& relevantEvents, bool allowDCForRelevantEvents); /*! * Build model from DFT. * - * @param labelOpts Options for labeling. * @param iteration Current number of iteration. * @param approximationThreshold Threshold determining when to skip exploring states. * @param approximationHeuristic Heuristic used for exploring states. */ - void buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH); + void buildModel(size_t iteration, double approximationThreshold = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH); /*! * Get the built model. @@ -221,10 +203,8 @@ namespace storm { /*! * Build the labeling. - * - * @param labelOpts Options for labeling. */ - void buildLabeling(LabelOptions const& labelOpts); + void buildLabeling(); /*! * Add a state to the explored states (if not already there). It also handles pseudo states. @@ -315,17 +295,15 @@ namespace storm { // List with ids of relevant events which should be observed. std::set const& relevantEvents; - //TODO: merge depending on relevant events - const bool mergeFailedStates = true; - // Heuristic used for approximation storm::builder::ApproximationHeuristic usedHeuristic; // Current id for new state size_t newIndex = 0; - // Id of failed state - size_t failedStateId = 0; + // Whether to use a unique state for all failed states + // If used, the unique failed state has the id 0 + bool uniqueFailedState = false; // Id of initial state size_t initialStateIndex = 0; diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index eb1795448..4dd2e8402 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 mergeFailedStates) : mDft(dft), mStateGenerationInfo(stateGenerationInfo), state(nullptr), mergeFailedStates(mergeFailedStates) { + DftNextStateGenerator::DftNextStateGenerator(storm::storage::DFT const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo) : mDft(dft), mStateGenerationInfo(stateGenerationInfo), state(nullptr), uniqueFailedState(false) { deterministicModel = !mDft.canHaveNondeterminism(); } @@ -135,9 +135,9 @@ namespace storm { // Get the id of the successor state StateType newStateId; - if (newState->hasFailed(mDft.getTopLevelIndex()) && mergeFailedStates) { + if (newState->hasFailed(mDft.getTopLevelIndex()) && uniqueFailedState) { // Use unique failed state - newStateId = mergeFailedStateId; + newStateId = 0; } else { // Propagate failsafe while (!queues.failsafePropagationDone()) { @@ -226,15 +226,16 @@ namespace storm { template StateBehavior DftNextStateGenerator::createMergeFailedState(StateToIdCallback const& stateToIdCallback) { - STORM_LOG_ASSERT(mergeFailedStates, "No unique failed state used."); - // Introduce explicit fail state + this->uniqueFailedState = true; + // Introduce explicit fail state with id 0 DFTStatePointer failedState = std::make_shared>(mDft, mStateGenerationInfo, 0); - mergeFailedStateId = stateToIdCallback(failedState); - STORM_LOG_TRACE("Introduce fail state with id: " << mergeFailedStateId); + size_t failedStateId = stateToIdCallback(failedState); + STORM_LOG_ASSERT(failedStateId == 0, "Unique failed state has not id 0."); + STORM_LOG_TRACE("Introduce fail state with id 0."); // Add self loop Choice choice(0, true); - choice.addProbability(mergeFailedStateId, storm::utility::one()); + choice.addProbability(0, storm::utility::one()); // No further exploration required StateBehavior result; diff --git a/src/storm-dft/generator/DftNextStateGenerator.h b/src/storm-dft/generator/DftNextStateGenerator.h index b77751521..9fab2ee1f 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 mergeFailedStates); + DftNextStateGenerator(storm::storage::DFT const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo); bool isDeterministicModel() const; std::vector getInitialStates(StateToIdCallback const& stateToIdCallback); @@ -55,11 +55,8 @@ namespace storm { // Current state DFTStatePointer state; - // Flag indication if all failed states should be merged into one. - bool mergeFailedStates = true; - - // Id of the merged failed state - StateType mergeFailedStateId = 0; + // Flag indication if all failed states should be merged into one unique failed state. + bool uniqueFailedState; // Flag indicating if the model is deterministic. bool deterministicModel = false; diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 19a091a50..eed303311 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, std::set const& relevantEvents, 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, bool allowDCForRelevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) { totalTimer.start(); dft_results results; @@ -37,14 +37,14 @@ namespace storm { results.push_back(result); } } else { - results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, approximationError, approximationHeuristic); + results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevantEvents, 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, std::set const& relevantEvents, 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, bool allowDCForRelevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) { STORM_LOG_TRACE("Check helper called"); std::vector> dfts; bool invResults = false; @@ -99,7 +99,7 @@ namespace storm { std::vector res; for(auto const ft : dfts) { // TODO: allow approximation in modularisation - dft_results ftResults = checkHelper(ft, {property}, symred, true, relevantEvents, 0.0); + dft_results ftResults = checkHelper(ft, {property}, symred, true, relevantEvents, allowDCForRelevantEvents, 0.0); STORM_LOG_ASSERT(ftResults.size() == 1, "Wrong number of results"); res.push_back(boost::get(ftResults[0])); } @@ -138,12 +138,12 @@ namespace storm { return results; } else { // No modularisation was possible - return checkDFT(dft, properties, symred, relevantEvents, approximationError, approximationHeuristic); + return checkDFT(dft, properties, symred, relevantEvents, allowDCForRelevantEvents, approximationError, approximationHeuristic); } } template - std::shared_ptr> DFTModelChecker::buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set const& relevantEvents) { + std::shared_ptr> DFTModelChecker::buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set const& relevantEvents, bool allowDCForRelevantEvents) { // TODO: use approximation? STORM_LOG_TRACE("Build model via composition"); std::vector> dfts; @@ -194,9 +194,8 @@ namespace storm { // Build a single CTMC STORM_LOG_DEBUG("Building Model..."); - storm::builder::ExplicitDFTModelBuilder builder(ft, symmetries, relevantEvents); - typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); - builder.buildModel(labeloptions, 0, 0.0); + storm::builder::ExplicitDFTModelBuilder builder(ft, symmetries, relevantEvents, allowDCForRelevantEvents); + builder.buildModel(0, 0.0); std::shared_ptr> model = builder.getModel(); explorationTimer.stop(); @@ -246,9 +245,8 @@ namespace storm { // Build a single CTMC STORM_LOG_DEBUG("Building Model..."); - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents); - typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); - builder.buildModel(labeloptions, 0, 0.0); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents, allowDCForRelevantEvents); + builder.buildModel(0, 0.0); std::shared_ptr> model = builder.getModel(); //model->printModelInformationToStream(std::cout); explorationTimer.stop(); @@ -258,7 +256,7 @@ namespace storm { } template - 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) { + typename DFTModelChecker::dft_results DFTModelChecker::checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, std::set const& relevantEvents, bool allowDCForRelevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) { explorationTimer.start(); // Find symmetries @@ -278,8 +276,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, relevantEvents); - typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents, allowDCForRelevantEvents); // TODO: compute approximation for all properties simultaneously? std::shared_ptr property = properties[0]; @@ -297,7 +294,7 @@ namespace storm { } STORM_LOG_DEBUG("Building model..."); // TODO refine model using existing model and MC results - builder.buildModel(labeloptions, iteration, approximationError, approximationHeuristic); + builder.buildModel(iteration, approximationError, approximationHeuristic); explorationTimer.stop(); buildingTimer.start(); @@ -344,9 +341,8 @@ namespace storm { // Build a single Markov Automaton auto ioSettings = storm::settings::getModule(); STORM_LOG_DEBUG("Building Model..."); - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents); - typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties, ioSettings.isExportExplicitSet() || ioSettings.isExportDotSet()); - builder.buildModel(labeloptions, 0, 0.0); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents, allowDCForRelevantEvents); + builder.buildModel(0, 0.0); std::shared_ptr> model = builder.getModel(); explorationTimer.stop(); diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h index 34568d2f4..4b4cd4d3d 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -52,11 +52,14 @@ namespace storm { * @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 approximationError Error allowed for approximation. Value 0 indicates no approximation. * @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, std::set const& relevantEvents = {}, 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 = {}, bool allowDCForRelevantEvents = true, double approximationError = 0.0, + storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH); /*! * Print timings of all operations to stream. @@ -92,11 +95,14 @@ 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. * @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, std::set const& relevantEvents, 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, bool allowDCForRelevantEvents = true, double approximationError = 0.0, + storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH); /*! * Internal helper for building a CTMC from a DFT via parallel composition. @@ -106,9 +112,12 @@ 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> buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set const& relevantEvents); + std::shared_ptr> buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, + bool symred, bool allowModularisation, std::set const& relevantEvents, + bool allowDCForRelevantEvents = true); /*! * Check model generated from DFT. @@ -117,12 +126,15 @@ 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. * * @return Model checking result */ - 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); + dft_results checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, std::set const& relevantEvents = {}, + bool allowDCForRelevantEvents = true, 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 fd365a1ea..140b0f175 100644 --- a/src/storm-dft/settings/modules/FaultTreeSettings.cpp +++ b/src/storm-dft/settings/modules/FaultTreeSettings.cpp @@ -19,6 +19,7 @@ namespace storm { const std::string FaultTreeSettings::symmetryReductionOptionShortName = "symred"; const std::string FaultTreeSettings::modularisationOptionName = "modularisation"; const std::string FaultTreeSettings::disableDCOptionName = "disabledc"; + const std::string FaultTreeSettings::allowDCRelevantOptionName = "allowdcrelevant"; const std::string FaultTreeSettings::relevantEventsOptionName = "relevantevents"; const std::string FaultTreeSettings::approximationErrorOptionName = "approximation"; const std::string FaultTreeSettings::approximationErrorOptionShortName = "approx"; @@ -31,10 +32,11 @@ namespace storm { FaultTreeSettings::FaultTreeSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build()); 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, disableDCOptionName, false, "Disable Don't 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()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of names of relevant events. 'all' marks all events as relevant, The default '' or 'none' marks only the top level event as relevant.").setDefaultValueString("").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, allowDCRelevantOptionName, false, "Allow Don't Care propagation for relevant events.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, 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.") @@ -57,6 +59,10 @@ namespace storm { return this->getOption(disableDCOptionName).getHasOptionBeenSet(); } + bool FaultTreeSettings::isAllowDCForRelevantEvents() const { + return this->getOption(allowDCRelevantOptionName).getHasOptionBeenSet(); + } + bool FaultTreeSettings::areRelevantEventsSet() const { return this->getOption(relevantEventsOptionName).getHasOptionBeenSet() && (this->getOption(relevantEventsOptionName).getArgumentByName("values").getValueAsString() != ""); } diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.h b/src/storm-dft/settings/modules/FaultTreeSettings.h index 1e88b48e4..16a726e04 100644 --- a/src/storm-dft/settings/modules/FaultTreeSettings.h +++ b/src/storm-dft/settings/modules/FaultTreeSettings.h @@ -40,6 +40,13 @@ namespace storm { */ bool isDisableDC() const; + /*! + * Retrieves whether the option to allow Dont Care propagation for relevant events is set. + * + * @return True iff the option was set. + */ + bool isAllowDCForRelevantEvents() const; + /*! * Retrieves whether the option to give relevant events is set. * @@ -106,6 +113,7 @@ namespace storm { static const std::string symmetryReductionOptionShortName; static const std::string modularisationOptionName; static const std::string disableDCOptionName; + static const std::string allowDCRelevantOptionName; static const std::string relevantEventsOptionName; static const std::string approximationErrorOptionName; static const std::string approximationErrorOptionShortName; diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 7538c4abc..21251f044 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -862,12 +862,14 @@ namespace storm { } template - void DFT::setRelevantEvents(std::set const& relevantEvents) const { + void DFT::setRelevantEvents(std::set const& relevantEvents, bool allowDCForRelevantEvents) const { for (auto const& elem : mElements) { if (relevantEvents.find(elem->id()) != relevantEvents.end()) { elem->setRelevance(true); + elem->setAllowDC(allowDCForRelevantEvents); } else { elem->setRelevance(false); + elem->setAllowDC(true); } } } diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index 2b8795a82..27079a6ba 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -321,8 +321,9 @@ 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 occuring are set to irrelevant. + * @param allowDCForRelevantEvents Flag whether Don't Care propagation is allowed even for relevant events. */ - void setRelevantEvents(std::set const& relevantEvents) const; + void setRelevantEvents(std::set const& relevantEvents, bool allowDCForRelevantEvents) const; private: std::tuple, std::vector, std::vector> getSortedParentAndDependencyIds(size_t index) const; diff --git a/src/storm-dft/storage/dft/elements/DFTElement.cpp b/src/storm-dft/storage/dft/elements/DFTElement.cpp index d9bba261a..57c3b1ee0 100644 --- a/src/storm-dft/storage/dft/elements/DFTElement.cpp +++ b/src/storm-dft/storage/dft/elements/DFTElement.cpp @@ -9,8 +9,7 @@ namespace storm { template bool DFTElement::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { - if (this->isRelevant()) { - // Relevant events are ignored for Don't Care propagation + if (!this->mAllowDC) { return false; } diff --git a/src/storm-dft/storage/dft/elements/DFTElement.h b/src/storm-dft/storage/dft/elements/DFTElement.h index f89f69c7a..27784dae0 100644 --- a/src/storm-dft/storage/dft/elements/DFTElement.h +++ b/src/storm-dft/storage/dft/elements/DFTElement.h @@ -51,7 +51,7 @@ namespace storm { * @param id Id. * @param name Name. */ - DFTElement(size_t id, std::string const& name) : mId(id), mName(name), mRank(-1), mRelevant(false) { + DFTElement(size_t id, std::string const& name) : mId(id), mName(name), mRank(-1), mRelevant(false), mAllowDC(true) { // Intentionally left empty. } @@ -134,6 +134,14 @@ namespace storm { this->mRelevant = relevant; } + /*! + * Set whether Don't Care propagation is allowed for this element. + * @param allowDC If true, the element is allowed to be set to Don't Care. + */ + virtual void setAllowDC(bool allowDC) const { + this->mAllowDC = allowDC; + } + /*! * Checks whether the element is a basic element. * @return True iff element is a BE. @@ -438,6 +446,7 @@ namespace storm { DFTDependencyVector mOutgoingDependencies; DFTRestrictionVector mRestrictions; mutable bool mRelevant; // Must be mutable to allow changes later on. TODO: avoid mutable + mutable bool mAllowDC; // Must be mutable to allow changes later on. TODO: avoid mutable }; diff --git a/src/test/storm-dft/api/DftApproximationTest.cpp b/src/test/storm-dft/api/DftApproximationTest.cpp index 7718d9218..e17fa200c 100644 --- a/src/test/storm-dft/api/DftApproximationTest.cpp +++ b/src/test/storm-dft/api/DftApproximationTest.cpp @@ -57,7 +57,7 @@ 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::analyzeDFT(*dft, properties, config.useSR, false, {}, errorBound, + typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, false, {}, true, errorBound, config.heuristic, false); return boost::get::approximation_result>(results[0]); } @@ -67,8 +67,8 @@ namespace { EXPECT_TRUE(storm::api::isWellFormed(*dft)); 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::analyzeDFT(*dft, properties, config.useSR, false, {}, errorBound, + std::vector > properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propertyStream.str())); + typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, false, {}, true, errorBound, config.heuristic, false); return boost::get::approximation_result>(results[0]); } diff --git a/src/test/storm-dft/api/DftModelBuildingTest.cpp b/src/test/storm-dft/api/DftModelBuildingTest.cpp index cbaa53e82..cd71be290 100644 --- a/src/test/storm-dft/api/DftModelBuildingTest.cpp +++ b/src/test/storm-dft/api/DftModelBuildingTest.cpp @@ -16,14 +16,12 @@ namespace { std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); std::map>> emptySymmetry; storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); - typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties, false); - // Set relevant events (none) std::set relevantEvents; // Build model - storm::builder::ExplicitDFTModelBuilder builder(*dft, symmetries, relevantEvents); - builder.buildModel(labeloptions, 0, 0.0); + storm::builder::ExplicitDFTModelBuilder builder(*dft, symmetries, relevantEvents, false); + builder.buildModel(0, 0.0); std::shared_ptr> model = builder.getModel(); EXPECT_EQ(8ul, model->getNumberOfStates()); EXPECT_EQ(13ul, model->getNumberOfTransitions()); @@ -31,8 +29,8 @@ namespace { // Set relevant events (all) relevantEvents = dft->getAllIds(); // Build model - storm::builder::ExplicitDFTModelBuilder builder2(*dft, symmetries, relevantEvents); - builder2.buildModel(labeloptions, 0, 0.0); + storm::builder::ExplicitDFTModelBuilder builder2(*dft, symmetries, relevantEvents, false); + builder2.buildModel(0, 0.0); model = builder2.getModel(); EXPECT_EQ(170ul, model->getNumberOfStates()); EXPECT_EQ(688ul, model->getNumberOfTransitions()); @@ -42,8 +40,8 @@ namespace { relevantEvents.clear(); relevantEvents.insert(dft->getIndex("H")); // Build model - storm::builder::ExplicitDFTModelBuilder builder3(*dft, symmetries, relevantEvents); - builder3.buildModel(labeloptions, 0, 0.0); + storm::builder::ExplicitDFTModelBuilder builder3(*dft, symmetries, relevantEvents, false); + builder3.buildModel(0, 0.0); model = builder3.getModel(); EXPECT_EQ(11ul, model->getNumberOfStates()); EXPECT_EQ(23ul, model->getNumberOfTransitions()); @@ -54,8 +52,8 @@ namespace { relevantEvents.insert(dft->getIndex("H")); relevantEvents.insert(dft->getIndex("I")); // Build model - storm::builder::ExplicitDFTModelBuilder builder4(*dft, symmetries, relevantEvents); - builder4.buildModel(labeloptions, 0, 0.0); + storm::builder::ExplicitDFTModelBuilder builder4(*dft, symmetries, relevantEvents, false); + builder4.buildModel(0, 0.0); model = builder4.getModel(); EXPECT_EQ(14ul, model->getNumberOfStates()); EXPECT_EQ(30ul, model->getNumberOfTransitions()); diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index baf30dc02..f49639ba3 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -81,7 +81,7 @@ namespace { relevantEvents = dft->getAllIds(); } typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, config.useMod, - relevantEvents); + relevantEvents, true); return boost::get(results[0]); }