Compute lower/upper bounds only when needed

Former-commit-id: 8f3af1ab10

src/builder/DftExplorationHeuristic.cpp

@@ -8,12 +8,12 @@ namespace storm {
     namespace builder {
 
         template<typename ValueType>
-        DFTExplorationHeuristic<ValueType>::DFTExplorationHeuristic(size_t id) : id(id), expand(false), lowerBound(storm::utility::zero<ValueType>()), upperBound(storm::utility::infinity<ValueType>()), depth(0), probability(storm::utility::one<ValueType>()) {
+        DFTExplorationHeuristic<ValueType>::DFTExplorationHeuristic(size_t id) : id(id), expand(true), lowerBound(storm::utility::zero<ValueType>()), upperBound(storm::utility::infinity<ValueType>()), depth(0), probability(storm::utility::one<ValueType>()) {
             // Intentionally left empty
         }
 
         template<typename ValueType>
-        DFTExplorationHeuristic<ValueType>::DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : id(id), expand(false), lowerBound(lowerBound), upperBound(upperBound), depth(predecessor.depth + 1) {
+        DFTExplorationHeuristic<ValueType>::DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) : id(id), expand(false), lowerBound(storm::utility::zero<ValueType>()), upperBound(storm::utility::zero<ValueType>()), depth(predecessor.depth + 1) {
             STORM_LOG_ASSERT(storm::utility::zero<ValueType>() < exitRate, "Exit rate is 0");
             probability = predecessor.probability * rate/exitRate;
         }

src/builder/DftExplorationHeuristic.h

@@ -22,7 +22,7 @@ namespace storm {
         public:
             DFTExplorationHeuristic(size_t id);
 
-            DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound);
+            DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate);
 
             void setBounds(ValueType lowerBound, ValueType upperBound);
 
@@ -76,7 +76,7 @@ namespace storm {
                 // Intentionally left empty
             }
 
-            DFTExplorationHeuristicNone(size_t id, DFTExplorationHeuristicNone<ValueType> const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : DFTExplorationHeuristic<ValueType>(id, predecessor, rate, exitRate, lowerBound, upperBound) {
+            DFTExplorationHeuristicNone(size_t id, DFTExplorationHeuristicNone<ValueType> const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic<ValueType>(id, predecessor, rate, exitRate) {
                 // Intentionally left empty
             }
 
@@ -85,7 +85,7 @@ namespace storm {
             }
 
             double getPriority() const override {
-                return this->id;
+                return 0;
             }
 
             bool isSkip(double approximationThreshold) const override {
@@ -104,7 +104,7 @@ namespace storm {
                 // Intentionally left empty
             }
 
-            DFTExplorationHeuristicDepth(size_t id, DFTExplorationHeuristicDepth<ValueType> const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : DFTExplorationHeuristic<ValueType>(id, predecessor, rate, exitRate, lowerBound, upperBound) {
+            DFTExplorationHeuristicDepth(size_t id, DFTExplorationHeuristicDepth<ValueType> const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic<ValueType>(id, predecessor, rate, exitRate) {
                 // Intentionally left empty
             }
 
@@ -137,7 +137,7 @@ namespace storm {
                 // Intentionally left empty
             }
 
-            DFTExplorationHeuristicProbability(size_t id, DFTExplorationHeuristicProbability<ValueType> const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : DFTExplorationHeuristic<ValueType>(id, predecessor, rate, exitRate, lowerBound, upperBound) {
+            DFTExplorationHeuristicProbability(size_t id, DFTExplorationHeuristicProbability<ValueType> const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic<ValueType>(id, predecessor, rate, exitRate) {
                 // Intentionally left empty
             }
 
@@ -161,7 +161,7 @@ namespace storm {
                 // Intentionally left empty
             }
 
-            DFTExplorationHeuristicBoundDifference(size_t id, DFTExplorationHeuristicBoundDifference<ValueType> const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : DFTExplorationHeuristic<ValueType>(id, predecessor, rate, exitRate, lowerBound, upperBound) {
+            DFTExplorationHeuristicBoundDifference(size_t id, DFTExplorationHeuristicBoundDifference<ValueType> const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic<ValueType>(id, predecessor, rate, exitRate) {
                 // Intentionally left empty
             }
 

src/builder/ExplicitDFTModelBuilderApprox.cpp

@@ -255,9 +255,6 @@ namespace storm {
                 if (currentState->isPseudoState()) {
                     // Create concrete state from pseudo state
                     currentState->construct();
-                    ValueType lowerBound = getLowerBound(currentState);
-                    ValueType upperBound = getUpperBound(currentState);
-                    currentExplorationHeuristic->setBounds(lowerBound, upperBound);
                 }
                 STORM_LOG_ASSERT(!currentState->isPseudoState(), "State is pseudo state.");
 
@@ -301,17 +298,8 @@ namespace storm {
                                 // Update heuristic values
                                 DFTStatePointer state = iter->second.first;
                                 if (!iter->second.second) {
-                                    ValueType lowerBound;
-                                    ValueType upperBound;
-                                    if (state->isPseudoState()) {
-                                        lowerBound = storm::utility::infinity<ValueType>();
-                                        upperBound = storm::utility::infinity<ValueType>();
-                                    } else {
-                                        lowerBound = getLowerBound(state);
-                                        upperBound = getUpperBound(state);
-                                    }
                                     // Initialize heuristic values
-                                    ExplorationHeuristicPointer heuristic = std::make_shared<ExplorationHeuristic>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass(), lowerBound, upperBound);
+                                    ExplorationHeuristicPointer heuristic = std::make_shared<ExplorationHeuristic>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass());
                                     iter->second.second = heuristic;
                                     if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->nrFailableDependencies() > 0 || (state->nrFailableDependencies() == 0 && state->nrFailableBEs() == 0)) {
                                         // Do not skip absorbing state or if reached by dependencies
@@ -453,6 +441,16 @@ namespace storm {
                 auto matrixEntry = matrix.getRow(it->first, 0).begin();
                 STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state.");
                 STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state.");
+
+                ExplorationHeuristicPointer heuristic = it->second.second;
+                if (storm::utility::isZero(heuristic->getUpperBound())) {
+                    // Initialize bounds
+                    ValueType lowerBound = getLowerBound(it->second.first);
+                    ValueType upperBound = getUpperBound(it->second.first);
+                    heuristic->setBounds(lowerBound, upperBound);
+                }
+
+                // Change bound
                 if (lowerBound) {
                     matrixEntry->setValue(it->second.second->getLowerBound());
                 } else {
@@ -489,6 +487,7 @@ namespace storm {
             for (size_t index = 0; index < state->nrNotFailableBEs(); ++index) {
                 rates[index + state->nrFailableBEs()] = state->getNotFailableBERate(index);
             }
+            STORM_LOG_ASSERT(rates.size() > 0, "State is absorbing");
 
             // TODO Matthias: works only for <64 BEs!
             for (size_t i = 1; i < 4 && i <= rates.size(); ++i) {