diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp index ea7c29354..2e0e0ef9f 100644 --- a/src/storm-cli-utilities/cli.cpp +++ b/src/storm-cli-utilities/cli.cpp @@ -1,8 +1,8 @@ #include "cli.h" -#include "storm/utility/resources.h" -#include "storm/utility/file.h" +#include "storm-cli-utilities/resources.h" +#include "storm/io/file.h" #include "storm-version-info/storm-version.h" #include "storm/utility/macros.h" #include "storm/utility/initialize.h" diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 0a0dc28c1..31e287fed 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -6,7 +6,7 @@ #include "storm-parsers/api/storm-parsers.h" #include "storm/utility/SignalHandler.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm/utility/macros.h" #include "storm/utility/NumberTraits.h" #include "storm/utility/Engine.h" diff --git a/src/storm/utility/resources.h b/src/storm-cli-utilities/resources.h similarity index 93% rename from src/storm/utility/resources.h rename to src/storm-cli-utilities/resources.h index 349796acd..a2e0b5ec1 100644 --- a/src/storm/utility/resources.h +++ b/src/storm-cli-utilities/resources.h @@ -1,6 +1,4 @@ -#ifndef STORM_UTILITY_RESOURCES_H_ -#define STORM_UTILITY_RESOURCES_H_ - +#pragma once #include #include #include @@ -55,5 +53,3 @@ namespace storm { } } } - -#endif /* STORM_UTILITY_RESOURCES_H_ */ diff --git a/src/storm-conv/api/storm-conv.cpp b/src/storm-conv/api/storm-conv.cpp index 14c140770..ef5b50a38 100644 --- a/src/storm-conv/api/storm-conv.cpp +++ b/src/storm-conv/api/storm-conv.cpp @@ -7,7 +7,7 @@ #include "storm/storage/jani/JaniScopeChanger.h" #include "storm/storage/jani/JSONExporter.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm/api/properties.h" #include "storm/settings/SettingsManager.h" diff --git a/src/storm-counterexamples/counterexamples/PathCounterexample.cpp b/src/storm-counterexamples/counterexamples/PathCounterexample.cpp index 5d8f18762..4c046065c 100644 --- a/src/storm-counterexamples/counterexamples/PathCounterexample.cpp +++ b/src/storm-counterexamples/counterexamples/PathCounterexample.cpp @@ -1,6 +1,6 @@ #include "storm-counterexamples/counterexamples/PathCounterexample.h" -#include "storm/utility/export.h" +#include "storm/io/export.h" namespace storm { namespace counterexamples { diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index f7a5093a7..9a2546eae 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -90,46 +90,25 @@ void processOptions() { dft = storm::api::applyTransformations(*dft, faultTreeSettings.isUniqueFailedBE(), true); STORM_LOG_DEBUG(dft->getElementsString()); - - dft->setDynamicBehaviorInfo(); - - storm::api::PreprocessingResult preResults; + // Compute minimal number of BE failures leading to system failure and + // maximal number of BE failures not leading to system failure yet. // TODO: always needed? - preResults.lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(*dft, useSMT, solverTimeout); - preResults.upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, useSMT, solverTimeout); - STORM_LOG_DEBUG("BE failure bounds" << std::endl << "========================================" << std::endl << - "Lower bound: " << std::to_string(preResults.lowerBEBound) << std::endl << - "Upper bound: " << std::to_string(preResults.upperBEBound)); - - // TODO: move into API call? - preResults.fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, useSMT, solverTimeout); + auto bounds = storm::api::computeBEFailureBounds(*dft, useSMT, solverTimeout); + STORM_LOG_DEBUG("BE failure bounds: lower bound: " << bounds.first << ", upper bound: " << bounds.second << "."); - if (preResults.fdepConflicts.empty()) { - STORM_LOG_DEBUG("No FDEP conflicts found"); + // Check which FDEPs actually introduce conflicts which need non-deterministic resolution + bool hasConflicts = storm::api::computeDependencyConflicts(*dft, useSMT, solverTimeout); + if (hasConflicts) { + STORM_LOG_DEBUG("FDEP conflicts found."); } else { - STORM_LOG_DEBUG("========================================" << std::endl << "FDEP CONFLICTS" << std::endl << "========================================"); - } - for (auto pair: preResults.fdepConflicts) { - STORM_LOG_DEBUG("Conflict between " << dft->getElement(pair.first)->name() << " and " << dft->getElement(pair.second)->name()); - } - - // Set the conflict map of the dft - std::set conflict_set; - for (auto conflict : preResults.fdepConflicts) { - conflict_set.insert(size_t(conflict.first)); - conflict_set.insert(size_t(conflict.second)); - } - for (size_t depId : dft->getDependencies()) { - if (!conflict_set.count(depId)) { - dft->setDependencyNotInConflict(depId); - } + STORM_LOG_DEBUG("No FDEP conflicts found."); } #ifdef STORM_HAVE_Z3 if (useSMT) { // Solve with SMT - STORM_LOG_DEBUG("Running DFT analysis with use of SMT"); + STORM_LOG_DEBUG("Running DFT analysis with use of SMT."); // Set dynamic behavior vector storm::api::analyzeDFTSMT(*dft, true); } @@ -184,54 +163,16 @@ void processOptions() { // Set relevant event names - std::vector relevantEventNames; - //Possible clash of relevantEvents and disableDC was already considered in FaultTreeSettings::check(). + std::vector additionalRelevantEventNames; if (faultTreeSettings.areRelevantEventsSet()) { - relevantEventNames = faultTreeSettings.getRelevantEvents(); + //Possible clash of relevantEvents and disableDC was already considered in FaultTreeSettings::check(). + additionalRelevantEventNames = faultTreeSettings.getRelevantEvents(); } else if (faultTreeSettings.isDisableDC()) { // All events are relevant - relevantEventNames = {"all"}; + additionalRelevantEventNames = {"all"}; } + std::set relevantEvents = storm::api::computeRelevantEvents(*dft, props, additionalRelevantEventNames); - // Events from properties are relevant as well - // Get necessary labels from properties - std::vector> atomicLabels; - for (auto property : props) { - property->gatherAtomicLabelFormulas(atomicLabels); - } - // Add relevant event names from properties - for (auto atomic : atomicLabels) { - std::string label = atomic->getLabel(); - if (label == "failed" or label == "skipped") { - // Ignore as these label will always be added if necessary - } else { - // Get name of event - if (boost::ends_with(label, "_failed")) { - relevantEventNames.push_back(label.substr(0, label.size() - 7)); - } else if (boost::ends_with(label, "_dc")) { - relevantEventNames.push_back(label.substr(0, label.size() - 3)); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Label '" << label << "' not known."); - } - } - } - - // Set relevant elements - std::set relevantEvents; // Per default no event (except the toplevel event) is relevant - for (std::string const& relevantName : relevantEventNames) { - if (relevantName == "none") { - // Only toplevel event is relevant - relevantEvents = {}; - break; - } else if (relevantName == "all") { - // All events are relevant - relevantEvents = dft->getAllIds(); - break; - } else { - // Find and add corresponding event id - relevantEvents.insert(dft->getIndex(relevantName)); - } - } // Analyze DFT // TODO allow building of state space even without properties diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index 22f7152ef..a14d7d2c7 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -12,17 +12,12 @@ #include "storm-dft/transformations/DftTransformator.h" #include "storm-dft/utility/FDEPConflictFinder.h" #include "storm-dft/utility/FailureBoundFinder.h" +#include "storm-dft/utility/RelevantEvents.h" #include "storm-gspn/api/storm-gspn.h" namespace storm { namespace api { - struct PreprocessingResult { - uint64_t lowerBEBound; - uint64_t upperBEBound; - std::vector> fdepConflicts; - }; - /*! * Load DFT from Galileo file. @@ -92,29 +87,51 @@ namespace storm { return transformedDFT; } - template - bool computeDependencyConflicts(storm::storage::DFT const& dft, bool useSMT, double solverTimeout) { - std::vector> fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, useSMT, solverTimeout); + template + std::pair computeBEFailureBounds(storm::storage::DFT const& dft, bool useSMT, double solverTimeout) { + uint64_t lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(dft, useSMT, solverTimeout); + uint64_t upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(dft, useSMT, solverTimeout); + return std::make_pair(lowerBEBound, upperBEBound); + } - if (fdepConflicts.empty()) { - return false; - } - for (auto pair: fdepConflicts) { + template + bool computeDependencyConflicts(storm::storage::DFT& dft, bool useSMT, double solverTimeout) { + // Initialize which DFT elements have dynamic behavior + dft.setDynamicBehaviorInfo(); + + std::vector> fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(dft, useSMT, solverTimeout); + + for (auto const& pair: fdepConflicts) { STORM_LOG_DEBUG("Conflict between " << dft.getElement(pair.first)->name() << " and " << dft.getElement(pair.second)->name()); } // Set the conflict map of the dft std::set conflict_set; - for (auto conflict : fdepConflicts) { + for (auto const& conflict : fdepConflicts) { conflict_set.insert(size_t(conflict.first)); conflict_set.insert(size_t(conflict.second)); } - for (size_t depId : dft->getDependencies()) { + for (size_t depId : dft.getDependencies()) { if (!conflict_set.count(depId)) { - dft->setDependencyNotInConflict(depId); + dft.setDependencyNotInConflict(depId); } } - return true; + return !fdepConflicts.empty(); + } + + /*! + * Get relevant event ids from given relevant event names and labels in properties. + * + * @param dft DFT. + * @param properties List of properties. All events occurring in a property are relevant. + * @param additionalRelevantEventNames List of names of additional relevant events. + * @return Set of relevant event ids. + */ + template + std::set computeRelevantEvents(storm::storage::DFT const& dft, std::vector> const& properties, std::vector const additionalRelevantEventNames) { + std::vector relevantNames = storm::utility::getRelevantEventNames(dft, properties); + relevantNames.insert(relevantNames.end(), additionalRelevantEventNames.begin(), additionalRelevantEventNames.end()); + return storm::utility::getRelevantEvents(dft, relevantNames); } /*! diff --git a/src/storm-dft/builder/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp index c02fb3364..cf720f2f2 100644 --- a/src/storm-dft/builder/DFTBuilder.cpp +++ b/src/storm-dft/builder/DFTBuilder.cpp @@ -27,14 +27,13 @@ namespace storm { if (itFind != mElements.end()) { // Child found DFTElementPointer childElement = itFind->second; - STORM_LOG_THROW(!childElement->isRestriction(), storm::exceptions::WrongFormatException, - "Restictor " << childElement->name() << " is not allowed as child of gate " - << gate->name()); - if(!childElement->isDependency()) { + if (childElement->isRestriction()) { + STORM_LOG_WARN("Restriction '" << child << "' is not used as input for gate '" << gate->name() << "', because restrictions have no output."); + } else if (childElement->isDependency()) { + STORM_LOG_WARN("Dependency '" << child << "' is not used as input for gate '" << gate->name() << "', because dependencies have no output."); + } else { gate->pushBackChild(childElement); childElement->addParent(gate); - } else { - STORM_LOG_TRACE("Ignore functional dependency " << child << " in gate " << gate->name()); } } else { // Child not found -> find first dependent event to assure that child is dependency @@ -187,8 +186,7 @@ namespace storm { case storm::storage::DFTElementType::SPARE: element = std::make_shared>(mNextId++, name); break; - case storm::storage::DFTElementType::BE_EXP: - case storm::storage::DFTElementType::BE_CONST: + case storm::storage::DFTElementType::BE: case storm::storage::DFTElementType::VOT: case storm::storage::DFTElementType::PDEP: // Handled separately @@ -254,6 +252,9 @@ namespace storm { void DFTBuilder::copyElement(DFTElementPointer element) { std::vector children; switch (element->type()) { + case storm::storage::DFTElementType::BE: + copyBE(std::static_pointer_cast>(element)); + break; case storm::storage::DFTElementType::AND: case storm::storage::DFTElementType::OR: case storm::storage::DFTElementType::PAND: @@ -267,18 +268,6 @@ namespace storm { copyGate(std::static_pointer_cast>(element), children); break; } - case storm::storage::DFTElementType::BE_EXP: - { - auto beExp = std::static_pointer_cast>(element); - addBasicElementExponential(beExp->name(), beExp->activeFailureRate(), beExp->dormancyFactor(), beExp->isTransient()); - break; - } - case storm::storage::DFTElementType::BE_CONST: - { - auto beConst = std::static_pointer_cast>(element); - addBasicElementConst(beConst->name(), beConst->failed()); - break; - } case storm::storage::DFTElementType::PDEP: { DFTDependencyPointer dependency = std::static_pointer_cast>(element); @@ -304,6 +293,27 @@ namespace storm { } } + template + void DFTBuilder::copyBE(DFTBEPointer be) { + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: + { + auto beConst = std::static_pointer_cast>(be); + addBasicElementConst(beConst->name(), beConst->failed()); + break; + } + case storm::storage::BEType::EXPONENTIAL: + { + auto beExp = std::static_pointer_cast>(be); + addBasicElementExponential(beExp->name(), beExp->activeFailureRate(), beExp->dormancyFactor(), beExp->isTransient()); + break; + } + default: + STORM_LOG_ASSERT(false, "BE type not known."); + break; + } + } + template void DFTBuilder::copyGate(DFTGatePointer gate, std::vector const& children) { switch (gate->type()) { diff --git a/src/storm-dft/builder/DFTBuilder.h b/src/storm-dft/builder/DFTBuilder.h index 2529ff5c1..0492d079e 100644 --- a/src/storm-dft/builder/DFTBuilder.h +++ b/src/storm-dft/builder/DFTBuilder.h @@ -25,6 +25,7 @@ namespace storm { using DFTElementPointer = std::shared_ptr>; using DFTElementVector = std::vector; + using DFTBEPointer = std::shared_ptr>; using DFTGatePointer = std::shared_ptr>; using DFTGateVector = std::vector; using DFTDependencyPointer = std::shared_ptr>; @@ -214,6 +215,13 @@ namespace storm { */ void copyElement(DFTElementPointer element); + /** + * Copy BE and insert it again in the builder.i + * + * @param be BE to copy. + */ + void copyBE(DFTBEPointer be); + /** * Copy gate with given children and insert it again in the builder. The current children of the element * are discarded. diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index 1f5f3c18f..d1c46cbed 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -495,6 +495,8 @@ namespace storm { template void ExplicitDFTModelBuilder::buildLabeling() { + bool isAddLabelsClaiming = storm::settings::getModule().isAddLabelsClaiming(); + // Build state labeling modelComponents.stateLabeling = storm::models::sparse::StateLabeling(modelComponents.transitionMatrix.getRowGroupCount()); // Initial state @@ -513,6 +515,17 @@ namespace storm { modelComponents.stateLabeling.addLabel(element->name() + "_dc"); } } + std::vector const>> spares; // Only filled if needed + if (isAddLabelsClaiming) { + // Collect labels for claiming + for (size_t spareId : dft.getSpareIndices()) { + auto const& spare = dft.getGate(spareId); + spares.push_back(spare); + for (auto const& child : spare->children()) { + modelComponents.stateLabeling.addLabel(spare->name() + "_claimed_" + child->name()); + } + } + } // Set labels to states if (this->uniqueFailedState) { @@ -546,6 +559,14 @@ namespace storm { } } } + if (isAddLabelsClaiming) { + for (auto const& spare : spares) { + size_t claimedChildId = dft.uses(state, *stateGenerationInfo, spare->id()); + if (claimedChildId != spare->id()) { + modelComponents.stateLabeling.addLabelToState(spare->name() + "_claimed_" + dft.getElement(claimedChildId)->name(), stateId); + } + } + } } STORM_LOG_TRACE(modelComponents.stateLabeling); @@ -748,8 +769,11 @@ namespace storm { // Consider only still operational BEs if (state->isOperational(id)) { auto be = dft.getBasicElement(id); - switch (be->type()) { - case storm::storage::DFTElementType::BE_EXP: + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: + // Ignore BE which cannot fail + continue; + case storm::storage::BEType::EXPONENTIAL: { // Get BE rate ValueType rate = state->getBERate(id); @@ -765,9 +789,6 @@ namespace storm { rateSum += rate; break; } - case storm::storage::DFTElementType::BE_CONST: - // Ignore BE which cannot fail - continue; default: STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->type() << "' is not known."); break; diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 0844f08f9..ab49cad13 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -26,7 +26,7 @@ namespace storm { size_t constFailedBeCounter = 0; std::shared_ptr const> constFailedBE = nullptr; for (auto &be : mDft.getBasicElements()) { - if (be->type() == storm::storage::DFTElementType::BE_CONST) { + if (be->beType() == storm::storage::BEType::CONSTANT) { auto constBe = std::static_pointer_cast const>(be); if (constBe->failed()) { constFailedBeCounter++; @@ -143,7 +143,8 @@ namespace storm { propagateFailure(newState, nextBE, queues); bool transient = false; - if (nextBE->type() == storm::storage::DFTElementType::BE_EXP) { + // TODO handle for all types of BEs. + if (nextBE->beType() == storm::storage::BEType::EXPONENTIAL) { auto beExp = std::static_pointer_cast const>(nextBE); transient = beExp->isTransient(); } @@ -194,7 +195,7 @@ namespace storm { } else { // Failure is due to "normal" BE failure // Set failure rate according to activation - STORM_LOG_THROW(nextBE->type() == storm::storage::DFTElementType::BE_EXP, storm::exceptions::NotSupportedException, "BE of type '" << nextBE->type() << "' is not supported."); + STORM_LOG_THROW(nextBE->beType() == storm::storage::BEType::EXPONENTIAL, storm::exceptions::NotSupportedException, "BE of type '" << nextBE->type() << "' is not supported."); auto beExp = std::static_pointer_cast const>(nextBE); bool isActive = true; if (mDft.hasRepresentant(beExp->id())) { diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index cdf9fc519..dd7a847ab 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -2,7 +2,7 @@ #include "SmtConstraint.cpp" #include -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm/utility/bitoperations.h" #include "storm-parsers/parser/ExpressionCreator.h" #include "storm/solver/SmtSolver.h" @@ -35,21 +35,30 @@ namespace storm { varNames.push_back("t_" + element->name()); timePointVariables.emplace(i, varNames.size() - 1); switch (element->type()) { - case storm::storage::DFTElementType::BE_EXP: - beVariables.push_back(varNames.size() - 1); - break; - case storm::storage::DFTElementType::BE_CONST: { - STORM_LOG_WARN("Constant BEs are only experimentally supported in the SMT encoding"); - // Constant BEs are initially either failed or failsafe, treat them differently - auto be = std::static_pointer_cast const>(element); - if (be->failed()) { - STORM_LOG_THROW(!failedBeIsSet, storm::exceptions::NotSupportedException, - "DFTs containing more than one constantly failed BE are not supported"); - notFailed = dft.nrBasicElements(); - failedBeVariables = varNames.size() - 1; - failedBeIsSet = true; - } else { - failsafeBeVariables.push_back(varNames.size() - 1); + case storm::storage::DFTElementType::BE: { + auto be = std::static_pointer_cast const>(element); + switch (be->beType()) { + case storm::storage::BEType::EXPONENTIAL: + beVariables.push_back(varNames.size() - 1); + break; + case storm::storage::BEType::CONSTANT: { + STORM_LOG_WARN("Constant BEs are only experimentally supported in the SMT encoding"); + // Constant BEs are initially either failed or failsafe, treat them differently + auto be = std::static_pointer_cast const>(element); + if (be->failed()) { + STORM_LOG_THROW(!failedBeIsSet, storm::exceptions::NotSupportedException, + "DFTs containing more than one constantly failed BE are not supported"); + notFailed = dft.nrBasicElements(); + failedBeVariables = varNames.size() - 1; + failedBeIsSet = true; + } else { + failsafeBeVariables.push_back(varNames.size() - 1); + } + break; + } + default: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "BE type '" << be->beType() << "' not known."); + break; } break; } @@ -146,8 +155,7 @@ namespace storm { } switch (element->type()) { - case storm::storage::DFTElementType::BE_EXP: - case storm::storage::DFTElementType::BE_CONST: + case storm::storage::DFTElementType::BE: // BEs were already considered before break; case storm::storage::DFTElementType::AND: @@ -208,19 +216,17 @@ namespace storm { std::vector> triggerConstraints; for (size_t i = 0; i < dft.nrElements(); ++i) { std::shared_ptr const> element = dft.getElement(i); - if (element->type() == storm::storage::DFTElementType::BE_CONST) { + if (element->isBasicElement()) { auto be = std::static_pointer_cast const>(element); - triggerConstraints.clear(); - for (auto const &dependency : be->ingoingDependencies()) { - triggerConstraints.push_back(std::make_shared( - timePointVariables.at(dependency->triggerEvent()->id()), notFailed)); - } - if (!triggerConstraints.empty()) { - constraints.push_back(std::make_shared( - std::make_shared(timePointVariables.at(be->id()), notFailed), - std::make_shared(triggerConstraints))); - constraints.back()->setDescription( - "Failsafe BE " + be->name() + " stays failsafe if no trigger fails"); + if (be->beType() == storm::storage::BEType::CONSTANT) { + triggerConstraints.clear(); + for (auto const &dependency : be->ingoingDependencies()) { + triggerConstraints.push_back(std::make_shared(timePointVariables.at(dependency->triggerEvent()->id()), notFailed)); + } + if (!triggerConstraints.empty()) { + constraints.push_back(std::make_shared(std::make_shared(timePointVariables.at(be->id()), notFailed), std::make_shared(triggerConstraints))); + constraints.back()->setDescription("Failsafe BE " + be->name() + " stays failsafe if no trigger fails"); + } } } } diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 8ca404609..00907ca7a 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -5,7 +5,7 @@ #include "storm/builder/ParallelCompositionBuilder.h" #include "storm/exceptions/UnmetRequirementException.h" #include "storm/utility/bitoperations.h" -#include "storm/utility/DirectEncodingExporter.h" +#include "storm/io/DirectEncodingExporter.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/models/ModelType.h" diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp index b387a1a1a..9e7e5f146 100644 --- a/src/storm-dft/parser/DFTGalileoParser.cpp +++ b/src/storm-dft/parser/DFTGalileoParser.cpp @@ -11,7 +11,7 @@ #include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/utility/macros.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" namespace storm { namespace parser { diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 0cda7ff08..a94332e37 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -10,7 +10,7 @@ #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/NotSupportedException.h" #include "storm/utility/macros.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm-parsers/parser/ValueParser.h" namespace storm { diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.cpp b/src/storm-dft/settings/modules/FaultTreeSettings.cpp index 5a6cc7243..917c2e299 100644 --- a/src/storm-dft/settings/modules/FaultTreeSettings.cpp +++ b/src/storm-dft/settings/modules/FaultTreeSettings.cpp @@ -21,6 +21,7 @@ namespace storm { const std::string FaultTreeSettings::disableDCOptionName = "disabledc"; const std::string FaultTreeSettings::allowDCRelevantOptionName = "allowdcrelevant"; const std::string FaultTreeSettings::relevantEventsOptionName = "relevantevents"; + const std::string FaultTreeSettings::addLabelsClaimingOptionName = "labels-claiming"; const std::string FaultTreeSettings::approximationErrorOptionName = "approximation"; const std::string FaultTreeSettings::approximationErrorOptionShortName = "approx"; const std::string FaultTreeSettings::approximationHeuristicOptionName = "approximationheuristic"; @@ -40,9 +41,11 @@ namespace storm { "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 names of relevant events. 'all' marks all events as relevant, The default '' or 'none' marks only the top level event as relevant.").setDefaultValueString( + "A comma separated list of names of relevant events. 'all' marks all events as relevant, The default '' 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, addLabelsClaimingOptionName, false, + "Add labels representing claiming operations.").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( @@ -86,6 +89,10 @@ namespace storm { return storm::parser::parseCommaSeperatedValues(this->getOption(relevantEventsOptionName).getArgumentByName("values").getValueAsString()); } + bool FaultTreeSettings::isAddLabelsClaiming() const { + return this->getOption(addLabelsClaimingOptionName).getHasOptionBeenSet(); + } + bool FaultTreeSettings::isApproximationErrorSet() const { return this->getOption(approximationErrorOptionName).getHasOptionBeenSet(); } diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.h b/src/storm-dft/settings/modules/FaultTreeSettings.h index 3099f4b8b..91fd452c8 100644 --- a/src/storm-dft/settings/modules/FaultTreeSettings.h +++ b/src/storm-dft/settings/modules/FaultTreeSettings.h @@ -61,6 +61,13 @@ namespace storm { */ std::vector getRelevantEvents() const; + /*! + * Retrieves whether the labels for claimings should be added in the Markov chain. + * + * @return True iff the option was set. + */ + bool isAddLabelsClaiming() const; + /*! * Retrieves whether the option to compute an approximation is set. * @@ -136,6 +143,7 @@ namespace storm { static const std::string disableDCOptionName; static const std::string allowDCRelevantOptionName; static const std::string relevantEventsOptionName; + static const std::string addLabelsClaimingOptionName; 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 6b79e1c1e..75d43eb47 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -206,8 +206,6 @@ namespace storm { break; } //BEs - case storage::DFTElementType::BE_EXP: - case storage::DFTElementType::BE_CONST: case storage::DFTElementType::BE: { auto be = std::static_pointer_cast>(currentElement); dynamicBehaviorVector[be->id()] = true; @@ -506,8 +504,7 @@ namespace storm { case DFTElementType::OR: builder.addOrElement(newParentName, childrenNames); break; - case DFTElementType::BE_EXP: - case DFTElementType::BE_CONST: + case DFTElementType::BE: case DFTElementType::VOT: case DFTElementType::PAND: case DFTElementType::SPARE: @@ -548,8 +545,7 @@ namespace storm { case DFTElementType::AND: case DFTElementType::OR: case DFTElementType::VOT: - case DFTElementType::BE_EXP: - case DFTElementType::BE_CONST: + case DFTElementType::BE: break; case DFTElementType::PAND: case DFTElementType::SPARE: @@ -577,8 +573,7 @@ namespace storm { case DFTElementType::VOT: ++noStatic; break; - case DFTElementType::BE_EXP: - case DFTElementType::BE_CONST: + case DFTElementType::BE: case DFTElementType::PAND: case DFTElementType::SPARE: case DFTElementType::POR: @@ -701,13 +696,7 @@ namespace storm { stream << storm::storage::toChar(DFTState::getElementState(status, stateGenerationInfo, elem->id())); if (elem->isSpareGate()) { stream << "["; - size_t nrUsedChild = status.getAsInt(stateGenerationInfo.getSpareUsageIndex(elem->id()), stateGenerationInfo.usageInfoBits()); - size_t useId; - if (nrUsedChild == getMaxSpareChildCount()) { - useId = elem->id(); - } else { - useId = getChild(elem->id(), nrUsedChild); - } + size_t useId = this->uses(status, stateGenerationInfo, elem->id()); if (useId == elem->id() || status[stateGenerationInfo.getSpareActivationIndex(useId)]) { stream << "actively "; } @@ -765,14 +754,17 @@ namespace storm { // Check independence of spare modules // TODO: comparing one element of each spare module sufficient? for (auto module1 = mSpareModules.begin(); module1 != mSpareModules.end(); ++module1) { - size_t firstElement = module1->second.front(); - for (auto module2 = std::next(module1); module2 != mSpareModules.end(); ++module2) { - if (std::find(module2->second.begin(), module2->second.end(), firstElement) != module2->second.end()) { - if (!wellformed) { - stream << std::endl; + if (!module1->second.empty()) { + // Empty modules are allowed for the primary module of a spare gate + size_t firstElement = module1->second.front(); + for (auto module2 = std::next(module1); module2 != mSpareModules.end(); ++module2) { + if (std::find(module2->second.begin(), module2->second.end(), firstElement) != module2->second.end()) { + if (!wellformed) { + stream << std::endl; + } + stream << "Spare modules of '" << getElement(module1->first)->name() << "' and '" << getElement(module2->first)->name() << "' should not overlap."; + wellformed = false; } - stream << "Spare modules of '" << getElement(module1->first)->name() << "' and '" << getElement(module2->first)->name() << "' should not overlap."; - wellformed = false; } } } @@ -1089,8 +1081,7 @@ namespace storm { size_t noRestriction = 0; for (auto const& elem : mElements) { switch (elem->type()) { - case DFTElementType::BE_EXP: - case DFTElementType::BE_CONST: + case DFTElementType::BE: ++noBE; break; case DFTElementType::AND: diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index c7c790350..9f5ecdea4 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -160,17 +160,17 @@ namespace storm { if (elem->isBasicElement()) { std::shared_ptr> be = std::static_pointer_cast>(elem); if (be->canFail()) { - switch (be->type()) { - case storm::storage::DFTElementType::BE_EXP: { + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: + result.push_back(be->id()); + break; + case storm::storage::BEType::EXPONENTIAL: { auto beExp = std::static_pointer_cast>(be); if (!beExp->isColdBasicElement()) { result.push_back(be->id()); } break; } - case storm::storage::DFTElementType::BE_CONST: - result.push_back(be->id()); - break; default: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "BE type '" << be->type() << "' is not supported."); } @@ -287,7 +287,25 @@ namespace storm { bool isFailsafe(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo) const { return storm::storage::DFTState::isFailsafe(state, stateGenerationInfo.getStateIndex(mTopLevelIndex)); } - + + /*! + * Return id of used child for a given spare gate. + * If no child is used the id of the spare gate is returned. + * + * @param state DFT state. + * @param stateGenerationInfo State generation information. + * @param id Id of spare gate. + * @return Id of used child. Id of spare gate if no child is used. + */ + size_t uses(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) const { + size_t nrUsedChild = storm::storage::DFTState::usesIndex(state, stateGenerationInfo, id); + if (nrUsedChild == getMaxSpareChildCount()) { + return id; + } else { + return getChild(id, nrUsedChild); + } + } + size_t getChild(size_t spareId, size_t nrUsedChild) const; size_t getNrChild(size_t spareId, size_t childId) const; diff --git a/src/storm-dft/storage/dft/DFTElementType.h b/src/storm-dft/storage/dft/DFTElementType.h index c76b071fe..fe0031c79 100644 --- a/src/storm-dft/storage/dft/DFTElementType.h +++ b/src/storm-dft/storage/dft/DFTElementType.h @@ -9,9 +9,8 @@ namespace storm { * Element types in a DFT. */ enum class DFTElementType { - BE_EXP, BE_CONST, - AND, OR, VOT, BE, + AND, OR, VOT, PAND, POR, SPARE, @@ -20,6 +19,16 @@ namespace storm { MUTEX }; + /*! + * BE types in a DFT. + */ + enum class BEType { + CONSTANT, + EXPONENTIAL, + SAMPLES + }; + + inline bool isGateType(DFTElementType const& type) { switch (type) { case DFTElementType::AND: @@ -29,8 +38,7 @@ namespace storm { case DFTElementType::POR: case DFTElementType::SPARE: return true; - case DFTElementType::BE_EXP: - case DFTElementType::BE_CONST: + case DFTElementType::BE: case DFTElementType::PDEP: case DFTElementType::SEQ: case DFTElementType::MUTEX: @@ -60,12 +68,10 @@ namespace storm { } } - inline std::string toString(DFTElementType const& tp) { - switch (tp) { - case DFTElementType::BE_EXP: - return "BE_EXP"; - case DFTElementType::BE_CONST: - return "BE_CONST"; + inline std::string toString(DFTElementType const& type) { + switch (type) { + case DFTElementType::BE: + return "BE"; case DFTElementType::AND: return "AND"; case DFTElementType::OR: @@ -90,9 +96,25 @@ namespace storm { } } + inline std::string toString(BEType const& type) { + switch (type) { + case BEType::CONSTANT: + return "CONST"; + case BEType::EXPONENTIAL: + return "EXPONENTIAL"; + default: + STORM_LOG_ASSERT(false, "BE type not known."); + return ""; + } + } + inline std::ostream& operator<<(std::ostream& os, DFTElementType const& type) { return os << toString(type); } + inline std::ostream& operator<<(std::ostream& os, BEType const& type) { + return os << toString(type); + } + } } diff --git a/src/storm-dft/storage/dft/DFTElements.h b/src/storm-dft/storage/dft/DFTElements.h index 36d671703..ab605e3e5 100644 --- a/src/storm-dft/storage/dft/DFTElements.h +++ b/src/storm-dft/storage/dft/DFTElements.h @@ -1,13 +1,18 @@ #pragma once -#include "storm-dft/storage/dft/elements/BEExponential.h" +// BE types #include "storm-dft/storage/dft/elements/BEConst.h" +#include "storm-dft/storage/dft/elements/BEExponential.h" +#include "storm-dft/storage/dft/elements/BESamples.h" + +// Gates #include "storm-dft/storage/dft/elements/DFTAnd.h" -#include "storm-dft/storage/dft/elements/DFTDependency.h" -#include "storm-dft/storage/dft/elements/DFTMutex.h" #include "storm-dft/storage/dft/elements/DFTOr.h" +#include "storm-dft/storage/dft/elements/DFTVot.h" #include "storm-dft/storage/dft/elements/DFTPand.h" #include "storm-dft/storage/dft/elements/DFTPor.h" -#include "storm-dft/storage/dft/elements/DFTSeq.h" #include "storm-dft/storage/dft/elements/DFTSpare.h" -#include "storm-dft/storage/dft/elements/DFTVot.h" + +#include "storm-dft/storage/dft/elements/DFTDependency.h" +#include "storm-dft/storage/dft/elements/DFTSeq.h" +#include "storm-dft/storage/dft/elements/DFTMutex.h" diff --git a/src/storm-dft/storage/dft/DFTIsomorphism.h b/src/storm-dft/storage/dft/DFTIsomorphism.h index 34287b540..701082443 100644 --- a/src/storm-dft/storage/dft/DFTIsomorphism.h +++ b/src/storm-dft/storage/dft/DFTIsomorphism.h @@ -57,15 +57,15 @@ namespace storage { BEColourClass() = default; - BEColourClass(storm::storage::DFTElementType t, ValueType a, ValueType p, size_t h) : type(t), hash(h), aRate(a), pRate(p) { - STORM_LOG_ASSERT(t == storm::storage::DFTElementType::BE_EXP, "Expected type BE_EXP but got type " << t); + BEColourClass(storm::storage::BEType t, ValueType a, ValueType p, size_t h) : type(t), hash(h), aRate(a), pRate(p) { + STORM_LOG_ASSERT(t == storm::storage::BEType::EXPONENTIAL, "Expected type EXPONENTIAL but got type " << t); } - BEColourClass(storm::storage::DFTElementType t, bool fail, size_t h) : type(t), hash(h), failed(fail) { - STORM_LOG_ASSERT(t == storm::storage::DFTElementType::BE_CONST, "Expected type BE_CONST but got type " << t); + BEColourClass(storm::storage::BEType t, bool fail, size_t h) : type(t), hash(h), failed(fail) { + STORM_LOG_ASSERT(t == storm::storage::BEType::CONSTANT, "Expected type CONSTANT but got type " << t); } - storm::storage::DFTElementType type; + storm::storage::BEType type; size_t hash; ValueType aRate; ValueType pRate; @@ -79,9 +79,9 @@ namespace storage { return false; } switch (lhs.type) { - case storm::storage::DFTElementType::BE_EXP: + case storm::storage::BEType::EXPONENTIAL: return lhs.hash == rhs.hash && lhs.aRate == rhs.aRate && lhs.pRate == rhs.pRate; - case storm::storage::DFTElementType::BE_CONST: + case storm::storage::BEType::CONSTANT: return lhs.hash == rhs.hash && lhs.failed == rhs.failed; default: STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << lhs.type << "' is not known."); @@ -271,21 +271,21 @@ namespace storage { protected: void colourize(std::shared_ptr> const& be) { - switch (be->type()) { - case storm::storage::DFTElementType::BE_EXP: + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: { - auto beExp = std::static_pointer_cast const>(be); - beColour[beExp->id()] = BEColourClass(beExp->type(), beExp->activeFailureRate(), beExp->passiveFailureRate(), beExp->nrParents()); + auto beConst = std::static_pointer_cast const>(be); + beColour[beConst->id()] = BEColourClass(beConst->beType(), beConst->failed(), beConst->nrParents()); break; } - case storm::storage::DFTElementType::BE_CONST: + case storm::storage::BEType::EXPONENTIAL: { - auto beConst = std::static_pointer_cast const>(be); - beColour[beConst->id()] = BEColourClass(beConst->type(), beConst->failed(), beConst->nrParents()); + auto beExp = std::static_pointer_cast const>(be); + beColour[beExp->id()] = BEColourClass(beExp->beType(), beExp->activeFailureRate(), beExp->passiveFailureRate(), beExp->nrParents()); break; } default: - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->type() << "' is not known."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->beType() << "' is not known."); break; } } @@ -299,21 +299,21 @@ namespace storage { void colourize(std::shared_ptr> const& dep) { // TODO this can be improved for n-ary dependencies. std::shared_ptr const> be = dep->dependentEvents()[0]; - switch (be->type()) { - case storm::storage::DFTElementType::BE_EXP: + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: { - auto beExp = std::static_pointer_cast const>(be); - depColour[dep->id()] = std::pair(dep->probability(), beExp->activeFailureRate()); + auto beConst = std::static_pointer_cast const>(be); + depColour[dep->id()] = std::pair(dep->probability(), beConst->failed() ? storm::utility::one() : storm::utility::zero()); break; } - case storm::storage::DFTElementType::BE_CONST: + case storm::storage::BEType::EXPONENTIAL: { - auto beConst = std::static_pointer_cast const>(be); - depColour[dep->id()] = std::pair(dep->probability(), beConst->failed() ? storm::utility::one() : storm::utility::zero()); + auto beExp = std::static_pointer_cast const>(be); + depColour[dep->id()] = std::pair(dep->probability(), beExp->activeFailureRate()); break; } default: - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->type() << "' is not known."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->beType() << "' is not known."); break; } } @@ -706,10 +706,10 @@ namespace std { groupHash |= (static_cast(bcc.type) & fivebitmask) << (62 - 5); switch (bcc.type) { - case storm::storage::DFTElementType::BE_EXP: - return (hasher(bcc.aRate) ^ hasher(bcc.pRate) << 8); - case storm::storage::DFTElementType::BE_CONST: + case storm::storage::BEType::CONSTANT: return (bcc.failed << 8); + case storm::storage::BEType::EXPONENTIAL: + return (hasher(bcc.aRate) ^ hasher(bcc.pRate) << 8); default: STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << bcc.type << "' is not known."); break; diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp index 082b4e8a6..4be919435 100644 --- a/src/storm-dft/storage/dft/DFTState.cpp +++ b/src/storm-dft/storage/dft/DFTState.cpp @@ -49,8 +49,12 @@ namespace storm { if (mDft.isBasicElement(index) && isOperational(index) && !isEventDisabledViaRestriction(index)) { std::shared_ptr> be = mDft.getBasicElement(index); if (be->canFail()) { - switch (be->type()) { - case storm::storage::DFTElementType::BE_EXP: + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: + failableElements.addBE(index); + STORM_LOG_TRACE("Currently failable: " << *be); + break; + case storm::storage::BEType::EXPONENTIAL: { auto beExp = std::static_pointer_cast const>(be); if (!beExp->isColdBasicElement() || !mDft.hasRepresentant(index) || isActive(mDft.getRepresentant(index))) { @@ -59,10 +63,6 @@ namespace storm { } break; } - case storm::storage::DFTElementType::BE_CONST: - failableElements.addBE(index); - STORM_LOG_TRACE("Currently failable: " << *be); - break; default: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "BE type '" << be->type() << "' is not supported."); break; @@ -315,7 +315,7 @@ namespace storm { template ValueType DFTState::getBERate(size_t id) const { STORM_LOG_ASSERT(mDft.isBasicElement(id), "Element is no BE."); - STORM_LOG_THROW(mDft.getBasicElement(id)->type() == storm::storage::DFTElementType::BE_EXP, storm::exceptions::NotSupportedException, "BE of type '" << mDft.getBasicElement(id)->type() << "' is not supported."); + STORM_LOG_THROW(mDft.getBasicElement(id)->beType() == storm::storage::BEType::EXPONENTIAL, storm::exceptions::NotSupportedException, "BE of type '" << mDft.getBasicElement(id)->type() << "' is not supported."); auto beExp = std::static_pointer_cast const>(mDft.getBasicElement(id)); if (mDft.hasRepresentant(id) && !isActive(mDft.getRepresentant(id))) { // Return passive failure rate @@ -380,8 +380,11 @@ namespace storm { if(mDft.isBasicElement(elem) && isOperational(elem) && !isEventDisabledViaRestriction(elem)) { std::shared_ptr> be = mDft.getBasicElement(elem); if (be->canFail()) { - switch (be->type()) { - case storm::storage::DFTElementType::BE_EXP: { + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: + // Nothing to do + break; + case storm::storage::BEType::EXPONENTIAL: { auto beExp = std::static_pointer_cast const>(be); if (beExp->isColdBasicElement()) { // Add to failable BEs @@ -389,9 +392,6 @@ namespace storm { } break; } - case storm::storage::DFTElementType::BE_CONST: - // Nothing to do - break; default: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "BE type '" << be->type() << "' is not supported."); } @@ -412,6 +412,11 @@ namespace storm { } } + template + uint_fast64_t DFTState::usesIndex(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) { + return state.getAsInt(stateGenerationInfo.getSpareUsageIndex(id), stateGenerationInfo.usageInfoBits()); + } + template uint_fast64_t DFTState::extractUses(size_t from) const { STORM_LOG_ASSERT(mStateGenerationInfo.usageInfoBits() < 64, "UsageInfoBit size too large."); diff --git a/src/storm-dft/storage/dft/DFTState.h b/src/storm-dft/storage/dft/DFTState.h index 9eb425d7e..9ebe12dba 100644 --- a/src/storm-dft/storage/dft/DFTState.h +++ b/src/storm-dft/storage/dft/DFTState.h @@ -259,6 +259,17 @@ namespace storm { * the spare. */ uint_fast64_t uses(size_t id) const; + + /** + * Returns the index of the used child for a spare gate. + * If no element is used, the maximal spare count is returned. + * + * @param state DFT state. + * @param stateGenerationInfo State generation info. + * @param id Id of spare gate. + * @return Index of used child. Maximal spare count if no child is usde. + */ + static uint_fast64_t usesIndex(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo, size_t id); /** * This method is commonly used to get the usage information for spares. diff --git a/src/storm-dft/storage/dft/DftJsonExporter.cpp b/src/storm-dft/storage/dft/DftJsonExporter.cpp index 506536ee5..c0a5bf2cb 100644 --- a/src/storm-dft/storage/dft/DftJsonExporter.cpp +++ b/src/storm-dft/storage/dft/DftJsonExporter.cpp @@ -1,6 +1,6 @@ #include "DftJsonExporter.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm/exceptions/NotSupportedException.h" #include @@ -88,8 +88,16 @@ namespace storm { } else if (element->isBasicElement()) { std::shared_ptr const> be = std::static_pointer_cast const>(element); // Set BE specific data - switch (element->type()) { - case storm::storage::DFTElementType::BE_EXP: + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: + { + auto beConst = std::static_pointer_cast const>(be); + std::stringstream stream; + nodeData["distribution"] = "const"; + nodeData["failed"] = beConst->failed(); + break; + } + case storm::storage::BEType::EXPONENTIAL: { auto beExp = std::static_pointer_cast const>(be); std::stringstream stream; @@ -101,16 +109,8 @@ namespace storm { nodeData["dorm"] = stream.str(); break; } - case storm::storage::DFTElementType::BE_CONST: - { - auto beConst = std::static_pointer_cast const>(be); - std::stringstream stream; - nodeData["distribution"] = "const"; - nodeData["failed"] = beConst->failed(); - break; - } default: - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->type() << "' is not known."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->beType() << "' is not known."); break; } } else { diff --git a/src/storm-dft/storage/dft/elements/BEConst.cpp b/src/storm-dft/storage/dft/elements/BEConst.cpp new file mode 100644 index 000000000..cb2457a04 --- /dev/null +++ b/src/storm-dft/storage/dft/elements/BEConst.cpp @@ -0,0 +1,16 @@ +#include "BEConst.h" + +namespace storm { + namespace storage { + + template + ValueType BEConst::getUnreliability(ValueType time) const { + return failed() ? storm::utility::one() : storm::utility::zero(); + } + + // Explicitly instantiate the class. + template class BEConst; + template class BEConst; + + } // namespace storage +} // namespace storm diff --git a/src/storm-dft/storage/dft/elements/BEConst.h b/src/storm-dft/storage/dft/elements/BEConst.h index 2cbf9fd38..6c82f19a4 100644 --- a/src/storm-dft/storage/dft/elements/BEConst.h +++ b/src/storm-dft/storage/dft/elements/BEConst.h @@ -23,8 +23,8 @@ namespace storm { // Intentionally empty } - DFTElementType type() const override { - return DFTElementType::BE_CONST; + BEType beType() const override { + return BEType::CONSTANT; } /*! @@ -39,8 +39,10 @@ namespace storm { return this->failed(); } + ValueType getUnreliability(ValueType time) const override; + bool isTypeEqualTo(DFTElement const& other) const override { - if (!DFTElement::isTypeEqualTo(other)) { + if (!DFTBE::isTypeEqualTo(other)) { return false; } auto& otherBE = static_cast const&>(other); diff --git a/src/storm-dft/storage/dft/elements/BEExponential.cpp b/src/storm-dft/storage/dft/elements/BEExponential.cpp new file mode 100644 index 000000000..a93113e31 --- /dev/null +++ b/src/storm-dft/storage/dft/elements/BEExponential.cpp @@ -0,0 +1,24 @@ +#include "BEExponential.h" + +#include "storm/exceptions/NotSupportedException.h" + +namespace storm { + namespace storage { + + template <> + double BEExponential::getUnreliability(double time) const { + // 1 - e^(-lambda * t) + return 1 - exp(-this->activeFailureRate() * time); + } + + template + ValueType BEExponential::getUnreliability(ValueType time) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Computing cumulative failure probability not supported for this data type."); + } + + // Explicitly instantiate the class. + template class BEExponential; + template class BEExponential; + + } +} diff --git a/src/storm-dft/storage/dft/elements/BEExponential.h b/src/storm-dft/storage/dft/elements/BEExponential.h index 1ed6221d6..f52d204bd 100644 --- a/src/storm-dft/storage/dft/elements/BEExponential.h +++ b/src/storm-dft/storage/dft/elements/BEExponential.h @@ -25,8 +25,8 @@ namespace storm { STORM_LOG_ASSERT(!storm::utility::isZero(failureRate), "Exponential failure rate should not be zero."); } - DFTElementType type() const override { - return DFTElementType::BE_EXP; + BEType beType() const override { + return BEType::EXPONENTIAL; } /*! @@ -50,14 +50,12 @@ namespace storm { * @return Dormancy factor. */ ValueType dormancyFactor() const { - if (storm::utility::isZero(this->activeFailureRate())) { - // Return default value of 1 - return storm::utility::one(); - } else { - return this->passiveFailureRate() / this->activeFailureRate(); - } + STORM_LOG_ASSERT(!storm::utility::isZero(this->activeFailureRate()), "Active failure rate of non-const BE should not be zero."); + return this->passiveFailureRate() / this->activeFailureRate(); } + ValueType getUnreliability(ValueType time) const override; + /*! * Return whether the BE experiences transient failures. * @return True iff BE is transient. @@ -80,7 +78,7 @@ namespace storm { } bool isTypeEqualTo(DFTElement const& other) const override { - if (!DFTElement::isTypeEqualTo(other)) { + if (!DFTBE::isTypeEqualTo(other)) { return false; } auto& otherBE = static_cast const&>(other); diff --git a/src/storm-dft/storage/dft/elements/BESamples.cpp b/src/storm-dft/storage/dft/elements/BESamples.cpp new file mode 100644 index 000000000..3fb6ec462 --- /dev/null +++ b/src/storm-dft/storage/dft/elements/BESamples.cpp @@ -0,0 +1,20 @@ +#include "BESamples.h" + +#include "storm/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace storage { + + template + ValueType BESamples::getUnreliability(ValueType time) const { + auto iter = mActiveSamples.find(time); + STORM_LOG_THROW(iter!= mActiveSamples.end(), storm::exceptions::InvalidArgumentException, "No sample for time point " << time << " given."); + return iter->second; + } + + // Explicitly instantiate the class. + template class BESamples; + template class BESamples; + + } +} diff --git a/src/storm-dft/storage/dft/elements/BESamples.h b/src/storm-dft/storage/dft/elements/BESamples.h new file mode 100644 index 000000000..79bc0b2c7 --- /dev/null +++ b/src/storm-dft/storage/dft/elements/BESamples.h @@ -0,0 +1,74 @@ +#pragma once + +#include "DFTBE.h" + +#include + +namespace storm { + namespace storage { + + /*! + * BE where the failure distribution is defined by samples. + * A sample defines the unreliability at a time point (i.e. the cumulative distribution function F(x)). + */ + template + class BESamples : public DFTBE { + + public: + /*! + * Constructor. + * @param id Id. + * @param name Name. + * @param activeSamples Samples defining unreliability in active state for certain time points. + */ + BESamples(size_t id, std::string const& name, std::map activeSamples) : + DFTBE(id, name), mActiveSamples(activeSamples) { + STORM_LOG_ASSERT(activeSamples.size() > 0, "At least one sample should be given."); + STORM_LOG_ASSERT(this->canFail(), "At least one sample should have a non-zero probability."); + } + + BEType beType() const override { + return BEType::SAMPLES; + } + + /*! + * Return samples defining unreliability in active state. + * @return Samples for active state. + */ + std::map const& activeSamples() const { + return mActiveSamples; + } + + ValueType getUnreliability(ValueType time) const override; + + bool canFail() const override { + // At least one sample is not zero + for (auto const& sample : mActiveSamples) { + if (!storm::utility::isZero(sample.second)) { + return true; + } + } + return true; + } + + bool isTypeEqualTo(DFTElement const& other) const override { + if (!DFTBE::isTypeEqualTo(other)) { + return false; + } + + auto& otherBE = static_cast const&>(other); + return mActiveSamples.size() == otherBE.activeSamples().size() && std::equal(mActiveSamples.begin(), mActiveSamples.end(), otherBE.activeSamples().begin()); + } + + std::string toString() const override { + std::stringstream stream; + stream << "{" << this->name() << "} BE samples(" << this->activeSamples().size() << " samples)"; + return stream.str(); + } + + private: + std::map mActiveSamples; + }; + + } +} diff --git a/src/storm-dft/storage/dft/elements/DFTBE.cpp b/src/storm-dft/storage/dft/elements/DFTBE.cpp new file mode 100644 index 000000000..369039547 --- /dev/null +++ b/src/storm-dft/storage/dft/elements/DFTBE.cpp @@ -0,0 +1,33 @@ +#include "DFTBE.h" + +#include "storm-dft/storage/dft/elements/DFTGate.h" +#include "storm-dft/storage/dft/elements/DFTDependency.h" + +namespace storm { + namespace storage { + + template + void DFTBE::extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const { + if (elemsInSubtree.count(this->id())) { + return; + } + DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); + if (elemsInSubtree.empty()) { + // Parent in the subDFT, i.e., it is *not* a subDFT + return; + } + for (auto const& inDep : ingoingDependencies()) { + inDep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); + if (elemsInSubtree.empty()) { + // Parent in the subDFT, i.e., it is *not* a subDFT + return; + } + } + } + + // Explicitly instantiate the class. + template class DFTBE; + template class DFTBE; + + } +} diff --git a/src/storm-dft/storage/dft/elements/DFTBE.h b/src/storm-dft/storage/dft/elements/DFTBE.h index 38eeb4de1..80f8d77e3 100644 --- a/src/storm-dft/storage/dft/elements/DFTBE.h +++ b/src/storm-dft/storage/dft/elements/DFTBE.h @@ -22,10 +22,29 @@ namespace storm { // Intentionally empty } + DFTElementType type() const override { + return DFTElementType::BE; + } + + /*! + * Get type of BE (constant, exponential, etc.). + * @return BE type. + */ + virtual BEType beType() const = 0; + size_t nrChildren() const override { return 0; } + /*! + * Return the unreliability of the BE up to the given time point. + * Computes the cumulative distribution function F(x) for time x. + * Note that the computation assumes the BE is always active. + * + * @return Cumulative failure probability. + */ + virtual ValueType getUnreliability(ValueType time) const = 0; + /*! * Return whether the BE can fail. * @return True iff BE is not failsafe. @@ -63,23 +82,7 @@ namespace storm { return true; } - void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override { - if (elemsInSubtree.count(this->id())) { - return; - } - DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); - if (elemsInSubtree.empty()) { - // Parent in the subDFT, i.e., it is *not* a subDFT - return; - } - for (auto const& inDep : ingoingDependencies()) { - inDep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); - if (elemsInSubtree.empty()) { - // Parent in the subDFT, i.e., it is *not* a subDFT - return; - } - } - } + void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override; bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { if (DFTElement::checkDontCareAnymore(state, queues)) { @@ -89,6 +92,14 @@ namespace storm { return false; } + bool isTypeEqualTo(DFTElement const& other) const override { + if (!DFTElement::isTypeEqualTo(other)) { + return false; + } + auto& otherBE = static_cast const&>(other); + return this->beType() == otherBE.beType(); + } + private: std::vector>> mIngoingDependencies; diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index 60a4d04e5..7a57fe8fa 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -122,11 +122,8 @@ namespace storm { // Check which type the element is and call the corresponding translate-function. switch (dftElement->type()) { - case storm::storage::DFTElementType::BE_EXP: - translateBEExponential(std::static_pointer_cast const>(dftElement)); - break; - case storm::storage::DFTElementType::BE_CONST: - translateBEConst(std::static_pointer_cast const>(dftElement)); + case storm::storage::DFTElementType::BE: + translateBE(std::static_pointer_cast const>(dftElement)); break; case storm::storage::DFTElementType::AND: translateAND(std::static_pointer_cast const>(dftElement)); @@ -167,6 +164,21 @@ namespace storm { } + template + void DftToGspnTransformator::translateBE(std::shared_ptr const> dftBE) { + switch (dftBE->beType()) { + case storm::storage::BEType::CONSTANT: + translateBEConst(std::static_pointer_cast const>(dftBE)); + break; + case storm::storage::BEType::EXPONENTIAL: + translateBEExponential(std::static_pointer_cast const>(dftBE)); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE type '" << dftBE->beType() << "' not known."); + break; + } + } + template void DftToGspnTransformator::translateBEExponential(std::shared_ptr const> dftBE) { double xcenter = mDft.getElementLayoutInfo(dftBE->id()).x; diff --git a/src/storm-dft/transformations/DftToGspnTransformator.h b/src/storm-dft/transformations/DftToGspnTransformator.h index 72b6d1831..d54687bea 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.h +++ b/src/storm-dft/transformations/DftToGspnTransformator.h @@ -61,6 +61,13 @@ namespace storm { */ void translateGSPNElements(); + /*! + * Translate a BE. + * + * @param dftBE The basic event. + */ + void translateBE(std::shared_ptr const> dftBE); + /*! * Translate an exponential BE. * diff --git a/src/storm-dft/transformations/DftTransformator.cpp b/src/storm-dft/transformations/DftTransformator.cpp index 6dcbdf17c..ea62a686c 100644 --- a/src/storm-dft/transformations/DftTransformator.cpp +++ b/src/storm-dft/transformations/DftTransformator.cpp @@ -20,22 +20,28 @@ namespace storm { for (size_t i = 0; i < dft.nrElements(); ++i) { std::shared_ptr const> element = dft.getElement(i); switch (element->type()) { - case storm::storage::DFTElementType::BE_EXP: { - auto be_exp = std::static_pointer_cast const>( - element); - builder.addBasicElementExponential(be_exp->name(), be_exp->activeFailureRate(), - be_exp->dormancyFactor()); - break; - } - case storm::storage::DFTElementType::BE_CONST: { - auto be_const = std::static_pointer_cast const>( - element); - if (be_const->canFail()) { - STORM_LOG_TRACE("Transform " + element->name() + " [BE (const failed)]"); - failedBEs.push_back(be_const->name()); + case storm::storage::DFTElementType::BE: { + auto be = std::static_pointer_cast const>(element); + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: { + auto beConst = std::static_pointer_cast const>(element); + if (beConst->canFail()) { + STORM_LOG_TRACE("Transform " + beConst->name() + " [BE (const failed)]"); + failedBEs.push_back(beConst->name()); + } + // All original constant BEs are set to failsafe, failed BEs are later triggered by a new element + builder.addBasicElementConst(beConst->name(), false); + break; + } + case storm::storage::BEType::EXPONENTIAL: { + auto beExp = std::static_pointer_cast const>(element); + builder.addBasicElementExponential(beExp->name(), beExp->activeFailureRate(), beExp->dormancyFactor(), beExp->isTransient()); + break; + } + default: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "BE type '" << be->beType() << "' not known."); + break; } - // All original constant BEs are set to failsafe, failed BEs are later triggered by a new element - builder.addBasicElementConst(be_const->name(), false); break; } case storm::storage::DFTElementType::AND: @@ -107,18 +113,23 @@ namespace storm { for (size_t i = 0; i < dft.nrElements(); ++i) { std::shared_ptr const> element = dft.getElement(i); switch (element->type()) { - case storm::storage::DFTElementType::BE_EXP: { - auto be_exp = std::static_pointer_cast const>( - element); - builder.addBasicElementExponential(be_exp->name(), be_exp->activeFailureRate(), - be_exp->dormancyFactor()); - break; - } - case storm::storage::DFTElementType::BE_CONST: { - auto be_const = std::static_pointer_cast const>( - element); - // All original constant BEs are set to failsafe, failed BEs are later triggered by a new element - builder.addBasicElementConst(be_const->name(), be_const->canFail()); + case storm::storage::DFTElementType::BE: { + auto be = std::static_pointer_cast const>(element); + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: { + auto beConst = std::static_pointer_cast const>(element); + builder.addBasicElementConst(beConst->name(), beConst->canFail()); + break; + } + case storm::storage::BEType::EXPONENTIAL: { + auto beExp = std::static_pointer_cast const>(element); + builder.addBasicElementExponential(beExp->name(), beExp->activeFailureRate(), beExp->dormancyFactor(), beExp->isTransient()); + break; + } + default: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "BE type '" << be->beType() << "' not known."); + break; + } break; } case storm::storage::DFTElementType::AND: diff --git a/src/storm-dft/utility/FDEPConflictFinder.cpp b/src/storm-dft/utility/FDEPConflictFinder.cpp index eb4447ffb..3b29c0976 100644 --- a/src/storm-dft/utility/FDEPConflictFinder.cpp +++ b/src/storm-dft/utility/FDEPConflictFinder.cpp @@ -25,29 +25,29 @@ namespace storm { if (dft.getDynamicBehavior()[dep1Index] && dft.getDynamicBehavior()[dep2Index]) { if (useSMT) { // if an SMT solver is to be used if (dft.getDependency(dep1Index)->triggerEvent() == dft.getDependency(dep2Index)->triggerEvent()) { - STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name() << ": Same trigger"); + STORM_LOG_TRACE("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name() << ": Same trigger"); res.emplace_back(std::pair(dep1Index, dep2Index)); } else { switch (smtChecker->checkDependencyConflict(dep1Index, dep2Index, timeout)) { case storm::solver::SmtSolver::CheckResult::Sat: - STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + STORM_LOG_TRACE("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); res.emplace_back(std::pair(dep1Index, dep2Index)); break; case storm::solver::SmtSolver::CheckResult::Unknown: - STORM_LOG_DEBUG("Unknown: Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + STORM_LOG_TRACE("Unknown: Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); res.emplace_back(std::pair(dep1Index, dep2Index)); break; default: - STORM_LOG_DEBUG("No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + STORM_LOG_TRACE("No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); break; } } } else { - STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + STORM_LOG_TRACE("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); res.emplace_back(std::pair(dep1Index, dep2Index)); } } else { - STORM_LOG_DEBUG("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + STORM_LOG_TRACE("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); break; } } @@ -70,10 +70,10 @@ namespace storm { for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) { dep2Index = dft.getDependencies().at(j); if (dft.getDynamicBehavior()[dep1Index] && dft.getDynamicBehavior()[dep2Index]) { - STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + STORM_LOG_TRACE("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); res.emplace_back(std::pair(dep1Index, dep2Index)); } else { - STORM_LOG_DEBUG("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + STORM_LOG_TRACE("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); break; } } @@ -88,4 +88,4 @@ namespace storm { class FDEPConflictFinder; } } -} \ No newline at end of file +} diff --git a/src/storm-dft/utility/FailureBoundFinder.cpp b/src/storm-dft/utility/FailureBoundFinder.cpp index d09caae83..fced153c2 100644 --- a/src/storm-dft/utility/FailureBoundFinder.cpp +++ b/src/storm-dft/utility/FailureBoundFinder.cpp @@ -15,8 +15,7 @@ namespace storm { // Count dependent events for (size_t i = 0; i < dft.nrElements(); ++i) { std::shared_ptr const> element = dft.getElement(i); - if (element->type() == storm::storage::DFTElementType::BE_EXP || - element->type() == storm::storage::DFTElementType::BE_CONST) { + if (element->isBasicElement()) { auto be = std::static_pointer_cast const>(element); if (be->hasIngoingDependencies()) { ++nrDepEvents; @@ -81,8 +80,7 @@ namespace storm { // Count dependent events for (size_t i = 0; i < dft.nrElements(); ++i) { std::shared_ptr const> element = dft.getElement(i); - if (element->type() == storm::storage::DFTElementType::BE_EXP || - element->type() == storm::storage::DFTElementType::BE_CONST) { + if (element->isBasicElement()) { auto be = std::static_pointer_cast const>(element); if (be->hasIngoingDependencies()) { ++nrDepEvents; @@ -236,4 +234,4 @@ namespace storm { class FailureBoundFinder; } } -} \ No newline at end of file +} diff --git a/src/storm-dft/utility/RelevantEvents.h b/src/storm-dft/utility/RelevantEvents.h new file mode 100644 index 000000000..127c0849c --- /dev/null +++ b/src/storm-dft/utility/RelevantEvents.h @@ -0,0 +1,69 @@ +#pragma once + +#include "storm-dft/storage/dft/DFT.h" +#include "storm-dft/settings/modules/FaultTreeSettings.h" + +namespace storm { + namespace utility { + + /*! + * Get relevant event names from labels in properties. + * + * @param dft DFT. + * @param properties List of properties. All events occurring in a property are relevant. + * @return List of relevant event names. + */ + template + std::vector getRelevantEventNames(storm::storage::DFT const& dft, std::vector> const& properties) { + // Get necessary labels from properties + std::vector> atomicLabels; + for (auto property : properties) { + property->gatherAtomicLabelFormulas(atomicLabels); + } + // Add relevant event names from properties + std::vector relevantEventNames; + for (auto atomic : atomicLabels) { + std::string label = atomic->getLabel(); + if (label == "failed" or label == "skipped") { + // Ignore as these label will always be added if necessary + } else { + // Get name of event + if (boost::ends_with(label, "_failed")) { + relevantEventNames.push_back(label.substr(0, label.size() - 7)); + } else if (boost::ends_with(label, "_dc")) { + relevantEventNames.push_back(label.substr(0, label.size() - 3)); + } else if (label.find("_claimed_") != std::string::npos) { + STORM_LOG_THROW(storm::settings::getModule().isAddLabelsClaiming(), storm::exceptions::InvalidArgumentException, "Claiming labels will not be exported but are required for label '" << label << "'. Try setting --labels-claiming."); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Label '" << label << "' not known."); + } + } + } + return relevantEventNames; + } + + /*! + * Get relevant event id from relevant event name. + * + * @param dft DFT. + * @param relevantEventNames Names of relevant events. + * @return Set of relevant event ids. + */ + template + std::set getRelevantEvents(storm::storage::DFT const& dft, std::vector const& relevantEventNames) { + // Set relevant elements + std::set relevantEvents; // Per default no event (except the toplevel event) is relevant + for (std::string const& relevantName : relevantEventNames) { + if (relevantName == "all") { + // All events are relevant + return dft.getAllIds(); + } else { + // Find and add corresponding event id + relevantEvents.insert(dft.getIndex(relevantName)); + } + } + return relevantEvents; + } + + } // namespace utility +} // namespace storm \ No newline at end of file diff --git a/src/storm-gspn/api/storm-gspn.cpp b/src/storm-gspn/api/storm-gspn.cpp index ea4faf9e0..4a7402f13 100644 --- a/src/storm-gspn/api/storm-gspn.cpp +++ b/src/storm-gspn/api/storm-gspn.cpp @@ -1,7 +1,7 @@ #include "storm-gspn/api/storm-gspn.h" #include "storm/settings/SettingsManager.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm-gspn/settings/modules/GSPNExportSettings.h" #include "storm-conv/settings/modules/JaniExportSettings.h" #include "storm-conv/api/storm-conv.h" diff --git a/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp b/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp index 4c77bc3a2..e272d27ec 100644 --- a/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp +++ b/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp @@ -88,7 +88,8 @@ namespace storm { if (name.compare("name") == 0) { builder.setGspnName(storm::adapters::XMLtoString(attr->getNodeValue())); } else if (name.compare("show-color-cmd") == 0 || - name.compare("show-fluid-cmd") == 0) { + name.compare("show-fluid-cmd") == 0 || + name.compare("zoom") == 0) { // ignore node } else { // Found node or attribute which is at the moment not handled by this parser. diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index fbb8c5971..65c68a6c9 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -34,7 +34,7 @@ #include "storm/storage/StronglyConnectedComponentDecomposition.h" #include "storm/storage/SymbolicModelDescription.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm/utility/initialize.h" #include "storm/utility/Stopwatch.h" #include "storm/utility/macros.h" diff --git a/src/storm-pars/api/export.h b/src/storm-pars/api/export.h index 69a6405de..43e199cce 100644 --- a/src/storm-pars/api/export.h +++ b/src/storm-pars/api/export.h @@ -1,4 +1,4 @@ -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm/utility/macros.h" #include "storm/exceptions/NotSupportedException.h" #include "storm/analysis/GraphConditions.h" diff --git a/src/storm-pars/api/region.h b/src/storm-pars/api/region.h index 0ee310b39..b147b664f 100644 --- a/src/storm-pars/api/region.h +++ b/src/storm-pars/api/region.h @@ -21,7 +21,7 @@ #include "storm/environment/Environment.h" #include "storm/api/transformation.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm/models/sparse/Model.h" #include "storm/exceptions/UnexpectedException.h" #include "storm/exceptions/InvalidOperationException.h" diff --git a/src/storm-pars/parser/ParameterRegionParser.cpp b/src/storm-pars/parser/ParameterRegionParser.cpp index bd2c0bef8..4c293ab54 100644 --- a/src/storm-pars/parser/ParameterRegionParser.cpp +++ b/src/storm-pars/parser/ParameterRegionParser.cpp @@ -4,7 +4,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/utility/constants.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" namespace storm { namespace parser { diff --git a/src/storm-parsers/parser/AtomicPropositionLabelingParser.cpp b/src/storm-parsers/parser/AtomicPropositionLabelingParser.cpp index a8afc93d7..fd18a3cb9 100644 --- a/src/storm-parsers/parser/AtomicPropositionLabelingParser.cpp +++ b/src/storm-parsers/parser/AtomicPropositionLabelingParser.cpp @@ -11,7 +11,7 @@ #include #include -#include "storm/utility/cstring.h" +#include "storm-parsers/util/cstring.h" #include "storm-parsers/parser/MappedFile.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/FileIoException.h" diff --git a/src/storm-parsers/parser/AutoParser.cpp b/src/storm-parsers/parser/AutoParser.cpp index 9e96af5e6..ecaec6293 100644 --- a/src/storm-parsers/parser/AutoParser.cpp +++ b/src/storm-parsers/parser/AutoParser.cpp @@ -12,7 +12,7 @@ #include "storm/adapters/RationalFunctionAdapter.h" -#include "storm/utility/cstring.h" +#include "storm-parsers/util/cstring.h" #include "storm/utility/OsDetection.h" namespace storm { diff --git a/src/storm-parsers/parser/DeterministicSparseTransitionParser.cpp b/src/storm-parsers/parser/DeterministicSparseTransitionParser.cpp index 1b3942dc8..146fa7811 100644 --- a/src/storm-parsers/parser/DeterministicSparseTransitionParser.cpp +++ b/src/storm-parsers/parser/DeterministicSparseTransitionParser.cpp @@ -8,7 +8,7 @@ #include #include "storm/utility/constants.h" -#include "storm/utility/cstring.h" +#include "storm-parsers/util/cstring.h" #include "storm-parsers/parser/MappedFile.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/WrongFormatException.h" diff --git a/src/storm-parsers/parser/DirectEncodingParser.cpp b/src/storm-parsers/parser/DirectEncodingParser.cpp index 4c17f7948..026425e5b 100644 --- a/src/storm-parsers/parser/DirectEncodingParser.cpp +++ b/src/storm-parsers/parser/DirectEncodingParser.cpp @@ -23,7 +23,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/utility/constants.h" #include "storm/utility/builder.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm/utility/macros.h" #include "storm/utility/SignalHandler.h" diff --git a/src/storm-parsers/parser/FormulaParser.cpp b/src/storm-parsers/parser/FormulaParser.cpp index e58bbfe70..37dad72d3 100644 --- a/src/storm-parsers/parser/FormulaParser.cpp +++ b/src/storm-parsers/parser/FormulaParser.cpp @@ -14,7 +14,7 @@ #include "storm/storage/expressions/ExpressionEvaluator.h" #include "FormulaParserGrammar.h" #include "storm/storage/expressions/ExpressionManager.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" namespace storm { namespace parser { diff --git a/src/storm-parsers/parser/ImcaMarkovAutomatonParser.cpp b/src/storm-parsers/parser/ImcaMarkovAutomatonParser.cpp index a10e3864b..e473c034d 100644 --- a/src/storm-parsers/parser/ImcaMarkovAutomatonParser.cpp +++ b/src/storm-parsers/parser/ImcaMarkovAutomatonParser.cpp @@ -2,7 +2,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/BuildSettings.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm/utility/builder.h" namespace storm { diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index e82ad294e..dc146ffdf 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -28,7 +28,7 @@ #include "storm/storage/jani/ArrayVariable.h" #include "storm/utility/macros.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" namespace storm { namespace parser { diff --git a/src/storm-parsers/parser/MappedFile.cpp b/src/storm-parsers/parser/MappedFile.cpp index d28e8e927..357a6e023 100644 --- a/src/storm-parsers/parser/MappedFile.cpp +++ b/src/storm-parsers/parser/MappedFile.cpp @@ -15,7 +15,7 @@ #include "storm/exceptions/FileIoException.h" #include "storm/utility/macros.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" namespace storm { namespace parser { diff --git a/src/storm-parsers/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/storm-parsers/parser/MarkovAutomatonSparseTransitionParser.cpp index 6d25e7f15..9316735b4 100644 --- a/src/storm-parsers/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/storm-parsers/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -5,7 +5,7 @@ #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/FileIoException.h" #include "storm-parsers/parser/MappedFile.h" -#include "storm/utility/cstring.h" +#include "storm-parsers/util/cstring.h" #include "storm/utility/constants.h" #include "storm/utility/macros.h" diff --git a/src/storm-parsers/parser/NondeterministicSparseTransitionParser.cpp b/src/storm-parsers/parser/NondeterministicSparseTransitionParser.cpp index 0b0fbc168..170d10286 100644 --- a/src/storm-parsers/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/storm-parsers/parser/NondeterministicSparseTransitionParser.cpp @@ -11,7 +11,7 @@ #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/WrongFormatException.h" -#include "storm/utility/cstring.h" +#include "storm-parsers/util/cstring.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp index 0368d843c..c95c42af2 100644 --- a/src/storm-parsers/parser/PrismParser.cpp +++ b/src/storm-parsers/parser/PrismParser.cpp @@ -6,7 +6,7 @@ #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidTypeException.h" #include "storm/utility/macros.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/UnexpectedException.h" diff --git a/src/storm-parsers/parser/ReadValues.h b/src/storm-parsers/parser/ReadValues.h index e39644867..669686222 100644 --- a/src/storm-parsers/parser/ReadValues.h +++ b/src/storm-parsers/parser/ReadValues.h @@ -1,7 +1,7 @@ #ifndef _STORM_PARSER_READVALUES_H #define _STORM_PARSER_READVALUES_H -#include "storm/utility/cstring.h" +#include "storm-parsers/util/cstring.h" namespace storm { diff --git a/src/storm-parsers/parser/SparseChoiceLabelingParser.cpp b/src/storm-parsers/parser/SparseChoiceLabelingParser.cpp index 8a741aaa5..83b7e73ce 100644 --- a/src/storm-parsers/parser/SparseChoiceLabelingParser.cpp +++ b/src/storm-parsers/parser/SparseChoiceLabelingParser.cpp @@ -5,7 +5,7 @@ #include "storm/exceptions/OutOfRangeException.h" #include "storm/exceptions/FileIoException.h" #include "storm-parsers/parser/MappedFile.h" -#include "storm/utility/cstring.h" +#include "storm-parsers/util/cstring.h" namespace storm { namespace parser { diff --git a/src/storm-parsers/parser/SparseItemLabelingParser.cpp b/src/storm-parsers/parser/SparseItemLabelingParser.cpp index 9e5e7b154..4a68c7b3e 100644 --- a/src/storm-parsers/parser/SparseItemLabelingParser.cpp +++ b/src/storm-parsers/parser/SparseItemLabelingParser.cpp @@ -4,7 +4,7 @@ #include #include -#include "storm/utility/cstring.h" +#include "storm-parsers/util/cstring.h" #include "storm-parsers/parser/MappedFile.h" #include "storm/utility/macros.h" diff --git a/src/storm-parsers/parser/SparseStateRewardParser.cpp b/src/storm-parsers/parser/SparseStateRewardParser.cpp index acb67e9fb..1bf83507a 100644 --- a/src/storm-parsers/parser/SparseStateRewardParser.cpp +++ b/src/storm-parsers/parser/SparseStateRewardParser.cpp @@ -4,7 +4,7 @@ #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/OutOfRangeException.h" #include "storm/exceptions/FileIoException.h" -#include "storm/utility/cstring.h" +#include "storm-parsers/util/cstring.h" #include "storm-parsers/parser/MappedFile.h" #include "storm/adapters/RationalFunctionAdapter.h" diff --git a/src/storm/utility/cstring.cpp b/src/storm-parsers/util/cstring.cpp similarity index 98% rename from src/storm/utility/cstring.cpp rename to src/storm-parsers/util/cstring.cpp index 6bf69a421..5b701eb00 100644 --- a/src/storm/utility/cstring.cpp +++ b/src/storm-parsers/util/cstring.cpp @@ -1,4 +1,4 @@ -#include "storm/utility/cstring.h" +#include "storm-parsers/util/cstring.h" #include diff --git a/src/storm/utility/cstring.h b/src/storm-parsers/util/cstring.h similarity index 85% rename from src/storm/utility/cstring.h rename to src/storm-parsers/util/cstring.h index 65168e525..f61866e4a 100644 --- a/src/storm/utility/cstring.h +++ b/src/storm-parsers/util/cstring.h @@ -1,12 +1,4 @@ -/* - * cstring.h - * - * Created on: 30.01.2014 - * Author: Manuel Sascha Weiand - */ - -#ifndef STORM_UTILITY_CSTRING_H_ -#define STORM_UTILITY_CSTRING_H_ +#pragma once #include @@ -49,5 +41,3 @@ namespace storm { } // namespace cstring } // namespace utility } // namespace storm - -#endif /* STORM_UTILITY_CSTRING_H_ */ diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp index 45b81f2c8..b1802a072 100644 --- a/src/storm-pgcl-cli/storm-pgcl.cpp +++ b/src/storm-pgcl-cli/storm-pgcl.cpp @@ -23,7 +23,7 @@ #include "storm-parsers/api/storm-parsers.h" #include "storm/storage/SymbolicModelDescription.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" /*! * Initialize the settings manager. diff --git a/src/storm-pgcl/parser/PgclParser.cpp b/src/storm-pgcl/parser/PgclParser.cpp index 2afe737be..2d8fff4a1 100755 --- a/src/storm-pgcl/parser/PgclParser.cpp +++ b/src/storm-pgcl/parser/PgclParser.cpp @@ -1,7 +1,7 @@ #include "PgclParser.h" // If the parser fails due to ill-formed data, this exception is thrown. #include "storm/exceptions/WrongFormatException.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" namespace storm { namespace parser { diff --git a/src/storm-pomdp/analysis/IterativePolicySearch.cpp b/src/storm-pomdp/analysis/IterativePolicySearch.cpp index 719def098..f41550e9a 100644 --- a/src/storm-pomdp/analysis/IterativePolicySearch.cpp +++ b/src/storm-pomdp/analysis/IterativePolicySearch.cpp @@ -1,5 +1,5 @@ #include "storm-pomdp/analysis/IterativePolicySearch.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm-pomdp/analysis/OneShotPolicySearch.h" #include "storm-pomdp/analysis/QualitativeAnalysis.h" diff --git a/src/storm-pomdp/analysis/OneShotPolicySearch.cpp b/src/storm-pomdp/analysis/OneShotPolicySearch.cpp index a39901eb4..0e2cdbe5d 100644 --- a/src/storm-pomdp/analysis/OneShotPolicySearch.cpp +++ b/src/storm-pomdp/analysis/OneShotPolicySearch.cpp @@ -1,4 +1,4 @@ -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm-pomdp/analysis/OneShotPolicySearch.h" diff --git a/src/storm-pomdp/analysis/WinningRegion.cpp b/src/storm-pomdp/analysis/WinningRegion.cpp index 7b3bed467..7b872a20a 100644 --- a/src/storm-pomdp/analysis/WinningRegion.cpp +++ b/src/storm-pomdp/analysis/WinningRegion.cpp @@ -1,7 +1,7 @@ #include #include #include -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm/utility/constants.h" #include "storm/storage/expressions/Expression.h" #include "storm/storage/expressions/ExpressionManager.h" diff --git a/src/storm/abstraction/MenuGameAbstractor.cpp b/src/storm/abstraction/MenuGameAbstractor.cpp index d75a8ddb4..25d008292 100644 --- a/src/storm/abstraction/MenuGameAbstractor.cpp +++ b/src/storm/abstraction/MenuGameAbstractor.cpp @@ -10,7 +10,7 @@ #include "storm/storage/dd/Add.h" #include "storm/storage/dd/Bdd.h" #include "storm/utility/dd.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm-config.h" #include "storm/adapters/RationalFunctionAdapter.h" diff --git a/src/storm/adapters/EigenAdapter.h b/src/storm/adapters/EigenAdapter.h index 8f7be92ee..6d00a6539 100644 --- a/src/storm/adapters/EigenAdapter.h +++ b/src/storm/adapters/EigenAdapter.h @@ -2,7 +2,7 @@ #include -#include "storm/utility/eigen.h" +#include "storm/adapters/eigen.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/storage/SparseMatrix.h" diff --git a/src/storm/adapters/GmmxxAdapter.h b/src/storm/adapters/GmmxxAdapter.h index a5e139db0..022f43d0c 100644 --- a/src/storm/adapters/GmmxxAdapter.h +++ b/src/storm/adapters/GmmxxAdapter.h @@ -2,7 +2,7 @@ #include -#include "storm/utility/gmm.h" +#include "storm/adapters/gmm.h" #include "storm/storage/SparseMatrix.h" diff --git a/src/storm/utility/eigen.h b/src/storm/adapters/eigen.h similarity index 100% rename from src/storm/utility/eigen.h rename to src/storm/adapters/eigen.h diff --git a/src/storm/utility/gmm.h b/src/storm/adapters/gmm.h similarity index 100% rename from src/storm/utility/gmm.h rename to src/storm/adapters/gmm.h diff --git a/src/storm/utility/sylvan.cpp b/src/storm/adapters/sylvan.cpp similarity index 93% rename from src/storm/utility/sylvan.cpp rename to src/storm/adapters/sylvan.cpp index 769b125d2..b055f9db2 100644 --- a/src/storm/utility/sylvan.cpp +++ b/src/storm/adapters/sylvan.cpp @@ -1,4 +1,4 @@ -#include "storm/utility/sylvan.h" +#include "storm/adapters/sylvan.h" namespace storm { namespace dd { diff --git a/src/storm/utility/sylvan.h b/src/storm/adapters/sylvan.h similarity index 100% rename from src/storm/utility/sylvan.h rename to src/storm/adapters/sylvan.h diff --git a/src/storm/api/export.h b/src/storm/api/export.h index e72496c39..e0d0fdf2a 100644 --- a/src/storm/api/export.h +++ b/src/storm/api/export.h @@ -2,9 +2,9 @@ #include "storm/settings/SettingsManager.h" -#include "storm/utility/DirectEncodingExporter.h" -#include "storm/utility/DDEncodingExporter.h" -#include "storm/utility/file.h" +#include "storm/io/DirectEncodingExporter.h" +#include "storm/io/DDEncodingExporter.h" +#include "storm/io/file.h" #include "storm/utility/macros.h" #include "storm/storage/Scheduler.h" diff --git a/src/storm/utility/DDEncodingExporter.cpp b/src/storm/io/DDEncodingExporter.cpp similarity index 96% rename from src/storm/utility/DDEncodingExporter.cpp rename to src/storm/io/DDEncodingExporter.cpp index 7ad4c303c..90278a683 100644 --- a/src/storm/utility/DDEncodingExporter.cpp +++ b/src/storm/io/DDEncodingExporter.cpp @@ -1,5 +1,5 @@ -#include "storm/utility/DDEncodingExporter.h" -#include "storm/utility/file.h" +#include "storm/io/DDEncodingExporter.h" +#include "storm/io/file.h" #include "storm/models/symbolic/StandardRewardModel.h" namespace storm { diff --git a/src/storm/utility/DDEncodingExporter.h b/src/storm/io/DDEncodingExporter.h similarity index 100% rename from src/storm/utility/DDEncodingExporter.h rename to src/storm/io/DDEncodingExporter.h diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/io/DirectEncodingExporter.cpp similarity index 99% rename from src/storm/utility/DirectEncodingExporter.cpp rename to src/storm/io/DirectEncodingExporter.cpp index f4798bc0d..495ed2cf3 100644 --- a/src/storm/utility/DirectEncodingExporter.cpp +++ b/src/storm/io/DirectEncodingExporter.cpp @@ -1,5 +1,5 @@ #include -#include "DirectEncodingExporter.h" +#include "storm/io/DirectEncodingExporter.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/constants.h" diff --git a/src/storm/utility/DirectEncodingExporter.h b/src/storm/io/DirectEncodingExporter.h similarity index 100% rename from src/storm/utility/DirectEncodingExporter.h rename to src/storm/io/DirectEncodingExporter.h diff --git a/src/storm/utility/export.h b/src/storm/io/export.h similarity index 98% rename from src/storm/utility/export.h rename to src/storm/io/export.h index f067f88b3..1a3dbd3fe 100644 --- a/src/storm/utility/export.h +++ b/src/storm/io/export.h @@ -5,7 +5,7 @@ #include #include "storm/utility/macros.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" namespace storm { diff --git a/src/storm/utility/file.h b/src/storm/io/file.h similarity index 100% rename from src/storm/utility/file.h rename to src/storm/io/file.h diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp index c1a6ff492..90a2aed8e 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp @@ -16,7 +16,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" -#include "storm/utility/export.h" +#include "storm/io/export.h" #include "storm/utility/solver.h" #include "storm/exceptions/UnexpectedException.h" diff --git a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp index fee359020..bd8215448 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp @@ -21,7 +21,7 @@ #include "storm/solver/LinearEquationSolver.h" #include "storm/utility/ProgressMeasurement.h" #include "storm/utility/SignalHandler.h" -#include "storm/utility/export.h" +#include "storm/io/export.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp index 559e0189f..a97905f7d 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp @@ -10,7 +10,7 @@ #include "storm/storage/geometry/Hyperrectangle.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" -#include "storm/utility/export.h" +#include "storm/io/export.h" #include "storm/exceptions/UnexpectedException.h" diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index b1ec53e30..bf9c9b9ad 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -29,7 +29,7 @@ #include "storm/utility/Stopwatch.h" #include "storm/utility/ProgressMeasurement.h" #include "storm/utility/SignalHandler.h" -#include "storm/utility/export.h" +#include "storm/io/export.h" #include "storm/utility/macros.h" #include "storm/utility/ConstantsComparator.h" diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 1e9722d7a..3b69fa62d 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -33,7 +33,7 @@ #include "storm/utility/Stopwatch.h" #include "storm/utility/ProgressMeasurement.h" #include "storm/utility/SignalHandler.h" -#include "storm/utility/export.h" +#include "storm/io/export.h" #include "storm/utility/NumberTraits.h" #include "storm/transformer/EndComponentEliminator.h" diff --git a/src/storm/models/sparse/DeterministicModel.cpp b/src/storm/models/sparse/DeterministicModel.cpp index 06419a6c0..ddcf7aead 100644 --- a/src/storm/models/sparse/DeterministicModel.cpp +++ b/src/storm/models/sparse/DeterministicModel.cpp @@ -3,7 +3,7 @@ #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/utility/constants.h" -#include "storm/utility/export.h" +#include "storm/io/export.h" namespace storm { namespace models { diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index b0137feda..bf9d69d4c 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -9,7 +9,7 @@ #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/utility/vector.h" -#include "storm/utility/export.h" +#include "storm/io/export.h" #include "storm/utility/NumberTraits.h" diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index 635cfee7b..2c882464e 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -8,7 +8,7 @@ #include "storm/storage/memorystructure/MemoryStructureBuilder.h" #include "storm/storage/memorystructure/SparseModelMemoryProduct.h" #include "storm/transformer/SubsystemBuilder.h" -#include "storm/utility/export.h" +#include "storm/io/export.h" namespace storm { namespace models { diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 027a24df6..4c797e524 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -42,7 +42,7 @@ #include "storm/settings/modules/HintSettings.h" #include "storm/settings/modules/OviSolverSettings.h" #include "storm/utility/macros.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm/utility/string.h" #include "storm/settings/Option.h" diff --git a/src/storm/solver/EigenLinearEquationSolver.h b/src/storm/solver/EigenLinearEquationSolver.h index 32697b615..e2d246665 100644 --- a/src/storm/solver/EigenLinearEquationSolver.h +++ b/src/storm/solver/EigenLinearEquationSolver.h @@ -2,7 +2,7 @@ #include "storm/solver/LinearEquationSolver.h" #include "storm/solver/SolverSelectionOptions.h" -#include "storm/utility/eigen.h" +#include "storm/adapters/eigen.h" namespace storm { namespace solver { diff --git a/src/storm/solver/GmmxxLinearEquationSolver.cpp b/src/storm/solver/GmmxxLinearEquationSolver.cpp index 9142ba1d6..1f954426e 100644 --- a/src/storm/solver/GmmxxLinearEquationSolver.cpp +++ b/src/storm/solver/GmmxxLinearEquationSolver.cpp @@ -7,7 +7,7 @@ #include "storm/environment/solver/GmmxxSolverEnvironment.h" #include "storm/exceptions/AbortException.h" #include "storm/utility/constants.h" -#include "storm/utility/gmm.h" +#include "storm/adapters/gmm.h" #include "storm/utility/vector.h" #include "storm/utility/SignalHandler.h" diff --git a/src/storm/solver/GmmxxLinearEquationSolver.h b/src/storm/solver/GmmxxLinearEquationSolver.h index f288e9f58..e9b11656d 100644 --- a/src/storm/solver/GmmxxLinearEquationSolver.h +++ b/src/storm/solver/GmmxxLinearEquationSolver.h @@ -3,7 +3,7 @@ #include -#include "storm/utility/gmm.h" +#include "storm/adapters/gmm.h" #include "storm/solver/LinearEquationSolver.h" #include "storm/solver/SolverSelectionOptions.h" diff --git a/src/storm/solver/SmtlibSmtSolver.cpp b/src/storm/solver/SmtlibSmtSolver.cpp index 1ef7fda76..1cd716f33 100644 --- a/src/storm/solver/SmtlibSmtSolver.cpp +++ b/src/storm/solver/SmtlibSmtSolver.cpp @@ -17,7 +17,7 @@ #include "storm/exceptions/IllegalArgumentException.h" #include "storm/exceptions/IllegalFunctionCallException.h" #include "storm/utility/macros.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/UnexpectedException.h" diff --git a/src/storm/solver/Z3LpSolver.cpp b/src/storm/solver/Z3LpSolver.cpp index 4c2baf05c..3c34cdac1 100644 --- a/src/storm/solver/Z3LpSolver.cpp +++ b/src/storm/solver/Z3LpSolver.cpp @@ -9,7 +9,7 @@ #include "storm/utility/macros.h" #include "storm/utility/constants.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm/storage/expressions/Expression.h" #include "storm/storage/expressions/ExpressionManager.h" diff --git a/src/storm/storage/Qvbs.cpp b/src/storm/storage/Qvbs.cpp index 71c012568..15a4494be 100644 --- a/src/storm/storage/Qvbs.cpp +++ b/src/storm/storage/Qvbs.cpp @@ -3,7 +3,7 @@ #include #include "storm/utility/macros.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm/utility/string.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/IOSettings.h" diff --git a/src/storm/storage/dd/Odd.cpp b/src/storm/storage/dd/Odd.cpp index 10fd878a9..d48ed2060 100644 --- a/src/storm/storage/dd/Odd.cpp +++ b/src/storm/storage/dd/Odd.cpp @@ -8,7 +8,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/NotSupportedException.h" diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.h b/src/storm/storage/dd/sylvan/InternalSylvanBdd.h index 0dadbf8a4..bd1ee3db1 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.h @@ -13,7 +13,7 @@ #include "storm/storage/dd/InternalBdd.h" #include "storm/storage/dd/InternalAdd.h" -#include "storm/utility/sylvan.h" +#include "storm/adapters/sylvan.h" namespace storm { namespace storage { diff --git a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp index 2b8a549cf..4bc73632c 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -11,7 +11,7 @@ #include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/InvalidSettingsException.h" -#include "storm/utility/sylvan.h" +#include "storm/adapters/sylvan.h" #include "storm-config.h" diff --git a/src/storm/storage/dd/sylvan/SylvanAddIterator.h b/src/storm/storage/dd/sylvan/SylvanAddIterator.h index e19d04fe9..f28673d0a 100644 --- a/src/storm/storage/dd/sylvan/SylvanAddIterator.h +++ b/src/storm/storage/dd/sylvan/SylvanAddIterator.h @@ -6,7 +6,7 @@ #include "storm/storage/dd/AddIterator.h" #include "storm/storage/expressions/SimpleValuation.h" -#include "storm/utility/sylvan.h" +#include "storm/adapters/sylvan.h" namespace storm { namespace dd { diff --git a/src/storm/storage/dd/sylvan/utility.h b/src/storm/storage/dd/sylvan/utility.h index 02a06a3bf..a33e02c57 100644 --- a/src/storm/storage/dd/sylvan/utility.h +++ b/src/storm/storage/dd/sylvan/utility.h @@ -1,6 +1,6 @@ #pragma once -#include "storm/utility/sylvan.h" +#include "storm/adapters/sylvan.h" #include diff --git a/src/storm/storage/expressions/Type.cpp b/src/storm/storage/expressions/Type.cpp index b585b8eae..bc92c859a 100644 --- a/src/storm/storage/expressions/Type.cpp +++ b/src/storm/storage/expressions/Type.cpp @@ -210,7 +210,7 @@ namespace storm { } Type Type::divide(Type const& other) const { - STORM_LOG_THROW(this->isNumericalType() && other.isNumericalType(), storm::exceptions::InvalidTypeException, "Operator requires numerical operands."); + STORM_LOG_THROW(this->isNumericalType() && other.isNumericalType(), storm::exceptions::InvalidTypeException, "Operator division requires numerical operands, got " << this->isNumericalType() << " and " << other.isNumericalType() << "." ); STORM_LOG_THROW(!this->isBitVectorType() && !other.isBitVectorType(), storm::exceptions::InvalidTypeException, "Operator requires non-bitvector operands."); return std::max(*this, other); } diff --git a/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.cpp b/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.cpp index 709fe4f6f..2d9606029 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.cpp @@ -2,7 +2,7 @@ #include "storm/adapters/RationalFunctionAdapter.h" -#include "storm/utility/eigen.h" +#include "storm/adapters/eigen.h" namespace storm { namespace storage { diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 46317c870..79748e5da 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -5,7 +5,7 @@ #include #include "storm/utility/macros.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/NotSupportedException.h" diff --git a/src/test/storm-dft/CMakeLists.txt b/src/test/storm-dft/CMakeLists.txt index a0e96ee36..a2ef04a4b 100644 --- a/src/test/storm-dft/CMakeLists.txt +++ b/src/test/storm-dft/CMakeLists.txt @@ -9,7 +9,7 @@ register_source_groups_from_filestructure("${ALL_FILES}" test) # Note that the tests also need the source files, except for the main file include_directories(${GTEST_INCLUDE_DIR}) -foreach (testsuite api) +foreach (testsuite api storage) file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp) add_executable (test-dft-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp) diff --git a/src/test/storm-dft/api/DftParserTest.cpp b/src/test/storm-dft/api/DftParserTest.cpp index 05edb5b73..2744254a4 100644 --- a/src/test/storm-dft/api/DftParserTest.cpp +++ b/src/test/storm-dft/api/DftParserTest.cpp @@ -26,8 +26,11 @@ namespace { STORM_SILENT_EXPECT_THROW(storm::api::loadDFTGalileoFile(file), storm::exceptions::WrongFormatException); } - TEST(DftParserTest, CatchSeqChildren) { + TEST(DftParserTest, LoadSeqChildren) { std::string file = STORM_TEST_RESOURCES_DIR "/dft/seqChild.dft"; - STORM_SILENT_EXPECT_THROW(storm::api::loadDFTGalileoFile(file), storm::exceptions::WrongFormatException); + std::shared_ptr> dft = storm::api::loadDFTGalileoFile(file); + EXPECT_EQ(4ul, dft->nrElements()); + EXPECT_EQ(2ul, dft->nrBasicElements()); + EXPECT_TRUE(storm::api::isWellFormed(*dft).first); } } diff --git a/src/test/storm-dft/api/DftTransformatorTest.cpp b/src/test/storm-dft/api/DftTransformatorTest.cpp index c249cd2df..bca6e4ae5 100644 --- a/src/test/storm-dft/api/DftTransformatorTest.cpp +++ b/src/test/storm-dft/api/DftTransformatorTest.cpp @@ -17,7 +17,7 @@ namespace { uint64_t constBeFailedCount = 0; uint64_t constBeFailsafeCount = 0; for (auto &be : bes) { - if (be->type() == storm::storage::DFTElementType::BE_CONST) { + if (be->beType() == storm::storage::BEType::CONSTANT) { if (be->canFail()) { ++constBeFailedCount; } else { @@ -66,4 +66,4 @@ namespace { EXPECT_EQ(4ul, transformedDft->nrBasicElements()); } -} \ No newline at end of file +} diff --git a/src/test/storm-dft/storage/DftBETest.cpp b/src/test/storm-dft/storage/DftBETest.cpp new file mode 100644 index 000000000..c73af3d9e --- /dev/null +++ b/src/test/storm-dft/storage/DftBETest.cpp @@ -0,0 +1,52 @@ +#include "test/storm_gtest.h" +#include "storm-config.h" + +#include "storm-dft/storage/dft/DFTElements.h" + +namespace { + + TEST(DftBETest, FailureConstant) { + storm::storage::BEConst be(0, "Test", true); + EXPECT_TRUE(be.failed()); + EXPECT_TRUE(be.canFail()); + + EXPECT_EQ(1, be.getUnreliability(0)); + EXPECT_EQ(1, be.getUnreliability(10)); + } + + TEST(DftBETest, FailureExponential) { + storm::storage::BEExponential be(0, "Test", 3, 0.5); + + EXPECT_TRUE(be.canFail()); + EXPECT_EQ(1.5, be.passiveFailureRate()); + + EXPECT_EQ(0, be.getUnreliability(0)); + EXPECT_FLOAT_EQ(0.7768698399, be.getUnreliability(0.5)); + EXPECT_FLOAT_EQ(0.9502129316, be.getUnreliability(1)); + EXPECT_FLOAT_EQ(0.9975212478, be.getUnreliability(2)); + } + + TEST(DftBETest, FailureSamples) { + // Weibull distribution with shape 5 and scale 1 + std::map samples = { + {0.0, 0.0}, + {0.25, 0.0009760858180243304}, + {0.5, 0.03076676552365587}, + {0.75, 0.21124907114638225}, + {1.0, 0.6321205588285577}, + {1.25, 0.9527242505937095}, + {1.5, 0.9994964109502631}, + {1.75, 0.999999925546118}, + {2.0, 0.9999999999999873} + }; + storm::storage::BESamples be(0, "Weibull", samples); + + EXPECT_TRUE(be.canFail()); + + EXPECT_EQ(0, be.getUnreliability(0)); + for (double i = 0; i <= 2.0; i += 0.25) { + EXPECT_FLOAT_EQ(1-exp(-pow(i, 5)), be.getUnreliability(i)); + } + } + +} diff --git a/src/test/storm/parser/MappedFileTest.cpp b/src/test/storm/parser/MappedFileTest.cpp index 14b1cbf33..69127e8d0 100644 --- a/src/test/storm/parser/MappedFileTest.cpp +++ b/src/test/storm/parser/MappedFileTest.cpp @@ -10,8 +10,8 @@ #include #include "storm-parsers/parser/MappedFile.h" -#include "storm/utility/cstring.h" -#include "storm/utility/file.h" +#include "storm-parsers/util/cstring.h" +#include "storm/io/file.h" #include "storm/exceptions/FileIoException.h" TEST(MappedFileTest, NonExistingFile) { diff --git a/src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp b/src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp index 030d1b07b..d1f1867d9 100644 --- a/src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp +++ b/src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp @@ -13,7 +13,7 @@ #include #include "storm-parsers/parser/MarkovAutomatonSparseTransitionParser.h" -#include "storm/utility/cstring.h" +#include "storm-parsers/util/cstring.h" #include "storm-parsers/parser/MarkovAutomatonParser.h" #include "storm/settings/SettingMemento.h" #include "storm/exceptions/WrongFormatException.h" diff --git a/src/test/storm/utility/FileTest.cpp b/src/test/storm/utility/FileTest.cpp index d804e653e..0150ad677 100644 --- a/src/test/storm/utility/FileTest.cpp +++ b/src/test/storm/utility/FileTest.cpp @@ -1,7 +1,7 @@ #include "test/storm_gtest.h" #include "storm-config.h" -#include "storm/utility/file.h" +#include "storm/io/file.h" TEST(FileTest, GetLine) { std::stringstream stream;