From 51e08bb1a5f8bf941a101c079c3527610c9a7af7 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 23 Mar 2018 09:31:03 +0100 Subject: [PATCH 1/3] removed old inPlaceMultiplier --- src/storm/solver/InPlaceMultiplier.cpp | 138 ------------------------- src/storm/solver/InPlaceMultiplier.h | 41 -------- src/storm/solver/Multiplier.cpp | 1 - 3 files changed, 180 deletions(-) delete mode 100644 src/storm/solver/InPlaceMultiplier.cpp delete mode 100644 src/storm/solver/InPlaceMultiplier.h diff --git a/src/storm/solver/InPlaceMultiplier.cpp b/src/storm/solver/InPlaceMultiplier.cpp deleted file mode 100644 index abfd4463a..000000000 --- a/src/storm/solver/InPlaceMultiplier.cpp +++ /dev/null @@ -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 - InPlaceMultiplier::InPlaceMultiplier(storm::storage::SparseMatrix const& matrix) : Multiplier(matrix) { - // Intentionally left empty. - } - - template - bool InPlaceMultiplier::parallelize(Environment const& env) const { -#ifdef STORM_HAVE_INTELTBB - return storm::settings::getModule().isUseIntelTbbSet(); -#else - return false; -#endif - } - - template - void InPlaceMultiplier::multiply(Environment const& env, std::vector const& x, std::vector const* b, std::vector& result) const { - std::vector* target = &result; - if (&x == &result) { - if (this->cachedVector) { - this->cachedVector->resize(x.size()); - } else { - this->cachedVector = std::make_unique>(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 - void InPlaceMultiplier::multiplyGaussSeidel(Environment const& env, std::vector& x, std::vector const* b) const { - this->matrix.multiplyWithVectorBackward(x, x, b); - } - - template - void InPlaceMultiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { - std::vector* target = &result; - if (&x == &result) { - if (this->cachedVector) { - this->cachedVector->resize(x.size()); - } else { - this->cachedVector = std::make_unique>(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 - void InPlaceMultiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices) const { - this->matrix.multiplyAndReduceBackward(dir, rowGroupIndices, x, b, x, choices); - } - - template - void InPlaceMultiplier::multiplyRow(uint64_t const& rowIndex, std::vector const& x, ValueType& value) const { - for (auto const& entry : this->matrix.getRow(rowIndex)) { - value += entry.getValue() * x[entry.getColumn()]; - } - } - - template - void InPlaceMultiplier::multiplyRow2(uint64_t const& rowIndex, std::vector const& x1, ValueType& val1, std::vector 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 - void InPlaceMultiplier::multAdd(std::vector const& x, std::vector const* b, std::vector& result) const { - this->matrix.multiplyWithVector(x, result, b); - } - - template - void InPlaceMultiplier::multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { - this->matrix.multiplyAndReduce(dir, rowGroupIndices, x, b, result, choices); - } - - template - void InPlaceMultiplier::multAddParallel(std::vector const& x, std::vector const* b, std::vector& 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 - void InPlaceMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* 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; -#ifdef STORM_HAVE_CARL - template class InPlaceMultiplier; - template class InPlaceMultiplier; -#endif - - } -} diff --git a/src/storm/solver/InPlaceMultiplier.h b/src/storm/solver/InPlaceMultiplier.h deleted file mode 100644 index d02c74bfb..000000000 --- a/src/storm/solver/InPlaceMultiplier.h +++ /dev/null @@ -1,41 +0,0 @@ -#pragma once - -#include "storm/solver/Multiplier.h" - -#include "storm/solver/OptimizationDirection.h" - -namespace storm { - namespace storage { - template - class SparseMatrix; - } - - namespace solver { - - template - class InPlaceMultiplier : public Multiplier { - public: - InPlaceMultiplier(storm::storage::SparseMatrix const& matrix); - - virtual void multiply(Environment const& env, std::vector const& x, std::vector const* b, std::vector& result) const override; - virtual void multiplyGaussSeidel(Environment const& env, std::vector& x, std::vector const* b) const override; - virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const override; - virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr) const override; - virtual void multiplyRow(uint64_t const& rowIndex, std::vector const& x, ValueType& value) const override; - virtual void multiplyRow2(uint64_t const& rowIndex, std::vector const& x1, ValueType& val1, std::vector const& x2, ValueType& val2) const override; - - - private: - bool parallelize(Environment const& env) const; - - void multAdd(std::vector const& x, std::vector const* b, std::vector& result) const; - - void multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; - - void multAddParallel(std::vector const& x, std::vector const* b, std::vector& result) const; - void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; - - }; - - } -} diff --git a/src/storm/solver/Multiplier.cpp b/src/storm/solver/Multiplier.cpp index 0da52a06a..26bb4d85b 100644 --- a/src/storm/solver/Multiplier.cpp +++ b/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 { From a03f9c80d283c6d7fdc0e4e17dd915efb80f28dd Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 26 Mar 2018 11:13:01 +0200 Subject: [PATCH 2/3] Updated README --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index d30d82ad9..6dcf702a0 100644 --- a/README.md +++ b/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 From 6fa88b1c14e68c49f64ca55b59bf3a1d9b68ffb0 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 26 Mar 2018 11:14:00 +0200 Subject: [PATCH 3/3] Disable unnecessary output for DFT model checking --- src/storm-dft-cli/storm-dft.cpp | 4 +- src/storm-dft/api/storm-dft.h | 16 ++++--- .../modelchecker/dft/DFTModelChecker.cpp | 48 +++++++++---------- .../storm-dft/api/DftModelCheckerTest.cpp | 2 +- 4 files changed, 37 insertions(+), 33 deletions(-) diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index f051570dc..9923330d0 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/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(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), faultTreeSettings.getApproximationError()); + storm::api::analyzeDFTApprox(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), faultTreeSettings.getApproximationError(), true); } else { - storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC()); + storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), true); } } diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index 003c03f14..db6d7b3e4 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -53,11 +53,13 @@ namespace storm { * @return Result. */ template - typename storm::modelchecker::DFTModelChecker::dft_results analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC) { + typename storm::modelchecker::DFTModelChecker::dft_results analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC, bool printOutput) { storm::modelchecker::DFTModelChecker modelChecker; typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, 0.0); - modelChecker.printTimings(); - modelChecker.printResults(); + if (printOutput) { + modelChecker.printTimings(); + modelChecker.printResults(); + } return results; } @@ -75,11 +77,13 @@ namespace storm { * @return Result. */ template - typename storm::modelchecker::DFTModelChecker::dft_results analyzeDFTApprox(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { + typename storm::modelchecker::DFTModelChecker::dft_results analyzeDFTApprox(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError, bool printOutput) { storm::modelchecker::DFTModelChecker modelChecker; typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, approximationError); - modelChecker.printTimings(); - modelChecker.printResults(); + if (printOutput) { + modelChecker.printTimings(); + modelChecker.printResults(); + } return results; } diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index c3e7996c7..31ba6789d 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -176,7 +176,7 @@ namespace storm { bool firstTime = true; std::shared_ptr> 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 builder(ft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilder::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 builder(dft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> 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>(); @@ -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(approxResult.first) && !storm::utility::isInfinity(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 builder(dft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties, storm::settings::getModule().isExportExplicitSet()); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> 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().isBisimulationSet()) { bisimulationTimer.start(); - STORM_LOG_INFO("Bisimulation..."); + STORM_LOG_DEBUG("Bisimulation..."); model = storm::api::performDeterministicSparseBisimulationMinimization>(model->template as>(), properties, storm::storage::BisimulationType::Weak)->template as>(); - 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 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 result(storm::api::verifyWithSparseEngine(model, storm::api::createTask(property, true))); STORM_LOG_ASSERT(result, "Result does not exist."); result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); ValueType resultValue = result->asExplicitQuantitativeCheckResult().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; } diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index 902108018..5db58d60d 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -65,7 +65,7 @@ namespace { std::shared_ptr> dft = storm::api::loadDFTGalileo(file); std::string property = "Tmin=? [F \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); - typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, config.useMod, config.useDC); + typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, config.useMod, config.useDC, false); return boost::get(results[0]); }