From bfbd96a0e6ae41e493788c2391989cc26e489f35 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 2 Jan 2017 14:05:50 +0100 Subject: [PATCH 01/23] 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 02/23] 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 03/23] 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 04/23] 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 05/23] 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;" From f16f18bbf6b4033f558fbcfb2667201548bb4ab1 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 10 Feb 2017 11:08:05 +0100 Subject: [PATCH 06/23] fix in Matrix-vector multiplication --- src/storm/storage/SparseMatrix.cpp | 77 +++++++++++++++--------------- 1 file changed, 39 insertions(+), 38 deletions(-) diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 3f70b8f2a..42b762b64 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1165,7 +1165,7 @@ namespace storm { return result; } - + template void SparseMatrix::multiplyWithVector(std::vector const& vector, std::vector& result) const { #ifdef STORM_HAVE_INTELTBB @@ -1178,59 +1178,60 @@ namespace storm { return multiplyWithVectorSequential(vector, result); #endif } - + template void SparseMatrix::multiplyWithVectorSequential(std::vector const& vector, std::vector& result) const { - const_iterator it = this->begin(); - const_iterator ite; - std::vector::const_iterator rowIterator = rowIndications.begin(); - typename std::vector::iterator resultIterator = result.begin(); - typename std::vector::iterator resultIteratorEnd = result.end(); - - // If the vector to multiply with and the target vector are actually the same, we need an auxiliary variable - // to store the intermediate result. if (&vector == &result) { - for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) { - ValueType tmpValue = storm::utility::zero(); - - for (ite = this->begin() + *(rowIterator + 1); it != ite; ++it) { - tmpValue += it->getValue() * vector[it->getColumn()]; - } - *resultIterator = tmpValue; - } + STORM_LOG_WARN("Matrix-vector-multiplication invoked but the target vector uses the same memory as the input vector. This requires to allocate auxiliary memory."); + std::vector tmpVector(this->getRowCount()); + multiplyWithVectorSequential(vector, tmpVector); + result = std::move(tmpVector); } else { + const_iterator it = this->begin(); + const_iterator ite; + std::vector::const_iterator rowIterator = rowIndications.begin(); + typename std::vector::iterator resultIterator = result.begin(); + typename std::vector::iterator resultIteratorEnd = result.end(); + for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) { *resultIterator = storm::utility::zero(); - + for (ite = this->begin() + *(rowIterator + 1); it != ite; ++it) { *resultIterator += it->getValue() * vector[it->getColumn()]; } } } } - + #ifdef STORM_HAVE_INTELTBB template void SparseMatrix::multiplyWithVectorParallel(std::vector const& vector, std::vector& result) const { - tbb::parallel_for(tbb::blocked_range(0, result.size(), 10), - [&] (tbb::blocked_range const& range) { - index_type startRow = range.begin(); - index_type endRow = range.end(); - const_iterator it = this->begin(startRow); - const_iterator ite; - std::vector::const_iterator rowIterator = this->rowIndications.begin() + startRow; - std::vector::const_iterator rowIteratorEnd = this->rowIndications.begin() + endRow; - typename std::vector::iterator resultIterator = result.begin() + startRow; - typename std::vector::iterator resultIteratorEnd = result.begin() + endRow; - - for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) { - *resultIterator = storm::utility::zero(); - - for (ite = this->begin() + *(rowIterator + 1); it != ite; ++it) { - *resultIterator += it->getValue() * vector[it->getColumn()]; + if (&vector == &result) { + STORM_LOG_WARN("Matrix-vector-multiplication invoked but the target vector uses the same memory as the input vector. This requires to allocate auxiliary memory."); + std::vector tmpVector(this->getRowCount()); + multiplyWithVectorParallel(vector, tmpVector); + result = std::move(tmpVector); + } else { + tbb::parallel_for(tbb::blocked_range(0, result.size(), 10), + [&] (tbb::blocked_range const& range) { + index_type startRow = range.begin(); + index_type endRow = range.end(); + const_iterator it = this->begin(startRow); + const_iterator ite; + std::vector::const_iterator rowIterator = this->rowIndications.begin() + startRow; + std::vector::const_iterator rowIteratorEnd = this->rowIndications.begin() + endRow; + typename std::vector::iterator resultIterator = result.begin() + startRow; + typename std::vector::iterator resultIteratorEnd = result.begin() + endRow; + + for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) { + *resultIterator = storm::utility::zero(); + + for (ite = this->begin() + *(rowIterator + 1); it != ite; ++it) { + *resultIterator += it->getValue() * vector[it->getColumn()]; + } } - } - }); + }); + } } #endif From d15348ab8015477bdf5c8066c17c71f5a13be09a Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 10 Feb 2017 15:20:51 +0100 Subject: [PATCH 07/23] Fixed problem with recompiling when using ninja --- resources/3rdparty/include_cpptemplate.cmake | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/resources/3rdparty/include_cpptemplate.cmake b/resources/3rdparty/include_cpptemplate.cmake index 3cf4f43b4..ea2a9ba31 100644 --- a/resources/3rdparty/include_cpptemplate.cmake +++ b/resources/3rdparty/include_cpptemplate.cmake @@ -17,7 +17,7 @@ ExternalProject_Add( INSTALL_COMMAND "" BUILD_IN_SOURCE 0 LOG_BUILD ON - BUILD_BYPRODUCTS ${CPPTEMPLATE_LIB_DIR}/cpptemplate${DYNAMIC_EXT} ${CPPTEMPLATE_LIB_DIR}/cpptemplate${STATIC_EXT} + BUILD_BYPRODUCTS ${CPPTEMPLATE_LIB_DIR}/cpptemplate${STATIC_EXT} ) set(CPPTEMPLATE_INCLUDE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/cpptemplate) @@ -26,4 +26,4 @@ add_dependencies(resources cpptemplate) message(STATUS "storm - Linking with cpptemplate.") add_imported_library(cpptempl STATIC ${CPPTEMPLATE_STATIC_LIBRARY} ${CPPTEMPLATE_INCLUDE_DIR}) -list(APPEND STORM_DEP_TARGETS cpptempl_STATIC) \ No newline at end of file +list(APPEND STORM_DEP_TARGETS cpptempl_STATIC) From e70f7716fe6402232637446fe85456ee9c1bdb10 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 10 Feb 2017 17:29:37 +0100 Subject: [PATCH 08/23] Fixed minor pcaa bugs that were introduced due to recent changes --- .../pcaa/SparseMaPcaaWeightVectorChecker.cpp | 16 +-- .../pcaa/SparsePcaaWeightVectorChecker.cpp | 116 +++++++++--------- 2 files changed, 65 insertions(+), 67 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index b1c29d25b..df2864b34 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -358,14 +358,10 @@ namespace storm { // compute a choice vector for the probabilistic states that is optimal w.r.t. the weighted reward vector minMax.solver->solveEquations(PS.weightedSolutionVector, minMax.b); auto newScheduler = minMax.solver->getScheduler(); - if(consideredObjectives.getNumberOfSetBits() == 1 && !storm::utility::isZero(weightVector[*consideredObjectives.begin()])) { + if(consideredObjectives.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*consideredObjectives.begin()])) { // In this case there is no need to perform the computation on the individual objectives optimalChoicesAtCurrentEpoch = newScheduler->getChoices(); - auto objIndex = *consideredObjectives.begin(); - PS.objectiveSolutionVectors[objIndex] = PS.weightedSolutionVector; - if(!storm::utility::isOne(weightVector[objIndex])) { - storm::utility::vector::scaleVectorInPlace(PS.objectiveSolutionVectors[objIndex], storm::utility::one()/weightVector[objIndex]); - } + PS.objectiveSolutionVectors[*consideredObjectives.begin()] = PS.weightedSolutionVector; } else { // check whether the linEqSolver needs to be updated, i.e., whether the scheduler has changed if(linEq.solver == nullptr || newScheduler->getChoices() != optimalChoicesAtCurrentEpoch) { @@ -407,13 +403,9 @@ namespace storm { storm::utility::vector::addVectors(MS.weightedRewardVector, MS.auxChoiceValues, MS.weightedSolutionVector); MS.toPS.multiplyWithVector(PS.weightedSolutionVector, MS.auxChoiceValues); storm::utility::vector::addVectors(MS.weightedSolutionVector, MS.auxChoiceValues, MS.weightedSolutionVector); - if(consideredObjectives.getNumberOfSetBits() == 1 && !storm::utility::isZero(weightVector[*consideredObjectives.begin()])) { + if(consideredObjectives.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*consideredObjectives.begin()])) { // In this case there is no need to perform the computation on the individual objectives - auto objIndex = *consideredObjectives.begin(); - MS.objectiveSolutionVectors[objIndex] = MS.weightedSolutionVector; - if(!storm::utility::isOne(weightVector[objIndex])) { - storm::utility::vector::scaleVectorInPlace(MS.objectiveSolutionVectors[objIndex], storm::utility::one()/weightVector[objIndex]); - } + MS.objectiveSolutionVectors[*consideredObjectives.begin()] = MS.weightedSolutionVector; } else { for(auto objIndex : consideredObjectives) { MS.toMS.multiplyWithVector(MS.objectiveSolutionVectors[objIndex], MS.auxChoiceValues); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index 6a353d580..64d067d1e 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -158,65 +158,71 @@ namespace storm { template void SparsePcaaWeightVectorChecker::unboundedIndividualPhase(std::vector const& weightVector) { - - if(objectivesWithNoUpperTimeBound.getNumberOfSetBits()==1) { - auto objIndex = *objectivesWithNoUpperTimeBound.begin(); - objectiveResults[objIndex] = weightedResult; - if(!storm::utility::isZero(weightVector[objIndex])) { - storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], storm::utility::one()/weightVector[objIndex]); - } + if(objectivesWithNoUpperTimeBound.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*objectivesWithNoUpperTimeBound.begin()])) { + objectiveResults[*objectivesWithNoUpperTimeBound.begin()] = weightedResult; for (uint_fast64_t objIndex2 = 0; objIndex2 < objectives.size(); ++objIndex2) { - if(objIndex != objIndex2) { + if(*objectivesWithNoUpperTimeBound.begin() != objIndex2) { objectiveResults[objIndex2] = std::vector(model.getNumberOfStates(), storm::utility::zero()); } } - } else { - storm::storage::SparseMatrix deterministicMatrix = model.getTransitionMatrix().selectRowsFromRowGroups(this->scheduler.getChoices(), true); - storm::storage::SparseMatrix deterministicBackwardTransitions = deterministicMatrix.transpose(); - std::vector deterministicStateRewards(deterministicMatrix.getRowCount()); - storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; - - // We compute an estimate for the results of the individual objectives which is obtained from the weighted result and the result of the objectives computed so far. - // Note that weightedResult = Sum_{i=1}^{n} w_i * objectiveResult_i. - std::vector weightedSumOfUncheckedObjectives = weightedResult; - ValueType sumOfWeightsOfUncheckedObjectives = storm::utility::vector::sum_if(weightVector, objectivesWithNoUpperTimeBound); - - for(uint_fast64_t const& objIndex : storm::utility::vector::getSortedIndices(weightVector)) { - if(objectivesWithNoUpperTimeBound.get(objIndex)){ - offsetsToLowerBound[objIndex] = storm::utility::zero(); - offsetsToUpperBound[objIndex] = storm::utility::zero(); - storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), model.getTransitionMatrix().getRowGroupIndices(), discreteActionRewards[objIndex]); - storm::storage::BitVector statesWithRewards = ~storm::utility::vector::filterZero(deterministicStateRewards); - // As target states, we pick the states from which no reward is reachable. - storm::storage::BitVector targetStates = ~storm::utility::graph::performProbGreater0(deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards); - - // Compute the estimate for this objective - if(!storm::utility::isZero(weightVector[objIndex])) { - objectiveResults[objIndex] = weightedSumOfUncheckedObjectives; - storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], storm::utility::one() / sumOfWeightsOfUncheckedObjectives); - } - - // Make sure that the objectiveResult is initialized in some way - objectiveResults[objIndex].resize(model.getNumberOfStates(), storm::utility::zero()); - - // Invoke the linear equation solver - objectiveResults[objIndex] = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(deterministicMatrix, - deterministicBackwardTransitions, - deterministicStateRewards, - targetStates, - false, //no qualitative checking, - linearEquationSolverFactory, - objectiveResults[objIndex]); - // Update the estimate for the next objectives. - if(!storm::utility::isZero(weightVector[objIndex])) { - storm::utility::vector::addScaledVector(weightedSumOfUncheckedObjectives, objectiveResults[objIndex], -weightVector[objIndex]); - sumOfWeightsOfUncheckedObjectives -= weightVector[objIndex]; - } - } else { - objectiveResults[objIndex] = std::vector(model.getNumberOfStates(), storm::utility::zero()); - } - } - } + } else { + storm::storage::SparseMatrix deterministicMatrix = model.getTransitionMatrix().selectRowsFromRowGroups(this->scheduler.getChoices(), true); + storm::storage::SparseMatrix deterministicBackwardTransitions = deterministicMatrix.transpose(); + std::vector deterministicStateRewards(deterministicMatrix.getRowCount()); + storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; + + // We compute an estimate for the results of the individual objectives which is obtained from the weighted result and the result of the objectives computed so far. + // Note that weightedResult = Sum_{i=1}^{n} w_i * objectiveResult_i. + std::vector weightedSumOfUncheckedObjectives = weightedResult; + ValueType sumOfWeightsOfUncheckedObjectives = storm::utility::vector::sum_if(weightVector, objectivesWithNoUpperTimeBound); + + for (uint_fast64_t const &objIndex : storm::utility::vector::getSortedIndices(weightVector)) { + if (objectivesWithNoUpperTimeBound.get(objIndex)) { + offsetsToLowerBound[objIndex] = storm::utility::zero(); + offsetsToUpperBound[objIndex] = storm::utility::zero(); + storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), model.getTransitionMatrix().getRowGroupIndices(), discreteActionRewards[objIndex]); + storm::storage::BitVector statesWithRewards = ~storm::utility::vector::filterZero(deterministicStateRewards); + // As maybestates we pick the states from which a state with reward is reachable + storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0(deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards); + + // Compute the estimate for this objective + if (!storm::utility::isZero(weightVector[objIndex])) { + objectiveResults[objIndex] = weightedSumOfUncheckedObjectives; + storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], storm::utility::one() / sumOfWeightsOfUncheckedObjectives); + } + // Make sure that the objectiveResult is initialized correctly + objectiveResults[objIndex].resize(model.getNumberOfStates(), storm::utility::zero()); + + if (!maybeStates.empty()) { + storm::storage::SparseMatrix submatrix = deterministicMatrix.getSubmatrix( + true, maybeStates, maybeStates, true); + // Converting the matrix from the fixpoint notation to the form needed for the equation + // system. That is, we go from x = A*x + b to (I-A)x = b. + submatrix.convertToEquationSystem(); + + // Prepare solution vector and rhs of the equation system. + std::vector x = storm::utility::vector::filterVector(objectiveResults[objIndex], maybeStates); + std::vector b = storm::utility::vector::filterVector(deterministicStateRewards, maybeStates); + + // Now solve the resulting equation system. + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(submatrix)); + solver->solveEquations(x, b); + + // Set the result for this objective accordingly + storm::utility::vector::setVectorValues(objectiveResults[objIndex], maybeStates, x); + storm::utility::vector::setVectorValues(objectiveResults[objIndex], ~maybeStates, storm::utility::zero()); + } + + // Update the estimate for the next objectives. + if (!storm::utility::isZero(weightVector[objIndex])) { + storm::utility::vector::addScaledVector(weightedSumOfUncheckedObjectives, objectiveResults[objIndex], -weightVector[objIndex]); + sumOfWeightsOfUncheckedObjectives -= weightVector[objIndex]; + } + } else { + objectiveResults[objIndex] = std::vector(model.getNumberOfStates(), storm::utility::zero()); + } + } + } } template From eee1a84562238e35ab0877ed538b0c4cb868d21a Mon Sep 17 00:00:00 2001 From: JK Date: Mon, 6 Feb 2017 18:09:30 +0100 Subject: [PATCH 09/23] fix, BinaryNumericalFunctionExpression: simplify for pow(a,b) in double context should not cast result to integer [with Linda Leuschner] Small test case: dtmc const double x = 1E-2; const double y = pow(1-x, 10); module M1 s: [0..2] init 0; [] s = 0 -> y:(s'=1) + (1-y):(s'=2); endmodule should satisfy Pmax>0 [F (s = 1)]. --- .../storage/expressions/BinaryNumericalFunctionExpression.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp index 1c0a7908e..5524ca52d 100644 --- a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp @@ -99,7 +99,7 @@ namespace storm { case OperatorType::Times: newValue = firstOperandEvaluation * secondOperandEvaluation; break; case OperatorType::Min: newValue = std::min(firstOperandEvaluation, secondOperandEvaluation); break; case OperatorType::Max: newValue = std::max(firstOperandEvaluation, secondOperandEvaluation); break; - case OperatorType::Power: newValue = static_cast(std::pow(firstOperandEvaluation, secondOperandEvaluation)); break; + case OperatorType::Power: newValue = std::pow(firstOperandEvaluation, secondOperandEvaluation); break; case OperatorType::Divide: STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Unable to simplify division."); break; } return std::shared_ptr(new RationalLiteralExpression(this->getManager(), newValue)); From e37d0bd5522caddfd5b1c82505da339ad36e53bb Mon Sep 17 00:00:00 2001 From: JK Date: Wed, 8 Feb 2017 18:56:37 +0100 Subject: [PATCH 10/23] ToRationalNumberVisitor: make evaluator optional --- .../storage/expressions/ToRationalNumberVisitor.cpp | 13 ++++++++++++- .../storage/expressions/ToRationalNumberVisitor.h | 7 ++++--- 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp index 26ad15b5a..c8931c7f3 100644 --- a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp +++ b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp @@ -7,6 +7,11 @@ namespace storm { namespace expressions { + template + ToRationalNumberVisitor::ToRationalNumberVisitor() : ExpressionVisitor() { + // Intentionally left empty. + } + template ToRationalNumberVisitor::ToRationalNumberVisitor(ExpressionEvaluatorBase const& evaluator) : ExpressionVisitor(), evaluator(evaluator) { // Intentionally left empty. @@ -19,7 +24,13 @@ namespace storm { template boost::any ToRationalNumberVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) { - bool conditionValue = evaluator.asBool(expression.getCondition()); + bool conditionValue; + if (evaluator) { + conditionValue = evaluator->asBool(expression.getCondition()); + } else { + // no evaluator, fall back to evaluateBool + conditionValue = expression.getCondition()->evaluateAsBool(); + } if (conditionValue) { return expression.getThenExpression()->accept(*this, data); } else { diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.h b/src/storm/storage/expressions/ToRationalNumberVisitor.h index 89cb9f81f..55576e5ad 100644 --- a/src/storm/storage/expressions/ToRationalNumberVisitor.h +++ b/src/storm/storage/expressions/ToRationalNumberVisitor.h @@ -16,7 +16,8 @@ namespace storm { template class ToRationalNumberVisitor : public ExpressionVisitor { public: - ToRationalNumberVisitor(ExpressionEvaluatorBase const& evaluator); + ToRationalNumberVisitor(); + ToRationalNumberVisitor(ExpressionEvaluatorBase const& evaluator); RationalNumberType toRationalNumber(Expression const& expression); @@ -36,8 +37,8 @@ namespace storm { private: std::unordered_map valueMapping; - // A reference to an expression evaluator (mainly for resolving the boolean condition in IfThenElse expressions) - ExpressionEvaluatorBase const& evaluator; + // An optional reference to an expression evaluator (mainly for resolving the boolean condition in IfThenElse expressions) + boost::optional const&> evaluator; }; } } From edee041b16c56507a50295467a5fb2c1037dd059 Mon Sep 17 00:00:00 2001 From: JK Date: Wed, 8 Feb 2017 22:29:29 +0100 Subject: [PATCH 11/23] BaseExpression: evaluateAsRational --- src/storm/storage/expressions/BaseExpression.cpp | 8 +++++++- src/storm/storage/expressions/BaseExpression.h | 10 ++++++++++ 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/src/storm/storage/expressions/BaseExpression.cpp b/src/storm/storage/expressions/BaseExpression.cpp index 7780351eb..4e07fd089 100644 --- a/src/storm/storage/expressions/BaseExpression.cpp +++ b/src/storm/storage/expressions/BaseExpression.cpp @@ -5,6 +5,7 @@ #include "storm/exceptions/InvalidAccessException.h" #include "storm/storage/expressions/Expressions.h" +#include "storm/storage/expressions/ToRationalNumberVisitor.h" namespace storm { namespace expressions { @@ -51,7 +52,12 @@ namespace storm { double BaseExpression::evaluateAsDouble(Valuation const*) const { STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double."); } - + + storm::RationalNumber BaseExpression::evaluateAsRational() const { + ToRationalNumberVisitor v; + return v.toRationalNumber(this->toExpression()); + } + uint_fast64_t BaseExpression::getArity() const { return 0; } diff --git a/src/storm/storage/expressions/BaseExpression.h b/src/storm/storage/expressions/BaseExpression.h index 325aa33d4..83c76f7ae 100644 --- a/src/storm/storage/expressions/BaseExpression.h +++ b/src/storm/storage/expressions/BaseExpression.h @@ -7,6 +7,7 @@ #include #include +#include "storm/adapters/NumberAdapter.h" #include "storm/storage/expressions/Type.h" #include "storm/utility/OsDetection.h" #include @@ -90,6 +91,15 @@ namespace storm { */ virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const; + /*! + * Evaluates the expression and returns the resulting rational number. + * If the return type of the expression is not a rational number + * or the expression could not be evaluated, an exception is thrown. + * + * @return The rational number value of the expression. + */ + virtual storm::RationalNumber evaluateAsRational() const; + /*! * Returns the arity of the expression. * From eebfa07618b52907fe21ea6c363dfb9fb3132536 Mon Sep 17 00:00:00 2001 From: JK Date: Wed, 8 Feb 2017 22:31:16 +0100 Subject: [PATCH 12/23] expressions: do simplification involving rationals exactly --- .../BinaryNumericalFunctionExpression.cpp | 14 ++++++--- .../expressions/BinaryRelationExpression.cpp | 29 ++++++++++--------- .../UnaryNumericalFunctionExpression.cpp | 15 +++++----- 3 files changed, 33 insertions(+), 25 deletions(-) diff --git a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp index 5524ca52d..3d2e09153 100644 --- a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp @@ -1,6 +1,7 @@ #include #include +#include "storm/adapters/NumberAdapter.h" #include "storm/storage/expressions/BinaryNumericalFunctionExpression.h" #include "storm/storage/expressions/IntegerLiteralExpression.h" #include "storm/storage/expressions/RationalLiteralExpression.h" @@ -90,16 +91,21 @@ namespace storm { } return std::shared_ptr(new IntegerLiteralExpression(this->getManager(), newValue)); } else if (this->hasRationalType()) { - double firstOperandEvaluation = firstOperandSimplified->evaluateAsDouble(); - double secondOperandEvaluation = secondOperandSimplified->evaluateAsDouble(); - double newValue = 0; + storm::RationalNumber firstOperandEvaluation = firstOperandSimplified->evaluateAsRational(); + storm::RationalNumber secondOperandEvaluation = secondOperandSimplified->evaluateAsRational(); + storm::RationalNumber newValue = 0; switch (this->getOperatorType()) { case OperatorType::Plus: newValue = firstOperandEvaluation + secondOperandEvaluation; break; case OperatorType::Minus: newValue = firstOperandEvaluation - secondOperandEvaluation; break; case OperatorType::Times: newValue = firstOperandEvaluation * secondOperandEvaluation; break; case OperatorType::Min: newValue = std::min(firstOperandEvaluation, secondOperandEvaluation); break; case OperatorType::Max: newValue = std::max(firstOperandEvaluation, secondOperandEvaluation); break; - case OperatorType::Power: newValue = std::pow(firstOperandEvaluation, secondOperandEvaluation); break; + case OperatorType::Power: { + STORM_LOG_THROW(carl::isInteger(secondOperandEvaluation), storm::exceptions::InvalidStateException, "Can not simplify pow() with fractional exponent."); + std::size_t exponent = carl::toInt(secondOperandEvaluation); + newValue = carl::pow(firstOperandEvaluation, exponent); + break; + } case OperatorType::Divide: STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Unable to simplify division."); break; } return std::shared_ptr(new RationalLiteralExpression(this->getManager(), newValue)); diff --git a/src/storm/storage/expressions/BinaryRelationExpression.cpp b/src/storm/storage/expressions/BinaryRelationExpression.cpp index 7602fbf3c..a610802e8 100644 --- a/src/storm/storage/expressions/BinaryRelationExpression.cpp +++ b/src/storm/storage/expressions/BinaryRelationExpression.cpp @@ -4,6 +4,7 @@ #include "storm/storage/expressions/BooleanLiteralExpression.h" #include "storm/utility/macros.h" +#include "storm/utility/constants.h" #include "storm/exceptions/InvalidTypeException.h" #include "storm/storage/expressions/ExpressionVisitor.h" @@ -48,28 +49,28 @@ namespace storm { std::shared_ptr secondOperandSimplified = this->getSecondOperand()->simplify(); if (firstOperandSimplified->isLiteral() && secondOperandSimplified->isLiteral()) { - boost::variant firstOperandEvaluation; - boost::variant secondOperandEvaluation; - + storm::RationalNumber firstOperandEvaluation; + storm::RationalNumber secondOperandEvaluation; + if (firstOperandSimplified->hasIntegerType()) { - firstOperandEvaluation = firstOperandSimplified->evaluateAsInt(); + firstOperandEvaluation = storm::utility::convertNumber(firstOperandSimplified->evaluateAsInt()); } else { - firstOperandEvaluation = firstOperandSimplified->evaluateAsDouble(); + firstOperandEvaluation = firstOperandSimplified->evaluateAsRational(); } if (secondOperandSimplified->hasIntegerType()) { - secondOperandEvaluation = secondOperandSimplified->evaluateAsInt(); + secondOperandEvaluation = storm::utility::convertNumber(secondOperandSimplified->evaluateAsInt()); } else { - secondOperandEvaluation = secondOperandSimplified->evaluateAsDouble(); + secondOperandEvaluation = secondOperandSimplified->evaluateAsRational(); } - + bool truthValue = false; switch (this->getRelationType()) { - case RelationType::Equal: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get(firstOperandEvaluation) : boost::get(firstOperandEvaluation)) == (secondOperandSimplified->hasIntegerType() ? boost::get(secondOperandEvaluation) : boost::get(secondOperandEvaluation)); break; - case RelationType::NotEqual: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get(firstOperandEvaluation) : boost::get(firstOperandEvaluation)) != (secondOperandSimplified->hasIntegerType() ? boost::get(secondOperandEvaluation) : boost::get(secondOperandEvaluation)); break; - case RelationType::Greater: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get(firstOperandEvaluation) : boost::get(firstOperandEvaluation)) > (secondOperandSimplified->hasIntegerType() ? boost::get(secondOperandEvaluation) : boost::get(secondOperandEvaluation)); break; - case RelationType::GreaterOrEqual: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get(firstOperandEvaluation) : boost::get(firstOperandEvaluation)) >= (secondOperandSimplified->hasIntegerType() ? boost::get(secondOperandEvaluation) : boost::get(secondOperandEvaluation)); break; - case RelationType::Less: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get(firstOperandEvaluation) : boost::get(firstOperandEvaluation)) < (secondOperandSimplified->hasIntegerType() ? boost::get(secondOperandEvaluation) : boost::get(secondOperandEvaluation)); break; - case RelationType::LessOrEqual: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get(firstOperandEvaluation) : boost::get(firstOperandEvaluation)) <= (secondOperandSimplified->hasIntegerType() ? boost::get(secondOperandEvaluation) : boost::get(secondOperandEvaluation)); break; + case RelationType::Equal: truthValue = firstOperandEvaluation == secondOperandEvaluation; break; + case RelationType::NotEqual: truthValue = firstOperandEvaluation != secondOperandEvaluation; break; + case RelationType::Greater: truthValue = firstOperandEvaluation > secondOperandEvaluation; break; + case RelationType::GreaterOrEqual: truthValue = firstOperandEvaluation >= secondOperandEvaluation; break; + case RelationType::Less: truthValue = firstOperandEvaluation < secondOperandEvaluation; break; + case RelationType::LessOrEqual: truthValue = firstOperandEvaluation <= secondOperandEvaluation; break; } return std::shared_ptr(new BooleanLiteralExpression(this->getManager(), truthValue)); } diff --git a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp index 2382e1399..9fc2c5639 100644 --- a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp +++ b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp @@ -2,11 +2,13 @@ #include +#include "storm/adapters/NumberAdapter.h" #include "storm/storage/expressions/UnaryNumericalFunctionExpression.h" #include "storm/storage/expressions/IntegerLiteralExpression.h" #include "storm/storage/expressions/RationalLiteralExpression.h" #include "ExpressionVisitor.h" #include "storm/utility/macros.h" +#include "storm/utility/constants.h" #include "storm/exceptions/InvalidTypeException.h" #include "storm/exceptions/InvalidOperationException.h" @@ -65,14 +67,13 @@ namespace storm { std::shared_ptr operandSimplified = this->getOperand()->simplify(); if (operandSimplified->isLiteral()) { - boost::variant operandEvaluation; + boost::variant operandEvaluation; if (operandSimplified->hasIntegerType()) { operandEvaluation = operandSimplified->evaluateAsInt(); } else { - operandEvaluation = operandSimplified->evaluateAsDouble(); + operandEvaluation = operandSimplified->evaluateAsRational(); } - boost::variant result; if (operandSimplified->hasIntegerType()) { int_fast64_t value = 0; switch (this->getOperatorType()) { @@ -82,11 +83,11 @@ namespace storm { } return std::shared_ptr(new IntegerLiteralExpression(this->getManager(), value)); } else { - double value = 0; + storm::RationalNumber value = storm::utility::zero(); switch (this->getOperatorType()) { - case OperatorType::Minus: value = -boost::get(operandEvaluation); break; - case OperatorType::Floor: value = std::floor(boost::get(operandEvaluation)); break; - case OperatorType::Ceil: value = std::ceil(boost::get(operandEvaluation)); break; + case OperatorType::Minus: value = -boost::get(operandEvaluation); break; + case OperatorType::Floor: value = carl::floor(boost::get(operandEvaluation)); break; + case OperatorType::Ceil: value = carl::ceil(boost::get(operandEvaluation)); break; } return std::shared_ptr(new RationalLiteralExpression(this->getManager(), value)); } From b623b4184e95b8421b3b68f3af3ab052eae25ad1 Mon Sep 17 00:00:00 2001 From: JK Date: Thu, 9 Feb 2017 10:37:48 +0100 Subject: [PATCH 13/23] constants.cpp: convertNumber(int_fast64_t) to RationalFunction, fix signed/unsigned cast --- src/storm/utility/constants.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index a6326d5e8..34a34ab04 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -397,7 +397,7 @@ namespace storm { template<> RationalFunction convertNumber(int_fast64_t const& number){ STORM_LOG_ASSERT(static_cast(number) == number, "Rationalizing failed, because the number is too large."); - return RationalFunction(carl::rationalize(static_cast(number))); + return RationalFunction(carl::rationalize(static_cast(number))); } template<> From 3c5c609e273bde33643c900e58368ea02a4d4101 Mon Sep 17 00:00:00 2001 From: JK Date: Thu, 9 Feb 2017 10:55:45 +0100 Subject: [PATCH 14/23] utility/cli.cpp, parseConstantDefinitionString: do constants parsing using rational number (exact) Uses convertNumber to obtain a rational number for double constants. Additionally, improve error message if something goes wrong during conversion. --- src/storm/utility/cli.cpp | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/storm/utility/cli.cpp b/src/storm/utility/cli.cpp index d7606149b..4798fd531 100644 --- a/src/storm/utility/cli.cpp +++ b/src/storm/utility/cli.cpp @@ -1,6 +1,7 @@ #include "storm/utility/cli.h" #include "storm/utility/macros.h" +#include "storm/utility/constants.h" #include "storm/exceptions/WrongFormatException.h" namespace storm { @@ -52,8 +53,12 @@ namespace storm { int_fast64_t integerValue = std::stoi(value); constantDefinitions[variable] = manager.integer(integerValue); } else if (variable.hasRationalType()) { - double doubleValue = std::stod(value); - constantDefinitions[variable] = manager.rational(doubleValue); + try { + storm::RationalNumber rationalValue = storm::utility::convertNumber(value); + constantDefinitions[variable] = manager.rational(rationalValue); + } catch (std::exception& e) { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Illegal constant definition string '" << constantName << "=" << value << "': " << e.what()); + } } } else { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Illegal constant definition string: unknown undefined constant '" << constantName << "'."); From d602d2660d93b580c45e26ed59a7b7f6810f5c02 Mon Sep 17 00:00:00 2001 From: JK Date: Mon, 13 Feb 2017 15:58:04 +0100 Subject: [PATCH 15/23] utility/constants.cpp: switch to carl::parse from carl::rationalize carl::parse supports more syntax variants for specifying rational numbers, e.g., 1.23e-10 (scientific notation), 1/24 (fractions), ... --- src/storm/utility/constants.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index 34a34ab04..f2d2b98a8 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -402,7 +402,7 @@ namespace storm { template<> RationalNumber convertNumber(std::string const& number) { - return carl::rationalize(number); + return carl::parse(number); } template<> From 9c581bd6350679cf0739b16a59a6e4e9c266fe07 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 14 Feb 2017 10:21:18 +0100 Subject: [PATCH 16/23] fixed two issues: missing include in ToRationalNumberVisitor and missing check for whether actions are reused in a JANI parallel composition --- .../storage/expressions/ToRationalNumberVisitor.h | 2 ++ src/storm/storage/jani/Model.cpp | 2 +- src/storm/storage/jani/ParallelComposition.cpp | 6 ++++-- src/test/builder/DdJaniModelBuilderTest.cpp | 10 ++++++++-- 4 files changed, 15 insertions(+), 5 deletions(-) diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.h b/src/storm/storage/expressions/ToRationalNumberVisitor.h index 55576e5ad..1f2b88f48 100644 --- a/src/storm/storage/expressions/ToRationalNumberVisitor.h +++ b/src/storm/storage/expressions/ToRationalNumberVisitor.h @@ -2,6 +2,8 @@ #include +#include + #include "storm/adapters/CarlAdapter.h" #include "storm/storage/expressions/Expression.h" diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 083b8f7fb..8f6791441 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -1134,7 +1134,7 @@ namespace storm { } bool Model::reusesActionsInComposition() const { - if(composition->isParallelComposition()) { + if (composition->isParallelComposition()) { return composition->asParallelComposition().areActionsReused(); } return false; diff --git a/src/storm/storage/jani/ParallelComposition.cpp b/src/storm/storage/jani/ParallelComposition.cpp index 1eaa0ff08..d81db1d91 100644 --- a/src/storm/storage/jani/ParallelComposition.cpp +++ b/src/storm/storage/jani/ParallelComposition.cpp @@ -195,13 +195,15 @@ namespace storm { for (auto const& vector : synchronizationVectors) { std::string const& action = vector.getInput(inputIndex); if (action != SynchronizationVector::NO_ACTION_INPUT) { - return true; + if (actions.find(action) != actions.end()) { + return true; + } actions.insert(action); } } // And check recursively, in case we have nested parallel composition if (subcompositions.at(inputIndex)->isParallelComposition()) { - if(subcompositions.at(inputIndex)->asParallelComposition().areActionsReused()) { + if (subcompositions.at(inputIndex)->asParallelComposition().areActionsReused()) { return true; } } diff --git a/src/test/builder/DdJaniModelBuilderTest.cpp b/src/test/builder/DdJaniModelBuilderTest.cpp index 14f5e8081..2622662dc 100644 --- a/src/test/builder/DdJaniModelBuilderTest.cpp +++ b/src/test/builder/DdJaniModelBuilderTest.cpp @@ -17,6 +17,8 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/IOSettings.h" +#include "storm/exceptions/InvalidSettingsException.h" + TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) { storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); @@ -363,7 +365,9 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) { inputVector.push_back("c"); inputVector.push_back("b"); synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "e")); - EXPECT_THROW(newComposition = std::make_shared(automataCompositions, synchronizationVectors), storm::exceptions::WrongFormatException); + newComposition = std::make_shared(automataCompositions, synchronizationVectors); + janiModel.setSystemComposition(newComposition); + EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::InvalidSettingsException); } TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) { @@ -419,7 +423,9 @@ TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) { inputVector.push_back("c"); inputVector.push_back("b"); synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "e")); - EXPECT_THROW(newComposition = std::make_shared(automataCompositions, synchronizationVectors), storm::exceptions::WrongFormatException); + newComposition = std::make_shared(automataCompositions, synchronizationVectors); + janiModel.setSystemComposition(newComposition); + EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::InvalidSettingsException); } TEST(DdJaniModelBuilderTest_Sylvan, Composition) { From 75130ab727ffb6ff4ff587c65f570a4d8db66cb3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 14 Feb 2017 10:38:46 +0100 Subject: [PATCH 17/23] added patch by Joachim Klein that forwards the boost version storm found to carl --- resources/3rdparty/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 64fc5d7b3..8c013f86f 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -201,7 +201,7 @@ if(USE_CARL) message("START CARL CONFIG PROCESS") file(MAKE_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download) execute_process( - COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}" + COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}" "-DBoost_LIBRARY_DIRS=${Boost_LIBRARY_DIRS}" "-DBoost_INCLUDE_DIRS=${Boost_INCLUDE_DIRS}" WORKING_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download OUTPUT_VARIABLE carlconfig_out RESULT_VARIABLE carlconfig_result) From 5d79eff2cd55cdfa4057d2c613fdfabe84363e7e Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 14 Feb 2017 18:25:26 +0100 Subject: [PATCH 18/23] Wrapper for file opening --- .../modelchecker/dft/DFTASFChecker.cpp | 23 +++--- src/storm-dft/parser/DFTGalileoParser.cpp | 17 ++-- src/storm-dft/parser/DFTJsonParser.cpp | 14 +--- src/storm-gspn-cli/storm-gspn.cpp | 8 +- src/storm-gspn/storm-gspn.h | 20 ++--- src/storm-pgcl-cli/storm-pgcl.cpp | 11 +-- src/storm-pgcl/parser/PgclParser.cpp | 9 ++- src/storm/abstraction/MenuGameAbstractor.cpp | 5 +- src/storm/cli/entrypoints.h | 8 +- .../modelchecker/region/ParameterRegion.cpp | 5 +- .../AtomicPropositionLabelingParser.cpp | 5 -- .../DeterministicSparseTransitionParser.cpp | 5 -- src/storm/parser/FormulaParser.cpp | 9 ++- src/storm/parser/JaniParser.cpp | 14 +--- src/storm/parser/MappedFile.cpp | 18 ++--- src/storm/parser/MappedFile.h | 8 -- .../MarkovAutomatonSparseTransitionParser.cpp | 5 -- ...NondeterministicSparseTransitionParser.cpp | 5 -- src/storm/parser/PrismParser.cpp | 10 +-- .../parser/SparseChoiceLabelingParser.cpp | 5 -- src/storm/parser/SparseStateRewardParser.cpp | 5 -- src/storm/settings/SettingsManager.cpp | 8 +- src/storm/solver/SmtlibSmtSolver.cpp | 13 +-- src/storm/storage/dd/Odd.cpp | 6 +- src/storm/storage/jani/JSONExporter.cpp | 18 ++--- src/storm/utility/export.h | 15 +--- src/storm/utility/file.h | 81 +++++++++++++++++++ src/storm/utility/storm.h | 13 +-- src/test/parser/MappedFileTest.cpp | 7 +- 29 files changed, 188 insertions(+), 182 deletions(-) create mode 100644 src/storm/utility/file.h diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 0d6cf2e31..55d968a2c 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -1,5 +1,6 @@ #include "DFTASFChecker.h" #include +#include "storm/utility/file.h" namespace storm { @@ -394,24 +395,22 @@ namespace storm { } void DFTASFChecker::toFile(std::string const& filename) { - std::ofstream ofs; - std::cout << "Writing to " << filename << std::endl; - ofs.open(filename); - ofs << "; time point variables" << std::endl; + std::ofstream stream; + storm::utility::openFile(filename, stream); + stream << "; time point variables" << std::endl; for (auto const& timeVarEntry : timePointVariables) { - ofs << "(declare-fun " << varNames[timeVarEntry.second] << "() Int)" << std::endl; + stream << "(declare-fun " << varNames[timeVarEntry.second] << "() Int)" << std::endl; } - ofs << "; claim variables" << std::endl; + stream << "; claim variables" << std::endl; for (auto const& claimVarEntry : claimVariables) { - ofs << "(declare-fun " << varNames[claimVarEntry.second] << "() Int)" << std::endl; + stream << "(declare-fun " << varNames[claimVarEntry.second] << "() Int)" << std::endl; } for (auto const& constraint : constraints) { - ofs << "; " << constraint->description() << std::endl; - ofs << "(assert " << constraint->toSmtlib2(varNames) << ")" << std::endl; + stream << "; " << constraint->description() << std::endl; + stream << "(assert " << constraint->toSmtlib2(varNames) << ")" << std::endl; } - ofs << "(check-sat)" << std::endl; - ofs.close(); - + stream << "(check-sat)" << std::endl; + storm::utility::closeFile(stream); } } } diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp index f872f4526..c5a88716c 100644 --- a/src/storm-dft/parser/DFTGalileoParser.cpp +++ b/src/storm-dft/parser/DFTGalileoParser.cpp @@ -10,6 +10,7 @@ #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/NotSupportedException.h" #include "storm/utility/macros.h" +#include "storm/utility/file.h" namespace storm { namespace parser { @@ -49,18 +50,10 @@ namespace storm { std::string parametricToken = "param"; std::ifstream file; - file.exceptions ( std::ifstream::failbit ); - try { - file.open(filename); - } - catch (std::ifstream::failure e) { - STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Exception during file opening on " << filename << "."); - return; - } - file.exceptions( std::ifstream::goodbit ); - + storm::utility::openFile(filename, file); std::string line; - while(std::getline(file, line)) { + + while (std::getline(file, line)) { bool success = true; STORM_LOG_TRACE("Parsing: " << line); size_t commentstarts = line.find("//"); @@ -143,7 +136,7 @@ namespace storm { if(!builder.setTopLevel(toplevelId)) { STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Top level id unknown."); } - file.close(); + storm::utility::closeFile(file); } template diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 9a5c5d047..faff4a099 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -10,6 +10,7 @@ #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/NotSupportedException.h" #include "storm/utility/macros.h" +#include "storm/utility/file.h" namespace storm { namespace parser { @@ -52,19 +53,10 @@ namespace storm { STORM_LOG_DEBUG("Parsing from JSON"); std::ifstream file; - file.exceptions ( std::ifstream::failbit ); - try { - file.open(filename); - } - catch (std::ifstream::failure e) { - STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Exception during file opening on " << filename << "."); - return; - } - file.exceptions( std::ifstream::goodbit ); - + storm::utility::openFile(filename, file); json parsedJson; parsedJson << file; - file.close(); + storm::utility::closeFile(file); // Start by building mapping from ids to names std::map nameMapping; diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index 2dd98e645..bbff2c9cc 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/src/storm-gspn-cli/storm-gspn.cpp @@ -56,19 +56,19 @@ void initializeSettings() { std::unordered_map parseCapacitiesList(std::string const& filename) { std::unordered_map map; - std::ifstream ifs; - ifs.open(filename); + std::ifstream stream; + storm::utility::openFile(filename, stream); std::string line; - while( std::getline(ifs, line) ) { + while ( std::getline(stream, line) ) { std::vector strs; boost::split(strs, line, boost::is_any_of("\t ")); STORM_LOG_THROW(strs.size() == 2, storm::exceptions::WrongFormatException, "Expect key value pairs"); std::cout << std::stoll(strs[1]) << std::endl; map[strs[0]] = std::stoll(strs[1]); } + storm::utility::closeFile(stream); return map; - } diff --git a/src/storm-gspn/storm-gspn.h b/src/storm-gspn/storm-gspn.h index de3811109..d043ce53d 100644 --- a/src/storm-gspn/storm-gspn.h +++ b/src/storm-gspn/storm-gspn.h @@ -8,6 +8,8 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GSPNExportSettings.h" +#include "storm/utility/file.h" + namespace storm { /** * Builds JANI model from GSPN. @@ -21,23 +23,23 @@ namespace storm { storm::settings::modules::GSPNExportSettings const& exportSettings = storm::settings::getModule(); if (exportSettings.isWriteToDotSet()) { std::ofstream fs; - fs.open(exportSettings.getWriteToDotFilename()); + storm::utility::openFile(exportSettings.getWriteToDotFilename(), fs); gspn.writeDotToStream(fs); - fs.close(); + storm::utility::closeFile(fs); } if (exportSettings.isWriteToPnproSet()) { std::ofstream fs; - fs.open(exportSettings.getWriteToPnproFilename()); + storm::utility::openFile(exportSettings.getWriteToPnproFilename(), fs); gspn.toPnpro(fs); - fs.close(); + storm::utility::closeFile(fs); } if (exportSettings.isWriteToPnmlSet()) { std::ofstream fs; - fs.open(exportSettings.getWriteToPnmlFilename()); + storm::utility::openFile(exportSettings.getWriteToPnmlFilename(), fs); gspn.toPnml(fs); - fs.close(); + storm::utility::closeFile(fs); } if (exportSettings.isDisplayStatsSet()) { @@ -48,13 +50,13 @@ namespace storm { if (exportSettings.isWriteStatsToFileSet()) { std::ofstream fs; - fs.open(exportSettings.getWriteStatsFilename()); + storm::utility::openFile(exportSettings.getWriteStatsFilename(), fs); gspn.writeStatsToStream(fs); - fs.close(); + storm::utility::closeFile(fs); } } -} \ No newline at end of file +} diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp index 6a6707177..2fa9385a2 100644 --- a/src/storm-pgcl-cli/storm-pgcl.cpp +++ b/src/storm-pgcl-cli/storm-pgcl.cpp @@ -47,13 +47,10 @@ void handleJani(storm::jani::Model& model) { void programGraphToDotFile(storm::ppg::ProgramGraph const& prog) { std::string filepath = storm::settings::getModule().getProgramGraphDotOutputFilename(); - std::ofstream ofs; - ofs.open(filepath, std::ofstream::out ); - if (ofs.is_open()) { - prog.printDot(ofs); - } else { - STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Cannot open " << filepath); - } + std::ofstream stream; + storm::utility::openFile(filepath, stream); + prog.printDot(stream); + storm::utility::closeFile(stream); } int main(const int argc, const char** argv) { diff --git a/src/storm-pgcl/parser/PgclParser.cpp b/src/storm-pgcl/parser/PgclParser.cpp index ca264de5f..6ecde3054 100755 --- a/src/storm-pgcl/parser/PgclParser.cpp +++ b/src/storm-pgcl/parser/PgclParser.cpp @@ -1,6 +1,7 @@ #include "PgclParser.h" // If the parser fails due to ill-formed data, this exception is thrown. #include "storm/exceptions/WrongFormatException.h" +#include "storm/utility/file.h" namespace storm { namespace parser { @@ -9,8 +10,8 @@ namespace storm { storm::pgcl::PgclProgram result; // Open file and initialize result. - std::ifstream inputFileStream(filename, std::ios::in); - STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'."); + std::ifstream inputFileStream; + storm::utility::openFile(filename, inputFileStream); // Now try to parse the contents of the file. try { @@ -18,12 +19,12 @@ namespace storm { result = parseFromString(fileContent, filename); } catch(std::exception& e) { // In case of an exception properly close the file before passing exception. - inputFileStream.close(); + storm::utility::closeFile(inputFileStream); throw e; } // Close the stream in case everything went smoothly and return result. - inputFileStream.close(); + storm::utility::closeFile(inputFileStream); return result; } diff --git a/src/storm/abstraction/MenuGameAbstractor.cpp b/src/storm/abstraction/MenuGameAbstractor.cpp index 164802c2b..9a0071571 100644 --- a/src/storm/abstraction/MenuGameAbstractor.cpp +++ b/src/storm/abstraction/MenuGameAbstractor.cpp @@ -7,6 +7,7 @@ #include "storm/storage/dd/Add.h" #include "storm/storage/dd/Bdd.h" #include "storm/utility/dd.h" +#include "storm/utility/file.h" #include "storm-config.h" #include "storm/adapters/CarlAdapter.h" @@ -47,7 +48,8 @@ namespace storm { template void MenuGameAbstractor::exportToDot(storm::abstraction::MenuGame const& currentGame, std::string const& filename, storm::dd::Bdd const& highlightStatesBdd, storm::dd::Bdd const& filter) const { - std::ofstream out(filename); + std::ofstream out; + storm::utility::openFile(filename, out); AbstractionInformation const& abstractionInformation = this->getAbstractionInformation(); storm::dd::Add filteredTransitions = filter.template toAdd() * currentGame.getTransitionMatrix(); @@ -130,6 +132,7 @@ namespace storm { } out << "}" << std::endl; + storm::utility::closeFile(out); } template class MenuGameAbstractor; diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index 3d1a9397e..79b030fb8 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -324,10 +324,10 @@ namespace storm { // And export if required. if(storm::settings::getModule().isExportExplicitSet()) { - std::ofstream ofs; - ofs.open(storm::settings::getModule().getExportExplicitFilename(), std::ofstream::out); - storm::exporter::explicitExportSparseModel(ofs, sparseModel, model.getParameterNames()); - ofs.close(); + std::ofstream stream; + storm::utility::openFile(storm::settings::getModule().getExportExplicitFilename(), stream); + storm::exporter::explicitExportSparseModel(stream, sparseModel, model.getParameterNames()); + storm::utility::closeFile(stream); } } diff --git a/src/storm/modelchecker/region/ParameterRegion.cpp b/src/storm/modelchecker/region/ParameterRegion.cpp index 27b683e8b..d328831fc 100644 --- a/src/storm/modelchecker/region/ParameterRegion.cpp +++ b/src/storm/modelchecker/region/ParameterRegion.cpp @@ -7,7 +7,8 @@ #include "storm/settings/modules/RegionSettings.h" #include "storm/exceptions/InvalidSettingsException.h" #include "storm/exceptions/InvalidArgumentException.h" -#include "utility/constants.h" +#include "storm/utility/constants.h" +#include "storm/utility/file.h" namespace storm { namespace modelchecker { @@ -283,7 +284,7 @@ namespace storm { } else{ //if we reach this point we can assume that the region is given as a file. - STORM_LOG_THROW(storm::parser::MappedFile::fileExistsAndIsReadable(storm::settings::getModule().getRegionFilePath().c_str()), storm::exceptions::InvalidSettingsException, "The path to the file in which the regions are specified is not valid."); + STORM_LOG_THROW(storm::utility::fileExistsAndIsReadable(storm::settings::getModule().getRegionFilePath()), storm::exceptions::InvalidSettingsException, "The path to the file in which the regions are specified is not valid."); storm::parser::MappedFile mf(storm::settings::getModule().getRegionFilePath().c_str()); regionsString = std::string(mf.getData(),mf.getDataSize()); } diff --git a/src/storm/parser/AtomicPropositionLabelingParser.cpp b/src/storm/parser/AtomicPropositionLabelingParser.cpp index bbb555460..4d55b4fe8 100644 --- a/src/storm/parser/AtomicPropositionLabelingParser.cpp +++ b/src/storm/parser/AtomicPropositionLabelingParser.cpp @@ -24,11 +24,6 @@ namespace storm { storm::models::sparse::StateLabeling AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(uint_fast64_t stateCount, std::string const & filename) { // Open the given file. - if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) { - STORM_LOG_ERROR("Error while parsing " << filename << ": The supplied Labeling input file does not exist or is not readable by this process."); - throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": The supplied Labeling input file does not exist or is not readable by this process."; - } - MappedFile file(filename.c_str()); char const* buf = file.getData(); diff --git a/src/storm/parser/DeterministicSparseTransitionParser.cpp b/src/storm/parser/DeterministicSparseTransitionParser.cpp index 7b53415cb..9aacb7e4c 100644 --- a/src/storm/parser/DeterministicSparseTransitionParser.cpp +++ b/src/storm/parser/DeterministicSparseTransitionParser.cpp @@ -41,11 +41,6 @@ namespace storm { // Enforce locale where decimal point is '.'. setlocale(LC_NUMERIC, "C"); - if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) { - STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable."); - throw storm::exceptions::FileIoException() << "The supplied Transition input file \"" << filename << "\" does not exist or is not readable by this process."; - } - // Open file. MappedFile file(filename.c_str()); char const* buf = file.getData(); diff --git a/src/storm/parser/FormulaParser.cpp b/src/storm/parser/FormulaParser.cpp index 6bb1687dc..e592f141c 100644 --- a/src/storm/parser/FormulaParser.cpp +++ b/src/storm/parser/FormulaParser.cpp @@ -15,6 +15,7 @@ #include "storm/storage/expressions/ExpressionEvaluator.h" #include "FormulaParserGrammar.h" #include "storm/storage/expressions/ExpressionManager.h" +#include "storm/utility/file.h" namespace storm { namespace parser { @@ -65,8 +66,8 @@ namespace storm { std::vector FormulaParser::parseFromFile(std::string const& filename) const { // Open file and initialize result. - std::ifstream inputFileStream(filename, std::ios::in); - STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'."); + std::ifstream inputFileStream; + storm::utility::openFile(filename, inputFileStream); std::vector properties; @@ -76,12 +77,12 @@ namespace storm { properties = parseFromString(fileContent); } catch(std::exception& e) { // In case of an exception properly close the file before passing exception. - inputFileStream.close(); + storm::utility::closeFile(inputFileStream); throw e; } // Close the stream in case everything went smoothly and return result. - inputFileStream.close(); + storm::utility::closeFile(inputFileStream); return properties; } diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index c8f0c15e8..826c8075b 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -18,6 +18,7 @@ #include #include "storm/utility/macros.h" +#include "storm/utility/file.h" namespace storm { namespace parser { @@ -64,18 +65,9 @@ namespace storm { void JaniParser::readFile(std::string const &path) { std::ifstream file; - file.exceptions ( std::ifstream::failbit ); - try { - file.open(path); - } - catch (std::ifstream::failure e) { - STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Exception during file opening on " << path << "."); - return; - } - file.exceptions( std::ifstream::goodbit ); - + storm::utility::openFile(path, file); parsedStructure << file; - file.close(); + storm::utility::closeFile(file); } std::pair> JaniParser::parseModel(bool parseProperties) { diff --git a/src/storm/parser/MappedFile.cpp b/src/storm/parser/MappedFile.cpp index e731ebf18..5b9f02714 100644 --- a/src/storm/parser/MappedFile.cpp +++ b/src/storm/parser/MappedFile.cpp @@ -15,10 +15,14 @@ #include "storm/exceptions/FileIoException.h" #include "storm/utility/macros.h" +#include "storm/utility/file.h" + namespace storm { namespace parser { MappedFile::MappedFile(const char* filename) { + STORM_LOG_THROW(storm::utility::fileExistsAndIsReadable(filename), storm::exceptions::FileIoException, "Error while reading " << filename << ": The file does not exist or is not readable."); + #if defined LINUX || defined MACOSX // Do file mapping for reasonable systems. @@ -29,15 +33,11 @@ namespace storm { #else if (stat64(filename, &(this->st)) != 0) { #endif - STORM_LOG_ERROR("Error in stat(" << filename << "): Probably, this file does not exist."); - throw exceptions::FileIoException() << "MappedFile Error in stat(): Probably, this file does not exist."; + STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Error in stat(" << filename << "): Probably, this file does not exist."); } this->file = open(filename, O_RDONLY); - if (this->file < 0) { - STORM_LOG_ERROR("Error in open(" << filename << "): Probably, we may not read this file."); - throw exceptions::FileIoException() << "MappedFile Error in open(): Probably, we may not read this file."; - } + STORM_LOG_THROW(this->file >= 0, storm::exceptions::FileIoException, "Error in open(" << filename << "): Probably, we may not read this file."); this->data = static_cast(mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0)); if (this->data == MAP_FAILED) { @@ -90,12 +90,6 @@ namespace storm { #endif } - bool MappedFile::fileExistsAndIsReadable(const char* filename) { - // Test by opening an input file stream and testing the stream flags. - std::ifstream fin(filename); - return fin.good(); - } - char const* MappedFile::getData() const { return data; } diff --git a/src/storm/parser/MappedFile.h b/src/storm/parser/MappedFile.h index f1be7f83c..aeeb7fa6f 100644 --- a/src/storm/parser/MappedFile.h +++ b/src/storm/parser/MappedFile.h @@ -49,14 +49,6 @@ namespace storm { */ ~MappedFile(); - /*! - * Tests whether the given file exists and is readable. - *qi - * @param filename Path and name of the file to be tested. - * @return True iff the file exists and is readable. - */ - static bool fileExistsAndIsReadable(const char* filename); - /*! * Returns a pointer to the beginning of the mapped file data. * diff --git a/src/storm/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/storm/parser/MarkovAutomatonSparseTransitionParser.cpp index 271f22516..25b62a2e2 100644 --- a/src/storm/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/storm/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -294,11 +294,6 @@ namespace storm { // Set the locale to correctly recognize floating point numbers. setlocale(LC_NUMERIC, "C"); - if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) { - STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable."); - throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": File does not exist or is not readable."; - } - // Open file and prepare pointer to buffer. MappedFile file(filename.c_str()); char const* buf = file.getData(); diff --git a/src/storm/parser/NondeterministicSparseTransitionParser.cpp b/src/storm/parser/NondeterministicSparseTransitionParser.cpp index a9e1b53b1..f9a1947b9 100644 --- a/src/storm/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/storm/parser/NondeterministicSparseTransitionParser.cpp @@ -39,11 +39,6 @@ namespace storm { // Enforce locale where decimal point is '.'. setlocale(LC_NUMERIC, "C"); - if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) { - STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable."); - throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": File does not exist or is not readable."; - } - // Open file. MappedFile file(filename.c_str()); char const* buf = file.getData(); diff --git a/src/storm/parser/PrismParser.cpp b/src/storm/parser/PrismParser.cpp index 436d27c5d..62ef9eebe 100644 --- a/src/storm/parser/PrismParser.cpp +++ b/src/storm/parser/PrismParser.cpp @@ -7,6 +7,7 @@ #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidTypeException.h" #include "storm/utility/macros.h" +#include "storm/utility/file.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/storage/expressions/ExpressionManager.h" @@ -17,9 +18,8 @@ namespace storm { namespace parser { storm::prism::Program PrismParser::parse(std::string const& filename) { // Open file and initialize result. - std::ifstream inputFileStream(filename); - STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'."); - + std::ifstream inputFileStream; + storm::utility::openFile(filename, inputFileStream); storm::prism::Program result; // Now try to parse the contents of the file. @@ -28,12 +28,12 @@ namespace storm { result = parseFromString(fileContent, filename); } catch(std::exception& e) { // In case of an exception properly close the file before passing exception. - inputFileStream.close(); + storm::utility::closeFile(inputFileStream); throw e; } // Close the stream in case everything went smoothly and return result. - inputFileStream.close(); + storm::utility::closeFile(inputFileStream); return result; } diff --git a/src/storm/parser/SparseChoiceLabelingParser.cpp b/src/storm/parser/SparseChoiceLabelingParser.cpp index c73d1def4..26395d057 100644 --- a/src/storm/parser/SparseChoiceLabelingParser.cpp +++ b/src/storm/parser/SparseChoiceLabelingParser.cpp @@ -13,11 +13,6 @@ namespace storm { std::vector SparseChoiceLabelingParser::parseChoiceLabeling(std::vector const& nondeterministicChoiceIndices, std::string const& filename) { // Open file. - if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) { - STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable."); - throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": File does not exist or is not readable."; - } - MappedFile file(filename.c_str()); char const* buf = file.getData(); diff --git a/src/storm/parser/SparseStateRewardParser.cpp b/src/storm/parser/SparseStateRewardParser.cpp index d010265a8..3df355578 100644 --- a/src/storm/parser/SparseStateRewardParser.cpp +++ b/src/storm/parser/SparseStateRewardParser.cpp @@ -17,11 +17,6 @@ namespace storm { template std::vector SparseStateRewardParser::parseSparseStateReward(uint_fast64_t stateCount, std::string const& filename) { // Open file. - if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) { - STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable."); - throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": File does not exist or is not readable."; - } - MappedFile file(filename.c_str()); char const* buf = file.getData(); diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 8fefca91c..bbd514c57 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -39,6 +39,7 @@ #include "storm/settings/modules/JitBuilderSettings.h" #include "storm/settings/modules/MultiObjectiveSettings.h" #include "storm/utility/macros.h" +#include "storm/utility/file.h" #include "storm/settings/Option.h" namespace storm { @@ -394,8 +395,8 @@ namespace storm { std::map> SettingsManager::parseConfigFile(std::string const& filename) const { std::map> result; - std::ifstream input(filename); - STORM_LOG_THROW(input.good(), storm::exceptions::OptionParserException, "Could not read from config file '" << filename << "'."); + std::ifstream input; + storm::utility::openFile(filename, input); bool globalScope = true; std::string activeModule = ""; @@ -480,7 +481,8 @@ namespace storm { } } } - + + storm::utility::closeFile(input); return result; } diff --git a/src/storm/solver/SmtlibSmtSolver.cpp b/src/storm/solver/SmtlibSmtSolver.cpp index de33d4f0b..a9da13e4e 100644 --- a/src/storm/solver/SmtlibSmtSolver.cpp +++ b/src/storm/solver/SmtlibSmtSolver.cpp @@ -16,9 +16,10 @@ #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/IllegalArgumentException.h" #include "storm/exceptions/IllegalFunctionCallException.h" -#include "utility/macros.h" -#include "adapters/CarlAdapter.h" -#include "exceptions/UnexpectedException.h" +#include "storm/utility/macros.h" +#include "storm/utility/file.h" +#include "storm/adapters/CarlAdapter.h" +#include "storm/exceptions/UnexpectedException.h" namespace storm { namespace solver { @@ -245,9 +246,9 @@ namespace storm { if (storm::settings::getModule().isExportSmtLibScriptSet()){ STORM_LOG_DEBUG("The SMT-LIBv2 commands are exportet to the given file"); - commandFile.open(storm::settings::getModule().getExportSmtLibScriptPath(), std::ios::trunc); - isCommandFileOpen=commandFile.is_open(); - STORM_LOG_THROW(isCommandFileOpen, storm::exceptions::InvalidArgumentException, "The file where the smt2commands should be written to could not be opened"); + storm::utility::openFile(storm::settings::getModule().getExportSmtLibScriptPath(), commandFile); + isCommandFileOpen = true; + // TODO also close file } //some initial commands diff --git a/src/storm/storage/dd/Odd.cpp b/src/storm/storage/dd/Odd.cpp index 23443a760..469b590b6 100644 --- a/src/storm/storage/dd/Odd.cpp +++ b/src/storm/storage/dd/Odd.cpp @@ -6,6 +6,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" +#include "storm/utility/file.h" namespace storm { namespace dd { @@ -86,7 +87,7 @@ namespace storm { void Odd::exportToDot(std::string const& filename) const { std::ofstream dotFile; - dotFile.open (filename); + storm::utility::openFile(filename, dotFile); // Print header. dotFile << "digraph \"ODD\" {" << std::endl << "center=true;" << std::endl << "edge [dir = none];" << std::endl; @@ -129,8 +130,7 @@ namespace storm { } dotFile << "}" << std::endl; - - dotFile.close(); + storm::utility::closeFile(dotFile); } void Odd::addToLevelToOddNodesMap(std::map>>& levelToOddNodesMap, uint_fast64_t level) const { diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 834ce8623..c39a6b79b 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -5,6 +5,7 @@ #include #include "storm/utility/macros.h" +#include "storm/utility/file.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/NotSupportedException.h" @@ -510,20 +511,11 @@ namespace storm { return modernjson::json(expression.getValueAsDouble()); } - - - - - - void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector const& formulas, std::string const& filepath, bool checkValid) { - std::ofstream ofs; - ofs.open (filepath, std::ofstream::out ); - if(ofs.is_open()) { - toStream(janiModel, formulas, ofs, checkValid); - } else { - STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Cannot open " << filepath); - } + std::ofstream stream; + storm::utility::openFile(filepath, stream); + toStream(janiModel, formulas, stream, checkValid); + storm::utility::closeFile(stream); } void JsonExporter::toStream(storm::jani::Model const& janiModel, std::vector const& formulas, std::ostream& os, bool checkValid) { diff --git a/src/storm/utility/export.h b/src/storm/utility/export.h index 3a6891780..b4f5020c0 100644 --- a/src/storm/utility/export.h +++ b/src/storm/utility/export.h @@ -12,7 +12,7 @@ #include #include "storm/utility/macros.h" -#include "storm/exceptions/FileIoException.h" +#include "storm/utility/file.h" //#include "storm/storage/parameters.h" //#include "storm/settings/modules/ParametricSettings.h" @@ -40,19 +40,11 @@ namespace storm { filestream.close(); } */ - - inline void exportStringToFile(std::string const& str, std::string filepath) { - std::ofstream filestream; - filestream.open(filepath); - STORM_LOG_THROW(filestream.is_open(), storm::exceptions::FileIoException , "Could not open file " << filepath << "."); - filestream << str; - } template inline void exportDataToCSVFile(std::string filepath, std::vector> const& data, boost::optional> const& columnHeaders) { std::ofstream filestream; - filestream.open(filepath); - STORM_LOG_THROW(filestream.is_open(), storm::exceptions::FileIoException , "Could not open file " << filepath << "."); + storm::utility::openFile(filepath, filestream); if(columnHeaders) { for(auto columnIt = columnHeaders->begin(); columnIt != columnHeaders->end(); ++columnIt) { @@ -73,10 +65,9 @@ namespace storm { } filestream << std::endl; } + storm::utility::closeFile(filestream); } } } - - #endif diff --git a/src/storm/utility/file.h b/src/storm/utility/file.h new file mode 100644 index 000000000..4e234dee5 --- /dev/null +++ b/src/storm/utility/file.h @@ -0,0 +1,81 @@ +/** + * @file: file.h + * @author: Sebastian Junges + * + * @since October 7, 2014 + */ + +#ifndef STORM_UTILITY_FILE_H_ +#define STORM_UTILITY_FILE_H_ + +#include + +#include "storm/utility/macros.h" +#include "storm/exceptions/FileIoException.h" + +namespace storm { + namespace utility { + + /*! + * Open the given file for writing. + * + * @param filename Path and name of the file to be tested. + * @param filestream Contains the file handler afterwards. + * @param append If true, the new content is appended instead of clearing the existing content. + */ + inline void openFile(std::string const& filepath, std::ofstream& filestream, bool append = false) { + if (append) { + filestream.open(filepath, std::ios::app); + } else { + filestream.open(filepath); + } + STORM_LOG_THROW(filestream, storm::exceptions::FileIoException , "Could not open file " << filepath << "."); + STORM_PRINT_AND_LOG("Write to file " << filepath << "." << std::endl); + } + + /*! + * Open the given file for reading. + * + * @param filename Path and name of the file to be tested. + * @param filestream Contains the file handler afterwards. + */ + inline void openFile(std::string const& filepath, std::ifstream& filestream) { + filestream.open(filepath); + STORM_LOG_THROW(filestream, storm::exceptions::FileIoException , "Could not open file " << filepath << "."); + } + + /*! + * Close the given file after writing. + * + * @param filestream Contains the file handler to close. + */ + inline void closeFile(std::ofstream& stream) { + stream.close(); + } + + /*! + * Close the given file after reading. + * + * @param filestream Contains the file handler to close. + */ + inline void closeFile(std::ifstream& stream) { + stream.close(); + } + + /*! + * Tests whether the given file exists and is readable. + * + * @param filename Path and name of the file to be tested. + * @return True iff the file exists and is readable. + */ + inline bool fileExistsAndIsReadable(std::string const& filename) { + // Test by opening an input file stream and testing the stream flags. + std::ifstream filestream; + filestream.open(filename); + return filestream.good(); + } + + } +} + +#endif diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index ef4785c1a..3aca0dbe2 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -97,6 +97,7 @@ #include "storm/exceptions/NotSupportedException.h" #include "storm/utility/Stopwatch.h" +#include "storm/utility/file.h" namespace storm { @@ -434,7 +435,7 @@ namespace storm { inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc::ConstraintCollector const& constraintCollector, std::string const& path) { std::ofstream filestream; - filestream.open(path); + storm::utility::openFile(path, filestream); // TODO: add checks. filestream << "!Parameters: "; std::set vars = result.gatherVariables(); @@ -445,7 +446,7 @@ namespace storm { std::copy(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::ostream_iterator>(filestream, "\n")); filestream << "!Graph-preserving Constraints: " << std::endl; std::copy(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::ostream_iterator>(filestream, "\n")); - filestream.close(); + storm::utility::closeFile(filestream); } template<> @@ -623,10 +624,10 @@ namespace storm { template void exportMatrixToFile(std::shared_ptr> model, std::string const& filepath) { STORM_LOG_THROW(model->getType() != storm::models::ModelType::Ctmc, storm::exceptions::NotImplementedException, "This functionality is not yet implemented." ); - std::ofstream ofs; - ofs.open (filepath, std::ofstream::out); - model->getTransitionMatrix().printAsMatlabMatrix(ofs); - ofs.close(); + std::ofstream stream; + storm::utility::openFile(filepath, stream); + model->getTransitionMatrix().printAsMatlabMatrix(stream); + storm::utility::closeFile(stream); } } diff --git a/src/test/parser/MappedFileTest.cpp b/src/test/parser/MappedFileTest.cpp index 3e8affe52..f33ee3aa2 100644 --- a/src/test/parser/MappedFileTest.cpp +++ b/src/test/parser/MappedFileTest.cpp @@ -11,6 +11,7 @@ #include #include "storm/parser/MappedFile.h" #include "storm/utility/cstring.h" +#include "storm/utility/file.h" #include "storm/exceptions/FileIoException.h" TEST(MappedFileTest, NonExistingFile) { @@ -41,12 +42,12 @@ TEST(MappedFileTest, ExistsAndReadble) { // Test the fileExistsAndIsReadable() method under various circumstances. // File exists and is readable. - ASSERT_TRUE(storm::parser::MappedFile::fileExistsAndIsReadable(STORM_TEST_RESOURCES_DIR "/txt/testStringFile.txt")); + ASSERT_TRUE(storm::utility::fileExistsAndIsReadable(STORM_TEST_RESOURCES_DIR "/txt/testStringFile.txt")); // File does not exist. - ASSERT_FALSE(storm::parser::MappedFile::fileExistsAndIsReadable(STORM_TEST_RESOURCES_DIR "/nonExistingFile.not")); + ASSERT_FALSE(storm::utility::fileExistsAndIsReadable(STORM_TEST_RESOURCES_DIR "/nonExistingFile.not")); // File exists but is not readable. // TODO: Find portable solution to providing a situation in which a file exists but is not readable. - //ASSERT_FALSE(storm::parser::MappedFile::fileExistsAndIsReadable(STORM_TEST_RESOURCES_DIR "/parser/unreadableFile.txt")); + //ASSERT_FALSE(storm::utility::fileExistsAndIsReadable(STORM_TEST_RESOURCES_DIR "/parser/unreadableFile.txt")); } From e847d71e1338a79c8852c0f09369fa93c31749a5 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 15 Feb 2017 15:45:44 +0100 Subject: [PATCH 19/23] SymbolicModel: getRewardModels. --- src/storm/models/symbolic/Model.cpp | 5 +++++ src/storm/models/symbolic/Model.h | 2 ++ 2 files changed, 7 insertions(+) diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index 1ebf69f48..483b4337a 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -192,6 +192,11 @@ namespace storm { bool Model::hasRewardModel() const { return !this->rewardModels.empty(); } + + template + std::unordered_map::RewardModelType> const& Model::getRewardModels() const { + return this->rewardModels; + } template void Model::printModelInformationToStream(std::ostream& out) const { diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h index 14c4edbc5..eecbdfdd6 100644 --- a/src/storm/models/symbolic/Model.h +++ b/src/storm/models/symbolic/Model.h @@ -246,6 +246,8 @@ namespace storm { * @return True iff the model has a reward model. */ bool hasRewardModel() const; + + std::unordered_map const& getRewardModels() const; /*! * Retrieves the number of reward models associated with this model. From 0ead111deac3cf1c92293cd662fee84491d42326 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 15 Feb 2017 15:57:29 +0100 Subject: [PATCH 20/23] SymbolicModel: getLabels --- src/storm/models/symbolic/Model.cpp | 9 +++++++++ src/storm/models/symbolic/Model.h | 2 ++ 2 files changed, 11 insertions(+) diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index 483b4337a..38f87d438 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -203,6 +203,15 @@ namespace storm { this->printModelInformationHeaderToStream(out); this->printModelInformationFooterToStream(out); } + + template + std::vector Model::getLabels() const { + std::vector labels; + for(auto const& entry : labelToExpressionMap) { + labels.push_back(entry.first); + } + return labels; + } template void Model::printModelInformationHeaderToStream(std::ostream& out) const { diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h index eecbdfdd6..f3db59f26 100644 --- a/src/storm/models/symbolic/Model.h +++ b/src/storm/models/symbolic/Model.h @@ -259,6 +259,8 @@ namespace storm { virtual void printModelInformationToStream(std::ostream& out) const override; virtual bool isSymbolicModel() const override; + + std::vector getLabels() const; protected: From 598dd85972bd063bf59ea96208ee454ddf702418 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 15 Feb 2017 16:22:43 +0100 Subject: [PATCH 21/23] SymbolicModel: getDeadlockStates --- src/storm/models/symbolic/Model.cpp | 5 +++++ src/storm/models/symbolic/Model.h | 7 ++++++- 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index 38f87d438..e88895560 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -71,6 +71,11 @@ namespace storm { storm::dd::Bdd const& Model::getInitialStates() const { return initialStates; } + + template + storm::dd::Bdd const& Model::getDeadlockStates() const { + return deadlockStates; + } template storm::dd::Bdd Model::getStates(std::string const& label) const { diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h index f3db59f26..4d70fbf1d 100644 --- a/src/storm/models/symbolic/Model.h +++ b/src/storm/models/symbolic/Model.h @@ -130,7 +130,12 @@ namespace storm { * @return The initial states of the model. */ storm::dd::Bdd const& getInitialStates() const; - + + /* + * Retrieves the deadlock states of the model. + */ + storm::dd::Bdd const& getDeadlockStates() const; + /*! * Returns the sets of states labeled with the given label. * From e5b526b7aef0974e40b607fac678c16a0d07a904 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 15 Feb 2017 16:23:50 +0100 Subject: [PATCH 22/23] SymbolicToSparseModel: MDPs --- .../SymbolicToSparseTransformer.cpp | 50 +++++++++++++++++++ .../transformer/SymbolicToSparseTransformer.h | 15 ++++++ 2 files changed, 65 insertions(+) create mode 100644 src/storm/transformer/SymbolicToSparseTransformer.cpp create mode 100644 src/storm/transformer/SymbolicToSparseTransformer.h diff --git a/src/storm/transformer/SymbolicToSparseTransformer.cpp b/src/storm/transformer/SymbolicToSparseTransformer.cpp new file mode 100644 index 000000000..4cb266354 --- /dev/null +++ b/src/storm/transformer/SymbolicToSparseTransformer.cpp @@ -0,0 +1,50 @@ +#include "SymbolicToSparseTransformer.h" + +#include "storm/storage/dd/DdManager.h" +#include "storm/storage/dd/Add.h" +#include "storm/storage/dd/Bdd.h" +#include "storm/models/symbolic/StandardRewardModel.h" + + +#include "storm/models/sparse/StandardRewardModel.h" + +namespace storm { + namespace transformer { + + template + std::shared_ptr> SymbolicMdpToSparseMdpTransformer::translate( + storm::models::symbolic::Mdp const& symbolicMdp) { + storm::dd::Odd odd = symbolicMdp.getReachableStates().createOdd(); + storm::storage::SparseMatrix transitionMatrix = symbolicMdp.getTransitionMatrix().toMatrix(symbolicMdp.getNondeterminismVariables(), odd, odd); + std::unordered_map> rewardModels; + for (auto const& rewardModelNameAndModel : symbolicMdp.getRewardModels()) { + boost::optional> stateRewards; + boost::optional> stateActionRewards; + boost::optional> transitionRewards; + if (rewardModelNameAndModel.second.hasStateRewards()) { + stateRewards = rewardModelNameAndModel.second.getStateRewardVector().toVector(odd); + } + if (rewardModelNameAndModel.second.hasStateActionRewards()) { + stateActionRewards = rewardModelNameAndModel.second.getStateActionRewardVector().toVector(odd); + } + if (rewardModelNameAndModel.second.hasTransitionRewards()) { + transitionRewards = rewardModelNameAndModel.second.getTransitionRewardMatrix().toMatrix(symbolicMdp.getNondeterminismVariables(), odd, odd); + } + rewardModels.emplace(rewardModelNameAndModel.first,storm::models::sparse::StandardRewardModel(stateRewards, stateActionRewards, transitionRewards)); + } + storm::models::sparse::StateLabeling labelling; + + labelling.addLabel("initial", symbolicMdp.getInitialStates().toVector(odd)); + labelling.addLabel("deadlock", symbolicMdp.getDeadlockStates().toVector(odd)); + for(auto const& label : symbolicMdp.getLabels()) { + labelling.addLabel(label, symbolicMdp.getStates(label).toVector(odd)); + } + return std::make_shared>(transitionMatrix, labelling, rewardModels); + + + } + + template class SymbolicMdpToSparseMdpTransformer; + template class SymbolicMdpToSparseMdpTransformer; + } +} \ No newline at end of file diff --git a/src/storm/transformer/SymbolicToSparseTransformer.h b/src/storm/transformer/SymbolicToSparseTransformer.h new file mode 100644 index 000000000..7ea46fff4 --- /dev/null +++ b/src/storm/transformer/SymbolicToSparseTransformer.h @@ -0,0 +1,15 @@ +#pragma once + +#include "storm/models/sparse/Mdp.h" +#include "storm/models/symbolic/Mdp.h" + +namespace storm { + namespace transformer { + + template + class SymbolicMdpToSparseMdpTransformer { + public: + static std::shared_ptr> translate(storm::models::symbolic::Mdp const& symbolicMdp); + }; + } +} From ce9ee672b50f02bd8228a4d5e8e62fb66f40e00d Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 15 Feb 2017 16:38:29 +0100 Subject: [PATCH 23/23] ExportExplicitToDot now added, thanks to Joachim Klein for pointing this out. --- src/storm/cli/entrypoints.h | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index 79b030fb8..8b968e756 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -329,6 +329,14 @@ namespace storm { storm::exporter::explicitExportSparseModel(stream, sparseModel, model.getParameterNames()); storm::utility::closeFile(stream); } + + // And export DOT if required. + if(storm::settings::getModule().isExportDotSet()) { + std::ofstream stream; + storm::utility::openFile(storm::settings::getModule().getExportDotFilename(), stream); + sparseModel->writeDotToStream(stream); + storm::utility::closeFile(stream); + } } template