From c4260d3d5af37dba8ec9dc9a9a38e48aa3bb38fc Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Wed, 18 May 2016 16:29:28 +0200
Subject: [PATCH] First try on approximation

Former-commit-id: 53c6738c729bb143e04d31876c17b9b5873cccd4
---
 src/builder/ExplicitDFTModelBuilder.cpp | 42 +++++++++++++++++++++++++
 src/builder/ExplicitDFTModelBuilder.h   |  3 ++
 2 files changed, 45 insertions(+)

diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp
index 4fb6131df..7cf1488be 100644
--- a/src/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/builder/ExplicitDFTModelBuilder.cpp
@@ -4,6 +4,8 @@
 #include <src/utility/constants.h>
 #include <src/utility/vector.h>
 #include <src/exceptions/UnexpectedException.h>
+#include "src/settings/modules/DebugSettings.h"
+#include "src/settings/SettingsManager.h"
 #include <map>
 
 namespace storm {
@@ -157,7 +159,24 @@ namespace storm {
             
             return model;
         }
+        
+        template<>
+        bool belowThreshold(double const& number) {
+            return number < 0.1;
+        }
+
+        template<>
+        bool belowThreshold(storm::RationalFunction const& number) {
+            storm::RationalFunction threshold = storm::utility::one<storm::RationalFunction>() / 10;
+            std::cout << number << " < " << threshold << ": " << (number < threshold) << std::endl;
+            std::map<storm::Variable, storm::RationalNumber> mapping;
+            
+            storm::RationalFunction eval(number.evaluate(mapping));
+            std::cout << "Evaluated: " << eval << std::endl;
+            return eval < threshold;
+        }
 
+        
         template <typename ValueType>
         std::pair<uint_fast64_t, bool> ExplicitDFTModelBuilder<ValueType>::exploreStates(DFTStatePointer const& state, size_t& rowOffset, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<uint_fast64_t>& markovianStates, std::vector<ValueType>& exitRates) {
             STORM_LOG_TRACE("Explore state: " << mDft.getStateString(state));
@@ -206,6 +225,29 @@ namespace storm {
                 STORM_LOG_ASSERT(nextBE, "NextBE is null.");
                 STORM_LOG_ASSERT(nextBEPair.second == hasDependencies, "Failure due to dependencies does not match.");
                 STORM_LOG_TRACE("With the failure of: " << nextBE->name() << " [" << nextBE->id() << "] in " << mDft.getStateString(state));
+                
+                if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isTestSet()) {
+                    if (!storm::utility::isZero(exitRate)) {
+                    ValueType rate = nextBE->activeFailureRate();
+                    ValueType div = rate / exitRate;
+                    if (!storm::utility::isZero(exitRate) && belowThreshold(div)) {
+                        // Set transition directly to failed state
+                        auto resultFind = outgoingRates.find(failedIndex);
+                        if (resultFind != outgoingRates.end()) {
+                            // Add to existing transition
+                            resultFind->second += rate;
+                            STORM_LOG_TRACE("Updated transition to " << resultFind->first << " with rate " << rate << " to new rate " << resultFind->second);
+                        } else {
+                            // Insert new transition
+                            outgoingRates.insert(std::make_pair(failedIndex, rate));
+                            STORM_LOG_TRACE("Added transition to " << failedIndex << " with rate " << rate);
+                        }
+                        exitRate += rate;
+                        std::cout << "IGNORE: " << nextBE->name() << " [" << nextBE->id() << "] with rate " << rate << std::endl;
+                        //STORM_LOG_TRACE("Ignore: " << nextBE->name() << " [" << nextBE->id() << "] with rate " << rate);
+                        continue;
+                    }}
+                }
 
                 // Propagate failures
                 storm::storage::DFTStateSpaceGenerationQueues<ValueType> queues;
diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h
index 3e78180d1..71bfada61 100644
--- a/src/builder/ExplicitDFTModelBuilder.h
+++ b/src/builder/ExplicitDFTModelBuilder.h
@@ -91,6 +91,9 @@ namespace storm {
             std::pair<bool, uint_fast64_t> checkForExploration(DFTStatePointer const& state);
 
         };
+        
+        template<typename ValueType>
+        bool belowThreshold(ValueType const& number);
     }
 }