From bfbd96a0e6ae41e493788c2391989cc26e489f35 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 2 Jan 2017 14:05:50 +0100 Subject: [PATCH 1/5] added some output for benchmarking --- src/storm/cli/cli.cpp | 5 ++ .../modelchecker/multiobjective/pcaa.cpp | 57 +++++++++++++++++-- .../pcaa/SparseMaPcaaWeightVectorChecker.cpp | 1 + .../multiobjective/pcaa/SparsePcaaQuery.h | 11 +++- .../pcaa/SparsePcaaWeightVectorChecker.h | 3 +- 5 files changed, 69 insertions(+), 8 deletions(-) diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index aaa601d15..b5606153f 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -140,6 +140,11 @@ namespace storm { if (wallclockMilliseconds != 0) { std::cout << " * wallclock time: " << (wallclockMilliseconds/1000) << "." << std::setw(3) << std::setfill('0') << (wallclockMilliseconds % 1000) << " seconds" << std::endl; } + std::cout << "STATISTICS_OVERALL_HEADERS;" << "memory;CPU time;wallclock time;" << std::endl; + std::cout << "STATISTICS_OVERALL_DATA;" + << ru.ru_maxrss/1024/1024 << ";" + << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << ";" + << (wallclockMilliseconds/1000) << "." << std::setw(3) << std::setfill('0') << (wallclockMilliseconds % 1000) << ";" << std::endl; #else HANDLE hProcess = GetCurrentProcess (); FILETIME ftCreation, ftExit, ftUser, ftKernel; diff --git a/src/storm/modelchecker/multiobjective/pcaa.cpp b/src/storm/modelchecker/multiobjective/pcaa.cpp index b7ca7cbc4..0bb19e6c8 100644 --- a/src/storm/modelchecker/multiobjective/pcaa.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa.cpp @@ -1,3 +1,4 @@ +#include #include "storm/modelchecker/multiobjective/pcaa.h" #include "storm/utility/macros.h" @@ -11,9 +12,11 @@ #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h" #include "storm/settings//SettingsManager.h" #include "storm/settings/modules/MultiObjectiveSettings.h" +#include "storm/settings/modules/GeneralSettings.h" #include "storm/exceptions/InvalidArgumentException.h" +#include "storm/utility/Stopwatch.h" namespace storm { namespace modelchecker { @@ -22,17 +25,17 @@ namespace storm { template std::unique_ptr performPcaa(SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula) { STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "Multi-objective Model checking on model with multiple initial states is not supported."); - + storm::utility::Stopwatch swPcaa,swPrep; #ifdef STORM_HAVE_CARL - + // If we consider an MA, ensure that it is closed if(model.isOfType(storm::models::ModelType::MarkovAutomaton)) { STORM_LOG_THROW(dynamic_cast const *>(&model)->isClosed(), storm::exceptions::InvalidArgumentException, "Unable to check multi-objective formula on non-closed Markov automaton."); } - + auto preprocessorResult = SparsePcaaPreprocessor::preprocess(model, formula); STORM_LOG_DEBUG("Preprocessing done. Result: " << preprocessorResult); - + auto preprocessedModelStates = preprocessorResult.preprocessedModel.getNumberOfStates(); std::unique_ptr> query; switch (preprocessorResult.queryType) { case SparsePcaaPreprocessorReturnType::QueryType::Achievability: @@ -48,12 +51,54 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unsupported multi-objective Query Type."); break; } - + swPrep.pause(); + storm::utility::Stopwatch swCheck; auto result = query->check(); - + swCheck.pause(); + swPcaa.pause(); + + std::cout << "STATISTICS_HEADERS;" + << "States;" + << "Transitions;" + << "Choices;" + << "Markovian states;" + << "Probabilistic states;" + << "Maximum exit rate E(s);" + << "Num of states after preprocessing;" + << "Query;" + << "Value iteration precision;" + << "Approximation precision;" + << "Time PCAA;" + << "Time Preprocessing;" + << "Time QueryCheck;" + << "Num of checked weight vectors;" + << "Vertices underApprox;" + << "Vertices overApprox;" + << "Max step bound;" + << std::endl; + + std::cout << "STATISTICS_DATA;" + << model.getNumberOfStates() << ";" + << model.getNumberOfTransitions() << ";" + << model.getNumberOfChoices() << ";" + << (model.isOfType(storm::models::ModelType::MarkovAutomaton) ? dynamic_cast const *>(&model)->getMarkovianStates().getNumberOfSetBits() : 0) << ";" + << (model.isOfType(storm::models::ModelType::MarkovAutomaton) ? ~(dynamic_cast const *>(&model)->getMarkovianStates()).getNumberOfSetBits() : model.getNumberOfStates()) << ";" + << (model.isOfType(storm::models::ModelType::MarkovAutomaton) ? dynamic_cast const *>(&model)->getMaximalExitRate() : 0) << ";" + << formula << ";" + << preprocessedModelStates << ";" + << settings::getModule().getPrecision() << ";" + << settings::getModule().getPrecision() << ";" + << swPcaa << ";" + << swPrep << ";" + << swCheck << ";"; + query->printInternalStatistics(); + std::cout << std::endl; + + if(settings::getModule().isExportPlotSet()) { query->exportPlotOfCurrentApproximation(storm::settings::getModule().getExportPlotDirectory()); } + return result; #else STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Multi-objective model checking requires carl."); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index 1c4dd8420..50c6f6aaa 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -69,6 +69,7 @@ namespace storm { auto lowerTimeBoundIt = lowerTimeBounds.begin(); auto upperTimeBoundIt = upperTimeBounds.begin(); uint_fast64_t currentEpoch = std::max(lowerTimeBounds.empty() ? 0 : lowerTimeBoundIt->first, upperTimeBounds.empty() ? 0 : upperTimeBoundIt->first); + this->maxStepBound = std::max(this->maxStepBound, currentEpoch); while(true) { // Update the objectives that are considered at the current time epoch as well as the (weighted) reward vectors. updateDataToCurrentEpoch(MS, PS, *minMax, consideredObjectives, currentEpoch, weightVector, lowerTimeBoundIt, lowerTimeBounds, upperTimeBoundIt, upperTimeBounds); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h index c0a891a13..cc9b33333 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h @@ -34,7 +34,16 @@ namespace storm { * This only works for 2 dimensional queries. */ void exportPlotOfCurrentApproximation(std::string const& destinationDir) const; - + + + void printInternalStatistics() const { + std::cout << refinementSteps.size() << ";" + << underApproximation->getVertices().size() << ";" + << overApproximation->getVertices().size() << ";" + << overApproximation->getVertices().size() << ";" + << weightVectorChecker->maxStepBound << ";"; + } + protected: /* diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h index 452f30189..4a60ba34c 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h @@ -77,7 +77,8 @@ namespace storm { * Note that check(..) has to be called before retrieving the scheduler. Otherwise, an exception is thrown. */ storm::storage::TotalScheduler const& getScheduler() const; - + + uint_fast64_t maxStepBound = 0; protected: From 35d7f70ad564c6b78df7a4387d2d68d23d92e677 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 4 Jan 2017 12:54:47 +0100 Subject: [PATCH 2/5] more output for benchmarking --- .../multiobjective/pcaa/SparsePcaaParetoQuery.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index 639589592..f709e1caf 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -53,11 +53,12 @@ namespace storm { template void SparsePcaaParetoQuery::exploreSetOfAchievablePoints() { - + std::cout << std::endl; //First consider the objectives individually for(uint_fast64_t objIndex = 0; objIndexobjectives.size() && !this->maxStepsPerformed(); ++objIndex) { WeightVector direction(this->objectives.size(), storm::utility::zero()); direction[objIndex] = storm::utility::one(); + std::cout << "STATISTICS_CURRPREC_CURRSTEPS;" << "\\infty" << ";" << this->refinementSteps.size() << std::endl; this->performRefinementStep(std::move(direction)); } @@ -81,6 +82,7 @@ namespace storm { return; } STORM_LOG_DEBUG("Current precision of the approximation of the pareto curve is ~" << storm::utility::convertNumber(farestDistance)); + std::cout << "STATISTICS_CURRPREC_CURRSTEPS;" << storm::utility::convertNumber(farestDistance) << ";" << this->refinementSteps.size() << std::endl; WeightVector direction = underApproxHalfspaces[farestHalfspaceIndex].normalVector(); this->performRefinementStep(std::move(direction)); } From 0b555d5d5911507b36da681674741c5980b7515e Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 9 Jan 2017 19:15:54 +0100 Subject: [PATCH 3/5] fixed closing of MAs: Previously, stateActionRewardVectors have not been handled properly. --- src/storm/models/sparse/MarkovAutomaton.cpp | 53 ++++++++------------- src/storm/models/sparse/Model.cpp | 5 ++ src/storm/models/sparse/Model.h | 7 +++ 3 files changed, 32 insertions(+), 33 deletions(-) diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 1979e08d0..40f9003c5 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -125,44 +125,31 @@ namespace storm { template void MarkovAutomaton::close() { if (!closed) { - // First, count the number of hybrid states to know how many Markovian choices - // will be removed. - uint_fast64_t numberOfHybridStates = 0; - for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { - if (this->isHybridState(state)) { - ++numberOfHybridStates; + // Get the choices that we will keep + storm::storage::BitVector keptChoices(this->getNumberOfChoices(), true); + for(auto state : this->getMarkovianStates()) { + if(this->getTransitionMatrix().getRowGroupSize(state) > 1) { + // The state is hybrid, hence, we remove the first choice. + keptChoices.set(this->getTransitionMatrix().getRowGroupIndices()[state], false); + // Afterwards, the state will no longer be Markovian. + this->markovianStates.set(state, false); + exitRates[state] = storm::utility::zero(); } } - - // Create the matrix for the new transition relation and the corresponding nondeterministic choice vector. - storm::storage::SparseMatrixBuilder newTransitionMatrixBuilder(0, 0, 0, false, true, this->getNumberOfStates()); - - // Now copy over all choices that need to be kept. - uint_fast64_t currentChoice = 0; - for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { - // Record the new beginning of choices of this state. - newTransitionMatrixBuilder.newRowGroup(currentChoice); - - // If the state is a hybrid state, closing it will make it a probabilistic state, so we remove the Markovian marking. - // Additionally, we need to remember whether we need to skip the first choice of the state when - // we assemble the new transition matrix. - uint_fast64_t offset = 0; - if (this->isHybridState(state)) { - this->markovianStates.set(state, false); - offset = 1; + // Remove the Markovian choices for the different model ingredients + this->getTransitionMatrix() = this->getTransitionMatrix().restrictRows(keptChoices); + for(auto& rewModel : this->getRewardModels()) { + if(rewModel.second.hasStateActionRewards()) { + rewModel.second.getStateActionRewardVector() = storm::utility::vector::filterVector(rewModel.second.getStateActionRewardVector(), keptChoices); } - - for (uint_fast64_t row = this->getTransitionMatrix().getRowGroupIndices()[state] + offset; row < this->getTransitionMatrix().getRowGroupIndices()[state + 1]; ++row) { - for (auto const& entry : this->getTransitionMatrix().getRow(row)) { - newTransitionMatrixBuilder.addNextValue(currentChoice, entry.getColumn(), entry.getValue()); - } - ++currentChoice; + if(rewModel.second.hasTransitionRewards()) { + rewModel.second.getTransitionRewardMatrix() = rewModel.second.getTransitionRewardMatrix().restrictRows(keptChoices); } } - - // Finalize the matrix and put the new transition data in place. - this->setTransitionMatrix(newTransitionMatrixBuilder.build()); - + if(this->hasChoiceLabeling()) { + this->getOptionalChoiceLabeling() = storm::utility::vector::filterVector(this->getOptionalChoiceLabeling().get(), keptChoices); + } + // Mark the automaton as closed. closed = true; } diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index b00ef9b6f..890cfdae7 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -167,6 +167,11 @@ namespace storm { boost::optional> const& Model::getOptionalChoiceLabeling() const { return choiceLabeling; } + + template + boost::optional>& Model::getOptionalChoiceLabeling() { + return choiceLabeling; + } template storm::models::sparse::StateLabeling const& Model::getStateLabeling() const { diff --git a/src/storm/models/sparse/Model.h b/src/storm/models/sparse/Model.h index 583ffbb93..70358191a 100644 --- a/src/storm/models/sparse/Model.h +++ b/src/storm/models/sparse/Model.h @@ -239,6 +239,13 @@ namespace storm { * @return The labels for the choices, if they're saved. */ boost::optional> const& getOptionalChoiceLabeling() const; + + /*! + * Retrieves an optional value that contains the choice labeling if there is one. + * + * @return The labels for the choices, if they're saved. + */ + boost::optional>& getOptionalChoiceLabeling(); /*! * Returns the state labeling associated with this model. From 362b3bf6c60a486804f538f2f01fcebfd8450ca1 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 9 Jan 2017 20:03:50 +0100 Subject: [PATCH 4/5] removed eigen usages --- resources/3rdparty/CMakeLists.txt | 5 ++-- src/storm/adapters/EigenAdapter.cpp | 8 +++-- src/storm/adapters/EigenAdapter.h | 2 +- src/storm/cli/cli.cpp | 4 +-- .../solver/EigenLinearEquationSolver.cpp | 29 +++++++++++-------- 5 files changed, 28 insertions(+), 20 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 6e85cf5b3..807317bcf 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -43,8 +43,8 @@ list(APPEND STORM_DEP_TARGETS gmm) ## ############################################################# -add_imported_library_interface(Eigen33 "${PROJECT_SOURCE_DIR}/resources/3rdparty/eigen-3.3-beta1") -list(APPEND STORM_DEP_TARGETS Eigen33) +# add_imported_library_interface(Eigen33 "${PROJECT_SOURCE_DIR}/resources/3rdparty/eigen-3.3-beta1") +# list(APPEND STORM_DEP_TARGETS Eigen33) ############################################################# @@ -585,3 +585,4 @@ if(ENABLE_CUDA) endif() add_custom_target(copy_resources_headers DEPENDS ${CMAKE_BINARY_DIR}/include/resources/3rdparty/sparsepp/sparsepp.h ${CMAKE_BINARY_DIR}/include/resources/3rdparty/sparsepp/sparsepp.h) + diff --git a/src/storm/adapters/EigenAdapter.cpp b/src/storm/adapters/EigenAdapter.cpp index b5a3ccbbf..74d8f87f2 100644 --- a/src/storm/adapters/EigenAdapter.cpp +++ b/src/storm/adapters/EigenAdapter.cpp @@ -5,6 +5,8 @@ namespace storm { template std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix) { +return nullptr; +/* // Build a list of triplets and let Eigen care about the insertion. std::vector> triplets; triplets.reserve(matrix.getNonzeroEntryCount()); @@ -18,13 +20,13 @@ namespace storm { std::unique_ptr> result = std::make_unique>(matrix.getRowCount(), matrix.getColumnCount()); result->setFromTriplets(triplets.begin(), triplets.end()); return result; - } + */ } template std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); #ifdef STORM_HAVE_CARL - template std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); - template std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); + // template std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); + // template std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); #endif } } diff --git a/src/storm/adapters/EigenAdapter.h b/src/storm/adapters/EigenAdapter.h index a205ebee4..642fc53f9 100644 --- a/src/storm/adapters/EigenAdapter.h +++ b/src/storm/adapters/EigenAdapter.h @@ -1,7 +1,7 @@ #pragma once #include - +#include #include "storm/utility/eigen.h" #include "storm/storage/SparseMatrix.h" diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index b5606153f..e9ca81fe6 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -135,14 +135,14 @@ namespace storm { getrusage(RUSAGE_SELF, &ru); std::cout << "Performance statistics:" << std::endl; - std::cout << " * peak memory usage: " << ru.ru_maxrss/1024/1024 << " mb" << std::endl; + std::cout << " * peak memory usage: " << ru.ru_maxrss/1024 << " mb" << std::endl; std::cout << " * CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl; if (wallclockMilliseconds != 0) { std::cout << " * wallclock time: " << (wallclockMilliseconds/1000) << "." << std::setw(3) << std::setfill('0') << (wallclockMilliseconds % 1000) << " seconds" << std::endl; } std::cout << "STATISTICS_OVERALL_HEADERS;" << "memory;CPU time;wallclock time;" << std::endl; std::cout << "STATISTICS_OVERALL_DATA;" - << ru.ru_maxrss/1024/1024 << ";" + << ru.ru_maxrss/1024 << ";" << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << ";" << (wallclockMilliseconds/1000) << "." << std::setw(3) << std::setfill('0') << (wallclockMilliseconds % 1000) << ";" << std::endl; #else diff --git a/src/storm/solver/EigenLinearEquationSolver.cpp b/src/storm/solver/EigenLinearEquationSolver.cpp index 31c2dda48..5c91aaf34 100644 --- a/src/storm/solver/EigenLinearEquationSolver.cpp +++ b/src/storm/solver/EigenLinearEquationSolver.cpp @@ -105,7 +105,8 @@ namespace storm { #endif template - EigenLinearEquationSolver::EigenLinearEquationSolver(storm::storage::SparseMatrix const& A, EigenLinearEquationSolverSettings const& settings) : eigenA(storm::adapters::EigenAdapter::toEigenSparseMatrix(A)), settings(settings) { + EigenLinearEquationSolver::EigenLinearEquationSolver(storm::storage::SparseMatrix const& A, EigenLinearEquationSolverSettings const& settings) : settings(settings) { +std::cout << "eigen eq solver disabled since it requires a custom version that we disabled in this build." << std::endl; // Intentionally left empty. } @@ -116,7 +117,7 @@ namespace storm { template void EigenLinearEquationSolver::setMatrix(storm::storage::SparseMatrix const& A) { - eigenA = storm::adapters::EigenAdapter::toEigenSparseMatrix(A); +// eigenA = storm::adapters::EigenAdapter::toEigenSparseMatrix(A); this->clearCache(); } @@ -131,7 +132,8 @@ namespace storm { template bool EigenLinearEquationSolver::solveEquations(std::vector& x, std::vector const& b) const { // Map the input vectors to Eigen's format. - auto eigenX = Eigen::Matrix::Map(x.data(), x.size()); +return false; +/* auto eigenX = Eigen::Matrix::Map(x.data(), x.size()); auto eigenB = Eigen::Matrix::Map(b.data(), b.size()); typename EigenLinearEquationSolverSettings::SolutionMethod solutionMethod = this->getSettings().getSolutionMethod(); @@ -218,12 +220,12 @@ namespace storm { } } } - return false; + return false; */ } template void EigenLinearEquationSolver::multiply(std::vector& x, std::vector const* b, std::vector& result) const { - // Typedef the map-type so we don't have to spell it out. + /* // Typedef the map-type so we don't have to spell it out. typedef decltype(Eigen::Matrix::Map(b->data(), b->size())) MapType; auto eigenX = Eigen::Matrix::Map(x.data(), x.size()); @@ -247,7 +249,8 @@ namespace storm { eigenResult = *eigenA * eigenX; } } - } +*/ + } template EigenLinearEquationSolverSettings& EigenLinearEquationSolver::getSettings() { @@ -261,19 +264,20 @@ namespace storm { template uint64_t EigenLinearEquationSolver::getMatrixRowCount() const { - return eigenA->rows(); + return 0; // eigenA->rows(); } template uint64_t EigenLinearEquationSolver::getMatrixColumnCount() const { - return eigenA->cols(); + return 0; //eigenA->cols(); } #ifdef STORM_HAVE_CARL // Specialization for storm::RationalNumber template<> bool EigenLinearEquationSolver::solveEquations(std::vector& x, std::vector const& b) const { - // Map the input vectors to Eigen's format. +return false; /* +// Map the input vectors to Eigen's format. auto eigenX = Eigen::Matrix::Map(x.data(), x.size()); auto eigenB = Eigen::Matrix::Map(b.data(), b.size()); @@ -281,12 +285,13 @@ namespace storm { solver.compute(*eigenA); solver._solve_impl(eigenB, eigenX); return solver.info() == Eigen::ComputationInfo::Success; - } + */ } // Specialization for storm::RationalFunction template<> bool EigenLinearEquationSolver::solveEquations(std::vector& x, std::vector const& b) const { - // Map the input vectors to Eigen's format. +return false; /* + // Map the input vectors to Eigen's format. auto eigenX = Eigen::Matrix::Map(x.data(), x.size()); auto eigenB = Eigen::Matrix::Map(b.data(), b.size()); @@ -294,7 +299,7 @@ namespace storm { solver.compute(*eigenA); solver._solve_impl(eigenB, eigenX); return solver.info() == Eigen::ComputationInfo::Success; - } + */} #endif template From fb0222cf62ce23cbc0e0b5c3fba62a3ee6d7f40b Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 12 Jan 2017 13:43:52 +0100 Subject: [PATCH 5/5] fixed new interface of stopwatch --- src/storm/modelchecker/multiobjective/pcaa.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa.cpp b/src/storm/modelchecker/multiobjective/pcaa.cpp index 0bb19e6c8..56475e27d 100644 --- a/src/storm/modelchecker/multiobjective/pcaa.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa.cpp @@ -25,7 +25,7 @@ namespace storm { template std::unique_ptr performPcaa(SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula) { STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "Multi-objective Model checking on model with multiple initial states is not supported."); - storm::utility::Stopwatch swPcaa,swPrep; + storm::utility::Stopwatch swPcaa(true), swPrep(true); #ifdef STORM_HAVE_CARL // If we consider an MA, ensure that it is closed @@ -51,11 +51,11 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unsupported multi-objective Query Type."); break; } - swPrep.pause(); - storm::utility::Stopwatch swCheck; + swPrep.stop(); + storm::utility::Stopwatch swCheck(true); auto result = query->check(); - swCheck.pause(); - swPcaa.pause(); + swCheck.stop(); + swPcaa.stop(); std::cout << "STATISTICS_HEADERS;" << "States;"