Browse Source

Use Heuristic None

Former-commit-id: 63f78f3db0
tempestpy_adaptions
Mavo 8 years ago
parent
commit
0d9cdd6ef8
  1. 7
      src/builder/ExplicitDFTModelBuilderApprox.cpp

7
src/builder/ExplicitDFTModelBuilderApprox.cpp

@ -33,11 +33,11 @@ namespace storm {
stateStorage(((dft.stateVectorSize() / 64) + 1) * 64), stateStorage(((dft.stateVectorSize() / 64) + 1) * 64),
// TODO Matthias: make choosable // TODO Matthias: make choosable
explorationQueue(dft.nrElements()+1, 0, 1) explorationQueue(dft.nrElements()+1, 0, 1)
//explorationQueue(141, 0, 0.02)
//explorationQueue(1001, 0, 0.001)
{ {
// Intentionally left empty. // Intentionally left empty.
// TODO Matthias: remove again // TODO Matthias: remove again
heuristic = storm::builder::ApproximationHeuristic::PROBABILITY;
heuristic = storm::builder::ApproximationHeuristic::NONE;
} }
template<typename ValueType, typename StateType> template<typename ValueType, typename StateType>
@ -97,7 +97,7 @@ namespace storm {
break; break;
case storm::builder::ApproximationHeuristic::PROBABILITY: case storm::builder::ApproximationHeuristic::PROBABILITY:
//approximationThreshold = std::pow(0.1, iteration) * approximationThreshold; //approximationThreshold = std::pow(0.1, iteration) * approximationThreshold;
approximationThreshold = 10 * std::pow(2, iteration);
approximationThreshold = iteration;//10 * std::pow(2, iteration);
break; break;
} }
exploreStateSpace(approximationThreshold); exploreStateSpace(approximationThreshold);
@ -267,6 +267,7 @@ namespace storm {
// Try to explore the next state // Try to explore the next state
generator.load(currentState); generator.load(currentState);
//if (nrExpandedStates > approximationThreshold) {
if (currentExplorationHeuristic->isSkip(approximationThreshold)) { if (currentExplorationHeuristic->isSkip(approximationThreshold)) {
// Skip the current state // Skip the current state
++nrSkippedStates; ++nrSkippedStates;

Loading…
Cancel
Save