Merge remote-tracking branch 'origin' into gamebased

README.md

@@ -30,7 +30,7 @@ Authors
 Storm has been developed at RWTH Aachen University.
 
 ###### Principal developers
-* Christian Dehnert
+* Christian Hensel
 * Sebastian Junges
 * Joost-Pieter Katoen
 * Tim Quatmann

src/storm-dft-cli/storm-dft.cpp

@@ -107,9 +107,9 @@ void processOptions() {
         // Carry out the actual analysis
         if (faultTreeSettings.isApproximationErrorSet()) {
             // Approximate analysis
-            storm::api::analyzeDFTApprox<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), faultTreeSettings.getApproximationError());
+            storm::api::analyzeDFTApprox<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), faultTreeSettings.getApproximationError(), true);
         } else {
-            storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC());
+            storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), true);
         }
 }
 

src/storm-dft/api/storm-dft.h

@@ -53,11 +53,13 @@ namespace storm {
          * @return Result.
          */
         template <typename ValueType>
-        typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, bool enableDC) {
+        typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, bool enableDC, bool printOutput) {
             storm::modelchecker::DFTModelChecker<ValueType> modelChecker;
             typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, 0.0);
+            if (printOutput) {
                 modelChecker.printTimings();
                 modelChecker.printResults();
+            }
             return results;
         }
 
