Renamed rateratio to probability

Former-commit-id: 6d07985b1d

src/builder/DftExplorationHeuristic.cpp

@@ -8,31 +8,36 @@ namespace storm {
     namespace builder {
 
         template<typename ValueType>
-        DFTExplorationHeuristic<ValueType>::DFTExplorationHeuristic(size_t id, size_t depth, ValueType rate, ValueType exitRate) : id(id), expand(false), depth(depth) {
+        DFTExplorationHeuristic<ValueType>::DFTExplorationHeuristic(size_t id) : id(id), expand(false), depth(0), probability(storm::utility::zero<ValueType>()) {
+            // Intentionally left empty
+        }
+
+        template<typename ValueType>
+        DFTExplorationHeuristic<ValueType>::DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) : id(id), expand(false), depth(predecessor.depth + 1) {
             STORM_LOG_ASSERT(storm::utility::zero<ValueType>() < exitRate, "Exit rate is 0");
-            rateRatio = rate/exitRate;
+            probability = predecessor.probability * rate/exitRate;
         }
 
         template<>
-        bool DFTExplorationHeuristicRateRatio<double>::updateHeuristicValues(size_t depth, double rate, double exitRate) {
+        bool DFTExplorationHeuristicProbability<double>::updateHeuristicValues(DFTExplorationHeuristic<double> const& predecessor, double rate, double exitRate) {
             STORM_LOG_ASSERT(exitRate > 0, "Exit rate is 0");
-            rateRatio += rate/exitRate;
+            probability += predecessor.getProbability() * rate/exitRate;
             return true;
         }
 
         template<>
-        bool DFTExplorationHeuristicRateRatio<storm::RationalFunction>::updateHeuristicValues(size_t depth, storm::RationalFunction rate, storm::RationalFunction exitRate) {
+        bool DFTExplorationHeuristicProbability<storm::RationalFunction>::updateHeuristicValues(DFTExplorationHeuristic<storm::RationalFunction> const& predecessor, storm::RationalFunction rate, storm::RationalFunction exitRate) {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work for rational functions.");
             return false;
         }
 
         template<>
-        double DFTExplorationHeuristicRateRatio<double>::getPriority() const {
+        double DFTExplorationHeuristicProbability<double>::getPriority() const {
-            return rateRatio;
+            return probability;
         }
 
         template<>
-        double DFTExplorationHeuristicRateRatio<storm::RationalFunction>::getPriority() const {
+        double DFTExplorationHeuristicProbability<storm::RationalFunction>::getPriority() const {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work for rational functions.");
         }
 
@@ -41,13 +46,13 @@ namespace storm {
         template class DFTExplorationHeuristic<double>;
         template class DFTExplorationHeuristicNone<double>;
         template class DFTExplorationHeuristicDepth<double>;
-        template class DFTExplorationHeuristicRateRatio<double>;
+        template class DFTExplorationHeuristicProbability<double>;
 
 #ifdef STORM_HAVE_CARL
         template class DFTExplorationHeuristic<storm::RationalFunction>;
         template class DFTExplorationHeuristicNone<storm::RationalFunction>;
         template class DFTExplorationHeuristicDepth<storm::RationalFunction>;
-        template class DFTExplorationHeuristicRateRatio<storm::RationalFunction>;
+        template class DFTExplorationHeuristicProbability<storm::RationalFunction>;
 #endif
     }
 }

src/builder/DftExplorationHeuristic.h

@@ -10,7 +10,7 @@ namespace storm {
         /*!
          * Enum representing the heuristic used for deciding which states to expand.
          */
-        enum class ApproximationHeuristic { NONE, DEPTH, RATERATIO };
+        enum class ApproximationHeuristic { NONE, DEPTH, PROBABILITY };
 
 
         /*!
@@ -20,9 +20,11 @@ namespace storm {
         class DFTExplorationHeuristic {
 
         public:
-            DFTExplorationHeuristic(size_t id, size_t depth, ValueType rate, ValueType exitRate);
+            DFTExplorationHeuristic(size_t id);
 
-            virtual bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) = 0;
+            DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate);
+
+            virtual bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) = 0;
 
             virtual double getPriority() const = 0;
 
@@ -40,21 +42,29 @@ namespace storm {
                 return depth;
             }
 
+            ValueType getProbability() const {
+                return probability;
+            }
+
         protected:
             size_t id;
             bool expand;
             size_t depth;
-            ValueType rateRatio;
+            ValueType probability;
         };
 
         template<typename ValueType>
         class DFTExplorationHeuristicNone : public DFTExplorationHeuristic<ValueType> {
         public:
-            DFTExplorationHeuristicNone(size_t id, size_t depth, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic<ValueType>(id, depth, rate, exitRate) {
+            DFTExplorationHeuristicNone(size_t id) : DFTExplorationHeuristic<ValueType>(id) {
+                // Intentionally left empty
+            }
+
+            DFTExplorationHeuristicNone(size_t id, DFTExplorationHeuristicNone<ValueType> const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic<ValueType>(id, predecessor, rate, exitRate) {
                 // Intentionally left empty
             }
 
-            bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) override {
+            bool updateHeuristicValues(DFTExplorationHeuristic<ValueType> const& predecessor, ValueType rate, ValueType exitRate) override {
                 return false;
             }
 
@@ -74,13 +84,17 @@ namespace storm {
         template<typename ValueType>
         class DFTExplorationHeuristicDepth : public DFTExplorationHeuristic<ValueType> {
         public:
-            DFTExplorationHeuristicDepth(size_t id, size_t depth, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic<ValueType>(id, depth, rate, exitRate) {
+            DFTExplorationHeuristicDepth(size_t id) : DFTExplorationHeuristic<ValueType>(id) {
                 // Intentionally left empty
             }
 
-            bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) override {
+            DFTExplorationHeuristicDepth(size_t id, DFTExplorationHeuristicDepth<ValueType> const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic<ValueType>(id, predecessor, rate, exitRate) {
-                if (depth < this->depth) {
+                // Intentionally left empty
-                    this->depth = depth;
+            }
+
+            bool updateHeuristicValues(DFTExplorationHeuristic<ValueType> const& predecessor, ValueType rate, ValueType exitRate) override {
+                if (predecessor.getDepth() < this->depth) {
+                    this->depth = predecessor.getDepth();
                     return true;
                 }
                 return false;
@@ -101,13 +115,17 @@ namespace storm {
         };
 
         template<typename ValueType>
-        class DFTExplorationHeuristicRateRatio : public DFTExplorationHeuristic<ValueType> {
+        class DFTExplorationHeuristicProbability : public DFTExplorationHeuristic<ValueType> {
         public:
-            DFTExplorationHeuristicRateRatio(size_t id, size_t depth, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic<ValueType>(id, depth, rate, exitRate) {
+            DFTExplorationHeuristicProbability(size_t id) : DFTExplorationHeuristic<ValueType>(id) {
+                // Intentionally left empty
+            }
+
+            DFTExplorationHeuristicProbability(size_t id, DFTExplorationHeuristicProbability<ValueType> const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic<ValueType>(id, predecessor, rate, exitRate) {
                 // Intentionally left empty
             }
 
-            bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) override;
+            bool updateHeuristicValues(DFTExplorationHeuristic<ValueType> const& predecessor, ValueType rate, ValueType exitRate) override;
 
             double getPriority() const override;
 
@@ -115,7 +133,7 @@ namespace storm {
                 return !this->expand && this->getPriority() < approximationThreshold;
             }
 
-            bool operator<(DFTExplorationHeuristicRateRatio<ValueType> const& other) const {
+            bool operator<(DFTExplorationHeuristicProbability<ValueType> const& other) const {
                 return this->getPriority() < other.getPriority();
             }
         };

src/builder/ExplicitDFTModelBuilderApprox.cpp

@@ -37,7 +37,7 @@ namespace storm {
         {
             // Intentionally left empty.
             // TODO Matthias: remove again
-            heuristic = storm::builder::ApproximationHeuristic::NONE;
+            heuristic = storm::builder::ApproximationHeuristic::PROBABILITY;
         }
 
         template<typename ValueType, typename StateType>
@@ -79,7 +79,7 @@ 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, 0, storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
+                ExplorationHeuristicPointer heuristic = std::make_shared<ExplorationHeuristic>(initialStateIndex);
                 heuristic->markExpand();
                 statesNotExplored[initialStateIndex].second = heuristic;
                 explorationQueue.push(heuristic);
@@ -95,8 +95,9 @@ namespace storm {
                 case storm::builder::ApproximationHeuristic::DEPTH:
                     approximationThreshold = iteration;
                     break;
-                case storm::builder::ApproximationHeuristic::RATERATIO:
+                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);
                     break;
             }
             exploreStateSpace(approximationThreshold);
@@ -298,12 +299,12 @@ namespace storm {
                                 DFTStatePointer state = iter->second.first;
                                 if (!iter->second.second) {
                                     // Initialize heuristic values
-                                    ExplorationHeuristicPointer heuristic = std::make_shared<ExplorationHeuristic>(stateProbabilityPair.first, currentExplorationHeuristic->getDepth() + 1, stateProbabilityPair.second, choice.getTotalMass());
+                                    ExplorationHeuristicPointer heuristic = std::make_shared<ExplorationHeuristic>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass());
                                     iter->second.second = heuristic;
                                     explorationQueue.push(heuristic);
                                 } else {
                                     double oldPriority = iter->second.second->getPriority();
-                                    if (iter->second.second->updateHeuristicValues(currentExplorationHeuristic->getDepth() + 1, stateProbabilityPair.second, choice.getTotalMass())) {
+                                    if (iter->second.second->updateHeuristicValues(*currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass())) {
                                         // Update priority queue
                                         ++fix;
                                         explorationQueue.update(iter->second.second, oldPriority);

src/settings/modules/DFTSettings.cpp

@@ -40,7 +40,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleGreaterValidatorIncluding(0.0)).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, rateratio}. Default is").setDefaultValueString("depth").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator({"depth", "rateratio"})).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator({"depth", "rateratio"})).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, propTimeBoundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleGreaterValidatorExcluding(0.0)).build()).build());
@@ -87,8 +87,8 @@ namespace storm {
                 std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString();
                 if (heuristicAsString == "depth") {
                     return storm::builder::ApproximationHeuristic::DEPTH;
-                } else if (heuristicAsString == "rateratio") {
+                } else if (heuristicAsString == "probability") {
-                    return storm::builder::ApproximationHeuristic::RATERATIO;
+                    return storm::builder::ApproximationHeuristic::PROBABILITY;
                 }
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation.");
             }