From dde9af6c44959254518f5d684a4a73c35184f049 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 22 Feb 2016 00:05:05 +0100 Subject: [PATCH] mergeFailedStates and some updates for SEQs Former-commit-id: 128a7e0da53e11d8853a07d799c15720724dca34 --- src/builder/ExplicitDFTModelBuilder.cpp | 87 +++++++++++++++-------- src/builder/ExplicitDFTModelBuilder.h | 5 ++ src/storage/dft/DFTBuilder.cpp | 1 + src/storage/dft/DFTElements.cpp | 4 ++ src/storage/dft/elements/DFTRestriction.h | 12 ++-- src/storm-dyftee.cpp | 2 +- 6 files changed, 74 insertions(+), 37 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 4900845a5..1840ba40a 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -57,36 +57,47 @@ namespace storm { template std::shared_ptr> ExplicitDFTModelBuilder::buildModel(LabelOptions const& labelOpts) { // Initialize - DFTStatePointer state = std::make_shared>(mDft, *mStateGenerationInfo, newIndex++); - mStates.findOrAdd(state->status(), state->getId()); - - std::queue stateQueue; - stateQueue.push(state); - bool deterministicModel = false; ModelComponents modelComponents; std::vector tmpMarkovianStates; storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); + + if(mergeFailedStates) { + newIndex++; + + transitionMatrixBuilder.newRowGroup(failedIndex); + transitionMatrixBuilder.addNextValue(failedIndex, failedIndex, storm::utility::one()); + STORM_LOG_TRACE("Added self loop for " << failedIndex); + modelComponents.exitRates.push_back(storm::utility::one()); + tmpMarkovianStates.push_back(failedIndex); + } + + DFTStatePointer state = std::make_shared>(mDft, *mStateGenerationInfo, newIndex++); + mStates.findOrAdd(state->status(), state->getId()); + initialStateIndex = state->getId(); + std::queue stateQueue; + stateQueue.push(state); + // Begin model generation bool deterministic = exploreStates(stateQueue, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates); - STORM_LOG_DEBUG("Generated " << mStates.size() << " states"); + STORM_LOG_DEBUG("Generated " << mStates.size() + (mergeFailedStates ? 1 : 0) << " states"); STORM_LOG_DEBUG("Model is " << (deterministic ? "deterministic" : "non-deterministic")); + size_t stateSize = mStates.size() + (mergeFailedStates ? 1 : 0); // Build Markov Automaton - modelComponents.markovianStates = storm::storage::BitVector(mStates.size(), tmpMarkovianStates); + modelComponents.markovianStates = storm::storage::BitVector(stateSize, tmpMarkovianStates); // Build transition matrix - modelComponents.transitionMatrix = transitionMatrixBuilder.build(); + modelComponents.transitionMatrix = transitionMatrixBuilder.build(stateSize, stateSize); STORM_LOG_DEBUG("Transition matrix: " << std::endl << modelComponents.transitionMatrix); STORM_LOG_DEBUG("Exit rates: " << modelComponents.exitRates); STORM_LOG_DEBUG("Markovian states: " << modelComponents.markovianStates); - assert(!deterministic || modelComponents.transitionMatrix.getRowCount() == modelComponents.transitionMatrix.getColumnCount()); - + // Build state labeling - modelComponents.stateLabeling = storm::models::sparse::StateLabeling(mStates.size()); + modelComponents.stateLabeling = storm::models::sparse::StateLabeling(mStates.size() + (mergeFailedStates ? 1 : 0)); // Initial state is always first state without any failure modelComponents.stateLabeling.addLabel("init"); - modelComponents.stateLabeling.addLabelToState("init", 0); + modelComponents.stateLabeling.addLabelToState("init", initialStateIndex); // Label all states corresponding to their status (failed, failsafe, failed BE) if(labelOpts.buildFailLabel) { modelComponents.stateLabeling.addLabel("failed"); @@ -103,10 +114,13 @@ namespace storm { } } + if(mergeFailedStates) { + modelComponents.stateLabeling.addLabelToState("failed", failedIndex); + } for (auto const& stateIdPair : mStates) { storm::storage::BitVector state = stateIdPair.first; size_t stateId = stateIdPair.second; - if (labelOpts.buildFailLabel && mDft.hasFailed(state, *mStateGenerationInfo)) { + if (!mergeFailedStates && labelOpts.buildFailLabel && mDft.hasFailed(state, *mStateGenerationInfo)) { modelComponents.stateLabeling.addLabelToState("failed", stateId); } if (labelOpts.buildFailSafeLabel && mDft.isFailsafe(state, *mStateGenerationInfo)) { @@ -151,13 +165,12 @@ namespace storm { template bool ExplicitDFTModelBuilder::exploreStates(std::queue& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector& markovianStates, std::vector& exitRates) { - assert(exitRates.empty()); - assert(markovianStates.empty()); // TODO Matthias: set Markovian states directly as bitvector? std::map outgoingTransitions; size_t rowOffset = 0; // Captures number of non-deterministic choices bool deterministic = true; - + + while (!stateQueue.empty()) { // Initialization outgoingTransitions.clear(); @@ -189,6 +202,7 @@ namespace storm { // Let BE fail while (smallest < failableCount) { + assert(!mDft.hasFailed(state)); STORM_LOG_TRACE("exploring from: " << mDft.getStateString(state)); // Construct new state as copy from original one @@ -207,11 +221,23 @@ namespace storm { queues.propagateFailure(parent); } } + for (DFTRestrictionPointer restr : nextBE->restrictions()) { + queues.checkRestrictionLater(restr); + } while (!queues.failurePropagationDone()) { DFTGatePointer next = queues.nextFailurePropagation(); next->checkFails(*newState, queues); } + + while(!queues.restrictionChecksDone()) { + DFTRestrictionPointer next = queues.nextRestrictionCheck(); + next->checkFails(*newState, queues); + } + + if(newState->isInvalid()) { + continue; + } while (!queues.failsafePropagationDone()) { DFTGatePointer next = queues.nextFailsafePropagation(); @@ -226,19 +252,24 @@ namespace storm { // Update failable dependencies newState->updateFailableDependencies(nextBE->id()); + bool dftFailed = newState->hasFailed(mDft.getTopLevelIndex()); size_t newStateId; - if (mStates.contains(newState->status())) { - // State already exists - newStateId = mStates.getValue(newState->status()); - STORM_LOG_TRACE("State " << mDft.getStateString(newState) << " already exists"); + if(dftFailed && mergeFailedStates) { + newStateId = failedIndex; } else { - // New state - newState->setId(newIndex++); - newStateId = mStates.findOrAdd(newState->status(), newState->getId()); - STORM_LOG_TRACE("New state " << mDft.getStateString(newState)); - - // Add state to search queue - stateQueue.push(newState); + if (mStates.contains(newState->status())) { + // State already exists + newStateId = mStates.getValue(newState->status()); + STORM_LOG_TRACE("State " << mDft.getStateString(newState) << " already exists"); + } else { + // New state + newState->setId(newIndex++); + newStateId = mStates.findOrAdd(newState->status(), newState->getId()); + STORM_LOG_TRACE("New state " << mDft.getStateString(newState)); + + // Add state to search queue + stateQueue.push(newState); + } } // Set transitions diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h index 522f2375c..42ca2755d 100644 --- a/src/builder/ExplicitDFTModelBuilder.h +++ b/src/builder/ExplicitDFTModelBuilder.h @@ -23,6 +23,8 @@ namespace storm { using DFTElementCPointer = std::shared_ptr const>; using DFTGatePointer = std::shared_ptr>; using DFTStatePointer = std::shared_ptr>; + using DFTRestrictionPointer = std::shared_ptr>; + // A structure holding the individual components of a model. struct ModelComponents { @@ -52,6 +54,9 @@ namespace storm { std::shared_ptr mStateGenerationInfo; storm::storage::BitVectorHashMap mStates; size_t newIndex = 0; + bool mergeFailedStates = true; + size_t failedIndex = 0; + size_t initialStateIndex = 0; public: struct LabelOptions { diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index 62b022635..213fce0df 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -130,6 +130,7 @@ namespace storm { mElements[name] = restr; mRestrictionChildNames[restr] = children; mRestrictions.push_back(restr); + return true; } template diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp index 9d21e5dd4..7bb8c2cf5 100644 --- a/src/storage/dft/DFTElements.cpp +++ b/src/storage/dft/DFTElements.cpp @@ -10,6 +10,7 @@ namespace storm { if (state.dontCare(mId)) { return false; } + // Check that no outgoing dependencies can be triggered anymore for (DFTDependencyPointer dependency : mOutgoingDependencies) { if (state.isOperational(dependency->dependentEvent()->id()) && state.isOperational(dependency->triggerEvent()->id())) { @@ -22,6 +23,9 @@ namespace storm { return false; } } + + + state.setDontCare(mId); return true; diff --git a/src/storage/dft/elements/DFTRestriction.h b/src/storage/dft/elements/DFTRestriction.h index 0d8651e50..46b6e23cc 100644 --- a/src/storage/dft/elements/DFTRestriction.h +++ b/src/storage/dft/elements/DFTRestriction.h @@ -116,10 +116,6 @@ namespace storm { } virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { - if(DFTElement::checkDontCareAnymore(state, queues)) { - childrenDontCare(state, queues); - return true; - } return false; } @@ -134,10 +130,6 @@ namespace storm { } - void childrenDontCare(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { - queues.propagateDontCare(mChildren); - } - bool hasFailsafeChild(DFTState& state) const { for(auto const& child : mChildren) { if(state.isFailsafe(child->id())) @@ -189,6 +181,10 @@ namespace storm { void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { + } + + bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) { + } virtual DFTElementType type() const override { diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 2160ed210..aa2e0879f 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -48,7 +48,7 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false) std::cout << "Bisimulation..." << std::endl; - if (model->isOfType(storm::models::ModelType::Ctmc)) { + if (model->getNumberOfStates() > 500 && model->isOfType(storm::models::ModelType::Ctmc)) { model = storm::performDeterministicSparseBisimulationMinimization>(model->template as>(), formulas, storm::storage::BisimulationType::Weak)->template as>(); }