diff --git a/src/builder/DftExplorationHeuristic.cpp b/src/builder/DftExplorationHeuristic.cpp new file mode 100644 index 000000000..1364026a1 --- /dev/null +++ b/src/builder/DftExplorationHeuristic.cpp @@ -0,0 +1,76 @@ +#include "src/builder/DftExplorationHeuristic.h" +#include "src/adapters/CarlAdapter.h" +#include "src/utility/macros.h" +#include "src/utility/constants.h" +#include "src/exceptions/NotImplementedException.h" +#include "src/storage/dft/DFTState.h" + +#include + +namespace storm { + namespace builder { + + template + DFTExplorationHeuristic::DFTExplorationHeuristic() : skip(true), depth(std::numeric_limits::max()), rate(storm::utility::zero()), exitRate(storm::utility::zero()) { + // Intentionally left empty + } + + template + bool DFTExplorationHeuristic::isSkip() const { + return skip; + } + + template + size_t DFTExplorationHeuristic::getDepth() const { + return depth; + } + + template + void DFTExplorationHeuristic::setHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) { + std::cout << "Set priority: " << depth << ", old: " << this->depth << std::endl; + this->depth = depth; + // TODO Matthias: update rates and exitRates as well + this->rate = rate; + this->exitRate = exitRate; + } + + template + double DFTExplorationHeuristic::getPriority() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Approximation works only for double."); + } + + template<> + double DFTExplorationHeuristic::getPriority() const { + // TODO Matthias: change according to heuristic + if (!skip) { + // TODO Matthias: change to non-magic number + return 0; + } + //return rate/exitRate; + return depth; + } + + template<> + double DFTExplorationHeuristic::getPriority() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Approximation works only for double."); + /*std::cout << (rate / exitRate) << " < " << threshold << ": " << (number < threshold) << std::endl; + std::map mapping; + storm::RationalFunction eval(number.evaluate(mapping)); + std::cout << "Evaluated: " << eval << std::endl; + return eval < threshold;*/ + } + + template + bool compareDepth(std::shared_ptr> stateA, std::shared_ptr> stateB) { + return stateA->getPriority() > stateB->getPriority(); + } + + template class DFTExplorationHeuristic; + template bool compareDepth(std::shared_ptr>, std::shared_ptr>); + +#ifdef STORM_HAVE_CARL + template class DFTExplorationHeuristic; + template bool compareDepth(std::shared_ptr>, std::shared_ptr>); +#endif + } +} diff --git a/src/builder/DftExplorationHeuristic.h b/src/builder/DftExplorationHeuristic.h new file mode 100644 index 000000000..59c35f812 --- /dev/null +++ b/src/builder/DftExplorationHeuristic.h @@ -0,0 +1,44 @@ +#ifndef STORM_BUILDER_DFTEXPLORATIONHEURISTIC_H_ +#define STORM_BUILDER_DFTEXPLORATIONHEURISTIC_H_ + +#include +#include + +namespace storm { + + // Forward declaration + namespace storage { + template + class DFTState; + } + + namespace builder { + + template + class DFTExplorationHeuristic { + + public: + DFTExplorationHeuristic(); + + void setHeuristicValues(size_t depth, ValueType rate, ValueType exitRate); + + bool isSkip() const; + + size_t getDepth() const; + + double getPriority() const; + + private: + bool skip; + size_t depth; + ValueType rate; + ValueType exitRate; + + }; + + template + bool compareDepth(std::shared_ptr> stateA, std::shared_ptr> stateB); + } +} + +#endif /* STORM_BUILDER_DFTEXPLORATIONHEURISTIC_H_ */ diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 0729fec59..3dedfd01d 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -25,15 +25,16 @@ namespace storm { template ExplicitDFTModelBuilderApprox::ExplicitDFTModelBuilderApprox(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : dft(dft), stateGenerationInfo(std::make_shared(dft.buildStateGenerationInfo(symmetries))), enableDC(enableDC), generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates), matrixBuilder(!generator.isDeterministicModel()), stateStorage(((dft.stateVectorSize() / 64) + 1) * 64) { // stateVectorSize is bound for size of bitvector + + // Compare states by their distance from the initial state + // TODO Matthias: customize + statesToExplore = std::priority_queue, std::function>(&storm::builder::compareDepth); } template - void ExplicitDFTModelBuilderApprox::buildModel(LabelOptions const& labelOpts, bool firstTime, double approximationError) { + void ExplicitDFTModelBuilderApprox::buildModel(LabelOptions const& labelOpts, bool firstTime, double approximationThreshold) { STORM_LOG_TRACE("Generating DFT state space"); - // Initialize - generator.setApproximationError(approximationError); - if (firstTime) { // Initialize modelComponents.markovianStates = storm::storage::BitVector(INITIAL_BITVECTOR_SIZE); @@ -72,7 +73,7 @@ namespace storm { initializeNextIteration(); } - exploreStateSpace(); + exploreStateSpace(approximationThreshold); size_t stateSize = stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0); modelComponents.markovianStates.resize(stateSize); @@ -169,7 +170,7 @@ namespace storm { size_t index = modelComponents.markovianStates.getNextSetIndex(0); while (index < modelComponents.markovianStates.size()) { markovianStatesNew.set(indexRemapping[index], false); - index = modelComponents.markovianStates.getNextSetIndex(index); + index = modelComponents.markovianStates.getNextSetIndex(index+1); } STORM_LOG_ASSERT(modelComponents.markovianStates.size() - modelComponents.markovianStates.getNumberOfSetBits() == markovianStatesNew.getNumberOfSetBits(), "Remapping of markovian states is wrong."); STORM_LOG_ASSERT(markovianStatesNew.size() == nrStates, "No. of states does not coincide with markovian size."); @@ -201,23 +202,24 @@ namespace storm { STORM_LOG_ASSERT(matrixBuilder.getCurrentRowGroup() == nrExpandedStates, "Row group size does not match."); - // Explore all skipped states now + // Push skipped states to explore queue + // TODO Matthias: remove for (auto const& skippedState : skippedStates) { - skippedState.second->setSkip(false); - statesToExplore.push_front(skippedState.second); + statesToExplore.push(skippedState.second); } skippedStates.clear(); } template - void ExplicitDFTModelBuilderApprox::exploreStateSpace() { + void ExplicitDFTModelBuilderApprox::exploreStateSpace(double approximationThreshold) { bool explorationFinished = false; size_t pseudoStatesToCheck = 0; while (!explorationFinished) { // Get the first state in the queue - DFTStatePointer currentState = statesToExplore.front(); + DFTStatePointer currentState = statesToExplore.top(); + STORM_LOG_ASSERT(stateStorage.stateToId.contains(currentState->status()), "State is not contained in state storage."); STORM_LOG_ASSERT(stateStorage.stateToId.getValue(currentState->status()) == currentState->getId(), "Ids of states do not coincide."); - statesToExplore.pop_front(); + statesToExplore.pop(); // Remember that the current row group was actually filled with the transitions of a different state matrixBuilder.setRemapping(currentState->getId()); @@ -227,7 +229,8 @@ namespace storm { // Try to explore the next state generator.load(currentState); - if (currentState->isSkip()) { + STORM_LOG_TRACE("Priority of state " <getId() << ": " << currentState->getPriority()); + if (currentState->getPriority() > approximationThreshold) { // Skip the current state STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState)); setMarkovian(true); @@ -464,7 +467,7 @@ namespace storm { stateId = state->getId(); stateStorage.stateToId.setOrAdd(state->status(), stateId); STORM_LOG_TRACE("Now create state " << dft.getStateString(state) << " with id " << stateId); - statesToExplore.push_front(state); + statesToExplore.push(state); } } else { // State does not exist yet @@ -483,7 +486,7 @@ namespace storm { stateId = stateStorage.stateToId.findOrAdd(state->status(), state->getId()); STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not match."); STORM_LOG_TRACE("New state: " << dft.getStateString(state)); - statesToExplore.push_front(state); + statesToExplore.push(state); // Reserve one slot for the new state in the remapping matrixBuilder.stateRemapping.push_back(0); diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h index b8658c6ce..65575735f 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/builder/ExplicitDFTModelBuilderApprox.h @@ -1,14 +1,15 @@ #ifndef EXPLICITDFTMODELBUILDERAPPROX_H #define EXPLICITDFTMODELBUILDERAPPROX_H -#include -#include -#include +#include "src/builder/DftExplorationHeuristic.h" +#include "src/models/sparse/StateLabeling.h" +#include "src/models/sparse/StandardRewardModel.h" +#include "src/models/sparse/Model.h" #include "src/generator/DftNextStateGenerator.h" -#include +#include "src/storage/SparseMatrix.h" #include "src/storage/sparse/StateStorage.h" -#include -#include +#include "src/storage/dft/DFT.h" +#include "src/storage/dft/SymmetricUnits.h" #include #include #include @@ -156,11 +157,11 @@ namespace storm { /*! * Build model from DFT. * - * @param labelOpts Options for labeling. - * @param firstTime Flag indicating if the model is built for the first time or rebuilt. - * @param approximationError Error allowed for approximation. + * @param labelOpts Options for labeling. + * @param firstTime Flag indicating if the model is built for the first time or rebuilt. + * @param approximationThreshold Threshold determining when to skip exploring states. */ - void buildModel(LabelOptions const& labelOpts, bool firstTime, double approximationError = 0.0); + void buildModel(LabelOptions const& labelOpts, bool firstTime, double approximationThreshold = 0.0); /*! * Get the built model. @@ -182,8 +183,10 @@ namespace storm { /*! * Explore state space of DFT. + * + * @param approximationThreshold Threshold to determine when to skip states. */ - void exploreStateSpace(); + void exploreStateSpace(double approximationThreshold); /*! * Initialize the matrix for a refinement iteration. @@ -237,7 +240,6 @@ namespace storm { */ std::shared_ptr> createModel(bool copy); - // Initial size of the bitvector. const size_t INITIAL_BITVECTOR_SIZE = 20000; // Offset used for pseudo states. @@ -280,14 +282,15 @@ namespace storm { // Internal information about the states that were explored. storm::storage::sparse::StateStorage stateStorage; - // A set of states that still need to be explored. - std::deque statesToExplore; + // A pniority queue of states that still need to be explored. + std::priority_queue, std::function> statesToExplore; // Holds all skipped states which were not yet expanded. More concretely it is a mapping from matrix indices // to the corresponding skipped states. // Notice that we need an ordered map here to easily iterate in increasing order over state ids. std::map skippedStates; }; + } } diff --git a/src/generator/DftNextStateGenerator.cpp b/src/generator/DftNextStateGenerator.cpp index 119ff9342..31d17fbe0 100644 --- a/src/generator/DftNextStateGenerator.cpp +++ b/src/generator/DftNextStateGenerator.cpp @@ -20,6 +20,7 @@ namespace storm { template std::vector DftNextStateGenerator::getInitialStates(StateToIdCallback const& stateToIdCallback) { DFTStatePointer initialState = std::make_shared>(mDft, mStateGenerationInfo, 0); + initialState->setHeuristicValues(0, storm::utility::zero(), storm::utility::zero()); // Register initial state StateType id = stateToIdCallback(initialState); @@ -75,7 +76,7 @@ namespace storm { STORM_LOG_ASSERT(!mDft.hasFailed(state), "Dft has failed."); // Construct new state as copy from original one - DFTStatePointer newState = std::make_shared>(*state); + DFTStatePointer newState = state->copy(); std::pair const>, bool> nextBEPair = newState->letNextBEFail(currentFailable); std::shared_ptr const>& nextBE = nextBEPair.first; STORM_LOG_ASSERT(nextBE, "NextBE is null."); @@ -150,15 +151,17 @@ namespace storm { if (!storm::utility::isOne(probability)) { // Add transition to state where dependency was unsuccessful - DFTStatePointer unsuccessfulState = std::make_shared>(*state); + DFTStatePointer unsuccessfulState = state->copy(); unsuccessfulState->letDependencyBeUnsuccessful(currentFailable); // Add state StateType unsuccessfulStateId = stateToIdCallback(unsuccessfulState); ValueType remainingProbability = storm::utility::one() - probability; choice.addProbability(unsuccessfulStateId, remainingProbability); STORM_LOG_TRACE("Added transition to " << unsuccessfulStateId << " with remaining probability " << remainingProbability); + unsuccessfulState->setHeuristicValues(state, remainingProbability, storm::utility::one()); } result.addChoice(std::move(choice)); + newState->setHeuristicValues(state, probability, storm::utility::one()); } else { // Failure is due to "normal" BE failure // Set failure rate according to activation @@ -171,14 +174,7 @@ namespace storm { STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Rate is 0."); choice.addProbability(newStateId, rate); STORM_LOG_TRACE("Added transition to " << newStateId << " with " << (isActive ? "active" : "passive") << " failure rate " << rate); - - // Check if new state needs expansion for approximation - if (approximationError > 0.0) { - if (checkSkipState(newState, rate, choice.getTotalMass(), approximationError)) { - STORM_LOG_TRACE("Will skip state " << newStateId); - newState->setSkip(true); - } - } + newState->setHeuristicValues(state, rate, choice.getTotalMass()); } ++currentFailable; @@ -213,37 +209,10 @@ namespace storm { return result; } - template - void DftNextStateGenerator::setApproximationError(double approximationError) { - this->approximationError = approximationError; - } - - template - bool DftNextStateGenerator::checkSkipState(DFTStatePointer const& state, ValueType rate, ValueType exitRate, double approximationError) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Approximation works only for double."); - } - - template<> - bool DftNextStateGenerator::checkSkipState(DFTStatePointer const& state, double rate, double exitRate, double approximationError) { - if (mDft.hasFailed(state) || mDft.isFailsafe(state) || (state->nrFailableDependencies() == 0 && state->nrFailableBEs() == 0)) { - // Do not skip absorbing state - return false; - } - // Skip if the rate to reach this state is low compared to all other outgoing rates from the predecessor - return rate/exitRate < approximationError; - } - - template<> - bool DftNextStateGenerator::checkSkipState(DFTStatePointer const& state, storm::RationalFunction rate, storm::RationalFunction exitRate, double approximationError) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Approximation works only for double."); - /*std::cout << (rate / exitRate) << " < " << threshold << ": " << (number < threshold) << std::endl; - std::map mapping; - storm::RationalFunction eval(number.evaluate(mapping)); - std::cout << "Evaluated: " << eval << std::endl; - return eval < threshold;*/ - } - template class DftNextStateGenerator; + +#ifdef STORM_HAVE_CARL template class DftNextStateGenerator; +#endif } } diff --git a/src/generator/DftNextStateGenerator.h b/src/generator/DftNextStateGenerator.h index 6fa815e44..8fdfbf471 100644 --- a/src/generator/DftNextStateGenerator.h +++ b/src/generator/DftNextStateGenerator.h @@ -42,13 +42,6 @@ namespace storm { */ StateBehavior createMergeFailedState(StateToIdCallback const& stateToIdCallback); - /*! - * Set a new value for the allowed approximation error. - * - * @param approximationError Allowed approximation error. - */ - void setApproximationError(double approximationError); - private: // The dft used for the generation of next states. @@ -72,20 +65,6 @@ namespace storm { // Flag indicating if the model is deterministic. bool deterministicModel = false; - // Allowed approximation error. - double approximationError = 0.0; - - /*! - * Check if the given state should be skipped for expansion. - * - * @param state State to check for expansion - * @param rate Rate of current state - * @param exitRate Exit rates of all outgoing transitions - * @param approximationError Allowed approximation error - * - * @return True, if the given state should be skipped. - */ - bool checkSkipState(DFTStatePointer const& state, ValueType rate, ValueType exitRate, double approximationError); }; } diff --git a/src/modelchecker/dft/DFTModelChecker.cpp b/src/modelchecker/dft/DFTModelChecker.cpp index 7ac2f1a8a..205e658f3 100644 --- a/src/modelchecker/dft/DFTModelChecker.cpp +++ b/src/modelchecker/dft/DFTModelChecker.cpp @@ -162,7 +162,7 @@ namespace storm { STORM_LOG_INFO("Building model..."); // TODO Matthias refine model using existing model and MC results currentApproximationError = pow(0.1, iteration) * approximationError; - builder.buildModel(labeloptions, iteration < 1, currentApproximationError); + builder.buildModel(labeloptions, iteration < 1, iteration); // TODO Matthias: possible to do bisimulation on approximated model and not on concrete one? diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index a38bd21b8..5e84b0c56 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -6,7 +6,7 @@ namespace storm { namespace storage { template - DFTState::DFTState(DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateVectorSize()), mId(id), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { + DFTState::DFTState(DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateVectorSize()), mId(id), mDft(dft), mStateGenerationInfo(stateGenerationInfo), exploreHeuristic() { // Initialize uses for(size_t spareId : mDft.getSpareIndices()) { @@ -55,6 +55,13 @@ namespace storm { } } + template + std::shared_ptr> DFTState::copy() const { + std::shared_ptr> stateCopy = std::make_shared>(*this); + stateCopy->exploreHeuristic = storm::builder::DFTExplorationHeuristic(); + return stateCopy; + } + template DFTElementState DFTState::getElementState(size_t id) const { return static_cast(getElementStateInt(id)); diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index c87008c9c..cd2b9eb0f 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -1,8 +1,9 @@ #ifndef DFTSTATE_H #define DFTSTATE_H -#include "../BitVector.h" -#include "DFTElementState.h" +#include "src/storage/dft/DFTElementState.h" +#include "src/storage/BitVector.h" +#include "src/builder/DftExplorationHeuristic.h" #include #include @@ -31,7 +32,7 @@ namespace storm { bool mValid = true; const DFT& mDft; const DFTStateGenerationInfo& mStateGenerationInfo; - bool mSkip = false; + storm::builder::DFTExplorationHeuristic exploreHeuristic; public: DFTState(DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id); @@ -40,7 +41,9 @@ namespace storm { * Construct state from underlying bitvector. */ DFTState(storm::storage::BitVector const& status, DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id); - + + std::shared_ptr> copy() const; + DFTElementState getElementState(size_t id) const; DFTDependencyState getDependencyState(size_t id) const; @@ -97,12 +100,20 @@ namespace storm { return !mValid; } - void setSkip(bool skip) { - mSkip = skip; + void setHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) { + exploreHeuristic.setHeuristicValues(depth, rate, exitRate); + } + + void setHeuristicValues(std::shared_ptr> oldState, ValueType rate, ValueType exitRate) { + if (hasFailed(mDft.getTopLevelIndex()) || isFailsafe(mDft.getTopLevelIndex()) || (nrFailableDependencies() == 0 && nrFailableBEs() == 0)) { + // Do not skip absorbing state + exploreHeuristic.setNotSkip(); + } + exploreHeuristic.setHeuristicValues(oldState->exploreHeuristic.getDepth() + 1, rate, exitRate); } - bool isSkip() const { - return mSkip; + double getPriority() const { + return exploreHeuristic.getPriority(); } storm::storage::BitVector const& status() const {