Several improvements

Former-commit-id: 047ebde33b

src/builder/ExplicitDFTModelBuilderApprox.cpp

@@ -34,7 +34,7 @@ namespace storm {
                 stateStorage(((dft.stateVectorSize() / 64) + 1) * 64),
                 // TODO Matthias: make choosable
                 //explorationQueue(dft.nrElements()+1, 0, 1)
-                explorationQueue(1001, 0, 0.001)
+                explorationQueue(200, 0, 0.9)
         {
             // Intentionally left empty.
             // TODO Matthias: remove again
@@ -291,9 +291,6 @@ namespace storm {
             size_t nrSkippedStates = 0;
             // TODO Matthias: do not empty queue every time but break before
             while (!explorationQueue.empty()) {
-                explorationQueue.fix();
-                //explorationQueue.print(std::cout);
-                //printNotExplored();
                 // Get the first state in the queue
                 ExplorationHeuristicPointer currentExplorationHeuristic = explorationQueue.popTop();
                 StateType currentId = currentExplorationHeuristic->getId();
@@ -602,17 +599,18 @@ namespace storm {
             }*/
 
             // Compute result with permutations of size <= 3
+            ValueType one = storm::utility::one<ValueType>();
             for (size_t i1 = 0; i1 < size; ++i1) {
                 // + 1/a
                 ValueType sum = rates[i1];
-                result += storm::utility::one<ValueType>() / sum;
+                result += one / sum;
                 for (size_t i2 = 0; i2 < i1; ++i2) {
                     // - 1/(a+b)
                     ValueType sum2 = sum + rates[i2];
-                    result -= storm::utility::one<ValueType>() / sum2;
+                    result -= one / sum2;
                     for (size_t i3 = 0; i3 < i2; ++i3) {
                         // + 1/(a+b+c)
-                        result += storm::utility::one<ValueType>() / (sum2 + rates[i3]);
+                        result += one / (sum2 + rates[i3]);
                     }
                 }
             }

src/modelchecker/dft/DFTModelChecker.cpp

@@ -17,13 +17,13 @@ namespace storm {
         template<typename ValueType>
         void DFTModelChecker<ValueType>::check(storm::storage::DFT<ValueType> const& origDft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool allowModularisation, bool enableDC, double approximationError) {
             // Initialize
-            this->buildingTime = std::chrono::duration<double>::zero();
             this->explorationTime = std::chrono::duration<double>::zero();
+            this->buildingTime = std::chrono::duration<double>::zero();
             this->bisimulationTime = std::chrono::duration<double>::zero();
             this->modelCheckingTime = std::chrono::duration<double>::zero();
             this->totalTime = std::chrono::duration<double>::zero();
             this->approximationError = approximationError;
-            std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
+            totalStart = std::chrono::high_resolution_clock::now();
 
             // Optimizing DFT
             storm::storage::DFT<ValueType> dft = origDft.optimize();
@@ -134,7 +134,7 @@ namespace storm {
 
         template<typename ValueType>
         typename DFTModelChecker<ValueType>::dft_result DFTModelChecker<ValueType>::checkDFT(storm::storage::DFT<ValueType> const& dft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool enableDC, double approximationError) {
-            std::chrono::high_resolution_clock::time_point buildingStart = std::chrono::high_resolution_clock::now();
+            std::chrono::high_resolution_clock::time_point checkingStart = std::chrono::high_resolution_clock::now();
 
             // Find symmetries
             std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
@@ -145,15 +145,12 @@ namespace storm {
                 STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries.");
                 STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries);
             }
-            std::chrono::high_resolution_clock::time_point buildingEnd = std::chrono::high_resolution_clock::now();
-            buildingTime += buildingEnd - buildingStart;
 
             if (approximationError > 0.0) {
                 // Comparator for checking the error of the approximation
                 storm::utility::ConstantsComparator<ValueType> comparator;
                 // Build approximate Markov Automata for lower and upper bound
                 approximation_result approxResult = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
-                std::chrono::high_resolution_clock::time_point explorationStart;
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
                 storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
                 typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
@@ -163,10 +160,12 @@ namespace storm {
                 size_t iteration = 0;
                 do {
                     // Iteratively build finer models
-                    explorationStart = std::chrono::high_resolution_clock::now();
+                    std::chrono::high_resolution_clock::time_point explorationStart = std::chrono::high_resolution_clock::now();
                     STORM_LOG_INFO("Building model...");
                     // TODO Matthias refine model using existing model and MC results
                     builder.buildModel(labeloptions, iteration, approximationError);
+                    std::chrono::high_resolution_clock::time_point explorationEnd = std::chrono::high_resolution_clock::now();
+                    explorationTime = explorationEnd - explorationStart;
 
                     // TODO Matthias: possible to do bisimulation on approximated model and not on concrete one?
 
@@ -176,7 +175,8 @@ namespace storm {
                     // We only output the info from the lower bound as the info for the upper bound is the same
                     STORM_LOG_INFO("No. states: " << model->getNumberOfStates());
                     STORM_LOG_INFO("No. transitions: " << model->getNumberOfTransitions());
-                    explorationTime += std::chrono::high_resolution_clock::now() - explorationStart;
+                    buildingTime += std::chrono::high_resolution_clock::now() - explorationEnd;
+
                     // Check lower bound
                     std::unique_ptr<storm::modelchecker::CheckResult> result = checkModel(model, formula);
                     result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
@@ -186,9 +186,9 @@ namespace storm {
 
                     // Build model for upper bound
                     STORM_LOG_INFO("Getting model for upper bound...");
-                    explorationStart = std::chrono::high_resolution_clock::now();
+                    explorationEnd = std::chrono::high_resolution_clock::now();
                     model = builder.getModelApproximation(probabilityFormula ? true : false);
-                    explorationTime += std::chrono::high_resolution_clock::now() - explorationStart;
+                    buildingTime += std::chrono::high_resolution_clock::now() - explorationEnd;
                     // Check upper bound
                     result = checkModel(model, formula);
                     result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
@@ -198,6 +198,8 @@ namespace storm {
 
                     ++iteration;
                     STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")");
+                    totalTime = std::chrono::high_resolution_clock::now() - totalStart;
+                    printTimings();
                     STORM_LOG_THROW(!storm::utility::isInfinity<ValueType>(approxResult.first) && !storm::utility::isInfinity<ValueType>(approxResult.second), storm::exceptions::NotSupportedException, "Approximation does not work if result might be infinity.");
                 } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError, probabilityFormula));
 
@@ -221,7 +223,7 @@ namespace storm {
                 //model->printModelInformationToStream(std::cout);
                 STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
                 STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
-                explorationTime += std::chrono::high_resolution_clock::now() - buildingEnd;
+                explorationTime += std::chrono::high_resolution_clock::now() - checkingStart;
 
                 // Model checking
                 std::unique_ptr<storm::modelchecker::CheckResult> result = checkModel(model, formula);
@@ -270,8 +272,8 @@ namespace storm {
         template<typename ValueType>
         void DFTModelChecker<ValueType>::printTimings(std::ostream& os) {
             os << "Times:" << std::endl;
-            os << "Building:\t" << buildingTime.count() << std::endl;
             os << "Exploration:\t" << explorationTime.count() << std::endl;
+            os << "Building:\t" << buildingTime.count() << std::endl;
             os << "Bisimulation:\t" << bisimulationTime.count() << std::endl;
             os << "Modelchecking:\t" << modelCheckingTime.count() << std::endl;
             os << "Total:\t\t" << totalTime.count() << std::endl;

src/modelchecker/dft/DFTModelChecker.h

@@ -61,6 +61,7 @@ namespace storm {
             std::chrono::duration<double> bisimulationTime = std::chrono::duration<double>::zero();
             std::chrono::duration<double> modelCheckingTime = std::chrono::duration<double>::zero();
             std::chrono::duration<double> totalTime = std::chrono::duration<double>::zero();
+            std::chrono::high_resolution_clock::time_point totalStart;
 
             // Model checking result
             dft_result checkResult;

src/storage/BucketPriorityQueue.cpp

@@ -2,11 +2,13 @@
 #include "src/utility/macros.h"
 #include "src/adapters/CarlAdapter.h"
 
+#include <cmath>
+
 namespace storm {
     namespace storage {
 
         template<typename ValueType>
-        BucketPriorityQueue<ValueType>::BucketPriorityQueue(size_t nrBuckets, double lowerValue, double stepPerBucket) : buckets(nrBuckets), currentBucket(nrBuckets), lowerValue(lowerValue), stepPerBucket(stepPerBucket), nrUnsortedItems(0) {
+        BucketPriorityQueue<ValueType>::BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio) : lowerValue(lowerValue), logBase(std::log(ratio)), nrBuckets(nrBuckets), nrUnsortedItems(0), buckets(nrBuckets), currentBucket(nrBuckets) {
             compare = ([this](HeuristicPointer a, HeuristicPointer b) {
                 return *a < *b;
             });
@@ -14,7 +16,7 @@ namespace storm {
 
         template<typename ValueType>
         void BucketPriorityQueue<ValueType>::fix() {
-            if (currentBucket < buckets.size() && nrUnsortedItems > buckets[currentBucket].size() / 10) {
+            if (currentBucket < nrBuckets && nrUnsortedItems > buckets[currentBucket].size() / 10) {
                 // Fix current bucket
                 std::make_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare);
                 nrUnsortedItems = 0;
@@ -23,13 +25,13 @@ namespace storm {
 
         template<typename ValueType>
         bool BucketPriorityQueue<ValueType>::empty() const {
-            return currentBucket == buckets.size() && immediateBucket.empty();
+            return currentBucket == nrBuckets && immediateBucket.empty();
         }
 
         template<typename ValueType>
         std::size_t BucketPriorityQueue<ValueType>::size() const {
             size_t size = immediateBucket.size();
-            for (size_t i = currentBucket; currentBucket < buckets.size(); ++i) {
+            for (size_t i = currentBucket; currentBucket < nrBuckets; ++i) {
                 size += buckets[i].size();
             }
             return size;
@@ -129,7 +131,7 @@ namespace storm {
             buckets[currentBucket].pop_back();
             if (buckets[currentBucket].empty()) {
                 // Find next bucket with elements
-                for ( ; currentBucket < buckets.size(); ++currentBucket) {
+                for ( ; currentBucket < nrBuckets; ++currentBucket) {
                     if (!buckets[currentBucket].empty()) {
                         nrUnsortedItems = buckets[currentBucket].size();
                         if (AUTOSORT) {
@@ -151,18 +153,21 @@ namespace storm {
         template<typename ValueType>
         size_t BucketPriorityQueue<ValueType>::getBucket(double priority) const {
             STORM_LOG_ASSERT(priority >= lowerValue, "Priority " << priority << " is too low");
-            size_t newBucket = (priority - lowerValue) / stepPerBucket;
-            if (HIGHER) {
-                newBucket = buckets.size()-1 - newBucket;
+            size_t newBucket = std::log(priority - lowerValue) / logBase;
+            if (newBucket >= nrBuckets) {
+                newBucket = nrBuckets - 1;
+            }
+            if (!HIGHER) {
+                newBucket = nrBuckets-1 - newBucket;
             }
-            //std::cout << "get Bucket: " << priority << ", " << newBucket << ", " << ((priority - lowerValue) / stepPerBucket) << std::endl;
-            STORM_LOG_ASSERT(newBucket < buckets.size(), "Priority " << priority << " is too high");
+            //std::cout << "get Bucket: " << priority << ", " << newBucket << std::endl;
+            STORM_LOG_ASSERT(newBucket < nrBuckets, "Priority " << priority << " is too high");
             return newBucket;
         }
 
         template<typename ValueType>
         void BucketPriorityQueue<ValueType>::print(std::ostream& out) const {
-            out << "Bucket priority queue with size " << buckets.size() << ", lower value: " << lowerValue << " and step per bucket: " << stepPerBucket << std::endl;
+            out << "Bucket priority queue with size " << buckets.size() << ", lower value: " << lowerValue << " and logBase: " << logBase << std::endl;
             out << "Immediate bucket: ";
             for (HeuristicPointer heuristic : immediateBucket) {
                 out << heuristic->getId() << ", ";
@@ -171,7 +176,7 @@ namespace storm {
             out << "Current bucket (" << currentBucket << ") has " << nrUnsortedItems  << " unsorted items" << std::endl;
             for (size_t bucket = 0; bucket < buckets.size(); ++bucket) {
                 if (!buckets[bucket].empty()) {
-                    out << "Bucket " << bucket << " (" << (HIGHER ? buckets.size() -1 - bucket * stepPerBucket : bucket * stepPerBucket) << "):" << std::endl;
+                    out << "Bucket " << bucket << ":" << std::endl;
                     for (HeuristicPointer heuristic : buckets[bucket]) {
                         out << "\t" << heuristic->getId() << ": " << heuristic->getPriority() << std::endl;
                     }
@@ -179,6 +184,14 @@ namespace storm {
             }
         }
 
+        template<typename ValueType>
+        void BucketPriorityQueue<ValueType>::printSizes(std::ostream& out) const {
+            out << "Bucket sizes: " << immediateBucket.size() << " | ";
+            for (size_t bucket = 0; bucket < buckets.size(); ++bucket) {
+                out << buckets[bucket].size() << " ";
+            }
+            std::cout << std::endl;
+        }
 
         // Template instantiations
         template class BucketPriorityQueue<double>;

src/storage/BucketPriorityQueue.h

@@ -16,7 +16,7 @@ namespace storm {
             using HeuristicPointer = std::shared_ptr<storm::builder::DFTExplorationHeuristicProbability<ValueType>>;
 
         public:
-            explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double stepPerBucket);
+            explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio);
 
             void fix();
 
@@ -36,10 +36,24 @@ namespace storm {
 
             void print(std::ostream& out) const;
 
+            void printSizes(std::ostream& out) const;
+
         private:
 
             size_t getBucket(double priority) const;
 
+            const double lowerValue;
+
+            const bool HIGHER = true;
+
+            const bool AUTOSORT = false;
+
+            const double logBase;
+
+            const size_t nrBuckets;
+
+            size_t nrUnsortedItems;
+
             // List of buckets
             std::vector<std::vector<HeuristicPointer>> buckets;
 
@@ -51,15 +65,6 @@ namespace storm {
 
             std::function<bool(HeuristicPointer, HeuristicPointer)> compare;
 
-            double lowerValue;
-
-            double stepPerBucket;
-
-            size_t nrUnsortedItems;
-
-            const bool HIGHER = true;
-
-            const bool AUTOSORT = false;
         };
 
     }