sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Make exploration heuristic choosable

main
Matthias Volk 7 years ago
parent
3dd0bffef9
commit
970430a6fb
2 changed files with 34 additions and 11 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 40
      src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
  2. 5
      src/storm-dft/builder/ExplicitDFTModelBuilder.h

40
src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
View File

@ -60,14 +60,9 @@ namespace storm {
generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates),
matrixBuilder(!generator.isDeterministicModel()),
stateStorage(dft.stateBitVectorSize()),
// TODO Matthias: make choosable
//explorationQueue(dft.nrElements()+1, 0, 1)
explorationQueue(200, 0, 0.9, false)
{
// Intentionally left empty.
// TODO Matthias: remove again
usedHeuristic = storm::builder::ApproximationHeuristic::DEPTH;
// Compute independent subtrees
if (dft.topLevelType() == storm::storage::DFTElementType::OR) {
// We only support this for approximation with top level element OR
@ -163,7 +158,21 @@ namespace storm {
STORM_LOG_TRACE("Initial state: " << initialStateIndex);
// Initialize heuristic values for inital state
STORM_LOG_ASSERT(!statesNotExplored.at(initialStateIndex).second, "Heuristic for initial state is already initialized");
ExplorationHeuristicPointer heuristic = std::make_shared<ExplorationHeuristic>(initialStateIndex);
ExplorationHeuristicPointer heuristic;
switch (usedHeuristic) {
case storm::builder::ApproximationHeuristic::NONE:
heuristic = std::make_shared<DFTExplorationHeuristicNone<ValueType>>(initialStateIndex);
break;
case storm::builder::ApproximationHeuristic::DEPTH:
heuristic = std::make_shared<DFTExplorationHeuristicDepth<ValueType>>(initialStateIndex);
break;
case storm::builder::ApproximationHeuristic::PROBABILITY:
heuristic = std::make_shared<DFTExplorationHeuristicProbability<ValueType>>(initialStateIndex);
break;
case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE:
heuristic = std::make_shared<DFTExplorationHeuristicBoundDifference<ValueType>>(initialStateIndex);
break;
}
heuristic->markExpand();
statesNotExplored[initialStateIndex].second = heuristic;
explorationQueue.push(heuristic);
@ -171,7 +180,7 @@ namespace storm {
initializeNextIteration();
}
if (approximationThreshold > 0) {
if (approximationThreshold > 0.0) {
switch (usedHeuristic) {
case storm::builder::ApproximationHeuristic::NONE:
// Do not change anything
@ -385,7 +394,22 @@ namespace storm {
DFTStatePointer state = iter->second.first;
if (!iter->second.second) {
// Initialize heuristic values
ExplorationHeuristicPointer heuristic = std::make_shared<ExplorationHeuristic>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass());
ExplorationHeuristicPointer heuristic;
switch (usedHeuristic) {
case storm::builder::ApproximationHeuristic::NONE:
heuristic = std::make_shared<DFTExplorationHeuristicNone<ValueType>>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass());
break;
case storm::builder::ApproximationHeuristic::DEPTH:
heuristic = std::make_shared<DFTExplorationHeuristicDepth<ValueType>>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass());
break;
case storm::builder::ApproximationHeuristic::PROBABILITY:
heuristic = std::make_shared<DFTExplorationHeuristicProbability<ValueType>>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass());
break;
case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE:
heuristic = std::make_shared<DFTExplorationHeuristicBoundDifference<ValueType>>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass());
break;
}
iter->second.second = heuristic;
if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->getFailableElements().hasDependencies() || (!state->getFailableElements().hasDependencies() && state->getFailableElements().hasBEs())) {
// Do not skip absorbing state or if reached by dependencies

5
src/storm-dft/builder/ExplicitDFTModelBuilder.h
View File

@ -29,8 +29,7 @@ namespace storm {
class ExplicitDFTModelBuilder {
using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>;
// TODO Matthias: make choosable
using ExplorationHeuristic = DFTExplorationHeuristicDepth<ValueType>;
using ExplorationHeuristic = DFTExplorationHeuristic<ValueType>;
using ExplorationHeuristicPointer = std::shared_ptr<ExplorationHeuristic>;
@ -343,7 +342,7 @@ namespace storm {
storm::storage::sparse::StateStorage<StateType> stateStorage;
// A priority queue of states that still need to be explored.
storm::storage::BucketPriorityQueue<ValueType> explorationQueue;
storm::storage::BucketPriorityQueue<ExplorationHeuristic> explorationQueue;
// A mapping of not yet explored states from the id to the tuple (state object, heuristic values).
std::map<StateType, std::pair<DFTStatePointer, ExplorationHeuristicPointer>> statesNotExplored;

Write Preview
Loading…
Cancel
Save