From 6b7bf3bba7abe115540cd3d20ec56fc5255cfd13 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Tue, 11 Oct 2016 22:50:16 +0200
Subject: [PATCH] Introduced heuristic depth with distance from initial state
Former-commit-id: 1b94ebc4f960f126b5338cdb0cee75aea0a42f1a
---
src/builder/DftExplorationHeuristic.cpp | 76 +++++++++++++++++++
src/builder/DftExplorationHeuristic.h | 44 +++++++++++
src/builder/ExplicitDFTModelBuilderApprox.cpp | 33 ++++----
src/builder/ExplicitDFTModelBuilderApprox.h | 31 ++++----
src/generator/DftNextStateGenerator.cpp | 49 +++---------
src/generator/DftNextStateGenerator.h | 21 -----
src/modelchecker/dft/DFTModelChecker.cpp | 2 +-
src/storage/dft/DFTState.cpp | 9 ++-
src/storage/dft/DFTState.h | 27 +++++--
9 files changed, 192 insertions(+), 100 deletions(-)
create mode 100644 src/builder/DftExplorationHeuristic.cpp
create mode 100644 src/builder/DftExplorationHeuristic.h
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 <limits>
+
+namespace storm {
+ namespace builder {
+
+ template<typename ValueType>
+ DFTExplorationHeuristic<ValueType>::DFTExplorationHeuristic() : skip(true), depth(std::numeric_limits<std::size_t>::max()), rate(storm::utility::zero<ValueType>()), exitRate(storm::utility::zero<ValueType>()) {
+ // Intentionally left empty
+ }
+
+ template<typename ValueType>
+ bool DFTExplorationHeuristic<ValueType>::isSkip() const {
+ return skip;
+ }
+
+ template<typename ValueType>
+ size_t DFTExplorationHeuristic<ValueType>::getDepth() const {
+ return depth;
+ }
+
+ template<typename ValueType>
+ void DFTExplorationHeuristic<ValueType>::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<typename ValueType>
+ double DFTExplorationHeuristic<ValueType>::getPriority() const {
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Approximation works only for double.");
+ }
+
+ template<>
+ double DFTExplorationHeuristic<double>::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<storm::RationalFunction>::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<storm::Variable, storm::RationalNumber> mapping;
+ storm::RationalFunction eval(number.evaluate(mapping));
+ std::cout << "Evaluated: " << eval << std::endl;
+ return eval < threshold;*/
+ }
+
+ template<typename ValueType>
+ bool compareDepth(std::shared_ptr<storm::storage::DFTState<ValueType>> stateA, std::shared_ptr<storm::storage::DFTState<ValueType>> stateB) {
+ return stateA->getPriority() > stateB->getPriority();
+ }
+
+ template class DFTExplorationHeuristic<double>;
+ template bool compareDepth(std::shared_ptr<storm::storage::DFTState<double>>, std::shared_ptr<storm::storage::DFTState<double>>);
+
+#ifdef STORM_HAVE_CARL
+ template class DFTExplorationHeuristic<storm::RationalFunction>;
+ template bool compareDepth(std::shared_ptr<storm::storage::DFTState<storm::RationalFunction>>, std::shared_ptr<storm::storage::DFTState<storm::RationalFunction>>);
+#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 <memory>
+#include <algorithm>
+
+namespace storm {
+
+ // Forward declaration
+ namespace storage {
+ template<typename ValueType>
+ class DFTState;
+ }
+
+ namespace builder {
+
+ template<typename ValueType>
+ 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<typename ValueType>
+ bool compareDepth(std::shared_ptr<storm::storage::DFTState<ValueType>> stateA, std::shared_ptr<storm::storage::DFTState<ValueType>> 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<typename ValueType, typename StateType>
ExplicitDFTModelBuilderApprox<ValueType, StateType>::ExplicitDFTModelBuilderApprox(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : dft(dft), stateGenerationInfo(std::make_shared<storm::storage::DFTStateGenerationInfo>(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<DFTStatePointer, std::deque<DFTStatePointer>, std::function<bool(DFTStatePointer, DFTStatePointer)>>(&storm::builder::compareDepth<ValueType>);
}
template<typename ValueType, typename StateType>
- void ExplicitDFTModelBuilderApprox<ValueType, StateType>::buildModel(LabelOptions const& labelOpts, bool firstTime, double approximationError) {
+ void ExplicitDFTModelBuilderApprox<ValueType, StateType>::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<typename ValueType, typename StateType>
- void ExplicitDFTModelBuilderApprox<ValueType, StateType>::exploreStateSpace() {
+ void ExplicitDFTModelBuilderApprox<ValueType, StateType>::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 " <<currentState->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 <src/models/sparse/StateLabeling.h>
-#include <src/models/sparse/StandardRewardModel.h>
-#include <src/models/sparse/Model.h>
+#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 <src/storage/SparseMatrix.h>
+#include "src/storage/SparseMatrix.h"
#include "src/storage/sparse/StateStorage.h"
-#include <src/storage/dft/DFT.h>
-#include <src/storage/dft/SymmetricUnits.h>
+#include "src/storage/dft/DFT.h"
+#include "src/storage/dft/SymmetricUnits.h"
#include <boost/container/flat_set.hpp>
#include <boost/optional/optional.hpp>
#include <stack>
@@ -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<storm::models::sparse::Model<ValueType>> 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<StateType> stateStorage;
- // A set of states that still need to be explored.
- std::deque<DFTStatePointer> statesToExplore;
+ // A pniority queue of states that still need to be explored.
+ std::priority_queue<DFTStatePointer, std::deque<DFTStatePointer>, std::function<bool(DFTStatePointer, DFTStatePointer)>> 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<StateType, DFTStatePointer> 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<typename ValueType, typename StateType>
std::vector<StateType> DftNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
DFTStatePointer initialState = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, mStateGenerationInfo, 0);
+ initialState->setHeuristicValues(0, storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
// 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<storm::storage::DFTState<ValueType>>(*state);
+ DFTStatePointer newState = state->copy();
std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType> const>, bool> nextBEPair = newState->letNextBEFail(currentFailable);
std::shared_ptr<storm::storage::DFTBE<ValueType> 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<storm::storage::DFTState<ValueType>>(*state);
+ DFTStatePointer unsuccessfulState = state->copy();
unsuccessfulState->letDependencyBeUnsuccessful(currentFailable);
// Add state
StateType unsuccessfulStateId = stateToIdCallback(unsuccessfulState);
ValueType remainingProbability = storm::utility::one<ValueType>() - probability;
choice.addProbability(unsuccessfulStateId, remainingProbability);
STORM_LOG_TRACE("Added transition to " << unsuccessfulStateId << " with remaining probability " << remainingProbability);
+ unsuccessfulState->setHeuristicValues(state, remainingProbability, storm::utility::one<ValueType>());
}
result.addChoice(std::move(choice));
+ newState->setHeuristicValues(state, probability, storm::utility::one<ValueType>());
} 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<typename ValueType, typename StateType>
- void DftNextStateGenerator<ValueType, StateType>::setApproximationError(double approximationError) {
- this->approximationError = approximationError;
- }
-
- template<typename ValueType, typename StateType>
- bool DftNextStateGenerator<ValueType, StateType>::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<double>::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<storm::RationalFunction>::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<storm::Variable, storm::RationalNumber> mapping;
- storm::RationalFunction eval(number.evaluate(mapping));
- std::cout << "Evaluated: " << eval << std::endl;
- return eval < threshold;*/
- }
-
template class DftNextStateGenerator<double>;
+
+#ifdef STORM_HAVE_CARL
template class DftNextStateGenerator<storm::RationalFunction>;
+#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<ValueType, StateType> 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<typename ValueType>
- DFTState<ValueType>::DFTState(DFT<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateVectorSize()), mId(id), mDft(dft), mStateGenerationInfo(stateGenerationInfo) {
+ DFTState<ValueType>::DFTState(DFT<ValueType> 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<typename ValueType>
+ std::shared_ptr<DFTState<ValueType>> DFTState<ValueType>::copy() const {
+ std::shared_ptr<DFTState<ValueType>> stateCopy = std::make_shared<storm::storage::DFTState<ValueType>>(*this);
+ stateCopy->exploreHeuristic = storm::builder::DFTExplorationHeuristic<ValueType>();
+ return stateCopy;
+ }
+
template<typename ValueType>
DFTElementState DFTState<ValueType>::getElementState(size_t id) const {
return static_cast<DFTElementState>(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 <sstream>
#include <memory>
@@ -31,7 +32,7 @@ namespace storm {
bool mValid = true;
const DFT<ValueType>& mDft;
const DFTStateGenerationInfo& mStateGenerationInfo;
- bool mSkip = false;
+ storm::builder::DFTExplorationHeuristic<ValueType> exploreHeuristic;
public:
DFTState(DFT<ValueType> 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<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id);
-
+
+ std::shared_ptr<DFTState<ValueType>> 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<storm::storage::DFTState<ValueType>> 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 {