Added storm-pars linker dependency to storm-dft and improved DftInsta…

…ntiator (#642)
moves-rwth · Jan 7, 2025 · 5823e1a · 5823e1a
2 parents ff357d3 + 4355a1a
commit 5823e1a
Show file tree

Hide file tree

Showing 3 changed files with 46 additions and 6 deletions.
diff --git a/src/storm-dft/CMakeLists.txt b/src/storm-dft/CMakeLists.txt
@@ -15,7 +15,7 @@ set_target_properties(storm-dft PROPERTIES DEFINE_SYMBOL "")
 list(APPEND STORM_TARGETS storm-dft)
 set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
 
-target_link_libraries(storm-dft PUBLIC storm storm-gspn storm-conv storm-parsers ${STORM_DFT_LINK_LIBRARIES})
+target_link_libraries(storm-dft PUBLIC storm storm-gspn storm-conv storm-parsers storm-pars ${STORM_DFT_LINK_LIBRARIES})
 
 # Install storm headers to include directory.
 foreach(HEADER ${STORM_DFT_HEADERS})

diff --git a/src/storm-dft/transformations/DftInstantiator.cpp b/src/storm-dft/transformations/DftInstantiator.cpp
@@ -24,19 +24,47 @@ std::shared_ptr<storm::dft::storage::DFT<ConstantType>> DftInstantiator<Parametr
                         builder.addBasicElementConst(beConst->name(), beConst->canFail());
                         break;
                     }
+                    case storm::dft::storage::elements::BEType::PROBABILITY: {
+                        auto beProb = std::static_pointer_cast<storm::dft::storage::elements::BEProbability<ParametricType> const>(element);
+                        ConstantType activeFailureProbability = instantiate_helper(beProb->activeFailureProbability(), valuation);
+                        ConstantType dormancyFactor = instantiate_helper(beProb->dormancyFactor(), valuation);
+                        builder.addBasicElementProbability(beProb->name(), activeFailureProbability, dormancyFactor);
+                        break;
+                    }
                     case storm::dft::storage::elements::BEType::EXPONENTIAL: {
                         auto beExp = std::static_pointer_cast<storm::dft::storage::elements::BEExponential<ParametricType> const>(element);
-                        ConstantType activeFailureRate = storm::utility::convertNumber<ConstantType>(beExp->activeFailureRate().evaluate(valuation));
-                        ConstantType dormancyFactor = storm::utility::convertNumber<ConstantType>(beExp->dormancyFactor().evaluate(valuation));
+                        ConstantType activeFailureRate = instantiate_helper(beExp->activeFailureRate(), valuation);
+                        ConstantType dormancyFactor = instantiate_helper(beExp->dormancyFactor(), valuation);
                         builder.addBasicElementExponential(beExp->name(), activeFailureRate, dormancyFactor, beExp->isTransient());
                         break;
                     }
+                    case storm::dft::storage::elements::BEType::ERLANG: {
+                        auto beErlang = std::static_pointer_cast<storm::dft::storage::elements::BEErlang<ParametricType> const>(element);
+                        ConstantType activeFailureRate = instantiate_helper(beErlang->activeFailureRate(), valuation);
+                        ConstantType dormancyFactor = instantiate_helper(beErlang->dormancyFactor(), valuation);
+                        builder.addBasicElementErlang(beErlang->name(), activeFailureRate, beErlang->phases(), dormancyFactor);
+                        break;
+                    }
+                    case storm::dft::storage::elements::BEType::WEIBULL: {
+                        auto beWeibull = std::static_pointer_cast<storm::dft::storage::elements::BEWeibull<ParametricType> const>(element);
+                        ConstantType shape = instantiate_helper(beWeibull->shape(), valuation);
+                        ConstantType rate = instantiate_helper(beWeibull->rate(), valuation);
+                        builder.addBasicElementWeibull(beWeibull->name(), shape, rate);
+                        break;
+                    }
+                    case storm::dft::storage::elements::BEType::LOGNORMAL: {
+                        auto beLogNormal = std::static_pointer_cast<storm::dft::storage::elements::BELogNormal<ParametricType> const>(element);
+                        ConstantType mean = instantiate_helper(beLogNormal->mean(), valuation);
+                        ConstantType stddev = instantiate_helper(beLogNormal->standardDeviation(), valuation);
+                        builder.addBasicElementLogNormal(beLogNormal->name(), mean, stddev);
+                        break;
+                    }
                     case storm::dft::storage::elements::BEType::SAMPLES: {
                         auto beSamples = std::static_pointer_cast<storm::dft::storage::elements::BESamples<ParametricType> const>(element);
                         std::map<ConstantType, ConstantType> activeSamples{};
                         for (auto &[time, prob] : beSamples->activeSamples()) {
-                            ConstantType timeInst = storm::utility::convertNumber<ConstantType>(time.evaluate(valuation));
-                            ConstantType probInst = storm::utility::convertNumber<ConstantType>(prob.evaluate(valuation));
+                            ConstantType timeInst = instantiate_helper(time, valuation);
+                            ConstantType probInst = instantiate_helper(prob, valuation);
                             activeSamples[timeInst] = probInst;
                         }
                         builder.addBasicElementSamples(beSamples->name(), activeSamples);
@@ -82,7 +110,7 @@ std::shared_ptr<storm::dft::storage::DFT<ConstantType>> DftInstantiator<Parametr
             case storm::dft::storage::elements::DFTElementType::PDEP: {
                 auto dependency = std::static_pointer_cast<storm::dft::storage::elements::DFTDependency<ParametricType> const>(element);
                 // Instantiate probability
-                ConstantType probability = storm::utility::convertNumber<ConstantType>(dependency->probability().evaluate(valuation));
+                ConstantType probability = instantiate_helper(dependency->probability(), valuation);
                 std::vector<std::string> children = {dependency->triggerEvent()->name()};
                 for (auto const &depEvent : dependency->dependentEvents()) {
                     children.push_back(depEvent->name());

diff --git a/src/storm-dft/transformations/DftInstantiator.h b/src/storm-dft/transformations/DftInstantiator.h
@@ -39,6 +39,18 @@ class DftInstantiator {
    private:
     storm::dft::storage::DFT<ParametricType> const& dft;
 
+    template<typename PT = ParametricType>
+    typename std::enable_if<std::is_same<PT, ConstantType>::value, ConstantType>::type instantiate_helper(
+        ParametricType const& function, storm::utility::parametric::Valuation<ParametricType> const& valuation) {
+        return storm::utility::parametric::substitute(function, valuation);
+    }
+
+    template<typename PT = ParametricType>
+    typename std::enable_if<!std::is_same<PT, ConstantType>::value, ConstantType>::type instantiate_helper(
+        ParametricType const& function, storm::utility::parametric::Valuation<ParametricType> const& valuation) {
+        return storm::utility::convertNumber<ConstantType>(storm::utility::parametric::evaluate(function, valuation));
+    }
+
     /*!
      * Get list of children names.
      * @param element DFT element.