@@ -75,11 +77,13 @@ namespace storm {
          * @return Result.
          */
         template <typename ValueType>
-        typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results analyzeDFTApprox(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) {
+        typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results analyzeDFTApprox(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError, bool printOutput) {
             storm::modelchecker::DFTModelChecker<ValueType> modelChecker;
             typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, approximationError);
+            if (printOutput) {
                 modelChecker.printTimings();
                 modelChecker.printResults();
+            }
             return results;
         }
 

src/storm-dft/modelchecker/dft/DFTModelChecker.cpp

@@ -176,7 +176,7 @@ namespace storm {
                 bool firstTime = true;
                 std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> composedModel;
                 for (auto const ft : dfts) {
-                    STORM_LOG_INFO("Building Model via parallel composition...");
+                    STORM_LOG_DEBUG("Building Model via parallel composition...");
                     explorationTimer.start();
 
                     // Find symmetries
@@ -185,12 +185,12 @@ namespace storm {
                     if(symred) {
                         auto colouring = ft.colourDFT();
                         symmetries = ft.findSymmetries(colouring);
-                        STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries.");
+                        STORM_LOG_DEBUG("Found " << symmetries.groups.size() << " symmetries.");
                         STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries);
                     }
 
                     // Build a single CTMC
-                    STORM_LOG_INFO("Building Model...");
+                    STORM_LOG_DEBUG("Building Model...");
                     storm::builder::ExplicitDFTModelBuilder<ValueType> builder(ft, symmetries, enableDC);
                     typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
                     builder.buildModel(labeloptions, 0, 0.0);
@@ -226,7 +226,7 @@ namespace storm {
                     }
 
                 }
-                composedModel->printModelInformationToStream(std::cout);
+                //composedModel->printModelInformationToStream(std::cout);
                 return composedModel;
             } else {
                 // No composition was possible
@@ -237,17 +237,17 @@ namespace storm {
                 if(symred) {
                     auto colouring = dft.colourDFT();
                     symmetries = dft.findSymmetries(colouring);
-                    STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries.");
+                    STORM_LOG_DEBUG("Found " << symmetries.groups.size() << " symmetries.");
                     STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries);
                 }
                 // Build a single CTMC
-                STORM_LOG_INFO("Building Model...");
+                STORM_LOG_DEBUG("Building Model...");
 
                 storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
                 typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
                 builder.buildModel(labeloptions, 0, 0.0);
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
-                model->printModelInformationToStream(std::cout);
+                //model->printModelInformationToStream(std::cout);
                 explorationTimer.stop();
                 STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs");
                 return model->template as<storm::models::sparse::Ctmc<ValueType>>();
@@ -264,7 +264,7 @@ namespace storm {
             if(symred) {
                 auto colouring = dft.colourDFT();
                 symmetries = dft.findSymmetries(colouring);
-                STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries.");
+                STORM_LOG_DEBUG("Found " << symmetries.groups.size() << " symmetries.");
                 STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries);
             }
 
@@ -292,7 +292,7 @@ namespace storm {
                     if (iteration > 0) {
                         explorationTimer.start();
                     }
-                    STORM_LOG_INFO("Building model...");
+                    STORM_LOG_DEBUG("Building model...");
                     // TODO Matthias refine model using existing model and MC results
                     builder.buildModel(labeloptions, iteration, approximationError);
                     explorationTimer.stop();
@@ -301,10 +301,10 @@ namespace storm {
                     // TODO Matthias: possible to do bisimulation on approximated model and not on concrete one?
 
                     // Build model for lower bound
-                    STORM_LOG_INFO("Getting model for lower bound...");
+                    STORM_LOG_DEBUG("Getting model for lower bound...");
                     model = builder.getModelApproximation(true, !probabilityFormula);
                     // We only output the info from the lower bound as the info for the upper bound is the same
-                    model->printModelInformationToStream(std::cout);
+                    //model->printModelInformationToStream(std::cout);
                     buildingTimer.stop();
 
                     // Check lower bounds
@@ -314,7 +314,7 @@ namespace storm {
                     approxResult.first = newResult[0];
 
                     // Build model for upper bound
-                    STORM_LOG_INFO("Getting model for upper bound...");
+                    STORM_LOG_DEBUG("Getting model for upper bound...");
                     buildingTimer.start();
                     model = builder.getModelApproximation(false, !probabilityFormula);
                     buildingTimer.stop();
@@ -326,25 +326,25 @@ namespace storm {
 
                     ++iteration;
                     STORM_LOG_ASSERT(comparator.isLess(approxResult.first, approxResult.second) || comparator.isEqual(approxResult.first, approxResult.second), "Under-approximation " << approxResult.first << " is greater than over-approximation " << approxResult.second);
-                    STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")");
+                    //STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")");
                     totalTimer.stop();
                     printTimings();
                     totalTimer.start();
                     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));
 
-                STORM_LOG_INFO("Finished approximation after " << iteration << " iteration" << (iteration > 1 ? "s." : "."));
+                //STORM_LOG_INFO("Finished approximation after " << iteration << " iteration" << (iteration > 1 ? "s." : "."));
                 dft_results results;
                 results.push_back(approxResult);
                 return results;
             } else {
                 // Build a single Markov Automaton
-                STORM_LOG_INFO("Building Model...");
+                STORM_LOG_DEBUG("Building Model...");
                 storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
                 typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
                 builder.buildModel(labeloptions, 0, 0.0);
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
-                model->printModelInformationToStream(std::cout);
+                //model->printModelInformationToStream(std::cout);
                 explorationTimer.stop();
 
                 // Export the model if required
@@ -373,15 +373,15 @@ namespace storm {
             // Bisimulation
             if (model->isOfType(storm::models::ModelType::Ctmc) && storm::settings::getModule<storm::settings::modules::GeneralSettings>().isBisimulationSet()) {
                 bisimulationTimer.start();
-                STORM_LOG_INFO("Bisimulation...");
+                STORM_LOG_DEBUG("Bisimulation...");
                 model =  storm::api::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(model->template as<storm::models::sparse::Ctmc<ValueType>>(), properties, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
-                STORM_LOG_INFO("No. states (Bisimulation): " << model->getNumberOfStates());
-                STORM_LOG_INFO("No. transitions (Bisimulation): " << model->getNumberOfTransitions());
+                STORM_LOG_DEBUG("No. states (Bisimulation): " << model->getNumberOfStates());
+                STORM_LOG_DEBUG("No. transitions (Bisimulation): " << model->getNumberOfTransitions());
                 bisimulationTimer.stop();
             }
 
             // Check the model
-            STORM_LOG_INFO("Model checking...");
+            STORM_LOG_DEBUG("Model checking...");
             modelCheckingTimer.start();
             std::vector<ValueType> results;
 
@@ -390,18 +390,18 @@ namespace storm {
             for (auto property : properties) {
                 singleModelCheckingTimer.reset();
                 singleModelCheckingTimer.start();
-                STORM_PRINT_AND_LOG("Model checking property " << *property << " ..." << std::endl);
+                //STORM_PRINT_AND_LOG("Model checking property " << *property << " ..." << std::endl);
                 std::unique_ptr<storm::modelchecker::CheckResult> result(storm::api::verifyWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(property, true)));
                 STORM_LOG_ASSERT(result, "Result does not exist.");
                 result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
                 ValueType resultValue = result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second;
-                STORM_PRINT_AND_LOG("Result (initial states): " << resultValue << std::endl);
+                //STORM_PRINT_AND_LOG("Result (initial states): " << resultValue << std::endl);
                 results.push_back(resultValue);
                 singleModelCheckingTimer.stop();
-                STORM_PRINT_AND_LOG("Time for model checking: " << singleModelCheckingTimer << "." << std::endl);
+                //STORM_PRINT_AND_LOG("Time for model checking: " << singleModelCheckingTimer << "." << std::endl);
             }
             modelCheckingTimer.stop();
-            STORM_LOG_INFO("Model checking done.");
+            STORM_LOG_DEBUG("Model checking done.");
             return results;
         }
 

src/storm/solver/InPlaceMultiplier.cpp

@@ -1,138 +0,0 @@
-#include "storm/solver/InPlaceMultiplier.h"
-
-#include "storm-config.h"
-
-#include "storm/environment/solver/MultiplierEnvironment.h"
-#include "storm/settings/SettingsManager.h"
-#include "storm/settings/modules/CoreSettings.h"
-
-#include "storm/storage/SparseMatrix.h"
-
-#include "storm/adapters/RationalNumberAdapter.h"
-#include "storm/adapters/RationalFunctionAdapter.h"
-
-#include "storm/utility/macros.h"
-
-namespace storm {
-    namespace solver {
-        
-        template<typename ValueType>
-        InPlaceMultiplier<ValueType>::InPlaceMultiplier(storm::storage::SparseMatrix<ValueType> const& matrix) : Multiplier<ValueType>(matrix) {
-            // Intentionally left empty.
-        }
-        
-        template<typename ValueType>
-        bool InPlaceMultiplier<ValueType>::parallelize(Environment const& env) const {
-#ifdef STORM_HAVE_INTELTBB
-            return storm::settings::getModule<storm::settings::modules::CoreSettings>().isUseIntelTbbSet();
-#else
-            return false;
-#endif
-        }
-        
-        template<typename ValueType>
-        void InPlaceMultiplier<ValueType>::multiply(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const {
-            std::vector<ValueType>* target = &result;
-            if (&x == &result) {
-                if (this->cachedVector) {
-                    this->cachedVector->resize(x.size());
-                } else {
-                    this->cachedVector = std::make_unique<std::vector<ValueType>>(x.size());
-                }
-                target = this->cachedVector.get();
-            }
-            if (parallelize(env)) {
-                multAddParallel(x, b, *target);
-            } else {
-                multAdd(x, b, *target);
-            }
-            if (&x == &result) {
-                std::swap(result, *this->cachedVector);
-            }
-        }
-        
-        template<typename ValueType>
-        void InPlaceMultiplier<ValueType>::multiplyGaussSeidel(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b) const {
-            this->matrix.multiplyWithVectorBackward(x, x, b);
-        }
-        
-        template<typename ValueType>
-        void InPlaceMultiplier<ValueType>::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const {
-            std::vector<ValueType>* target = &result;
-            if (&x == &result) {
-                if (this->cachedVector) {
-                    this->cachedVector->resize(x.size());
-                } else {
-                    this->cachedVector = std::make_unique<std::vector<ValueType>>(x.size());
-                }
-                target = this->cachedVector.get();
-            }
-            if (parallelize(env)) {
-                multAddReduceParallel(dir, rowGroupIndices, x, b, *target, choices);
-            } else {
-                multAddReduce(dir, rowGroupIndices, x, b, *target, choices);
-            }
-            if (&x == &result) {
-                std::swap(result, *this->cachedVector);
-            }
-        }
-        
-        template<typename ValueType>
-        void InPlaceMultiplier<ValueType>::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices) const {
-            this->matrix.multiplyAndReduceBackward(dir, rowGroupIndices, x, b, x, choices);
-        }
-        
-        template<typename ValueType>
-        void InPlaceMultiplier<ValueType>::multiplyRow(uint64_t const& rowIndex, std::vector<ValueType> const& x, ValueType& value) const {
-            for (auto const& entry : this->matrix.getRow(rowIndex)) {
-                value += entry.getValue() * x[entry.getColumn()];
-            }
-        }
-        
-        template<typename ValueType>
-        void InPlaceMultiplier<ValueType>::multiplyRow2(uint64_t const& rowIndex, std::vector<ValueType> const& x1, ValueType& val1, std::vector<ValueType> const& x2, ValueType& val2) const {
-            for (auto const& entry : this->matrix.getRow(rowIndex)) {
-                val1 += entry.getValue() * x1[entry.getColumn()];
-                val2 += entry.getValue() * x2[entry.getColumn()];
-            }
-        }
-
-
-        template<typename ValueType>
-        void InPlaceMultiplier<ValueType>::multAdd(std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const {
-            this->matrix.multiplyWithVector(x, result, b);
-        }
-        
-        template<typename ValueType>
-        void InPlaceMultiplier<ValueType>::multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices) const {
-            this->matrix.multiplyAndReduce(dir, rowGroupIndices, x, b, result, choices);
-        }
-        
-        template<typename ValueType>
-        void InPlaceMultiplier<ValueType>::multAddParallel(std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const {
-#ifdef STORM_HAVE_INTELTBB
-            this->matrix.multiplyWithVectorParallel(x, result, b);
-#else
-            STORM_LOG_WARN("Storm was built without support for Intel TBB, defaulting to sequential version.");
-            multAdd(x, b, result);
-#endif
-        }
-                
-        template<typename ValueType>
-        void InPlaceMultiplier<ValueType>::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices) const {
-#ifdef STORM_HAVE_INTELTBB
-            this->matrix.multiplyAndReduceParallel(dir, rowGroupIndices, x, b, result, choices);
-#else
-            STORM_LOG_WARN("Storm was built without support for Intel TBB, defaulting to sequential version.");
-            multAddReduce(dir, rowGroupIndices, x, b, result, choices);
-#endif
-        }
-
-        template class InPlaceMultiplier<double>;
-#ifdef STORM_HAVE_CARL
-        template class InPlaceMultiplier<storm::RationalNumber>;
-        template class InPlaceMultiplier<storm::RationalFunction>;
-#endif
-        
-    }
-}

src/storm/solver/InPlaceMultiplier.h

@@ -1,41 +0,0 @@
-#pragma once
-
-#include "storm/solver/Multiplier.h"
-
-#include "storm/solver/OptimizationDirection.h"
-
-namespace storm {
-    namespace storage {
-        template<typename ValueType>
-        class SparseMatrix;
-    }
-    
-    namespace solver {
-        
-        template<typename ValueType>
-        class InPlaceMultiplier : public Multiplier<ValueType> {
-        public:
-            InPlaceMultiplier(storm::storage::SparseMatrix<ValueType> const& matrix);
-            
-            virtual void multiply(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const override;
-            virtual void multiplyGaussSeidel(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b) const override;
-            virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices = nullptr) const override;
-            virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices = nullptr) const override;
-            virtual void multiplyRow(uint64_t const& rowIndex, std::vector<ValueType> const& x, ValueType& value) const override;
-            virtual void multiplyRow2(uint64_t const& rowIndex, std::vector<ValueType> const& x1, ValueType& val1, std::vector<ValueType> const& x2, ValueType& val2) const override;
-
-
-        private:
-            bool parallelize(Environment const& env) const;
-            
-            void multAdd(std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const;
-            
-            void multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices = nullptr) const;
-            
-            void multAddParallel(std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const;
-            void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices = nullptr) const;
-            
-        };
-        
-    }
-}

src/storm/solver/Multiplier.cpp

@@ -11,7 +11,6 @@
 #include "storm/solver/SolverSelectionOptions.h"
 #include "storm/solver/NativeMultiplier.h"
 #include "storm/solver/GmmxxMultiplier.h"
-#include "storm/solver/InPlaceMultiplier.h"
 #include "storm/environment/solver/MultiplierEnvironment.h"
 
 namespace storm {

src/test/storm-dft/api/DftModelCheckerTest.cpp

@@ -65,7 +65,7 @@ namespace {
             std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileo<double>(file);
             std::string property = "Tmin=? [F \"failed\"]";
             std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
-            typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod, config.useDC);
+            typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod, config.useDC, false);
             return boost::get<double>(results[0]);
         }