diff --git a/resources/examples/testfiles/dft/const_be_test.dft b/resources/examples/testfiles/dft/const_be_test.dft new file mode 100644 index 000000000..1f5721275 --- /dev/null +++ b/resources/examples/testfiles/dft/const_be_test.dft @@ -0,0 +1,8 @@ +toplevel "A"; +"A" and "I" "J" "K" "L"; +"DEP1" fdep "I" "J" "K"; + +"I" prob=1; +"J" prob=1; +"K" prob=1; +"L" lambda=1.0 dorm=0.5; diff --git a/resources/examples/testfiles/dft/seq_conflict_test.dft b/resources/examples/testfiles/dft/seq_conflict_test.dft new file mode 100644 index 000000000..77b22e0f2 --- /dev/null +++ b/resources/examples/testfiles/dft/seq_conflict_test.dft @@ -0,0 +1,12 @@ +toplevel "A"; +"A" and "I" "B"; +"SEQ_dynamic" seq "I" "B"; +"B" or "J" "K"; +"DEP1_1" fdep "T1" "I"; +"DEP1_2" fdep "T1" "J"; +"DEP1_3" fdep "T1" "K"; + +"I" lambda=0.5 dorm=0; +"J" lambda=0.5 dorm=0; +"K" lambda=0.5 dorm=0; +"T1" lambda=0.5 dorm=0; \ No newline at end of file diff --git a/resources/examples/testfiles/dft/spare_conflict_test.dft b/resources/examples/testfiles/dft/spare_conflict_test.dft new file mode 100644 index 000000000..e7d076fa7 --- /dev/null +++ b/resources/examples/testfiles/dft/spare_conflict_test.dft @@ -0,0 +1,12 @@ +toplevel "A"; +"A" pand "SP1" "SP2"; +"SP1" wsp "I" "J"; +"SP2" wsp "J" "K"; +"DEP1" fdep "T1" "I"; +"DEP2" fdep "T2" "K"; + +"I" lambda=0.5 dorm=0; +"J" lambda=0.5 dorm=0; +"K" lambda=0.5 dorm=0; +"T1" lambda=0.5 dorm=0; +"T2" lambda=0.5 dorm=0; \ No newline at end of file diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index f4f133b8a..47d33c0a1 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -42,6 +42,7 @@ #include "storm/settings/modules/AbstractionSettings.h" #include "storm/settings/modules/ResourceSettings.h" #include "storm/settings/modules/ModelCheckerSettings.h" +#include "storm/settings/modules/TransformationSettings.h" #include "storm/storage/Qvbs.h" #include "storm/utility/Stopwatch.h" @@ -350,11 +351,18 @@ namespace storm { auto generalSettings = storm::settings::getModule(); auto bisimulationSettings = storm::settings::getModule(); auto ioSettings = storm::settings::getModule(); + auto transformationSettings = storm::settings::getModule(); std::pair>, bool> result = std::make_pair(model, false); if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { result.first = preprocessSparseMarkovAutomaton(result.first->template as>()); + if (transformationSettings.isChainEliminationSet() && + result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { + result.first = storm::transformer::NonMarkovianChainTransformer::eliminateNonmarkovianStates( + result.first->template as>(), + !transformationSettings.isIgnoreLabelingSet()); + } result.second = true; } @@ -637,19 +645,31 @@ namespace storm { template void verifyProperties(SymbolicInput const& input, std::function(std::shared_ptr const& formula, std::shared_ptr const& states)> const& verificationCallback, std::function const&)> const& postprocessingCallback = PostprocessingIdentity()) { + auto transformationSettings = storm::settings::getModule(); auto const& properties = input.preprocessedProperties ? input.preprocessedProperties.get() : input.properties; for (auto const& property : properties) { printModelCheckingProperty(property); + bool ignored = false; storm::utility::Stopwatch watch(true); std::unique_ptr result; try { - result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula()); + auto rawFormula = property.getRawFormula(); + if (transformationSettings.isChainEliminationSet() && + !storm::transformer::NonMarkovianChainTransformer::preservesFormula(*rawFormula)) { + STORM_LOG_WARN("Property is not preserved by elimination of non-markovian states."); + ignored = true; + } else { + result = verificationCallback(property.getRawFormula(), + property.getFilter().getStatesFormula()); + } } catch (storm::exceptions::BaseException const& ex) { STORM_LOG_WARN("Cannot handle property: " << ex.what()); } watch.stop(); - postprocessingCallback(result); - printResult(result, property, &watch); + if (!ignored) { + postprocessingCallback(result); + printResult(result, property, &watch); + } } } diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 591f2ee2b..f14d3e6ca 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -7,11 +7,14 @@ #include "storm-dft/settings/modules/FaultTreeSettings.h" #include #include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/ResourceSettings.h" +#include "storm/settings/modules/TransformationSettings.h" #include "storm/utility/initialize.h" #include "storm-cli-utilities/cli.h" #include "storm-parsers/api/storm-parsers.h" +#include "storm-dft/transformations/DftTransformator.h" /*! @@ -26,7 +29,9 @@ void processOptions() { storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule(); storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule(); storm::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule(); + storm::settings::modules::TransformationSettings const &transformationSettings = storm::settings::getModule(); + auto dftTransformator = storm::transformations::dft::DftTransformator(); if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model given."); @@ -51,12 +56,15 @@ void processOptions() { storm::api::exportDFTToJsonFile(*dft, dftIOSettings.getExportJsonFilename()); } - if (dftIOSettings.isExportToSmt()) { - // Export to json - storm::api::exportDFTToSMT(*dft, dftIOSettings.getExportSmtFilename()); - return; + // Limit to one constantly failed BE + if (faultTreeSettings.isUniqueFailedBE()) { + dft = dftTransformator.transformUniqueFailedBe(*dft); } + // Eliminate non-binary dependencies + if (!dft->getDependencies().empty()) { + dft = dftTransformator.transformBinaryFDEPs(*dft); + } // Check well-formedness of DFT std::stringstream stream; if (!dft->checkWellFormedness(stream)) { @@ -77,16 +85,72 @@ void processOptions() { return; } + // SMT + if (dftIOSettings.isExportToSmt()) { + // Export to smtlib2 + storm::api::exportDFTToSMT(*dft, dftIOSettings.getExportSmtFilename()); + return; + } + + bool useSMT = false; + uint64_t solverTimeout = 10; +#ifdef STORM_HAVE_Z3 + if (faultTreeSettings.solveWithSMT()) { + useSMT = true; + STORM_PRINT("Use SMT for preprocessing" << std::endl) + } +#endif + + dft->setDynamicBehaviorInfo(); + + storm::api::PreprocessingResult preResults; + 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) << std::endl); + + preResults.fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, useSMT, + solverTimeout); + + if (preResults.fdepConflicts.empty()) { + STORM_LOG_DEBUG("No FDEP conflicts found" << std::endl); + } else { + STORM_LOG_DEBUG("========================================" << std::endl << + "FDEP CONFLICTS" << std::endl << + "========================================" + << std::endl); + } + for (auto pair: preResults.fdepConflicts) { + STORM_LOG_DEBUG("Conflict between " << dft->getElement(pair.first)->name() << " and " + << dft->getElement(pair.second)->name() << std::endl); + } + + // 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); + } + } + #ifdef STORM_HAVE_Z3 if (faultTreeSettings.solveWithSMT()) { // Solve with SMT - STORM_LOG_DEBUG("Running DFT analysis with use of SMT"); + STORM_LOG_DEBUG("Running DFT analysis with use of SMT" << std::endl); + // Set dynamic behavior vector storm::api::analyzeDFTSMT(*dft, true); - return; } #endif + // From now on we analyse DFT via model checking // Set min or max @@ -184,7 +248,6 @@ void processOptions() { } } - // Analyze DFT // TODO allow building of state space even without properties if (props.empty()) { @@ -195,7 +258,10 @@ void processOptions() { approximationError = faultTreeSettings.getApproximationError(); } storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, - faultTreeSettings.isAllowDCForRelevantEvents(), approximationError, faultTreeSettings.getApproximationHeuristic(), true); + faultTreeSettings.isAllowDCForRelevantEvents(), approximationError, + faultTreeSettings.getApproximationHeuristic(), + transformationSettings.isChainEliminationSet(), + transformationSettings.isIgnoreLabelingSet(), true); } } diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index 623d75a16..b4deb1cfa 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -31,45 +31,32 @@ namespace storm { } template<> - void exportDFTToSMT(storm::storage::DFT const& dft, std::string const& file) { + void exportDFTToSMT(storm::storage::DFT const &dft, std::string const &file) { storm::modelchecker::DFTASFChecker asfChecker(dft); asfChecker.convert(); asfChecker.toFile(file); } template<> - void exportDFTToSMT(storm::storage::DFT const& dft, std::string const& file) { + void exportDFTToSMT(storm::storage::DFT const &dft, std::string const &file) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export to SMT does not support this data type."); } template<> - std::vector + void analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput) { + uint64_t solverTimeout = 10; + storm::modelchecker::DFTASFChecker smtChecker(dft); smtChecker.toSolver(); - std::vector results; - - results.push_back(smtChecker.checkTleNeverFailed()); - uint64_t lower_bound = smtChecker.getLeastFailureBound(); - uint64_t upper_bound = smtChecker.getAlwaysFailedBound(); - if (printOutput) { - // TODO add suitable output function, maybe add query descriptions for better readability - for (size_t i = 0; i < results.size(); ++i) { - std::string tmp = "unknown"; - if (results.at(i) == storm::solver::SmtSolver::CheckResult::Sat) { - tmp = "SAT"; - } else if (results.at(i) == storm::solver::SmtSolver::CheckResult::Unsat) { - tmp = "UNSAT"; - } - } - std::cout << "Lower bound: " << std::to_string(lower_bound) << std::endl; - std::cout << "Upper bound: " << std::to_string(upper_bound) << std::endl; - } - return results; + // Removed bound computation etc. here + smtChecker.setSolverTimeout(solverTimeout); + smtChecker.checkTleNeverFailed(); + smtChecker.unsetSolverTimeout(); } template<> - std::vector + void analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Analysis by SMT not supported for this data type."); diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index c0f54f68b..1d053dc87 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -8,11 +8,19 @@ #include "storm-dft/modelchecker/dft/DFTModelChecker.h" #include "storm-dft/modelchecker/dft/DFTASFChecker.h" #include "storm-dft/transformations/DftToGspnTransformator.h" +#include "storm-dft/utility/FDEPConflictFinder.h" +#include "storm-dft/utility/FailureBoundFinder.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. @@ -71,6 +79,8 @@ namespace storm { * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events. * @param approximationError Allowed approximation error. Value 0 indicates no approximation. * @param approximationHeuristic Heuristic used for state space exploration. + * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA + * @param ignoreLabeling If true, the labeling of states is ignored during state elimination * @param printOutput If true, model information, timings, results, etc. are printed. * @return Results. */ @@ -78,11 +88,14 @@ namespace storm { typename storm::modelchecker::DFTModelChecker::dft_results analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred = true, bool allowModularisation = true, std::set const& relevantEvents = {}, bool allowDCForRelevantEvents = true, double approximationError = 0.0, - storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool printOutput = false) { + storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, + bool eliminateChains = false, bool ignoreLabeling = false, bool printOutput = false) { storm::modelchecker::DFTModelChecker modelChecker(printOutput); typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevantEvents, approximationError, - approximationHeuristic); + approximationHeuristic, + eliminateChains, + ignoreLabeling); if (printOutput) { modelChecker.printTimings(); modelChecker.printResults(results); @@ -98,7 +111,7 @@ namespace storm { * @return Result result vector */ template - std::vector + void analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput); /*! @@ -126,7 +139,7 @@ namespace storm { * @param file File. */ template - void exportDFTToSMT(storm::storage::DFT const& dft, std::string const& file); + void exportDFTToSMT(storm::storage::DFT const &dft, std::string const &file); /*! * Transform DFT to GSPN. diff --git a/src/storm-dft/builder/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp index 9bb40a8b6..c02fb3364 100644 --- a/src/storm-dft/builder/DFTBuilder.cpp +++ b/src/storm-dft/builder/DFTBuilder.cpp @@ -77,7 +77,6 @@ namespace storm { childElement->addOutgoingDependency(elem.first); } } - STORM_LOG_ASSERT(!binaryDependencies || dependencies.size() == 1, "Dependency '" << elem.first->name() << "' should only have one dependent element."); for (auto& be : dependencies) { elem.first->addDependentEvent(be); be->addIngoingDependency(elem.first); diff --git a/src/storm-dft/builder/DFTBuilder.h b/src/storm-dft/builder/DFTBuilder.h index 9ce85db0f..2529ff5c1 100644 --- a/src/storm-dft/builder/DFTBuilder.h +++ b/src/storm-dft/builder/DFTBuilder.h @@ -43,7 +43,8 @@ namespace storm { std::unordered_map mLayoutInfo; public: - DFTBuilder(bool defaultInclusive = true, bool binaryDependencies = true) : pandDefaultInclusive(defaultInclusive), porDefaultInclusive(defaultInclusive), binaryDependencies(binaryDependencies) { + DFTBuilder(bool defaultInclusive = true) : pandDefaultInclusive(defaultInclusive), + porDefaultInclusive(defaultInclusive) { } @@ -107,41 +108,13 @@ namespace storm { std::string trigger = children[0]; //TODO: collect constraints for SMT solving - //0 <= probability <= 1 - if (binaryDependencies && !storm::utility::isOne(probability) && children.size() > 2) { - // Introduce additional element for first capturing the probabilistic dependency - std::string nameAdditional = name + "_additional"; - addBasicElementConst(nameAdditional, false); - // First consider probabilistic dependency - addDepElement(name + "_pdep", {children.front(), nameAdditional}, probability); - // Then consider dependencies to the children if probabilistic dependency failed - std::vector newChildren = children; - newChildren[0] = nameAdditional; - addDepElement(name, newChildren, storm::utility::one()); - return true; - } else { - // Add dependencies - if(binaryDependencies) { - for (size_t i = 1; i < children.size(); ++i) { - std::string nameDep = name + "_" + std::to_string(i); - if (nameInUse(nameDep)) { - STORM_LOG_ERROR("Element with name '" << name << "' already exists."); - return false; - } - STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2, "PDep with multiple children supported."); - DFTDependencyPointer element = std::make_shared>(mNextId++, nameDep, probability); - mElements[element->name()] = element; - mDependencyChildNames[element] = {trigger, children[i]}; - mDependencies.push_back(element); - } - } else { - DFTDependencyPointer element = std::make_shared>(mNextId++, name, probability); - mElements[element->name()] = element; - mDependencyChildNames[element] = children; - mDependencies.push_back(element); - } - return true; - } + DFTDependencyPointer element = std::make_shared>(mNextId++, + name, + probability); + mElements[element->name()] = element; + mDependencyChildNames[element] = children; + mDependencies.push_back(element); + return true; } bool addVotElement(std::string const& name, unsigned threshold, std::vector const& children) { @@ -263,13 +236,13 @@ namespace storm { void topoVisit(DFTElementPointer const& n, std::map>& visited, DFTElementVector& L); DFTElementVector topoSort(); + + std::vector computeHasDynamicBehavior(DFTElementVector elements); // If true, the standard gate adders make a pand inclusive, and exclusive otherwise. bool pandDefaultInclusive; // If true, the standard gate adders make a pand inclusive, and exclusive otherwise. bool porDefaultInclusive; - - bool binaryDependencies; }; } diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index d673e57c5..7a12ad4a7 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -14,6 +14,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/logic/AtomicLabelFormula.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" +#include "storm/transformer/NonMarkovianChainTransformer.h" namespace storm { @@ -164,6 +165,26 @@ namespace storm { STORM_LOG_ASSERT(stateStorage.initialStateIndices.size() == 1, "Only one initial state assumed."); initialStateIndex = stateStorage.initialStateIndices[0]; STORM_LOG_TRACE("Initial state: " << initialStateIndex); + + // DFT may be instantly failed due to a constant failure + // in this case a model only consisting of the uniqueFailedState suffices + if (initialStateIndex == 0 && this->uniqueFailedState) { + modelComponents.markovianStates.resize(1); + modelComponents.deterministicModel = generator.isDeterministicModel(); + + STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates); + STORM_LOG_DEBUG("Model has 1 state"); + STORM_LOG_DEBUG( + "Model is " << (generator.isDeterministicModel() ? "deterministic" : "non-deterministic")); + + // Build transition matrix + modelComponents.transitionMatrix = matrixBuilder.builder.build(1, 1); + STORM_LOG_TRACE("Transition matrix: " << std::endl << modelComponents.transitionMatrix); + + buildLabeling(); + return; + } + // Initialize heuristic values for inital state STORM_LOG_ASSERT(!statesNotExplored.at(initialStateIndex).second, "Heuristic for initial state is already initialized"); ExplorationHeuristicPointer heuristic; @@ -651,9 +672,7 @@ namespace storm { maComponents.exitRates = std::move(modelComponents.exitRates); ma = std::make_shared>(std::move(maComponents)); } - if (ma->hasOnlyTrivialNondeterminism()) { - // Markov automaton can be converted into CTMC - // TODO: change components which were not moved accordingly + if (ma->isConvertibleToCtmc()) { model = ma->convertToCtmc(); } else { model = ma; diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index fcec7bb70..29dc71238 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -23,11 +23,53 @@ namespace storm { template std::vector DftNextStateGenerator::getInitialStates(StateToIdCallback const& stateToIdCallback) { DFTStatePointer initialState = std::make_shared>(mDft, mStateGenerationInfo, 0); + size_t constFailedBeCounter = 0; + std::shared_ptr const> constFailedBE = nullptr; + for (auto &be : mDft.getBasicElements()) { + if (be->type() == storm::storage::DFTElementType::BE_CONST) { + auto constBe = std::static_pointer_cast const>(be); + if (constBe->failed()) { + constFailedBeCounter++; + STORM_LOG_THROW(constFailedBeCounter < 2, storm::exceptions::NotSupportedException, + "DFTs with more than one constantly failed BE are not supported. Try using the option '--uniquefailedbe'."); + constFailedBE = constBe; + } + } + } + StateType id; + if (constFailedBeCounter == 0) { + // Register initial state + id = stateToIdCallback(initialState); + } else { + initialState->letNextBEFail(constFailedBE->id(), false); + // Propagate the constant failure to reach the real initial state + storm::storage::DFTStateSpaceGenerationQueues queues; + propagateFailure(initialState, constFailedBE, queues); + + if (initialState->hasFailed(mDft.getTopLevelIndex()) && uniqueFailedState) { + propagateFailsafe(initialState, constFailedBE, queues); - // Register initial state - StateType id = stateToIdCallback(initialState); + // Update failable dependencies + initialState->updateFailableDependencies(constFailedBE->id()); + initialState->updateDontCareDependencies(constFailedBE->id()); + initialState->updateFailableInRestrictions(constFailedBE->id()); + + // Unique failed state + id = 0; + } else { + propagateFailsafe(initialState, constFailedBE, queues); + + // Update failable dependencies + initialState->updateFailableDependencies(constFailedBE->id()); + initialState->updateDontCareDependencies(constFailedBE->id()); + initialState->updateFailableInRestrictions(constFailedBE->id()); + + id = stateToIdCallback(initialState); + } + } initialState->setId(id); + return {id}; } @@ -78,13 +120,8 @@ namespace storm { Choice choice(0, !exploreDependencies); // Let BE fail - bool isFirst = true; while (!state->getFailableElements().isEnd()) { - if (takeFirstDependency && exploreDependencies && !isFirst) { - // We discard further exploration as we already chose one dependent event - break; - } - isFirst = false; + //TODO outside // Construct new state as copy from original one DFTStatePointer newState = state->copy(); @@ -97,31 +134,7 @@ namespace storm { // Propagate storm::storage::DFTStateSpaceGenerationQueues queues; - // Propagate failure - for (DFTGatePointer parent : nextBE->parents()) { - if (newState->isOperational(parent->id())) { - queues.propagateFailure(parent); - } - } - // Propagate failures - while (!queues.failurePropagationDone()) { - DFTGatePointer next = queues.nextFailurePropagation(); - next->checkFails(*newState, queues); - newState->updateFailableDependencies(next->id()); - newState->updateFailableInRestrictions(next->id()); - } - - // Check restrictions - for (DFTRestrictionPointer restr : nextBE->restrictions()) { - queues.checkRestrictionLater(restr); - } - // Check restrictions - while(!queues.restrictionChecksDone()) { - DFTRestrictionPointer next = queues.nextRestrictionCheck(); - next->checkFails(*newState, queues); - newState->updateFailableDependencies(next->id()); - newState->updateFailableInRestrictions(next->id()); - } + propagateFailure(newState, nextBE, queues); bool transient = false; if (nextBE->type() == storm::storage::DFTElementType::BE_EXP) { @@ -142,18 +155,7 @@ namespace storm { // Use unique failed state newStateId = 0; } else { - // Propagate failsafe - while (!queues.failsafePropagationDone()) { - DFTGatePointer next = queues.nextFailsafePropagation(); - next->checkFailsafe(*newState, queues); - } - - // Propagate dont cares - // Relevance is considered for each element independently - while (!queues.dontCarePropagationDone()) { - DFTElementPointer next = queues.nextDontCarePropagation(); - next->checkDontCareAnymore(*newState, queues); - } + propagateFailsafe(newState, nextBE, queues); // Update failable dependencies newState->updateFailableDependencies(nextBE->id()); @@ -166,7 +168,7 @@ namespace storm { // Set transitions if (exploreDependencies) { - // Failure is due to dependency -> add non-deterministic choice + // Failure is due to dependency -> add non-deterministic choice if necessary ValueType probability = mDft.getDependency(state->getFailableElements().get())->probability(); choice.addProbability(newStateId, probability); STORM_LOG_TRACE("Added transition to " << newStateId << " with probability " << probability); @@ -227,6 +229,56 @@ namespace storm { return result; } + template + void DftNextStateGenerator::propagateFailure(DFTStatePointer newState, + std::shared_ptr const> &nextBE, + storm::storage::DFTStateSpaceGenerationQueues &queues) { + // Propagate failure + for (DFTGatePointer parent : nextBE->parents()) { + if (newState->isOperational(parent->id())) { + queues.propagateFailure(parent); + } + } + // Propagate failures + while (!queues.failurePropagationDone()) { + DFTGatePointer next = queues.nextFailurePropagation(); + next->checkFails(*newState, queues); + newState->updateFailableDependencies(next->id()); + newState->updateFailableInRestrictions(next->id()); + } + + // Check restrictions + for (DFTRestrictionPointer restr : nextBE->restrictions()) { + queues.checkRestrictionLater(restr); + } + // Check restrictions + while (!queues.restrictionChecksDone()) { + DFTRestrictionPointer next = queues.nextRestrictionCheck(); + next->checkFails(*newState, queues); + newState->updateFailableDependencies(next->id()); + newState->updateFailableInRestrictions(next->id()); + } + + } + + template + void DftNextStateGenerator::propagateFailsafe(DFTStatePointer newState, + std::shared_ptr const> &nextBE, + storm::storage::DFTStateSpaceGenerationQueues &queues) { + // Propagate failsafe + while (!queues.failsafePropagationDone()) { + DFTGatePointer next = queues.nextFailsafePropagation(); + next->checkFailsafe(*newState, queues); + } + + // Propagate dont cares + // Relevance is considered for each element independently + while (!queues.dontCarePropagationDone()) { + DFTElementPointer next = queues.nextDontCarePropagation(); + next->checkDontCareAnymore(*newState, queues); + } + } + template StateBehavior DftNextStateGenerator::createMergeFailedState(StateToIdCallback const& stateToIdCallback) { this->uniqueFailedState = true; diff --git a/src/storm-dft/generator/DftNextStateGenerator.h b/src/storm-dft/generator/DftNextStateGenerator.h index fc7580a13..1e912655f 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.h +++ b/src/storm-dft/generator/DftNextStateGenerator.h @@ -48,6 +48,26 @@ namespace storm { */ StateBehavior createMergeFailedState(StateToIdCallback const& stateToIdCallback); + /** + * Propagate the failures in a given state if the given BE fails + * + * @param newState starting state of the propagation + * @param nextBE BE whose failure is propagated + */ + void + propagateFailure(DFTStatePointer newState, std::shared_ptr const> &nextBE, + storm::storage::DFTStateSpaceGenerationQueues &queues); + + /** + * Propagate the failsafe state in a given state if the given BE fails + * + * @param newState starting state of the propagation + * @param nextBE BE whose failure is propagated + */ + void + propagateFailsafe(DFTStatePointer newState, std::shared_ptr const> &nextBE, + storm::storage::DFTStateSpaceGenerationQueues &queues); + private: /*! diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index b43edf72b..558e2a45c 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -24,6 +24,9 @@ namespace storm { void DFTASFChecker::convert() { std::vector beVariables; + uint64_t failedBeVariables; + std::vector failsafeBeVariables; + bool failedBeIsSet = false; notFailed = dft.nrBasicElements() + 1; // Value indicating the element is not failed // Initialize variables @@ -35,9 +38,21 @@ namespace storm { case storm::storage::DFTElementType::BE_EXP: beVariables.push_back(varNames.size() - 1); break; - case storm::storage::DFTElementType::BE_CONST: - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Constant BEs are not supported in SMT translation."); + 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); + } break; + } case storm::storage::DFTElementType::SPARE: { auto spare = std::static_pointer_cast const>(element); @@ -66,14 +81,50 @@ namespace storm { // Generate constraints - // All BEs have to fail (first part of constraint 12) + // All exponential BEs have to fail (first part of constraint 12) for (auto const &beV : beVariables) { - constraints.push_back(std::make_shared(beV, 1, dft.nrBasicElements())); + constraints.push_back(std::make_shared(beV, 1, notFailed - 1)); + } + + // Constantly failsafe BEs may also be fail-safe + for (auto const &beV : failsafeBeVariables) { + constraints.push_back(std::make_shared(beV, 1, notFailed)); } - // No two BEs fail at the same time (second part of constraint 12) - constraints.push_back(std::make_shared(beVariables)); - constraints.back()->setDescription("No two BEs fail at the same time"); + // Constantly failed BEs fail before other types + if (failedBeIsSet) { + constraints.push_back(std::make_shared(failedBeVariables, 0)); + } + + + std::vector allBeVariables; + allBeVariables.insert(std::end(allBeVariables), std::begin(beVariables), std::end(beVariables)); + allBeVariables.insert(std::end(allBeVariables), std::begin(failsafeBeVariables), + std::end(failsafeBeVariables)); + + // No two exponential BEs fail at the same time (second part of constraint 12) + if (beVariables.size() > 1) { + constraints.push_back(std::make_shared(beVariables)); + constraints.back()->setDescription("No two BEs fail at the same time"); + } + + bool descFlag = true; + for (auto const &failsafeBe : failsafeBeVariables) { + std::vector > unequalConstraints; + for (auto const &otherBe: allBeVariables) { + if (otherBe != failsafeBe) { + unequalConstraints.push_back(std::make_shared(failsafeBe, otherBe)); + } + } + constraints.push_back( + std::make_shared(std::make_shared(failsafeBe, notFailed), + std::make_shared(unequalConstraints))); + if (descFlag) { + constraints.back()->setDescription( + "Initially failsafe BEs don't fail at the same time as other BEs"); + descFlag = false; + } + } // Initialize claim variables in [1, |BE|+1] for (auto const &claimVariable : claimVariables) { @@ -135,6 +186,45 @@ namespace storm { // Handle dependencies addMarkovianConstraints(); + + // Failsafe BEs may only fail in non-Markovian states (i.e. if they were triggered) + std::vector> failsafeNotIConstr; + for (uint64_t i = 0; i < dft.nrBasicElements(); ++i) { + failsafeNotIConstr.clear(); + for (auto const &beV : failsafeBeVariables) { + failsafeNotIConstr.push_back(std::make_shared(beV, i + 1)); + } + // If state i+1 is Markovian (i.e. m_i = true), all failsafeBEVariables are not equal to i+1 + constraints.push_back( + std::make_shared(std::make_shared(markovianVariables.at(i), true), + std::make_shared(failsafeNotIConstr))); + if (i == 0) { + constraints.back()->setDescription("Failsafe BEs fail only if they are triggered"); + } + } + + + // A failsafe BE only stays failsafe if no trigger has been triggered + 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) { + 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"); + } + } + } + } // Constraint Generator Functions @@ -341,7 +431,7 @@ namespace storm { auto const &trigger = dependency->triggerEvent(); std::vector dependentIndices; for (size_t j = 0; j < dependentEvents.size(); ++j) { - dependentIndices.push_back(dependentEvents[j]->id()); + dependentIndices.push_back(timePointVariables.at(dependentEvents[j]->id())); } constraints.push_back(std::make_shared(dependencyVariables.at(i), dependentIndices)); @@ -513,7 +603,6 @@ namespace storm { for (auto const &constraint : constraints) { solver->add(constraint->toExpression(varNames, manager)); } - } storm::solver::SmtSolver::CheckResult DFTASFChecker::checkTleFailsWithEq(uint64_t bound) { @@ -565,6 +654,7 @@ namespace storm { DFTASFChecker::checkFailsLeqWithEqNonMarkovianState(uint64_t checkbound, uint64_t nrNonMarkovian) { STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); std::vector markovianIndices; + checkbound = std::min(checkbound, markovianVariables.size()); // Get Markovian variable indices up until given timepoint for (uint64_t i = 0; i < checkbound; ++i) { markovianIndices.push_back(markovianVariables.at(i)); @@ -576,7 +666,6 @@ namespace storm { timePointVariables.at(dft.getTopLevelIndex()), checkbound); std::shared_ptr manager = solver->getManager().getSharedPointer(); solver->add(tleFailedConstr->toExpression(varNames, manager)); - // Constraint that a given number of non-Markovian states are visited std::shared_ptr nonMarkovianConstr = std::make_shared( markovianIndices, nrNonMarkovian); @@ -587,158 +676,76 @@ namespace storm { } storm::solver::SmtSolver::CheckResult - DFTASFChecker::checkFailsAtTimepointWithOnlyMarkovianState(uint64_t timepoint) { + DFTASFChecker::checkFailsAtTimepointWithEqNonMarkovianState(uint64_t timepoint, uint64_t nrNonMarkovian) { STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); std::vector markovianIndices; - // Get Markovian variable indices + timepoint = std::min(timepoint, markovianVariables.size()); + // Get Markovian variable indices up until given timepoint for (uint64_t i = 0; i < timepoint; ++i) { markovianIndices.push_back(markovianVariables.at(i)); } // Set backtracking marker to check several properties without reconstructing DFT encoding solver->push(); - // Constraint that toplevel element can fail with less than 'checkNumber' Markovian states visited - std::shared_ptr countConstr = std::make_shared( - markovianIndices, timepoint); - // Constraint that TLE fails at timepoint - std::shared_ptr timepointConstr = std::make_shared( + // Constraint that TLE fails before or during given timepoint + std::shared_ptr tleFailedConstr = std::make_shared( timePointVariables.at(dft.getTopLevelIndex()), timepoint); std::shared_ptr manager = solver->getManager().getSharedPointer(); - solver->add(countConstr->toExpression(varNames, manager)); - solver->add(timepointConstr->toExpression(varNames, manager)); + solver->add(tleFailedConstr->toExpression(varNames, manager)); + // Constraint that a given number of non-Markovian states are visited + std::shared_ptr nonMarkovianConstr = std::make_shared( + markovianIndices, nrNonMarkovian); + solver->add(nonMarkovianConstr->toExpression(varNames, manager)); storm::solver::SmtSolver::CheckResult res = solver->check(); solver->pop(); return res; } - uint64_t DFTASFChecker::correctLowerBound(uint64_t bound, uint_fast64_t timeout) { - STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); - STORM_LOG_DEBUG("Lower bound correction - try to correct bound " << std::to_string(bound)); - uint64_t boundCandidate = bound; - uint64_t nrDepEvents = 0; - uint64_t nrNonMarkovian = 0; - // Count dependent events - for (size_t i = 0; i < dft.nrElements(); ++i) { - std::shared_ptr const> element = dft.getElement(i); - if (element->isBasicElement()) { - auto be = std::static_pointer_cast const>(element); - if (be->hasIngoingDependencies()) { - ++nrDepEvents; - } - } - } - // Only need to check as long as bound candidate + nr of non-Markovians to check is smaller than number of dependent events - while (nrNonMarkovian <= nrDepEvents && boundCandidate > 0) { - STORM_LOG_TRACE( - "Lower bound correction - check possible bound " << std::to_string(boundCandidate) << " with " - << std::to_string(nrNonMarkovian) - << " non-Markovian states"); - setSolverTimeout(timeout * 1000); - storm::solver::SmtSolver::CheckResult tmp_res = - checkFailsLeqWithEqNonMarkovianState(boundCandidate + nrNonMarkovian, nrNonMarkovian); - unsetSolverTimeout(); - switch (tmp_res) { - case storm::solver::SmtSolver::CheckResult::Sat: - /* If SAT, there is a sequence where only boundCandidate-many BEs fail directly and rest is nonMarkovian. - * Bound candidate is vaild, therefore check the next one */ - STORM_LOG_TRACE("Lower bound correction - SAT"); - --boundCandidate; - break; - case storm::solver::SmtSolver::CheckResult::Unknown: - // If any query returns unknown, we cannot be sure about the bound and fall back to the naive one - STORM_LOG_DEBUG("Lower bound correction - Solver returned 'Unknown', corrected to 1"); - return 1; - default: - // if query is UNSAT, increase number of non-Markovian states and try again - STORM_LOG_TRACE("Lower bound correction - UNSAT"); - ++nrNonMarkovian; - break; - } - } - // if for one candidate all queries are UNSAT, it is not valid. Return last valid candidate - STORM_LOG_DEBUG("Lower bound correction - corrected bound to " << std::to_string(boundCandidate + 1)); - return boundCandidate + 1; - } - - uint64_t DFTASFChecker::correctUpperBound(uint64_t bound, uint_fast64_t timeout) { - STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); - STORM_LOG_DEBUG("Upper bound correction - try to correct bound " << std::to_string(bound)); - - while (bound > 1) { - setSolverTimeout(timeout * 1000); - storm::solver::SmtSolver::CheckResult tmp_res = - checkFailsAtTimepointWithOnlyMarkovianState(bound); - unsetSolverTimeout(); - switch (tmp_res) { - case storm::solver::SmtSolver::CheckResult::Sat: - STORM_LOG_DEBUG("Upper bound correction - corrected bound to " << std::to_string(bound)); - return bound; - case storm::solver::SmtSolver::CheckResult::Unknown: - STORM_LOG_DEBUG("Upper bound correction - Solver returned 'Unknown', corrected to "); - return bound; - default: - --bound; - break; - - } - } - STORM_LOG_DEBUG("Upper bound correction - corrected bound to " << std::to_string(bound)); - return bound; - } - - uint64_t DFTASFChecker::getLeastFailureBound(uint_fast64_t timeout) { - STORM_LOG_TRACE("Compute lower bound for number of BE failures necessary for the DFT to fail"); - STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); - uint64_t bound = 0; - while (bound < notFailed) { - setSolverTimeout(timeout * 1000); - storm::solver::SmtSolver::CheckResult tmp_res = checkTleFailsWithLeq(bound); - unsetSolverTimeout(); - switch (tmp_res) { - case storm::solver::SmtSolver::CheckResult::Sat: - if (!dft.getDependencies().empty()) { - return correctLowerBound(bound, timeout); - } else { - return bound; - } - case storm::solver::SmtSolver::CheckResult::Unknown: - STORM_LOG_DEBUG("Lower bound: Solver returned 'Unknown'"); - return bound; - default: - ++bound; - break; - } + storm::solver::SmtSolver::CheckResult + DFTASFChecker::checkDependencyConflict(uint64_t dep1Index, uint64_t dep2Index, uint64_t timeout) { + std::vector> andConstr; + std::vector> orConstr; + STORM_LOG_DEBUG( + "Check " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + andConstr.clear(); + // AND FDEP1 is triggered before FDEP2 is resolved + andConstr.push_back(std::make_shared( + timePointVariables.at(dep1Index), timePointVariables.at(dep2Index))); + andConstr.push_back(std::make_shared( + timePointVariables.at(dep1Index), dependencyVariables.at(dep2Index))); + std::shared_ptr betweenConstr1 = std::make_shared(andConstr); + + andConstr.clear(); + // AND FDEP2 is triggered before FDEP1 is resolved + andConstr.push_back(std::make_shared( + timePointVariables.at(dep2Index), timePointVariables.at(dep1Index))); + andConstr.push_back(std::make_shared( + timePointVariables.at(dep2Index), dependencyVariables.at(dep1Index))); + std::shared_ptr betweenConstr2 = std::make_shared(andConstr); + + orConstr.clear(); + // Either one of the above constraints holds + orConstr.push_back(betweenConstr1); + orConstr.push_back(betweenConstr2); + + // Both FDEPs were triggered before dependent elements have failed + andConstr.clear(); + andConstr.push_back(std::make_shared( + timePointVariables.at(dep1Index), dependencyVariables.at(dep1Index))); + andConstr.push_back(std::make_shared( + timePointVariables.at(dep2Index), dependencyVariables.at(dep2Index))); + andConstr.push_back(std::make_shared(orConstr)); + + std::shared_ptr checkConstr = std::make_shared(andConstr); - } - return bound; + std::shared_ptr manager = solver->getManager().getSharedPointer(); + solver->push(); + solver->add(checkConstr->toExpression(varNames, manager)); + setSolverTimeout(timeout * 1000); + storm::solver::SmtSolver::CheckResult res = solver->check(); + unsetSolverTimeout(); + solver->pop(); + return res; } - uint64_t DFTASFChecker::getAlwaysFailedBound(uint_fast64_t timeout) { - STORM_LOG_TRACE("Compute bound for number of BE failures such that the DFT always fails"); - STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); - if (checkTleNeverFailed() == storm::solver::SmtSolver::CheckResult::Sat) { - return notFailed; - } - uint64_t bound = notFailed - 1; - while (bound >= 0) { - setSolverTimeout(timeout * 1000); - storm::solver::SmtSolver::CheckResult tmp_res = checkTleFailsWithEq(bound); - unsetSolverTimeout(); - switch (tmp_res) { - case storm::solver::SmtSolver::CheckResult::Sat: - if (!dft.getDependencies().empty()) { - return correctUpperBound(bound, timeout); - } else { - return bound; - } - case storm::solver::SmtSolver::CheckResult::Unknown: - STORM_LOG_DEBUG("Upper bound: Solver returned 'Unknown'"); - return bound; - default: - --bound; - break; - } - } - return bound; - } } } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index 84310b775..8a6e3fda2 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -44,6 +44,7 @@ namespace storm { using ValueType = double; public: DFTASFChecker(storm::storage::DFT const&); + /** * Generate general variables and constraints for the DFT and store them in the corresponding maps and vectors * @@ -80,21 +81,18 @@ namespace storm { storm::solver::SmtSolver::CheckResult checkTleFailsWithLeq(uint64_t bound); /** - * Get the minimal number of BEs necessary for the TLE to fail (lower bound for number of failures to check) + * Check if two given dependencies are conflicting in their resolution, i.e. check if non-determinism may occur. + * Note that this is a very conservative check using SMT formulae. + * We only check if sequences exist, where one of the dependencies is triggered before the other is completely resolved * - * @param timeout timeout for each query in seconds, defaults to 10 seconds - * @return the minimal number + * @param dep1Index Index of the first dependency + * @param dep2Index Index of the second dependency + * @param timeout timeout for the solver + * @return "Sat" if the dependencies are conflicting, "Unsat" if they are not, otherwise "Unknown" */ - uint64_t getLeastFailureBound(uint_fast64_t timeout = 10); + storm::solver::SmtSolver::CheckResult + checkDependencyConflict(uint64_t dep1Index, uint64_t dep2Index, uint64_t timeout = 10); - /** - * Get the number of BE failures for which the TLE always fails (upper bound for number of failures to check). - * Note that the returned value may be higher than the real one when dependencies are present. - * - * @param timeout timeout for each query in seconds, defaults to 10 seconds - * @return the number - */ - uint64_t getAlwaysFailedBound(uint_fast64_t timeout = 10); /** * Set the timeout of the solver @@ -107,8 +105,14 @@ namespace storm { * Unset the timeout for the solver */ void unsetSolverTimeout(); - - private: + + /** + * Get a reference to the DFT + */ + storm::storage::DFT const &getDFT() { + return dft; + } + /** * Helper function to check if the TLE fails before or at a given timepoint while visiting exactly * a given number of non-Markovian states @@ -122,34 +126,16 @@ namespace storm { checkFailsLeqWithEqNonMarkovianState(uint64_t checkbound, uint64_t nrNonMarkovian); /** - * Helper function that checks if the DFT can fail at a timepoint while visiting less than a given number of Markovian states + * Helper function that checks if the DFT can fail at a timepoint while visiting a given number of Markovian states * * @param timepoint point in time to check * @return "Sat" if a sequence of BE failures exists such that less than checkNumber Markovian states are visited, * "Unsat" if it does not, otherwise "Unknown" */ - storm::solver::SmtSolver::CheckResult checkFailsAtTimepointWithOnlyMarkovianState(uint64_t timepoint); - - /** - * Helper function for correction of least failure bound when dependencies are present. - * The main idea is to check if a later point of failure for the TLE than the pre-computed bound exists, but - * up until that point the number of non-Markovian states visited is so large, that less than the pre-computed bound BEs fail by themselves. - * The corrected bound is then (newTLEFailureTimepoint)-(nrNonMarkovianStatesVisited). This term is minimized. - * - * @param bound known lower bound to be corrected - * @param timeout timeout timeout for each query in seconds - * @return the corrected bound - */ - uint64_t correctLowerBound(uint64_t bound, uint_fast64_t timeout); - - /** - * Helper function for correction of bound for number of BEs such that the DFT always fails when dependencies are present - * - * @param bound known bound to be corrected - * @param timeout timeout timeout for each query in seconds - * @return the corrected bound - */ - uint64_t correctUpperBound(uint64_t bound, uint_fast64_t timeout); + storm::solver::SmtSolver::CheckResult + checkFailsAtTimepointWithEqNonMarkovianState(uint64_t timepoint, uint64_t nrNonMarkovian); + + private: uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const; diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 4e4befb1e..ca62ea406 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -7,6 +7,7 @@ #include "storm/utility/DirectEncodingExporter.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/models/ModelType.h" #include "storm-dft/builder/ExplicitDFTModelBuilder.h" #include "storm-dft/storage/dft/DFTIsomorphism.h" @@ -17,7 +18,13 @@ namespace storm { namespace modelchecker { template - typename DFTModelChecker::dft_results DFTModelChecker::check(storm::storage::DFT const& origDft, std::vector> const& properties, bool symred, bool allowModularisation, std::set const& relevantEvents, bool allowDCForRelevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) { + typename DFTModelChecker::dft_results + DFTModelChecker::check(storm::storage::DFT const &origDft, + std::vector> const &properties, + bool symred, bool allowModularisation, std::set const &relevantEvents, + bool allowDCForRelevantEvents, double approximationError, + storm::builder::ApproximationHeuristic approximationHeuristic, + bool eliminateChains, bool ignoreLabeling) { totalTimer.start(); dft_results results; @@ -30,21 +37,32 @@ namespace storm { // TODO: distinguish for all properties, not only for first one if (properties[0]->isTimeOperatorFormula() && allowModularisation) { // Use parallel composition as modularisation approach for expected time - std::shared_ptr> model = buildModelViaComposition(dft, properties, symred, true, relevantEvents); + std::shared_ptr> model = buildModelViaComposition(dft, + properties, + symred, true, + relevantEvents); // Model checking std::vector resultsValue = checkModel(model, properties); for (ValueType result : resultsValue) { results.push_back(result); } } else { - results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevantEvents, approximationError, approximationHeuristic); + results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, + allowDCForRelevantEvents, approximationError, approximationHeuristic, + eliminateChains, ignoreLabeling); } totalTimer.stop(); return results; } template - typename DFTModelChecker::dft_results DFTModelChecker::checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set const& relevantEvents, bool allowDCForRelevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) { + typename DFTModelChecker::dft_results + DFTModelChecker::checkHelper(storm::storage::DFT const &dft, + property_vector const &properties, bool symred, + bool allowModularisation, std::set const &relevantEvents, + bool allowDCForRelevantEvents, double approximationError, + storm::builder::ApproximationHeuristic approximationHeuristic, + bool eliminateChains, bool ignoreLabeling) { STORM_LOG_TRACE("Check helper called"); std::vector> dfts; bool invResults = false; @@ -52,7 +70,7 @@ namespace storm { size_t nrM = 0; // K out of M // Try modularisation - if(allowModularisation) { + if (allowModularisation) { switch (dft.topLevelType()) { case storm::storage::DFTElementType::AND: STORM_LOG_TRACE("top modularisation called AND"); @@ -73,9 +91,10 @@ namespace storm { STORM_LOG_TRACE("top modularisation called VOT"); dfts = dft.topModularisation(); STORM_LOG_TRACE("Modularisation into " << dfts.size() << " submodules."); - nrK = std::static_pointer_cast const>(dft.getTopLevelGate())->threshold(); + nrK = std::static_pointer_cast const>( + dft.getTopLevelGate())->threshold(); nrM = dfts.size(); - if(nrK <= nrM/2) { + if (nrK <= nrM / 2) { nrK -= 1; invResults = true; } @@ -87,7 +106,7 @@ namespace storm { } // Perform modularisation - if(dfts.size() > 1) { + if (dfts.size() > 1) { STORM_LOG_TRACE("Recursive CHECK Call"); // TODO: compute simultaneously dft_results results; @@ -97,39 +116,42 @@ namespace storm { } else { // Recursively call model checking std::vector res; - for(auto const ft : dfts) { + for (auto const ft : dfts) { // TODO: allow approximation in modularisation - dft_results ftResults = checkHelper(ft, {property}, symred, true, relevantEvents, allowDCForRelevantEvents, 0.0); + dft_results ftResults = checkHelper(ft, {property}, symred, true, relevantEvents, + allowDCForRelevantEvents, 0.0); STORM_LOG_ASSERT(ftResults.size() == 1, "Wrong number of results"); res.push_back(boost::get(ftResults[0])); } // Combine modularisation results - STORM_LOG_TRACE("Combining all results... K=" << nrK << "; M=" << nrM << "; invResults=" << (invResults?"On":"Off")); + STORM_LOG_TRACE("Combining all results... K=" << nrK << "; M=" << nrM << "; invResults=" + << (invResults ? "On" : "Off")); ValueType result = storm::utility::zero(); - int limK = invResults ? -1 : nrM+1; + int limK = invResults ? -1 : nrM + 1; int chK = invResults ? -1 : 1; // WARNING: there is a bug for computing permutations with more than 32 elements - STORM_LOG_THROW(res.size() < 32, storm::exceptions::NotSupportedException, "Permutations work only for < 32 elements"); - for(int cK = nrK; cK != limK; cK += chK ) { + STORM_LOG_THROW(res.size() < 32, storm::exceptions::NotSupportedException, + "Permutations work only for < 32 elements"); + for (int cK = nrK; cK != limK; cK += chK) { STORM_LOG_ASSERT(cK >= 0, "ck negative."); size_t permutation = smallestIntWithNBitsSet(static_cast(cK)); do { - STORM_LOG_TRACE("Permutation="<() - result; } results.push_back(result); @@ -138,19 +160,25 @@ namespace storm { return results; } else { // No modularisation was possible - return checkDFT(dft, properties, symred, relevantEvents, allowDCForRelevantEvents, approximationError, approximationHeuristic); + return checkDFT(dft, properties, symred, relevantEvents, allowDCForRelevantEvents, approximationError, + approximationHeuristic, eliminateChains, ignoreLabeling); } } template - std::shared_ptr> DFTModelChecker::buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set const& relevantEvents, bool allowDCForRelevantEvents) { + std::shared_ptr> + DFTModelChecker::buildModelViaComposition(storm::storage::DFT const &dft, + property_vector const &properties, bool symred, + bool allowModularisation, + std::set const &relevantEvents, + bool allowDCForRelevantEvents) { // TODO: use approximation? STORM_LOG_TRACE("Build model via composition"); std::vector> dfts; bool isAnd = true; // Try modularisation - if(allowModularisation) { + if (allowModularisation) { switch (dft.topLevelType()) { case storm::storage::DFTElementType::AND: STORM_LOG_TRACE("top modularisation called AND"); @@ -174,7 +202,7 @@ namespace storm { } // Perform modularisation via parallel composition - if(dfts.size() > 1) { + if (dfts.size() > 1) { STORM_LOG_TRACE("Recursive CHECK Call"); bool firstTime = true; std::shared_ptr> composedModel; @@ -185,7 +213,7 @@ namespace storm { // Find symmetries std::map>> emptySymmetry; storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); - if(symred) { + if (symred) { auto colouring = ft.colourDFT(); symmetries = ft.findSymmetries(colouring); STORM_LOG_DEBUG("Found " << symmetries.groups.size() << " symmetries."); @@ -199,24 +227,31 @@ namespace storm { std::shared_ptr> model = builder.getModel(); explorationTimer.stop(); - STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); + STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), + storm::exceptions::NotSupportedException, + "Parallel composition only applicable for CTMCs"); std::shared_ptr> ctmc = model->template as>(); // Apply bisimulation to new CTMC bisimulationTimer.start(); - ctmc = storm::api::performDeterministicSparseBisimulationMinimization>(ctmc, properties, storm::storage::BisimulationType::Weak)->template as>(); + ctmc = storm::api::performDeterministicSparseBisimulationMinimization>( + ctmc, properties, + storm::storage::BisimulationType::Weak)->template as>(); bisimulationTimer.stop(); if (firstTime) { composedModel = ctmc; firstTime = false; } else { - composedModel = storm::builder::ParallelCompositionBuilder::compose(composedModel, ctmc, isAnd); + composedModel = storm::builder::ParallelCompositionBuilder::compose(composedModel, + ctmc, isAnd); } // Apply bisimulation to parallel composition bisimulationTimer.start(); - composedModel = storm::api::performDeterministicSparseBisimulationMinimization>(composedModel, properties, storm::storage::BisimulationType::Weak)->template as>(); + composedModel = storm::api::performDeterministicSparseBisimulationMinimization>( + composedModel, properties, + storm::storage::BisimulationType::Weak)->template as>(); bisimulationTimer.stop(); STORM_LOG_DEBUG("No. states (Composed): " << composedModel->getNumberOfStates()); @@ -236,7 +271,7 @@ namespace storm { // Find symmetries std::map>> emptySymmetry; storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); - if(symred) { + if (symred) { auto colouring = dft.colourDFT(); symmetries = dft.findSymmetries(colouring); STORM_LOG_DEBUG("Found " << symmetries.groups.size() << " symmetries."); @@ -245,24 +280,33 @@ namespace storm { // Build a single CTMC STORM_LOG_DEBUG("Building Model..."); - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents, allowDCForRelevantEvents); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents, + allowDCForRelevantEvents); builder.buildModel(0, 0.0); std::shared_ptr> model = builder.getModel(); //model->printModelInformationToStream(std::cout); explorationTimer.stop(); - STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); + STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), + storm::exceptions::NotSupportedException, + "Parallel composition only applicable for CTMCs"); return model->template as>(); } } template - typename DFTModelChecker::dft_results DFTModelChecker::checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, std::set const& relevantEvents, bool allowDCForRelevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) { + typename DFTModelChecker::dft_results + DFTModelChecker::checkDFT(storm::storage::DFT const &dft, + property_vector const &properties, bool symred, + std::set const &relevantEvents, bool allowDCForRelevantEvents, + double approximationError, + storm::builder::ApproximationHeuristic approximationHeuristic, + bool eliminateChains, bool ignoreLabeling) { explorationTimer.start(); // Find symmetries std::map>> emptySymmetry; storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); - if(symred) { + if (symred) { auto colouring = dft.colourDFT(); symmetries = dft.findSymmetries(colouring); STORM_LOG_DEBUG("Found " << symmetries.groups.size() << " symmetries."); @@ -273,10 +317,12 @@ namespace storm { // Comparator for checking the error of the approximation storm::utility::ConstantsComparator comparator; // Build approximate Markov Automata for lower and upper bound - approximation_result approxResult = std::make_pair(storm::utility::zero(), storm::utility::zero()); + approximation_result approxResult = std::make_pair(storm::utility::zero(), + storm::utility::zero()); std::shared_ptr> model; std::vector newResult; - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents, allowDCForRelevantEvents); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents, + allowDCForRelevantEvents); // TODO: compute approximation for all properties simultaneously? std::shared_ptr property = properties[0]; @@ -285,7 +331,9 @@ namespace storm { } bool probabilityFormula = property->isProbabilityOperatorFormula(); - STORM_LOG_ASSERT((property->isTimeOperatorFormula() && !probabilityFormula) || (!property->isTimeOperatorFormula() && probabilityFormula), "Probability formula not initialized correctly"); + STORM_LOG_ASSERT((property->isTimeOperatorFormula() && !probabilityFormula) || + (!property->isTimeOperatorFormula() && probabilityFormula), + "Probability formula not initialized correctly"); size_t iteration = 0; do { // Iteratively build finer models @@ -310,7 +358,9 @@ namespace storm { // Check lower bounds newResult = checkModel(model, {property}); STORM_LOG_ASSERT(newResult.size() == 1, "Wrong size for result vector."); - STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(newResult[0], approxResult.first), "New under-approximation " << newResult[0] << " is smaller than old result " << approxResult.first); + STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(newResult[0], approxResult.first), + "New under-approximation " << newResult[0] << " is smaller than old result " + << approxResult.first); approxResult.first = newResult[0]; // Build model for upper bound @@ -321,17 +371,27 @@ namespace storm { // Check upper bound newResult = checkModel(model, {property}); STORM_LOG_ASSERT(newResult.size() == 1, "Wrong size for result vector."); - STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(approxResult.second, newResult[0]), "New over-approximation " << newResult[0] << " is greater than old result " << approxResult.second); + STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(approxResult.second, newResult[0]), + "New over-approximation " << newResult[0] << " is greater than old result " + << approxResult.second); approxResult.second = newResult[0]; ++iteration; - STORM_LOG_ASSERT(comparator.isLess(approxResult.first, approxResult.second) || comparator.isEqual(approxResult.first, approxResult.second), "Under-approximation " << approxResult.first << " is greater than over-approximation " << approxResult.second); + STORM_LOG_ASSERT(comparator.isLess(approxResult.first, approxResult.second) || + comparator.isEqual(approxResult.first, approxResult.second), + "Under-approximation " << approxResult.first + << " is greater than over-approximation " + << approxResult.second); //STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")"); totalTimer.stop(); printTimings(); totalTimer.start(); - STORM_LOG_THROW(!storm::utility::isInfinity(approxResult.first) && !storm::utility::isInfinity(approxResult.second), storm::exceptions::NotSupportedException, "Approximation does not work if result might be infinity."); - } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError, probabilityFormula)); + STORM_LOG_THROW(!storm::utility::isInfinity(approxResult.first) && + !storm::utility::isInfinity(approxResult.second), + storm::exceptions::NotSupportedException, + "Approximation does not work if result might be infinity."); + } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError, + probabilityFormula)); //STORM_LOG_INFO("Finished approximation after " << iteration << " iteration" << (iteration > 1 ? "s." : ".")); dft_results results; @@ -341,9 +401,15 @@ namespace storm { // Build a single Markov Automaton auto ioSettings = storm::settings::getModule(); STORM_LOG_DEBUG("Building Model..."); - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents, allowDCForRelevantEvents); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents, + allowDCForRelevantEvents); builder.buildModel(0, 0.0); std::shared_ptr> model = builder.getModel(); + if (eliminateChains && model->isOfType(storm::models::ModelType::MarkovAutomaton)) { + auto ma = std::static_pointer_cast>(model); + model = storm::transformer::NonMarkovianChainTransformer::eliminateNonmarkovianStates(ma, + !ignoreLabeling); + } explorationTimer.stop(); // Print model information @@ -376,12 +442,17 @@ namespace storm { } template - std::vector DFTModelChecker::checkModel(std::shared_ptr>& model, property_vector const& properties) { + std::vector + DFTModelChecker::checkModel(std::shared_ptr> &model, + property_vector const &properties) { // Bisimulation - if (model->isOfType(storm::models::ModelType::Ctmc) && storm::settings::getModule().isBisimulationSet()) { + if (model->isOfType(storm::models::ModelType::Ctmc) && + storm::settings::getModule().isBisimulationSet()) { bisimulationTimer.start(); STORM_LOG_DEBUG("Bisimulation..."); - model = storm::api::performDeterministicSparseBisimulationMinimization>(model->template as>(), properties, storm::storage::BisimulationType::Weak)->template as>(); + model = storm::api::performDeterministicSparseBisimulationMinimization>( + model->template as>(), properties, + storm::storage::BisimulationType::Weak)->template as>(); STORM_LOG_DEBUG("No. states (Bisimulation): " << model->getNumberOfStates()); STORM_LOG_DEBUG("No. transitions (Bisimulation): " << model->getNumberOfTransitions()); bisimulationTimer.stop(); @@ -398,7 +469,9 @@ namespace storm { singleModelCheckingTimer.reset(); singleModelCheckingTimer.start(); //STORM_PRINT_AND_LOG("Model checking property " << *property << " ..." << std::endl); - std::unique_ptr result(storm::api::verifyWithSparseEngine(model, storm::api::createTask(property, true))); + std::unique_ptr result( + storm::api::verifyWithSparseEngine(model, storm::api::createTask(property, + true))); STORM_LOG_ASSERT(result, "Result does not exist."); result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); ValueType resultValue = result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; @@ -413,13 +486,15 @@ namespace storm { } template - bool DFTModelChecker::isApproximationSufficient(ValueType , ValueType , double , bool ) { + bool DFTModelChecker::isApproximationSufficient(ValueType, ValueType, double, bool) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Approximation works only for double."); } template<> - bool DFTModelChecker::isApproximationSufficient(double lowerBound, double upperBound, double approximationError, bool relative) { - STORM_LOG_THROW(!std::isnan(lowerBound) && !std::isnan(upperBound), storm::exceptions::NotSupportedException, "Approximation does not work if result is NaN."); + bool DFTModelChecker::isApproximationSufficient(double lowerBound, double upperBound, + double approximationError, bool relative) { + STORM_LOG_THROW(!std::isnan(lowerBound) && !std::isnan(upperBound), + storm::exceptions::NotSupportedException, "Approximation does not work if result is NaN."); if (relative) { return upperBound - lowerBound <= approximationError; } else { @@ -428,17 +503,17 @@ namespace storm { } template - void DFTModelChecker::printTimings(std::ostream& os) { + void DFTModelChecker::printTimings(std::ostream &os) { os << "Times:" << std::endl; os << "Exploration:\t" << explorationTimer << std::endl; os << "Building:\t" << buildingTimer << std::endl; - os << "Bisimulation:\t" << bisimulationTimer<< std::endl; + os << "Bisimulation:\t" << bisimulationTimer << std::endl; os << "Modelchecking:\t" << modelCheckingTimer << std::endl; os << "Total:\t\t" << totalTimer << std::endl; } template - void DFTModelChecker::printResults(dft_results const& results, std::ostream& os) { + void DFTModelChecker::printResults(dft_results const &results, std::ostream &os) { bool first = true; os << "Result: ["; for (auto result : results) { @@ -453,10 +528,14 @@ namespace storm { } - template class DFTModelChecker; + template + class DFTModelChecker; #ifdef STORM_HAVE_CARL - template class DFTModelChecker; + + template + class DFTModelChecker; + #endif } } diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h index 4b4cd4d3d..9b898725a 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -55,11 +55,14 @@ namespace storm { * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events. * @param approximationError Error allowed for approximation. Value 0 indicates no approximation. * @param approximationHeuristic Heuristic used for state space exploration. + * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA + * @param ignoreLabeling If true, the labeling of states is ignored during state elimination * @return Model checking results for the given properties.. */ dft_results check(storm::storage::DFT const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true, std::set const& relevantEvents = {}, bool allowDCForRelevantEvents = true, double approximationError = 0.0, - storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH); + storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, + bool eliminateChains = false, bool ignoreLabeling = false); /*! * Print timings of all operations to stream. @@ -98,11 +101,14 @@ namespace storm { * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events. * @param approximationError Error allowed for approximation. Value 0 indicates no approximation. * @param approximationHeuristic Heuristic used for approximation. + * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA + * @param ignoreLabeling If true, the labeling of states is ignored during state elimination * @return Model checking results (or in case of approximation two results for lower and upper bound) */ dft_results checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set const& relevantEvents, bool allowDCForRelevantEvents = true, double approximationError = 0.0, - storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH); + storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, + bool eliminateChains = false, bool ignoreLabeling = false); /*! * Internal helper for building a CTMC from a DFT via parallel composition. @@ -129,12 +135,15 @@ namespace storm { * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events. * @param approximationError Error allowed for approximation. Value 0 indicates no approximation. * @param approximationHeuristic Heuristic used for approximation. + * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA + * @param ignoreLabeling If true, the labeling of states is ignored during state elimination * * @return Model checking result */ dft_results checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, std::set const& relevantEvents = {}, bool allowDCForRelevantEvents = true, double approximationError = 0.0, - storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH); + storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, + bool eliminateChains = false, bool ignoreLabeling = false); /*! * Check the given markov model for the given properties. diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp index 78e963d05..9cc092718 100644 --- a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp +++ b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp @@ -344,6 +344,31 @@ namespace storm { uint64_t value; }; + class IsNotConstantValue : public SmtConstraint { + public: + IsNotConstantValue(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) { + } + + virtual ~IsNotConstantValue() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + assert(varIndex < varNames.size()); + sstr << "(distinct " << varNames.at(varIndex) << " " << value << ")"; + return sstr.str(); + } + + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + return manager->getVariableExpression(varNames.at(varIndex)) != manager->integer(value); + } + + private: + uint64_t varIndex; + uint64_t value; + }; + class IsLessConstant : public SmtConstraint { public: @@ -469,6 +494,29 @@ namespace storm { uint64_t var2Index; }; + class IsUnequal : public SmtConstraint { + public: + IsUnequal(uint64_t varIndex1, uint64_t varIndex2) : var1Index(varIndex1), var2Index(varIndex2) { + } + + virtual ~IsUnequal() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + return "(distinct " + varNames.at(var1Index) + " " + varNames.at(var2Index) + ")"; + } + + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + return manager->getVariableExpression(varNames.at(var1Index)) != + manager->getVariableExpression(varNames.at(var2Index)); + } + + private: + uint64_t var1Index; + uint64_t var2Index; + }; + class IsLess : public SmtConstraint { public: @@ -493,6 +541,52 @@ namespace storm { uint64_t var2Index; }; + class IsLessEqual : public SmtConstraint { + public: + IsLessEqual(uint64_t varIndex1, uint64_t varIndex2) : var1Index(varIndex1), var2Index(varIndex2) { + } + + virtual ~IsLessEqual() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + return "(<= " + varNames.at(var1Index) + " " + varNames.at(var2Index) + ")"; + } + + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + return manager->getVariableExpression(varNames.at(var1Index)) <= + manager->getVariableExpression(varNames.at(var2Index)); + } + + private: + uint64_t var1Index; + uint64_t var2Index; + }; + + class IsGreaterEqual : public SmtConstraint { + public: + IsGreaterEqual(uint64_t varIndex1, uint64_t varIndex2) : var1Index(varIndex1), var2Index(varIndex2) { + } + + virtual ~IsGreaterEqual() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + return "(>= " + varNames.at(var1Index) + " " + varNames.at(var2Index) + ")"; + } + + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + return manager->getVariableExpression(varNames.at(var1Index)) >= + manager->getVariableExpression(varNames.at(var2Index)); + } + + private: + uint64_t var1Index; + uint64_t var2Index; + }; + class PairwiseDifferent : public SmtConstraint { public: diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp index 865ed40bf..e463bed37 100644 --- a/src/storm-dft/parser/DFTGalileoParser.cpp +++ b/src/storm-dft/parser/DFTGalileoParser.cpp @@ -32,8 +32,9 @@ namespace storm { } template - storm::storage::DFT DFTGalileoParser::parseDFT(const std::string& filename, bool defaultInclusive, bool binaryDependencies) { - storm::builder::DFTBuilder builder(defaultInclusive, binaryDependencies); + storm::storage::DFT + DFTGalileoParser::parseDFT(const std::string &filename, bool defaultInclusive) { + storm::builder::DFTBuilder builder(defaultInclusive); ValueParser valueParser; // Regular expression to detect comments // taken from: https://stackoverflow.com/questions/9449887/removing-c-c-style-comments-using-boostregex @@ -301,6 +302,24 @@ namespace storm { case Constant: if (storm::utility::isZero(firstValDistribution) || storm::utility::isOne(firstValDistribution)) { return builder.addBasicElementProbability(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs + } else { + // Model constant BEs with probability 0 < p < 1 + bool success = true; + if (!builder.nameInUse("constantBeTrigger")) { + // Use a unique constantly failed element that triggers failsafe elements probabilistically + success = success && builder.addBasicElementProbability("constantBeTrigger", + storm::utility::one(), + storm::utility::one(), + false); + } + std::vector childNames; + childNames.push_back("constantBeTrigger"); + success = success && + builder.addBasicElementProbability(parseName(name), storm::utility::zero(), + storm::utility::one(), false); + childNames.push_back(parseName(name)); + return success && + builder.addDepElement(parseName(name) + "_pdep", childNames, firstValDistribution); } STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Constant distribution is not supported for basic element '" << name << "' in line " << lineNo << "."); break; diff --git a/src/storm-dft/parser/DFTGalileoParser.h b/src/storm-dft/parser/DFTGalileoParser.h index 664533cce..2a6f473ec 100644 --- a/src/storm-dft/parser/DFTGalileoParser.h +++ b/src/storm-dft/parser/DFTGalileoParser.h @@ -26,11 +26,10 @@ namespace storm { * * @param filename File. * @param defaultInclusive Flag indicating if priority gates are inclusive by default. - * @param binaryDependencies Flag indicating if dependencies should be converted to binary dependencies. * * @return DFT. */ - static storm::storage::DFT parseDFT(std::string const& filename, bool defaultInclusive = true, bool binaryDependencies = true); + static storm::storage::DFT parseDFT(std::string const &filename, bool defaultInclusive = true); private: /*! diff --git a/src/storm-dft/settings/DftSettings.cpp b/src/storm-dft/settings/DftSettings.cpp index 43f0b0f51..4ff3e2aaf 100644 --- a/src/storm-dft/settings/DftSettings.cpp +++ b/src/storm-dft/settings/DftSettings.cpp @@ -23,6 +23,7 @@ #include "storm-conv/settings/modules/JaniExportSettings.h" #include "storm-gspn/settings/modules/GSPNSettings.h" #include "storm-gspn/settings/modules/GSPNExportSettings.h" +#include "storm/settings/modules/TransformationSettings.h" namespace storm { @@ -37,6 +38,7 @@ namespace storm { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); + storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.cpp b/src/storm-dft/settings/modules/FaultTreeSettings.cpp index b45c37498..3fa4d6529 100644 --- a/src/storm-dft/settings/modules/FaultTreeSettings.cpp +++ b/src/storm-dft/settings/modules/FaultTreeSettings.cpp @@ -26,6 +26,7 @@ namespace storm { const std::string FaultTreeSettings::approximationHeuristicOptionName = "approximationheuristic"; const std::string FaultTreeSettings::maxDepthOptionName = "maxdepth"; const std::string FaultTreeSettings::firstDependencyOptionName = "firstdep"; + const std::string FaultTreeSettings::uniqueFailedBEOptionName = "uniquefailedbe"; #ifdef STORM_HAVE_Z3 const std::string FaultTreeSettings::solveWithSmtOptionName = "smt"; #endif @@ -53,6 +54,8 @@ namespace storm { {"depth", "probability", "bounddifference"})).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, maxDepthOptionName, false, "Maximal depth for state space exploration.").addArgument( storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("depth", "The maximal depth.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, uniqueFailedBEOptionName, false, + "Use a unique constantly failed BE.").build()); #ifdef STORM_HAVE_Z3 this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build()); #endif @@ -115,6 +118,10 @@ namespace storm { return this->getOption(firstDependencyOptionName).getHasOptionBeenSet(); } + bool FaultTreeSettings::isUniqueFailedBE() const { + return this->getOption(uniqueFailedBEOptionName).getHasOptionBeenSet(); + } + #ifdef STORM_HAVE_Z3 bool FaultTreeSettings::solveWithSMT() const { diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.h b/src/storm-dft/settings/modules/FaultTreeSettings.h index 5ed230bfb..6c5298f7b 100644 --- a/src/storm-dft/settings/modules/FaultTreeSettings.h +++ b/src/storm-dft/settings/modules/FaultTreeSettings.h @@ -103,6 +103,13 @@ namespace storm { */ bool isTakeFirstDependency() const; + /*! + * Retrieves whether the DFT should be transformed to contain at most one constantly failed BE. + * + * @return True iff the option was set. + */ + bool isUniqueFailedBE() const; + #ifdef STORM_HAVE_Z3 /*! @@ -134,6 +141,7 @@ namespace storm { static const std::string approximationHeuristicOptionName; static const std::string maxDepthOptionName; static const std::string firstDependencyOptionName; + static const std::string uniqueFailedBEOptionName; #ifdef STORM_HAVE_Z3 static const std::string solveWithSmtOptionName; #endif diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 9534bf68b..890eba04a 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -16,11 +16,17 @@ namespace storm { namespace storage { template - DFT::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mNrRepresentatives(0), - mTopLevelIndex(tle->id()), mMaxSpareChildCount(0) { + DFT::DFT(DFTElementVector const &elements, DFTElementPointer const &tle) : + mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mNrRepresentatives(0), mTopLevelIndex(tle->id()), mMaxSpareChildCount(0) { // Check that ids correspond to indices in the element vector STORM_LOG_ASSERT(elementIndicesCorrect(), "Ids incorrect."); + // Initialize dynamic behavior vector with TRUE to preserve correct behavior + // We don't directly call setDynamicBehaviorInfo to not slow down DFT generation if possible + mDynamicBehavior = std::vector(mElements.size()); + std::fill(mDynamicBehavior.begin(), mDynamicBehavior.end(), true); + size_t nrRepresentatives = 0; + for (auto& elem : mElements) { if (isRepresentative(elem->id())) { ++mNrRepresentatives; @@ -47,6 +53,7 @@ namespace storm { } } else if (elem->isDependency()) { mDependencies.push_back(elem->id()); + mDependencyInConflict.insert(std::make_pair(elem->id(), true)); } } @@ -85,6 +92,151 @@ namespace storm { mStateVectorSize = DFTStateGenerationInfo::getStateVectorSize(nrElements(), mNrOfSpares, mNrRepresentatives, mMaxSpareChildCount); } + template + void DFT::setDynamicBehaviorInfo() { + std::vector dynamicBehaviorVector(mElements.size(), false); + + std::queue elementQueue; + + // deal with all dynamic elements + for (auto const &element : mElements) { + switch (element->type()) { + case storage::DFTElementType::PAND: + case storage::DFTElementType::POR: + case storage::DFTElementType::MUTEX: { + auto gate = std::static_pointer_cast>(element); + dynamicBehaviorVector[gate->id()] = true; + for (auto const &child : gate->children()) { + // only enqueue static children + if (!dynamicBehaviorVector.at(child->id())) { + elementQueue.push(child); + } + } + break; + } + // TODO different cases + case storage::DFTElementType::SPARE: { + auto spare = std::static_pointer_cast>(element); + + // Iterate over all children (representatives of spare modules) + for (auto const &child : spare->children()) { + // Case 1: Shared Module + // If child only has one parent, it is this SPARE -> nothing to check + if (child->nrParents() > 1) { + // TODO make more efficient by directly setting ALL spares which share a module to be dynamic + for (auto const &parent : child->parents()) { + if (parent->isSpareGate() and parent->id() != spare->id()) { + dynamicBehaviorVector[spare->id()] = true; + break; // inner loop + } + } + } + // Case 2: Triggering outside events + // If the SPARE was already detected to have dynamic behavior, do not proceed + if (!dynamicBehaviorVector[spare->id()]) { + for (auto const &memberID : module(child->id())) { + // Iterate over all members of the module child represents + auto member = getElement(memberID); + for (auto const dep : member->outgoingDependencies()) { + // If the member has outgoing dependencies, check if those trigger something outside the module + for (auto const depEvent : dep->dependentEvents()) { + // If a dependent event is not found in the module, SPARE is dynamic + if (std::find(module(child->id()).begin(), module(child->id()).end(), + depEvent->id()) == module(child->id()).end()) { + dynamicBehaviorVector[spare->id()] = true; + break; //depEvent-loop + } + } + if (dynamicBehaviorVector[spare->id()]) { break; } //dependency-loop + } + if (dynamicBehaviorVector[spare->id()]) { break; } //module-loop + } + + } + if (dynamicBehaviorVector[spare->id()]) { break; } //child-loop + } + // if during the computation, dynamic behavior was detected, add children to queue + if (dynamicBehaviorVector[spare->id()]) { + for (auto const &child : spare->children()) { + // only enqueue static children + if (!dynamicBehaviorVector.at(child->id())) { + elementQueue.push(child); + } + } + } + break; + } + case storage::DFTElementType::SEQ: { + auto seq = std::static_pointer_cast>(element); + // A SEQ only has dynamic behavior if not all children are BEs + if (!seq->allChildrenBEs()) { + dynamicBehaviorVector[seq->id()] = true; + for (auto const &child : seq->children()) { + // only enqueue static children + if (!dynamicBehaviorVector.at(child->id())) { + elementQueue.push(child); + } + } + } + break; + } + default: { + break; + } + + } + } + // propagate dynamic behavior + while (!elementQueue.empty()) { + DFTElementPointer currentElement = elementQueue.front(); + elementQueue.pop(); + switch (currentElement->type()) { + // Static Gates + case storage::DFTElementType::AND: + case storage::DFTElementType::OR: + case storage::DFTElementType::VOT: { + // check all parents and if one has dynamic behavior, propagate it + dynamicBehaviorVector[currentElement->id()] = true; + auto gate = std::static_pointer_cast>(currentElement); + for (auto const &child : gate->children()) { + // only enqueue static children + if (!dynamicBehaviorVector.at(child->id())) { + elementQueue.push(child); + } + } + 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; + // add all ingoing dependencies to queue + for (auto const &dep : be->ingoingDependencies()) { + if (!dynamicBehaviorVector.at(dep->id())) { + elementQueue.push(dep); + } + } + break; + } + case storage::DFTElementType::PDEP: { + auto dep = std::static_pointer_cast>(currentElement); + dynamicBehaviorVector[dep->id()] = true; + // add all ingoing dependencies to queue + auto trigger = dep->triggerEvent(); + if (!dynamicBehaviorVector.at(trigger->id())) { + elementQueue.push(trigger); + } + break; + } + default: + break; + } + } + mDynamicBehavior = dynamicBehaviorVector; + } + template DFTStateGenerationInfo DFT::buildStateGenerationInfo(storm::storage::DFTIndependentSymmetries const& symmetries) const { DFTStateGenerationInfo generationInfo(nrElements(), mNrOfSpares, mNrRepresentatives, mMaxSpareChildCount); diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index f3eaecc63..6a00be126 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -69,9 +69,11 @@ namespace storm { std::vector> mSymmetries; std::map mLayoutInfo; mutable std::vector mRelevantEvents; + std::vector mDynamicBehavior; + std::map mDependencyInConflict; public: - DFT(DFTElementVector const& elements, DFTElementPointer const& tle); + DFT(DFTElementVector const &elements, DFTElementPointer const &tle); DFTStateGenerationInfo buildStateGenerationInfo(storm::storage::DFTIndependentSymmetries const& symmetries) const; @@ -82,6 +84,8 @@ namespace storm { DFT optimize() const; void copyElements(std::vector elements, storm::builder::DFTBuilder builder) const; + + void setDynamicBehaviorInfo(); size_t stateBitVectorSize() const { // Ensure multiple of 64 @@ -130,11 +134,26 @@ namespace storm { return mSpareModules.find(representativeId)->second; } } + + bool isDependencyInConflict(size_t id) const { + STORM_LOG_ASSERT(isDependency(id), "Not a dependency."); + return mDependencyInConflict.at(id); + } + + + void setDependencyNotInConflict(size_t id) { + STORM_LOG_ASSERT(isDependency(id), "Not a dependency."); + mDependencyInConflict.at(id) = false; + } std::vector const& getDependencies() const { return mDependencies; } + std::vector const &getDynamicBehavior() const { + return mDynamicBehavior; + } + std::vector nonColdBEs() const { std::vector result; for (DFTElementPointer elem : mElements) { diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp index cd174c553..082b4e8a6 100644 --- a/src/storm-dft/storage/dft/DFTState.cpp +++ b/src/storm-dft/storage/dft/DFTState.cpp @@ -82,7 +82,7 @@ namespace storm { STORM_LOG_ASSERT(dependencyId == dependency->id(), "Ids do not match."); assert(dependency->dependentEvents().size() == 1); if (hasFailed(dependency->triggerEvent()->id()) && getElementState(dependency->dependentEvents()[0]->id()) == DFTElementState::Operational) { - failableElements.addDependency(dependencyId); + failableElements.addDependency(dependency->id(), mDft.isDependencyInConflict(dependency->id())); STORM_LOG_TRACE("New dependency failure: " << *dependency); } } @@ -239,7 +239,7 @@ namespace storm { // Check if restriction prevents failure of dependent event if (!isEventDisabledViaRestriction(dependency->dependentEvents()[0]->id())) { // Add dependency as possible failure - failableElements.addDependency(dependency->id()); + failableElements.addDependency(dependency->id(), mDft.isDependencyInConflict(dependency->id())); STORM_LOG_TRACE("New dependency failure: " << *dependency); addedFailableDependency = true; } diff --git a/src/storm-dft/storage/dft/DFTState.h b/src/storm-dft/storage/dft/DFTState.h index f0429b99d..9eb425d7e 100644 --- a/src/storm-dft/storage/dft/DFTState.h +++ b/src/storm-dft/storage/dft/DFTState.h @@ -33,9 +33,18 @@ namespace storm { currentlyFailableBE.set(id); } - void addDependency(size_t id) { - if (std::find(mFailableDependencies.begin(), mFailableDependencies.end(), id) == mFailableDependencies.end()) { - mFailableDependencies.push_back(id); + void addDependency(size_t id, bool isConflicting) { + if (isConflicting) { + if (std::find(mFailableConflictingDependencies.begin(), mFailableConflictingDependencies.end(), + id) == mFailableConflictingDependencies.end()) { + mFailableConflictingDependencies.push_back(id); + } + } else { + if (std::find(mFailableNonconflictingDependencies.begin(), + mFailableNonconflictingDependencies.end(), id) == + mFailableNonconflictingDependencies.end()) { + mFailableNonconflictingDependencies.push_back(id); + } } } @@ -44,21 +53,36 @@ namespace storm { } void removeDependency(size_t id) { - auto it = std::find(mFailableDependencies.begin(), mFailableDependencies.end(), id); - if (it != mFailableDependencies.end()) { - mFailableDependencies.erase(it); + auto it1 = std::find(mFailableConflictingDependencies.begin(), + mFailableConflictingDependencies.end(), id); + if (it1 != mFailableConflictingDependencies.end()) { + mFailableConflictingDependencies.erase(it1); + return; + } + auto it2 = std::find(mFailableNonconflictingDependencies.begin(), + mFailableNonconflictingDependencies.end(), id); + if (it2 != mFailableNonconflictingDependencies.end()) { + mFailableNonconflictingDependencies.erase(it2); + return; } } void clear() { currentlyFailableBE.clear(); - mFailableDependencies.clear(); + mFailableConflictingDependencies.clear(); + mFailableNonconflictingDependencies.clear(); } void init(bool dependency) const { this->dependency = dependency; if (this->dependency) { - itDep = mFailableDependencies.begin(); + if (!mFailableNonconflictingDependencies.empty()) { + itDep = mFailableNonconflictingDependencies.begin(); + conflicting = false; + } else { + itDep = mFailableConflictingDependencies.begin(); + conflicting = true; + } } else { it = currentlyFailableBE.begin(); } @@ -77,7 +101,12 @@ namespace storm { bool isEnd() const { if (dependency) { - return itDep == mFailableDependencies.end(); + if (!conflicting) { + // If we are handling the non-conflicting FDEPs, end after the first element + return itDep != mFailableNonconflictingDependencies.begin(); + } else { + return itDep == mFailableConflictingDependencies.end(); + } } else { return it == currentlyFailableBE.end(); } @@ -96,7 +125,7 @@ namespace storm { }; bool hasDependencies() const { - return !mFailableDependencies.empty(); + return !mFailableConflictingDependencies.empty() || !mFailableNonconflictingDependencies.empty(); } bool hasBEs() const { @@ -104,9 +133,12 @@ namespace storm { } mutable bool dependency; + mutable bool conflicting; storm::storage::BitVector currentlyFailableBE; - std::vector mFailableDependencies; + std::vector mFailableConflictingDependencies; + std::vector mFailableNonconflictingDependencies; + std::set remainingRelevantEvents; mutable storm::storage::BitVector::const_iterator it; mutable std::vector::const_iterator itDep; diff --git a/src/storm-dft/transformations/DftTransformator.cpp b/src/storm-dft/transformations/DftTransformator.cpp new file mode 100644 index 000000000..473f4249b --- /dev/null +++ b/src/storm-dft/transformations/DftTransformator.cpp @@ -0,0 +1,253 @@ +#include "DftTransformator.h" +#include "storm/exceptions/NotImplementedException.h" + +namespace storm { + namespace transformations { + namespace dft { + template + DftTransformator::DftTransformator() { + } + + template + std::shared_ptr> + DftTransformator::transformUniqueFailedBe(storm::storage::DFT const &dft) { + STORM_LOG_DEBUG("Start transformation UniqueFailedBe"); + storm::builder::DFTBuilder builder = storm::builder::DFTBuilder(true); + // NOTE: if probabilities for constant BEs are introduced, change this to vector of tuples (name, prob) + std::vector failedBEs; + + 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()); + } + // 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: + builder.addAndElement(element->name(), getChildrenVector(element)); + break; + case storm::storage::DFTElementType::OR: + builder.addOrElement(element->name(), getChildrenVector(element)); + break; + case storm::storage::DFTElementType::VOT: { + auto vot = std::static_pointer_cast const>(element); + builder.addVotElement(vot->name(), vot->threshold(), getChildrenVector(vot)); + break; + } + case storm::storage::DFTElementType::PAND: { + auto pand = std::static_pointer_cast const>(element); + builder.addPandElement(pand->name(), getChildrenVector(pand), pand->isInclusive()); + break; + } + case storm::storage::DFTElementType::POR: { + auto por = std::static_pointer_cast const>(element); + builder.addPandElement(por->name(), getChildrenVector(por), por->isInclusive()); + break; + } + case storm::storage::DFTElementType::SPARE: + builder.addSpareElement(element->name(), getChildrenVector(element)); + break; + case storm::storage::DFTElementType::PDEP: { + auto dep = std::static_pointer_cast const>( + element); + builder.addDepElement(dep->name(), getChildrenVector(dep), dep->probability()); + break; + } + case storm::storage::DFTElementType::SEQ: + builder.addSequenceEnforcer(element->name(), getChildrenVector(element)); + break; + case storm::storage::DFTElementType::MUTEX: + builder.addMutex(element->name(), getChildrenVector(element)); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, + "DFT type '" << element->type() << "' not known."); + break; + } + + } + // At this point the DFT is an exact copy of the original, except for all constant failure probabilities being 0 + + // Introduce new constantly failed BE and FDEPs to trigger all failures + if (!failedBEs.empty()) { + STORM_LOG_TRACE("Add Unique_Constant_Failure [BE (const failed)]"); + builder.addBasicElementConst("Unique_Constant_Failure", true); + failedBEs.insert(std::begin(failedBEs), "Unique_Constant_Failure"); + STORM_LOG_TRACE("Add Failure_Trigger [FDEP]"); + builder.addDepElement("Failure_Trigger", failedBEs, storm::utility::one()); + } + + builder.setTopLevel(dft.getTopLevelGate()->name()); + + STORM_LOG_DEBUG("Transformation UniqueFailedBe complete"); + return std::make_shared>(builder.build()); + } + + template + std::shared_ptr> + DftTransformator::transformBinaryFDEPs(storm::storage::DFT const &dft) { + STORM_LOG_DEBUG("Start transformation BinaryFDEPs"); + storm::builder::DFTBuilder builder = storm::builder::DFTBuilder(true); + + 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()); + break; + } + case storm::storage::DFTElementType::AND: + builder.addAndElement(element->name(), getChildrenVector(element)); + break; + case storm::storage::DFTElementType::OR: + builder.addOrElement(element->name(), getChildrenVector(element)); + break; + case storm::storage::DFTElementType::VOT: { + auto vot = std::static_pointer_cast const>(element); + builder.addVotElement(vot->name(), vot->threshold(), getChildrenVector(vot)); + break; + } + case storm::storage::DFTElementType::PAND: { + auto pand = std::static_pointer_cast const>(element); + builder.addPandElement(pand->name(), getChildrenVector(pand), pand->isInclusive()); + break; + } + case storm::storage::DFTElementType::POR: { + auto por = std::static_pointer_cast const>(element); + builder.addPandElement(por->name(), getChildrenVector(por), por->isInclusive()); + break; + } + case storm::storage::DFTElementType::SPARE: + builder.addSpareElement(element->name(), getChildrenVector(element)); + break; + case storm::storage::DFTElementType::PDEP: { + auto dep = std::static_pointer_cast const>( + element); + auto children = getChildrenVector(dep); + if (!storm::utility::isOne(dep->probability())) { + if (children.size() > 2) { + STORM_LOG_TRACE("Transform " + element->name() + " [PDEP]"); + // Introduce additional element for first capturing the probabilistic dependency + std::string nameAdditional = dep->name() + "_additional"; + STORM_LOG_TRACE("Add auxilliary BE " << nameAdditional); + builder.addBasicElementConst(nameAdditional, false); + STORM_LOG_TRACE("Add " << dep->name() << "_pdep [PDEP]"); + // First consider probabilistic dependency + builder.addDepElement(dep->name() + "_pdep", {children.front(), nameAdditional}, + dep->probability()); + // Then consider dependencies to the children if probabilistic dependency failed + children.erase(children.begin()); + size_t i = 1; + for (auto const &child : children) { + std::string nameDep = dep->name() + "_" + std::to_string(i); + if (builder.nameInUse(nameDep)) { + STORM_LOG_ERROR("Element with name '" << nameDep << "' already exists."); + } + STORM_LOG_TRACE("Add " << nameDep << " [FDEP]"); + builder.addDepElement(nameDep, {dep->name() + "_additional", child}, + storm::utility::one()); + ++i; + } + } else { + builder.addDepElement(dep->name(), children, dep->probability()); + } + } else { + // Add dependencies + for (size_t i = 1; i < children.size(); ++i) { + std::string nameDep; + if (children.size() == 2) { + nameDep = dep->name(); + } else { + nameDep = dep->name() + "_" + std::to_string(i); + STORM_LOG_TRACE("Transform " + element->name() + " [FDEP]"); + STORM_LOG_TRACE("Add " + nameDep + " [FDEP]"); + } + if (builder.nameInUse(nameDep)) { + STORM_LOG_ERROR("Element with name '" << nameDep << "' already exists."); + } + STORM_LOG_ASSERT(storm::utility::isOne(dep->probability()) || children.size() == 2, + "PDEP with multiple children supported."); + builder.addDepElement(nameDep, {children[0], children[i]}, + storm::utility::one()); + } + } + break; + } + case storm::storage::DFTElementType::SEQ: + builder.addSequenceEnforcer(element->name(), getChildrenVector(element)); + break; + case storm::storage::DFTElementType::MUTEX: + builder.addMutex(element->name(), getChildrenVector(element)); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, + "DFT type '" << element->type() << "' not known."); + break; + } + + } + + builder.setTopLevel(dft.getTopLevelGate()->name()); + + STORM_LOG_DEBUG("Transformation BinaryFDEPs complete"); + return std::make_shared>(builder.build()); + } + + template + std::vector DftTransformator::getChildrenVector( + std::shared_ptr const> element) { + std::vector res; + if (element->isDependency()) { + // Dependencies have to be handled separately + auto dependency = std::static_pointer_cast const>(element); + res.push_back(dependency->triggerEvent()->name()); + for (auto const &depEvent : dependency->dependentEvents()) { + res.push_back(depEvent->name()); + } + } else { + auto elementWithChildren = std::static_pointer_cast const>( + element); + for (auto const &child : elementWithChildren->children()) { + res.push_back(child->name()); + } + } + return res; + } + + // Explicitly instantiate the class. + template + class DftTransformator; + +#ifdef STORM_HAVE_CARL + + template + class DftTransformator; + +#endif + } + } +} diff --git a/src/storm-dft/transformations/DftTransformator.h b/src/storm-dft/transformations/DftTransformator.h new file mode 100644 index 000000000..c8e832f1b --- /dev/null +++ b/src/storm-dft/transformations/DftTransformator.h @@ -0,0 +1,35 @@ +#include "storm-dft/storage/dft/DFT.h" +#include "storm-dft/builder/DFTBuilder.h" +#include "storm/utility/macros.h" + +namespace storm { + namespace transformations { + namespace dft { + + /*! + * Transformator for DFT -> DFT. + */ + template + class DftTransformator { + + public: + /*! + * Constructor. + * + * @param dft DFT + */ + DftTransformator(); + + std::shared_ptr> + transformUniqueFailedBe(storm::storage::DFT const &dft); + + std::shared_ptr> + transformBinaryFDEPs(storm::storage::DFT const &dft); + + private: + std::vector + getChildrenVector(std::shared_ptr const> element); + }; + } + } +} diff --git a/src/storm-dft/utility/FDEPConflictFinder.cpp b/src/storm-dft/utility/FDEPConflictFinder.cpp new file mode 100644 index 000000000..53f63ae4b --- /dev/null +++ b/src/storm-dft/utility/FDEPConflictFinder.cpp @@ -0,0 +1,111 @@ +#include "FDEPConflictFinder.h" + +namespace storm { + namespace dft { + namespace utility { + + std::vector> + FDEPConflictFinder::getDependencyConflicts(storm::storage::DFT const &dft, + bool useSMT, + uint_fast64_t timeout) { + + std::shared_ptr smtChecker = nullptr; + if (useSMT) { + storm::modelchecker::DFTASFChecker checker(dft); + smtChecker = std::make_shared(checker); + smtChecker->toSolver(); + } + + std::vector> res; + uint64_t dep1Index; + uint64_t dep2Index; + for (size_t i = 0; i < dft.getDependencies().size(); ++i) { + dep1Index = dft.getDependencies().at(i); + for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) { + dep2Index = dft.getDependencies().at(j); + 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"); + 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()); + 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()); + res.emplace_back(std::pair(dep1Index, dep2Index)); + break; + default: + STORM_LOG_DEBUG( + "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()); + 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()); + break; + } + } + } + return res; + } + + std::vector> + FDEPConflictFinder::getDependencyConflicts(storm::storage::DFT const &dft, + bool useSMT, + uint_fast64_t timeout) { + if (useSMT) { + STORM_LOG_WARN("SMT encoding for rational functions is not supported"); + } + + std::vector> res; + uint64_t dep1Index; + uint64_t dep2Index; + for (size_t i = 0; i < dft.getDependencies().size(); ++i) { + dep1Index = dft.getDependencies().at(i); + 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()); + 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()); + break; + } + } + } + return res; + } + + class FDEPConflictFinder; + + } + } +} \ No newline at end of file diff --git a/src/storm-dft/utility/FDEPConflictFinder.h b/src/storm-dft/utility/FDEPConflictFinder.h new file mode 100644 index 000000000..831bfd248 --- /dev/null +++ b/src/storm-dft/utility/FDEPConflictFinder.h @@ -0,0 +1,29 @@ +#include +#include "storm-dft/storage/dft/DFT.h" +#include "storm-dft/modelchecker/dft/DFTASFChecker.h" + +namespace storm { + namespace dft { + namespace utility { + class FDEPConflictFinder { + public: + /** + * Get a vector of index pairs of FDEPs in the DFT which are conflicting. Two FDEPs are conflicting if + * their simultaneous triggering may cause unresolvable non-deterministic behavior. + * + * @param dft the DFT + * @param useSMT if set, an SMT solver is used to refine the conflict set + * @param timeout timeout for each query in seconds, defaults to 10 seconds + * @return a vector of pairs of indices. The indices in a pair refer to FDEPs which are conflicting + */ + static std::vector> + getDependencyConflicts(storm::storage::DFT const &dft, + bool useSMT = false, uint_fast64_t timeout = 10); + + static std::vector> + getDependencyConflicts(storm::storage::DFT const &dft, + bool useSMT = false, uint_fast64_t timeout = 10); + }; + } + } +} diff --git a/src/storm-dft/utility/FailureBoundFinder.cpp b/src/storm-dft/utility/FailureBoundFinder.cpp new file mode 100644 index 000000000..d09caae83 --- /dev/null +++ b/src/storm-dft/utility/FailureBoundFinder.cpp @@ -0,0 +1,239 @@ +#include "FailureBoundFinder.h" + +namespace storm { + namespace dft { + namespace utility { + uint64_t + FailureBoundFinder::correctLowerBound(std::shared_ptr smtchecker, + uint64_t bound, uint_fast64_t timeout) { + STORM_LOG_DEBUG("Lower bound correction - try to correct bound " << std::to_string(bound)); + uint64_t boundCandidate = bound; + uint64_t nrDepEvents = 0; + uint64_t nrNonMarkovian = 0; + auto dft = smtchecker->getDFT(); + + // 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) { + auto be = std::static_pointer_cast const>(element); + if (be->hasIngoingDependencies()) { + ++nrDepEvents; + } + } + } + + // Only need to check as long as bound candidate + nr of non-Markovians to check is smaller than number of dependent events + while (nrNonMarkovian <= nrDepEvents && boundCandidate >= 0) { + if (nrNonMarkovian == 0 and boundCandidate == 0) { + nrNonMarkovian = 1; + } + STORM_LOG_TRACE( + "Lower bound correction - check possible bound " << std::to_string(boundCandidate) + << " with " + << std::to_string(nrNonMarkovian) + << " non-Markovian states"); + // The uniqueness transformation for constantly failed BEs guarantees that a DFT never fails + // in step 0 without intermediate non-Markovians, thus forcibly set nrNonMarkovian + smtchecker->setSolverTimeout(timeout * 1000); + storm::solver::SmtSolver::CheckResult tmp_res = + smtchecker->checkFailsLeqWithEqNonMarkovianState(boundCandidate + nrNonMarkovian, + nrNonMarkovian); + smtchecker->unsetSolverTimeout(); + switch (tmp_res) { + case storm::solver::SmtSolver::CheckResult::Sat: + /* If SAT, there is a sequence where only boundCandidate-many BEs fail directly and rest is nonMarkovian. + * Bound candidate is vaild, therefore check the next one */ + STORM_LOG_TRACE("Lower bound correction - SAT"); + // Prevent integer underflow + if (boundCandidate == 0) { + STORM_LOG_DEBUG("Lower bound correction - corrected bound to 0"); + return 0; + } + --boundCandidate; + break; + case storm::solver::SmtSolver::CheckResult::Unknown: + // If any query returns unknown, we cannot be sure about the bound and fall back to the naive one + STORM_LOG_DEBUG("Lower bound correction - Solver returned 'Unknown', corrected to 1"); + return 1; + default: + // if query is UNSAT, increase number of non-Markovian states and try again + STORM_LOG_TRACE("Lower bound correction - UNSAT"); + ++nrNonMarkovian; + break; + } + } + // if for one candidate all queries are UNSAT, it is not valid. Return last valid candidate + STORM_LOG_DEBUG("Lower bound correction - corrected bound to " << std::to_string(boundCandidate + 1)); + return boundCandidate + 1; + } + + uint64_t + FailureBoundFinder::correctUpperBound(std::shared_ptr smtchecker, + uint64_t bound, uint_fast64_t timeout) { + STORM_LOG_DEBUG("Upper bound correction - try to correct bound " << std::to_string(bound)); + uint64_t boundCandidate = bound; + uint64_t nrDepEvents = 0; + uint64_t nrNonMarkovian = 0; + uint64_t currentTimepoint = 0; + auto dft = smtchecker->getDFT(); + // 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) { + auto be = std::static_pointer_cast const>(element); + if (be->hasIngoingDependencies()) { + ++nrDepEvents; + } + } + } + while (boundCandidate >= 0) { + currentTimepoint = bound + 1; + while (currentTimepoint - boundCandidate > 0) { + --currentTimepoint; + nrNonMarkovian = currentTimepoint - boundCandidate; + STORM_LOG_TRACE( + "Upper bound correction - candidate " << std::to_string(boundCandidate) + << " check split " + << + std::to_string(currentTimepoint) << "|" + << std::to_string(nrNonMarkovian)); + smtchecker->setSolverTimeout(timeout * 1000); + storm::solver::SmtSolver::CheckResult tmp_res = + smtchecker->checkFailsAtTimepointWithEqNonMarkovianState(currentTimepoint, + nrNonMarkovian); + smtchecker->unsetSolverTimeout(); + switch (tmp_res) { + case storm::solver::SmtSolver::CheckResult::Sat: + STORM_LOG_TRACE("Upper bound correction - SAT"); + STORM_LOG_DEBUG("Upper bound correction - corrected to bound " << boundCandidate << + " (TLE can fail at sequence point " + << std::to_string( + currentTimepoint) + << " with " + << std::to_string( + nrNonMarkovian) + << " non-Markovian states)"); + return boundCandidate; + case storm::solver::SmtSolver::CheckResult::Unknown: + // If any query returns unknown, we cannot be sure about the bound and fall back to the naive one + STORM_LOG_DEBUG( + "Upper bound correction - Solver returned 'Unknown', corrected to bound " + << bound); + return bound; + default: + // if query is UNSAT, increase number of non-Markovian states and try again + STORM_LOG_TRACE("Lower bound correction - UNSAT"); + break; + } + } + --boundCandidate; + } + + // if for one candidate all queries are UNSAT, it is not valid. Return last valid candidate + STORM_LOG_DEBUG("Upper bound correction - corrected bound to " << std::to_string(boundCandidate)); + return boundCandidate; + } + + uint64_t FailureBoundFinder::getLeastFailureBound(storm::storage::DFT const &dft, + bool useSMT, uint_fast64_t timeout) { + if (useSMT) { + STORM_LOG_TRACE("Compute lower bound for number of BE failures necessary for the DFT to fail"); + + storm::modelchecker::DFTASFChecker smtchecker(dft); + smtchecker.toSolver(); + + uint64_t bound = 0; + while (bound < dft.nrBasicElements() + 1) { + smtchecker.setSolverTimeout(timeout * 1000); + storm::solver::SmtSolver::CheckResult tmp_res = smtchecker.checkTleFailsWithLeq(bound); + smtchecker.unsetSolverTimeout(); + switch (tmp_res) { + case storm::solver::SmtSolver::CheckResult::Sat: + if (!dft.getDependencies().empty()) { + return correctLowerBound( + std::make_shared(smtchecker), bound, + timeout); + } else { + return bound; + } + case storm::solver::SmtSolver::CheckResult::Unknown: + STORM_LOG_DEBUG("Lower bound: Solver returned 'Unknown'"); + return bound; + default: + ++bound; + break; + } + + } + + return bound; + } else { + // naive bound + return 1; + } + } + + uint64_t FailureBoundFinder::getLeastFailureBound(storm::storage::DFT const &dft, + bool useSMT, uint_fast64_t timeout) { + if (useSMT) { + STORM_LOG_WARN("SMT encoding does not support rational functions"); + } + return 1; + } + + uint64_t FailureBoundFinder::getAlwaysFailedBound(storm::storage::DFT const &dft, bool useSMT, + uint_fast64_t timeout) { + STORM_LOG_TRACE("Compute bound for number of BE failures such that the DFT always fails"); + if (useSMT) { + + storm::modelchecker::DFTASFChecker smtchecker(dft); + smtchecker.toSolver(); + + if (smtchecker.checkTleNeverFailed() == storm::solver::SmtSolver::CheckResult::Sat) { + return dft.nrBasicElements() + 1; + } + uint64_t bound = dft.nrBasicElements(); + while (bound >= 0) { + smtchecker.setSolverTimeout(timeout * 1000); + storm::solver::SmtSolver::CheckResult tmp_res = smtchecker.checkTleFailsWithEq(bound); + smtchecker.unsetSolverTimeout(); + switch (tmp_res) { + case storm::solver::SmtSolver::CheckResult::Sat: + if (!dft.getDependencies().empty()) { + return correctUpperBound( + std::make_shared(smtchecker), bound, + timeout); + } else { + return bound; + } + case storm::solver::SmtSolver::CheckResult::Unknown: + STORM_LOG_DEBUG("Upper bound: Solver returned 'Unknown'"); + return bound; + default: + --bound; + break; + } + } + return bound; + } else { + // naive bound + return dft.nrBasicElements() + 1; + } + } + + uint64_t + FailureBoundFinder::getAlwaysFailedBound(storm::storage::DFT const &dft, bool useSMT, + uint_fast64_t timeout) { + if (useSMT) { + STORM_LOG_WARN("SMT encoding does not support rational functions"); + } + return dft.nrBasicElements() + 1; + } + + class FailureBoundFinder; + } + } +} \ No newline at end of file diff --git a/src/storm-dft/utility/FailureBoundFinder.h b/src/storm-dft/utility/FailureBoundFinder.h new file mode 100644 index 000000000..f4186da98 --- /dev/null +++ b/src/storm-dft/utility/FailureBoundFinder.h @@ -0,0 +1,73 @@ +#include +#include "storm-dft/storage/dft/DFT.h" +#include "storm-dft/modelchecker/dft/DFTASFChecker.h" + +namespace storm { + namespace dft { + namespace utility { + class FailureBoundFinder { + public: + /** + * Get the minimal number of BEs necessary for the TLE to fail (lower bound for number of failures to check) + * + * @param dft the DFT to check + * @param useSMT if set, an SMT solver is used to improve the bounds + * @param timeout timeout for each query in seconds, defaults to 10 seconds + * @return the minimal number + */ + static uint64_t getLeastFailureBound(storm::storage::DFT const &dft, + bool useSMT = false, + uint_fast64_t timeout = 10); + + static uint64_t getLeastFailureBound(storm::storage::DFT const &dft, + bool useSMT = false, + uint_fast64_t timeout = 10); + + /** + * Get the number of BE failures for which the TLE always fails (upper bound for number of failures to check). + * + * @param dft the DFT to check + * @param useSMT if set, an SMT solver is used to improve the bounds + * @param timeout timeout for each query in seconds, defaults to 10 seconds + * @return the number + */ + static uint64_t getAlwaysFailedBound(storm::storage::DFT const &dft, + bool useSMT = false, + uint_fast64_t timeout = 10); + + static uint64_t getAlwaysFailedBound(storm::storage::DFT const &dft, + bool useSMT = false, + uint_fast64_t timeout = 10); + + private: + /** + * Helper function for correction of least failure bound when dependencies are present. + * The main idea is to check if a later point of failure for the TLE than the pre-computed bound exists, but + * up until that point the number of non-Markovian states visited is so large, that less than the pre-computed bound BEs fail by themselves. + * The corrected bound is then (newTLEFailureTimepoint)-(nrNonMarkovianStatesVisited). This term is minimized. + * + * @param smtchecker the SMT checker to use + * @param bound known lower bound to be corrected + * @param timeout timeout timeout for each query in seconds + * @return the corrected bound + */ + static uint64_t + correctLowerBound(std::shared_ptr smtchecker, uint64_t bound, + uint_fast64_t timeout); + + /** + * Helper function for correction of bound for number of BEs such that the DFT always fails when dependencies are present + * + * @param smtchecker the SMT checker to use + * @param bound known bound to be corrected + * @param timeout timeout timeout for each query in seconds + * @return the corrected bound + */ + static uint64_t + correctUpperBound(std::shared_ptr smtchecker, uint64_t bound, + uint_fast64_t timeout); + }; + } + } +} + diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index fe5f50993..18b27627d 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -21,6 +21,7 @@ #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/BisimulationSettings.h" +#include "storm/settings/modules/TransformationSettings.h" #include "storm/exceptions/BaseException.h" #include "storm/exceptions/InvalidSettingsException.h" @@ -141,6 +142,7 @@ namespace storm { auto generalSettings = storm::settings::getModule(); auto bisimulationSettings = storm::settings::getModule(); auto parametricSettings = storm::settings::getModule(); + auto transformationSettings = storm::settings::getModule(); PreprocessResult result(model, false); @@ -153,6 +155,18 @@ namespace storm { result.model = storm::cli::preprocessSparseModelBisimulation(result.model->template as>(), input, bisimulationSettings); result.changed = true; } + + if (transformationSettings.isChainEliminationSet() && + model->isOfType(storm::models::ModelType::MarkovAutomaton)) { + auto eliminationResult = storm::api::eliminateNonMarkovianChains( + result.model->template as>(), + storm::api::extractFormulasFromProperties(input.properties), + transformationSettings.isIgnoreLabelingSet()); + result.model = eliminationResult.first; + // Set transformed properties as new properties in input + result.formulas = eliminationResult.second; + result.changed = true; + } if (parametricSettings.transformContinuousModel() && (model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::MarkovAutomaton))) { auto transformResult = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*model->template as>()), storm::api::extractFormulasFromProperties(input.properties)); diff --git a/src/storm/api/transformation.h b/src/storm/api/transformation.h index 0fb25b2f2..4dcaf7f61 100644 --- a/src/storm/api/transformation.h +++ b/src/storm/api/transformation.h @@ -2,6 +2,7 @@ #include "storm/transformer/ContinuousToDiscreteTimeModelTransformer.h" #include "storm/transformer/SymbolicToSparseTransformer.h" +#include "storm/transformer/NonMarkovianChainTransformer.h" #include "storm/utility/macros.h" #include "storm/utility/builder.h" @@ -10,7 +11,30 @@ namespace storm { namespace api { - + + /*! + * Eliminates chains of non-Markovian states from a given Markov Automaton + */ + template + std::pair>, std::vector>> + eliminateNonMarkovianChains(std::shared_ptr> const &ma, + std::vector> const &formulas, + bool ignoreLabeling) { + + auto newFormulas = storm::transformer::NonMarkovianChainTransformer::checkAndTransformFormulas( + formulas); + STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), + "The state elimination does not preserve all properties."); + STORM_LOG_WARN_COND(!ignoreLabeling, + "Labels are ignored for the state elimination. This may cause incorrect results."); + return std::make_pair( + storm::transformer::NonMarkovianChainTransformer::eliminateNonmarkovianStates(ma, + !ignoreLabeling), + newFormulas); + + } + + /*! * Transforms the given continuous model to a discrete time model. * If such a transformation does not preserve one of the given formulas, a warning is issued. diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 9d6869d84..85f6b5d21 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -1,3 +1,5 @@ +#include + #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/adapters/RationalFunctionAdapter.h" @@ -16,7 +18,7 @@ namespace storm { namespace models { namespace sparse { - + template MarkovAutomaton::MarkovAutomaton(storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, @@ -25,7 +27,7 @@ namespace storm { : MarkovAutomaton(storm::storage::sparse::ModelComponents(transitionMatrix, stateLabeling, rewardModels, true, markovianStates)) { // Intentionally left empty } - + template MarkovAutomaton::MarkovAutomaton(storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, @@ -34,23 +36,23 @@ namespace storm { : MarkovAutomaton(storm::storage::sparse::ModelComponents(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), true, std::move(markovianStates))) { // Intentionally left empty } - + template MarkovAutomaton::MarkovAutomaton(storm::storage::sparse::ModelComponents const& components) : NondeterministicModel(ModelType::MarkovAutomaton, components), markovianStates(components.markovianStates.get()) { - + if (components.exitRates) { exitRates = components.exitRates.get(); } - + if (components.rateTransitions) { this->turnRatesToProbabilities(); } closed = this->checkIsClosed(); } - + template MarkovAutomaton::MarkovAutomaton(storm::storage::sparse::ModelComponents&& components) : NondeterministicModel(ModelType::MarkovAutomaton, std::move(components)), markovianStates(std::move(components.markovianStates.get())) { - + if (components.exitRates) { exitRates = std::move(components.exitRates.get()); } @@ -60,52 +62,52 @@ namespace storm { } closed = this->checkIsClosed(); } - + template bool MarkovAutomaton::isClosed() const { return closed; } - + template bool MarkovAutomaton::isHybridState(storm::storage::sparse::state_type state) const { return isMarkovianState(state) && (this->getTransitionMatrix().getRowGroupSize(state) > 1); } - + template bool MarkovAutomaton::isMarkovianState(storm::storage::sparse::state_type state) const { return this->markovianStates.get(state); } - + template bool MarkovAutomaton::isProbabilisticState(storm::storage::sparse::state_type state) const { return !this->markovianStates.get(state); } - + template std::vector const& MarkovAutomaton::getExitRates() const { return this->exitRates; } - + template std::vector& MarkovAutomaton::getExitRates() { return this->exitRates; } - + template ValueType const& MarkovAutomaton::getExitRate(storm::storage::sparse::state_type state) const { return this->exitRates[state]; } - + template ValueType MarkovAutomaton::getMaximalExitRate() const { return storm::utility::vector::max_if(this->exitRates, this->markovianStates); } - + template storm::storage::BitVector const& MarkovAutomaton::getMarkovianStates() const { return this->markovianStates; } - + template void MarkovAutomaton::close() { if (!closed) { @@ -120,16 +122,16 @@ namespace storm { exitRates[state] = storm::utility::zero(); } } - + if (!keptChoices.full()) { *this = std::move(*storm::transformer::buildSubsystem(*this, storm::storage::BitVector(this->getNumberOfStates(), true), keptChoices, false).model->template as>()); } - + // Mark the automaton as closed. closed = true; } } - + template void MarkovAutomaton::turnRatesToProbabilities() { bool assertRates = (this->exitRates.size() == this->getNumberOfStates()); @@ -137,7 +139,7 @@ namespace storm { STORM_LOG_THROW(this->exitRates.empty(), storm::exceptions::InvalidArgumentException, "The specified exit rate vector has an unexpected size."); this->exitRates.reserve(this->getNumberOfStates()); } - + storm::utility::ConstantsComparator comparator; for (uint_fast64_t state = 0; state< this->getNumberOfStates(); ++state) { uint_fast64_t row = this->getTransitionMatrix().getRowGroupIndices()[state]; @@ -163,12 +165,12 @@ namespace storm { } } } - + template bool MarkovAutomaton::isConvertibleToCtmc() const { return isClosed() && markovianStates.full(); } - + template bool MarkovAutomaton::hasOnlyTrivialNondeterminism() const { // Check every state @@ -185,7 +187,7 @@ namespace storm { } return true; } - + template bool MarkovAutomaton::checkIsClosed() const { for (auto state : markovianStates) { @@ -195,7 +197,7 @@ namespace storm { } return true; } - + template std::shared_ptr> MarkovAutomaton::convertToCtmc() const { if (isClosed() && markovianStates.full()) { @@ -265,7 +267,7 @@ namespace storm { return std::make_shared>(std::move(rateMatrix), std::move(stateLabeling)); } - + template void MarkovAutomaton::printModelInformationToStream(std::ostream& out) const { this->printModelInformationHeaderToStream(out); @@ -274,13 +276,15 @@ namespace storm { out << "Max. Rate.: \t" << this->getMaximalExitRate() << std::endl; this->printModelInformationFooterToStream(out); } - - + + template class MarkovAutomaton; #ifdef STORM_HAVE_CARL + template class MarkovAutomaton; - + template class MarkovAutomaton>; + template class MarkovAutomaton; #endif } // namespace sparse diff --git a/src/storm/models/sparse/MarkovAutomaton.h b/src/storm/models/sparse/MarkovAutomaton.h index b5a7f347f..c7ca80f35 100644 --- a/src/storm/models/sparse/MarkovAutomaton.h +++ b/src/storm/models/sparse/MarkovAutomaton.h @@ -147,6 +147,7 @@ namespace storm { * @return The resulting CTMC. */ std::shared_ptr> convertToCtmc() const; + virtual void printModelInformationToStream(std::ostream& out) const override; diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index f3b9009b2..cc68677e3 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -37,6 +37,7 @@ #include "storm/settings/modules/JitBuilderSettings.h" #include "storm/settings/modules/MultiObjectiveSettings.h" #include "storm/settings/modules/MultiplierSettings.h" +#include "storm/settings/modules/TransformationSettings.h" #include "storm/utility/macros.h" #include "storm/utility/file.h" #include "storm/utility/string.h" @@ -670,6 +671,7 @@ namespace storm { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); + storm::settings::addModule(); } } diff --git a/src/storm/settings/modules/TransformationSettings.cpp b/src/storm/settings/modules/TransformationSettings.cpp new file mode 100644 index 000000000..75b1c3daf --- /dev/null +++ b/src/storm/settings/modules/TransformationSettings.cpp @@ -0,0 +1,49 @@ +#include "TransformationSettings.h" + +#include "storm/settings/Option.h" +#include "storm/settings/OptionBuilder.h" +#include "storm/exceptions/InvalidSettingsException.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string TransformationSettings::moduleName = "transformation"; + + const std::string TransformationSettings::chainEliminationOptionName = "eliminate-chains"; + const std::string TransformationSettings::ignoreLabelingOptionName = "ec-ignore-labeling"; + + + TransformationSettings::TransformationSettings() : ModuleSettings(moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, chainEliminationOptionName, false, + "If set, chains of non-Markovian states are eliminated if the resulting model is a Markov Automaton.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, ignoreLabelingOptionName, false, + "If set, the elimination of chains ignores the labels for all non-Markovian states. This may cause wrong results.").build()); + } + + bool TransformationSettings::isChainEliminationSet() const { + return this->getOption(chainEliminationOptionName).getHasOptionBeenSet(); + } + + bool TransformationSettings::isIgnoreLabelingSet() const { + return this->getOption(ignoreLabelingOptionName).getHasOptionBeenSet(); + } + + + bool TransformationSettings::check() const { + // Ensure that labeling preservation is only set if chain elimination is set + STORM_LOG_THROW(isChainEliminationSet() || !isIgnoreLabelingSet(), + storm::exceptions::InvalidSettingsException, + "Label preservation can only be chosen if chain elimination is applied."); + + return true; + } + + void TransformationSettings::finalize() { + //Intentionally left empty + } + + + } // namespace modules + } // namespace settings +} // namespace storm diff --git a/src/storm/settings/modules/TransformationSettings.h b/src/storm/settings/modules/TransformationSettings.h new file mode 100644 index 000000000..ba646c763 --- /dev/null +++ b/src/storm/settings/modules/TransformationSettings.h @@ -0,0 +1,56 @@ +#ifndef STORM_TRANSFORMATIONSETTINGS_H +#define STORM_TRANSFORMATIONSETTINGS_H + +#include "storm-config.h" +#include "storm/settings/modules/ModuleSettings.h" + +namespace storm { + namespace settings { + namespace modules { + + /*! + * This class represents the model transformer settings + */ + class TransformationSettings : public ModuleSettings { + public: + + /*! + * Creates a new set of transformer settings. + */ + TransformationSettings(); + + /*! + * Retrieves whether the option to eliminate chains of non-Markovian states was set. + * + * @return True if the option to eliminate chains of non-Markovian states was set. + */ + bool isChainEliminationSet() const; + + + /*! + * Retrieves whether the preserve-labeling option for jani was set. + * + * @return True if the preserve-labeling option was set. + */ + bool isIgnoreLabelingSet() const; + + + bool check() const override; + + void finalize() override; + + // The name of the module. + static const std::string moduleName; + + private: + // Define the string names of the options as constants. + static const std::string chainEliminationOptionName; + static const std::string ignoreLabelingOptionName; + + }; + + } // namespace modules + } // namespace settings +} // namespace storm + +#endif //STORM_TRANSFORMATIONSETTINGS_H diff --git a/src/storm/transformer/NonMarkovianChainTransformer.cpp b/src/storm/transformer/NonMarkovianChainTransformer.cpp new file mode 100644 index 000000000..be5e57858 --- /dev/null +++ b/src/storm/transformer/NonMarkovianChainTransformer.cpp @@ -0,0 +1,299 @@ +#include + +#include "NonMarkovianChainTransformer.h" + +#include "storm/logic/Formulas.h" +#include "storm/logic/FragmentSpecification.h" + +#include "storm/storage/sparse/ModelComponents.h" +#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/utility/constants.h" +#include "storm/utility/ConstantsComparator.h" +#include "storm/utility/vector.h" +#include "storm/utility/macros.h" +#include "storm/utility/graph.h" + +namespace storm { + namespace transformer { + + template + std::shared_ptr> + NonMarkovianChainTransformer::eliminateNonmarkovianStates( + std::shared_ptr> ma, + bool preserveLabels) { + // TODO reward models + + STORM_LOG_WARN_COND(preserveLabels, "Labels are not preserved! Results may be incorrect."); + STORM_LOG_WARN("Reward Models and Choice Labelings are ignored!"); + if (ma->isClosed() && ma->getMarkovianStates().full()) { + storm::storage::sparse::ModelComponents components( + ma->getTransitionMatrix(), ma->getStateLabeling(), ma->getRewardModels(), false); + components.exitRates = ma->getExitRates(); + if (ma->hasChoiceLabeling()) { + components.choiceLabeling = ma->getChoiceLabeling(); + } + if (ma->hasStateValuations()) { + components.stateValuations = ma->getStateValuations(); + } + if (ma->hasChoiceOrigins()) { + components.choiceOrigins = ma->getChoiceOrigins(); + } + return std::make_shared>( + std::move(components)); + } + + std::map eliminationMapping; + std::set statesToKeep; + std::queue changedStates; + std::queue queue; + + storm::storage::SparseMatrix backwards = ma->getBackwardTransitions(); + + // Determine the state remapping + for (uint_fast64_t base_state = 0; base_state < ma->getNumberOfStates(); ++base_state) { + STORM_LOG_ASSERT(!ma->isHybridState(base_state), "Base state is hybrid."); + if (ma->isMarkovianState(base_state)) { + queue.push(base_state); + + while (!queue.empty()) { + auto currState = queue.front(); + queue.pop(); + + auto currLabels = ma->getLabelsOfState(currState); + + // Get predecessors from matrix + typename storm::storage::SparseMatrix::rows entriesInRow = backwards.getRow( + currState); + for (auto entryIt = entriesInRow.begin(), entryIte = entriesInRow.end(); + entryIt != entryIte; ++entryIt) { + uint_fast64_t predecessor = entryIt->getColumn(); + if (!ma->isMarkovianState(predecessor) && !statesToKeep.count(predecessor)) { + if (!preserveLabels || currLabels == ma->getLabelsOfState(predecessor)) { + // If labels are not to be preserved or states are labeled the same + if (!eliminationMapping.count(predecessor)) { + eliminationMapping[predecessor] = base_state; + queue.push(predecessor); + } else if (eliminationMapping[predecessor] != base_state) { + eliminationMapping.erase(predecessor); + statesToKeep.insert(predecessor); + changedStates.push(predecessor); + } + } else { + // Labels are to be preserved and states have different labels + if (eliminationMapping.count(predecessor)) { + eliminationMapping.erase(predecessor); + } + statesToKeep.insert(predecessor); + changedStates.push(predecessor); + } + } + } + } + } + } + + // Correct the mapping with the states which have to be kept + while (!changedStates.empty()) { + uint_fast64_t base_state = changedStates.front(); + queue.push(base_state); + + while (!queue.empty()) { + auto currState = queue.front(); + queue.pop(); + + auto currLabels = ma->getLabelsOfState(currState); + + // Get predecessors from matrix + typename storm::storage::SparseMatrix::rows entriesInRow = backwards.getRow( + currState); + for (auto entryIt = entriesInRow.begin(), entryIte = entriesInRow.end(); + entryIt != entryIte; ++entryIt) { + uint_fast64_t predecessor = entryIt->getColumn(); + if (!ma->isMarkovianState(predecessor) && !statesToKeep.count(predecessor)) { + if (!preserveLabels || currLabels == ma->getLabelsOfState(predecessor)) { + // If labels are not to be preserved or states are labeled the same + if (!eliminationMapping.count(predecessor)) { + eliminationMapping[predecessor] = base_state; + queue.push(predecessor); + } else if (eliminationMapping[predecessor] != base_state) { + eliminationMapping.erase(predecessor); + statesToKeep.insert(predecessor); + changedStates.push(predecessor); + } + } else { + // Labels are to be preserved and states have different labels + if (eliminationMapping.count(predecessor)) { + eliminationMapping.erase(predecessor); + } + statesToKeep.insert(predecessor); + changedStates.push(predecessor); + } + } + } + } + + changedStates.pop(); + } + + // At this point, we hopefully have a valid mapping which eliminates a lot of states + + STORM_LOG_TRACE("Elimination Mapping" << std::endl); + for (auto entry : eliminationMapping) { + STORM_LOG_TRACE(std::to_string(entry.first) << " -> " << std::to_string(entry.second) << std::endl); + } + STORM_LOG_INFO("Eliminating " << eliminationMapping.size() << " states" << std::endl); + + // TODO explore if one can construct elimination mapping and state remapping in one step + + // Construct a mapping of old state space to new one + std::vector stateRemapping(ma->getNumberOfStates(), -1); + uint_fast64_t currentNewState = 0; + for (uint_fast64_t state = 0; state < ma->getNumberOfStates(); ++state) { + if (eliminationMapping.count(state) > 0) { + if (stateRemapping[eliminationMapping[state]] == uint_fast64_t(-1)) { + stateRemapping[eliminationMapping[state]] = currentNewState; + stateRemapping[state] = currentNewState; + ++currentNewState; + queue.push(eliminationMapping[state]); + } else { + stateRemapping[state] = stateRemapping[eliminationMapping[state]]; + } + } else if (stateRemapping[state] == uint_fast64_t(-1)) { + stateRemapping[state] = currentNewState; + queue.push(state); + ++currentNewState; + } + } + + uint64_t newStateCount = ma->getNumberOfStates() - eliminationMapping.size(); + // Build the new MA + storm::storage::SparseMatrix newTransitionMatrix; + storm::models::sparse::StateLabeling newStateLabeling( + newStateCount); + storm::storage::BitVector newMarkovianStates(ma->getNumberOfStates() - eliminationMapping.size(), + false); + std::vector newExitRates; + //TODO choice labeling + boost::optional newChoiceLabeling; + + // Initialize the matrix builder and helper variables + storm::storage::SparseMatrixBuilder matrixBuilder = storm::storage::SparseMatrixBuilder( + 0, 0, 0, false, true, 0); + uint_fast64_t currentRow = 0; + uint_fast64_t state = 0; + while (!queue.empty()) { + state = queue.front(); + queue.pop(); + + for (auto const &label : ma->getLabelsOfState(state)) { + if (!newStateLabeling.containsLabel(label)) { + newStateLabeling.addLabel(label); + } + + newStateLabeling.addLabelToState(label, stateRemapping[state]); + } + + // Use a set to not include redundant rows + std::set> rowSet; + for (uint_fast64_t row = 0; row < ma->getTransitionMatrix().getRowGroupSize(state); ++row) { + std::map transitions; + for (typename storm::storage::SparseMatrix::const_iterator itEntry = ma->getTransitionMatrix().getRow( + state, row).begin(); + itEntry != ma->getTransitionMatrix().getRow(state, row).end(); ++itEntry) { + uint_fast64_t newId = stateRemapping[itEntry->getColumn()]; + if (transitions.count(newId) == 0) { + transitions[newId] = itEntry->getValue(); + } else { + transitions[newId] += itEntry->getValue(); + } + } + rowSet.insert(transitions); + } + + // correctly set rates + auto rate = storm::utility::zero(); + + if (ma->isMarkovianState(state)) { + newMarkovianStates.set(stateRemapping[state], true); + rate = ma->getExitRates().at(state); + } + + newExitRates.push_back(rate); + // Build matrix + matrixBuilder.newRowGroup(currentRow); + for (auto const &row : rowSet) { + for (auto const &transition : row) { + matrixBuilder.addNextValue(currentRow, transition.first, transition.second); + STORM_LOG_TRACE(stateRemapping[state] << "->" << transition.first << " : " << transition.second + << std::endl); + } + ++currentRow; + } + } + // explicitly force dimensions of the matrix in case a column is missing + newTransitionMatrix = matrixBuilder.build(newStateCount, newStateCount, newStateCount); + + storm::storage::sparse::ModelComponents newComponents = storm::storage::sparse::ModelComponents( + std::move(newTransitionMatrix), std::move(newStateLabeling)); + + newComponents.rateTransitions = false; + newComponents.markovianStates = std::move(newMarkovianStates); + newComponents.exitRates = std::move(newExitRates); + auto model = std::make_shared>( + std::move(newComponents)); + if (model->isConvertibleToCtmc()) { + return model->convertToCtmc(); + } else { + return model; + } + } + + template + bool NonMarkovianChainTransformer::preservesFormula( + storm::logic::Formula const &formula) { + storm::logic::FragmentSpecification fragment = storm::logic::propositional(); + + fragment.setProbabilityOperatorsAllowed(true); + fragment.setGloballyFormulasAllowed(true); + fragment.setReachabilityProbabilityFormulasAllowed(true); + fragment.setUntilFormulasAllowed(true); + fragment.setTimeBoundedUntilFormulasAllowed(true); + + return formula.isInFragment(fragment); + } + + template + std::vector> + NonMarkovianChainTransformer::checkAndTransformFormulas( + std::vector> const &formulas) { + std::vector> result; + + for (auto const &f : formulas) { + if (preservesFormula(*f)) { + result.push_back(f); + } else { + STORM_LOG_INFO("Non-Markovian chain elimination does not preserve formula " << *f); + } + } + return result; + } + + + template + class NonMarkovianChainTransformer; + + template + class NonMarkovianChainTransformer>; +#ifdef STORM_HAVE_CARL + + template + class NonMarkovianChainTransformer; + + template + class NonMarkovianChainTransformer; + +#endif + } +} + diff --git a/src/storm/transformer/NonMarkovianChainTransformer.h b/src/storm/transformer/NonMarkovianChainTransformer.h new file mode 100644 index 000000000..317be4b2d --- /dev/null +++ b/src/storm/transformer/NonMarkovianChainTransformer.h @@ -0,0 +1,46 @@ +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/logic/Formula.h" + +namespace storm { + namespace transformer { + /** + * Transformer for eliminating chains of non-Markovian states (instantaneous path fragment leading to the same outcome) from Markov Automata + */ + template> + class NonMarkovianChainTransformer { + public: + + /** + * Generates a model with the same basic behavior as the input, but eliminates non-Markovian chains. + * If no non-determinism occurs, a CTMC is generated. + * + * @param ma the input Markov Automaton + * @param preserveLabels if set, the procedure considers the labels of non-Markovian states when eliminating states + * @return a reference to the new Mmodel after eliminating non-Markovian states + */ + static std::shared_ptr< + models::sparse::Model < ValueType, RewardModelType>> eliminateNonmarkovianStates(std::shared_ptr< + models::sparse::MarkovAutomaton < ValueType, RewardModelType>> ma, + bool preserveLabels = true + ); + + /** + * Check if the property specified by the given formula is preserved by the transformation. + * + * @param formula the formula to check + * @return true, if the property is preserved + */ + static bool preservesFormula(storm::logic::Formula const &formula); + + /** + * Checks for the given formulae if the specified properties are preserved and removes formulae of properties which are not preserved. + * + * @param formulas + * @return vector containing all fomulae which are valid for the transformed model + */ + static std::vector> + checkAndTransformFormulas(std::vector> const &formulas); + }; + } +} + diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index e011eb12c..14d640e1f 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -2,6 +2,7 @@ #include "storm-config.h" #include "storm-dft/api/storm-dft.h" +#include "storm-dft/transformations/DftTransformator.h" #include "storm-parsers/api/storm-parsers.h" namespace { @@ -73,7 +74,9 @@ namespace { } double analyzeMTTF(std::string const& file) { - std::shared_ptr> dft = storm::api::loadDFTGalileoFile(file); + storm::transformations::dft::DftTransformator dftTransformator = storm::transformations::dft::DftTransformator(); + std::shared_ptr> dft = dftTransformator.transformBinaryFDEPs( + *(storm::api::loadDFTGalileoFile(file))); EXPECT_TRUE(storm::api::isWellFormed(*dft)); std::string property = "Tmin=? [F \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); @@ -86,8 +89,9 @@ namespace { return boost::get(results[0]); } - double analyzeReliability(std::string const& file, double bound) { - std::shared_ptr> dft = storm::api::loadDFTGalileoFile(file); + double analyzeReliability(std::string const &file, double bound) { + storm::transformations::dft::DftTransformator dftTransformator = storm::transformations::dft::DftTransformator(); + std::shared_ptr> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile(file))); EXPECT_TRUE(storm::api::isWellFormed(*dft)); std::string property = "Pmin=? [F<=" + std::to_string(bound) + " \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties( @@ -147,17 +151,28 @@ namespace { } TYPED_TEST(DftModelCheckerTest, FdepMTTF) { - double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep2.dft"); - EXPECT_FLOAT_EQ(result, 2); - result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep3.dft"); - EXPECT_FLOAT_EQ(result, 2.5); if (this->getConfig().useMod) { EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep.dft"), storm::exceptions::NotSupportedException); +EXPECT_THROW(this-> +analyzeMTTF(STORM_TEST_RESOURCES_DIR +"/dft/fdep2.dft"), storm::exceptions::NotSupportedException); +EXPECT_THROW(this-> +analyzeMTTF(STORM_TEST_RESOURCES_DIR +"/dft/fdep3.dft"), storm::exceptions::NotSupportedException); EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep4.dft"), storm::exceptions::NotSupportedException); EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft"), storm::exceptions::NotSupportedException); } else { - result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep.dft"); +double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR +"/dft/fdep.dft"); EXPECT_FLOAT_EQ(result, 2 / 3.0); +result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR +"/dft/fdep2.dft"); +EXPECT_FLOAT_EQ(result, +2); +result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR +"/dft/fdep3.dft"); +EXPECT_FLOAT_EQ(result, +2.5); result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep4.dft"); EXPECT_FLOAT_EQ(result, 1); result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft"); @@ -168,13 +183,24 @@ namespace { TYPED_TEST(DftModelCheckerTest, PdepMTTF) { double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep.dft"); EXPECT_FLOAT_EQ(result, 8 / 3.0); - result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep3.dft"); - EXPECT_FLOAT_EQ(result, 67 / 24.0); + if (this->getConfig().useMod) { - result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep2.dft"); - EXPECT_FLOAT_EQ(result, 38 / 15.0); +EXPECT_THROW(this-> +analyzeMTTF(STORM_TEST_RESOURCES_DIR +"/dft/pdep2.dft"), storm::exceptions::NotSupportedException); +EXPECT_THROW(this-> +analyzeMTTF(STORM_TEST_RESOURCES_DIR +"/dft/pdep3.dft"), storm::exceptions::NotSupportedException); EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft"), storm::exceptions::NotSupportedException); } else { +result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR +"/dft/pdep2.dft"); +EXPECT_FLOAT_EQ(result, +38 / 15.0); +result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR +"/dft/pdep3.dft"); +EXPECT_FLOAT_EQ(result, +67 / 24.0); result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft"); EXPECT_EQ(result, storm::utility::infinity()); } @@ -210,8 +236,6 @@ namespace { EXPECT_FLOAT_EQ(result, 6); result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq5.dft"); EXPECT_EQ(result, storm::utility::infinity()); - result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq6.dft"); - EXPECT_FLOAT_EQ(result, 30000); result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/mutex.dft"); EXPECT_FLOAT_EQ(result, 0.5); @@ -219,6 +243,21 @@ namespace { EXPECT_FLOAT_EQ(result, storm::utility::infinity()); result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/mutex3.dft"); EXPECT_FLOAT_EQ(result, storm::utility::infinity()); +if (this-> + +getConfig() + +.useMod){ +EXPECT_THROW(this-> +analyzeMTTF(STORM_TEST_RESOURCES_DIR +"/dft/seq6.dft"), storm::exceptions::NotSupportedException); +} +else { +result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR +"/dft/seq6.dft"); +EXPECT_FLOAT_EQ(result, +30000); +} } TYPED_TEST(DftModelCheckerTest, Symmetry) { diff --git a/src/test/storm-dft/api/DftSmtTest.cpp b/src/test/storm-dft/api/DftSmtTest.cpp index 95bcad150..f23a433c9 100644 --- a/src/test/storm-dft/api/DftSmtTest.cpp +++ b/src/test/storm-dft/api/DftSmtTest.cpp @@ -42,8 +42,8 @@ namespace { storm::modelchecker::DFTASFChecker smtChecker(*dft); smtChecker.convert(); smtChecker.toSolver(); - EXPECT_EQ(smtChecker.getLeastFailureBound(30), uint64_t(2)); - EXPECT_EQ(smtChecker.getAlwaysFailedBound(30), uint64_t(4)); + EXPECT_EQ(storm::dft::utility::FailureBoundFinder::getLeastFailureBound(*dft, true, 30), uint64_t(2)); + EXPECT_EQ(storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, true, 30), uint64_t(4)); } TEST(DftSmtTest, FDEPBoundTest) { @@ -53,7 +53,44 @@ namespace { storm::modelchecker::DFTASFChecker smtChecker(*dft); smtChecker.convert(); smtChecker.toSolver(); - EXPECT_EQ(smtChecker.getLeastFailureBound(30), uint64_t(1)); - EXPECT_EQ(smtChecker.getAlwaysFailedBound(30), uint64_t(5)); + EXPECT_EQ(storm::dft::utility::FailureBoundFinder::getLeastFailureBound(*dft, true, 30), uint64_t(1)); + EXPECT_EQ(storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, true, 30), uint64_t(5)); + } + + TEST(DftSmtTest, FDEPConflictTest) { + std::shared_ptr> dft = + storm::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/spare_conflict_test.dft"); + EXPECT_TRUE(storm::api::isWellFormed(*dft)); + std::vector true_vector(10, true); + + dft->setDynamicBehaviorInfo(); + EXPECT_EQ(dft->getDynamicBehavior(), true_vector); + + EXPECT_TRUE(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).empty()); + } + + TEST(DftSmtTest, FDEPConflictSPARETest) { + std::shared_ptr> dft = + storm::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/spare_conflict_test.dft"); + EXPECT_TRUE(storm::api::isWellFormed(*dft)); + std::vector true_vector(10, true); + + dft->setDynamicBehaviorInfo(); + EXPECT_EQ(dft->getDynamicBehavior(), true_vector); + + EXPECT_TRUE(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).empty()); + } + + TEST(DftSmtTest, FDEPConflictSEQTest) { + std::shared_ptr> dft = + storm::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/seq_conflict_test.dft"); + EXPECT_TRUE(storm::api::isWellFormed(*dft)); + std::vector expected_dynamic_vector(dft->nrElements(), true); + expected_dynamic_vector.at(dft->getTopLevelIndex()) = false; + + dft->setDynamicBehaviorInfo(); + EXPECT_EQ(dft->getDynamicBehavior(), expected_dynamic_vector); + + EXPECT_EQ(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).size(), uint64_t(3)); } } \ No newline at end of file diff --git a/src/test/storm-dft/api/DftTransformatorTest.cpp b/src/test/storm-dft/api/DftTransformatorTest.cpp new file mode 100644 index 000000000..97646fd83 --- /dev/null +++ b/src/test/storm-dft/api/DftTransformatorTest.cpp @@ -0,0 +1,69 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm-dft/api/storm-dft.h" +#include "storm-dft/transformations/DftTransformator.h" + +namespace { + + TEST(DftTransformatorTest, UniqueConstantFailedTest) { + std::string file = STORM_TEST_RESOURCES_DIR "/dft/const_be_test.dft"; + std::shared_ptr> originalDft = storm::api::loadDFTGalileoFile(file); + auto dftTransformator = storm::transformations::dft::DftTransformator(); + std::shared_ptr> transformedDft = dftTransformator.transformUniqueFailedBe( + *originalDft); + + auto bes = transformedDft->getBasicElements(); + uint64_t constBeFailedCount = 0; + uint64_t constBeFailsafeCount = 0; + for (auto &be : bes) { + if (be->type() == storm::storage::DFTElementType::BE_CONST) { + if (be->canFail()) { + ++constBeFailedCount; + } else { + ++constBeFailsafeCount; + } + } + } + + EXPECT_EQ(1ul, constBeFailedCount); + EXPECT_EQ(3ul, constBeFailsafeCount); + } + + TEST(DftTransformatorTest, BinaryFDEPTest) { + std::string file = STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft"; + std::shared_ptr> originalDft = storm::api::loadDFTGalileoFile(file); + auto dftTransformator = storm::transformations::dft::DftTransformator(); + std::shared_ptr> transformedDft = dftTransformator.transformBinaryFDEPs( + *originalDft); + + uint64_t dependencyCount = transformedDft->getDependencies().size(); + + EXPECT_EQ(2ul, dependencyCount); + } + + TEST(DftTransformatorTest, PDEPTransformTest) { + std::string file = STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft"; + std::shared_ptr> originalDft = storm::api::loadDFTGalileoFile(file); + auto dftTransformator = storm::transformations::dft::DftTransformator(); + std::shared_ptr> transformedDft = dftTransformator.transformBinaryFDEPs( + *originalDft); + + uint64_t fdepCount = 0; + uint64_t pdepCount = 0; + + for (auto depIndex : transformedDft->getDependencies()) { + auto dep = transformedDft->getDependency(depIndex); + if (dep->probability() == 1) { + ++fdepCount; + } else { + ++pdepCount; + } + } + + EXPECT_EQ(1ul, pdepCount); + EXPECT_EQ(2ul, fdepCount); + EXPECT_EQ(4ul, transformedDft->nrBasicElements()); + } + +} \ No newline at end of file