From 3f2a5ffa62a15d9cdbfdf78c5c24c3bef2a47663 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 27 Aug 2020 17:32:28 +0200 Subject: [PATCH 01/33] Lra Tests: Added a test case for sound model checking --- .../csl/LraCtmcCslModelCheckerTest.cpp | 17 ++++++++++++++++- .../prctl/mdp/LraMdpPrctlModelCheckerTest.cpp | 15 ++++++++++++++- 2 files changed, 30 insertions(+), 2 deletions(-) diff --git a/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp index 75e41cdf2..f0e1dd5d8 100755 --- a/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp @@ -209,6 +209,20 @@ namespace { } }; + class SoundEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models + static const CtmcEngine engine = CtmcEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Ctmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setForceSoundness(true); + return env; + } + }; + template class LraCtmcCslModelCheckerTest : public ::testing::Test { public: @@ -317,7 +331,8 @@ namespace { GBSparseNativeSorEnvironment, DistrSparseGmmxxGmresIluEnvironment, DistrSparseEigenDoubleLUEnvironment, - ValueIterationSparseEnvironment + ValueIterationSparseEnvironment, + SoundEnvironment > TestingTypes; TYPED_TEST_SUITE(LraCtmcCslModelCheckerTest, TestingTypes,); diff --git a/src/test/storm/modelchecker/prctl/mdp/LraMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/LraMdpPrctlModelCheckerTest.cpp index 0dc55deb9..64ce6342d 100755 --- a/src/test/storm/modelchecker/prctl/mdp/LraMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/LraMdpPrctlModelCheckerTest.cpp @@ -53,6 +53,18 @@ namespace { } }; + class SparseSoundEnvironment { + public: + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setForceSoundness(true); + return env; + } + }; + class SparseRationalLinearProgrammingEnvironment { public: static const bool isExact = true; @@ -100,7 +112,8 @@ namespace { typedef ::testing::Types< SparseValueTypeValueIterationEnvironment, - SparseValueTypeLinearProgrammingEnvironment + SparseValueTypeLinearProgrammingEnvironment, + SparseSoundEnvironment #ifdef STORM_HAVE_Z3_OPTIMIZE , SparseRationalLinearProgrammingEnvironment #endif From 3919c475add8d4ca5d0c045bc5f8ea96fcd9b848 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 27 Aug 2020 17:32:51 +0200 Subject: [PATCH 02/33] Added some progress information in topological solvers. --- .../solver/TopologicalLinearEquationSolver.cpp | 13 ++++++++++--- .../TopologicalMinMaxLinearEquationSolver.cpp | 11 ++++++++++- 2 files changed, 20 insertions(+), 4 deletions(-) diff --git a/src/storm/solver/TopologicalLinearEquationSolver.cpp b/src/storm/solver/TopologicalLinearEquationSolver.cpp index ba1a6e2db..76e4ce3ea 100644 --- a/src/storm/solver/TopologicalLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalLinearEquationSolver.cpp @@ -4,6 +4,8 @@ #include "storm/utility/constants.h" #include "storm/utility/vector.h" +#include "storm/utility/Stopwatch.h" +#include "storm/utility/ProgressMeasurement.h" #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidEnvironmentException.h" #include "storm/exceptions/UnexpectedException.h" @@ -61,7 +63,10 @@ namespace storm { if (!this->sortedSccDecomposition || (needAdaptPrecision && !this->longestSccChainSize)) { STORM_LOG_TRACE("Creating SCC decomposition."); + storm::utility::Stopwatch sccSw(true); createSortedSccDecomposition(needAdaptPrecision); + sccSw.stop(); + STORM_LOG_INFO("SCC decomposition computed in " << sccSw << ". Found " << this->sortedSccDecomposition->size() << " SCC(s) containing a total of " << x.size() << " states. Average SCC size is " << static_cast(this->getMatrixRowCount()) / static_cast(this->sortedSccDecomposition->size()) << "."); } // We do not need to adapt the precision if all SCCs are trivial (i.e., the system is acyclic) @@ -69,7 +74,6 @@ namespace storm { storm::Environment sccSolverEnvironment = getEnvironmentForUnderlyingSolver(env, needAdaptPrecision); - STORM_LOG_INFO("Found " << this->sortedSccDecomposition->size() << " SCC(s). Average size is " << static_cast(this->getMatrixRowCount()) / static_cast(this->sortedSccDecomposition->size()) << "."); if (this->longestSccChainSize) { STORM_LOG_INFO("Longest SCC chain size is " << this->longestSccChainSize.get() << "."); } @@ -79,8 +83,12 @@ namespace storm { if (this->sortedSccDecomposition->size() == 1) { returnValue = solveFullyConnectedEquationSystem(sccSolverEnvironment, x, b); } else { + // Solve each SCC individually storm::storage::BitVector sccAsBitVector(x.size(), false); uint64_t sccIndex = 0; + storm::utility::ProgressMeasurement progress("states"); + progress.setMaxCount(x.size()); + progress.startNewMeasurement(0); for (auto const& scc : *this->sortedSccDecomposition) { if (scc.size() == 1) { returnValue = solveTrivialScc(*scc.begin(), x, b) && returnValue; @@ -92,6 +100,7 @@ namespace storm { returnValue = solveScc(sccSolverEnvironment, sccAsBitVector, x, b) && returnValue; } ++sccIndex; + progress.updateProgress(sccIndex); if (storm::utility::resources::isTerminate()) { STORM_LOG_WARN("Topological solver aborted after analyzing " << sccIndex << "/" << this->sortedSccDecomposition->size() << " SCCs."); break; @@ -177,8 +186,6 @@ namespace storm { if (asEquationSystem) { sccA.convertToEquationSystem(); } -// std::cout << "Solving SCC " << scc << std::endl; -// std::cout << "Matrix is " << sccA << std::endl; this->sccSolver->setMatrix(std::move(sccA)); // x Vector diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index e22b53985..7c366e436 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -5,6 +5,8 @@ #include "storm/utility/constants.h" #include "storm/utility/vector.h" +#include "storm/utility/Stopwatch.h" +#include "storm/utility/ProgressMeasurement.h" #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidEnvironmentException.h" #include "storm/exceptions/UnexpectedException.h" @@ -51,8 +53,10 @@ namespace storm { if (!this->sortedSccDecomposition || (needAdaptPrecision && !this->longestSccChainSize)) { STORM_LOG_TRACE("Creating SCC decomposition."); + storm::utility::Stopwatch sccSw(true); createSortedSccDecomposition(needAdaptPrecision); - STORM_LOG_INFO("Found " << this->sortedSccDecomposition->size() << " SCC(s). Average size is " << static_cast(this->A->getRowGroupCount()) / static_cast(this->sortedSccDecomposition->size()) << "."); + sccSw.stop(); + STORM_LOG_INFO("SCC decomposition computed in " << sccSw << ". Found " << this->sortedSccDecomposition->size() << " SCC(s) containing a total of " << x.size() << " states. Average SCC size is " << static_cast(this->A->getRowGroupCount()) / static_cast(this->sortedSccDecomposition->size()) << "."); } // We do not need to adapt the precision if all SCCs are trivial (i.e., the system is acyclic) @@ -69,6 +73,7 @@ namespace storm { // Handle the case where there is just one large SCC returnValue = solveFullyConnectedEquationSystem(sccSolverEnvironment, dir, x, b); } else { + // Solve each SCC individually if (this->isTrackSchedulerSet()) { if (this->schedulerChoices) { this->schedulerChoices.get().resize(x.size()); @@ -79,6 +84,9 @@ namespace storm { storm::storage::BitVector sccRowGroupsAsBitVector(x.size(), false); storm::storage::BitVector sccRowsAsBitVector(b.size(), false); uint64_t sccIndex = 0; + storm::utility::ProgressMeasurement progress("states"); + progress.setMaxCount(x.size()); + progress.startNewMeasurement(0); for (auto const& scc : *this->sortedSccDecomposition) { if (scc.size() == 1) { returnValue = solveTrivialScc(*scc.begin(), dir, x, b) && returnValue; @@ -95,6 +103,7 @@ namespace storm { returnValue = solveScc(sccSolverEnvironment, dir, sccRowGroupsAsBitVector, sccRowsAsBitVector, x, b) && returnValue; } ++sccIndex; + progress.updateProgress(sccIndex); if (storm::utility::resources::isTerminate()) { STORM_LOG_WARN("Topological solver aborted after analyzing " << sccIndex << "/" << this->sortedSccDecomposition->size() << " SCCs."); break; From 5bcdb5f95aaf441f1f8e4cf2b05ff011662bf487 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 27 Aug 2020 17:33:22 +0200 Subject: [PATCH 03/33] Fixed --sound switch for LRA properties on deterministic models. --- .../SparseDeterministicInfiniteHorizonHelper.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp index 511a67787..23ceaf9cb 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp @@ -405,6 +405,8 @@ namespace storm { solver->setBounds(*lowerUpperBounds.first, *lowerUpperBounds.second); // Check solver requirements auto requirements = solver->getRequirements(env); + requirements.clearUpperBounds(); + requirements.clearLowerBounds(); STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UnmetRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); sspValues.assign(sspMatrixVector.first.getRowCount(), (*lowerUpperBounds.first + *lowerUpperBounds.second) / storm::utility::convertNumber(2)); solver->solveEquations(env, sspValues, sspMatrixVector.second); From 21c07ebd42913c281864db0a295270976252496e Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 27 Aug 2020 17:35:15 +0200 Subject: [PATCH 04/33] DdPrismModelBuilder: Fixed a warning for zero-reward models that was triggered in some cases where the reward model is actually non-zero --- src/storm/builder/DdPrismModelBuilder.cpp | 27 +++++++++++------------ 1 file changed, 13 insertions(+), 14 deletions(-) diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index b08e9295d..79c7fb8a3 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -1166,14 +1166,14 @@ namespace storm { } template - void checkRewards(storm::dd::Add const& rewards) { - STORM_LOG_WARN_COND(rewards.getMin() >= 0, "The reward model assigns negative rewards to some states."); - STORM_LOG_WARN_COND(!rewards.isZero(), "The reward model does not assign any non-zero rewards."); + void checkRewards(storm::dd::Add const& rewards, std::string const& rewardType) { + STORM_LOG_WARN_COND(rewards.getMin() >= 0, "The reward model assigns negative " << rewardType << " to some states."); + STORM_LOG_WARN_COND(!rewards.isZero(), "The reward model declares " << rewardType << " but does not assign any non-zero values."); } template - void checkRewards(storm::dd::Add const& rewards) { - STORM_LOG_WARN_COND(!rewards.isZero(), "The reward model does not assign any non-zero rewards."); + void checkRewards(storm::dd::Add const& rewards, std::string const& rewardType) { + STORM_LOG_WARN_COND(!rewards.isZero(), "The reward model declares " << rewardType << " but does not assign any non-zero values."); } template @@ -1191,12 +1191,11 @@ namespace storm { // Restrict the rewards to those states that satisfy the condition. rewards = reachableStatesAdd * states * rewards; - // Perform some sanity checks. - checkRewards(rewards); - // Add the rewards to the global state reward vector. stateRewards.get() += rewards; } + // Perform some sanity checks. + checkRewards(stateRewards.get(), "state rewards"); } // Next, build the state-action reward vector. @@ -1228,9 +1227,6 @@ namespace storm { stateActionRewardDd *= actionDd.transitionsDd.sumAbstract(generationInfo.columnMetaVariables); } - // Perform some sanity checks. - checkRewards(stateActionRewardDd); - // Add the rewards to the global transition reward matrix. stateActionRewards.get() += stateActionRewardDd; } @@ -1243,6 +1239,9 @@ namespace storm { stateActionRewards.get() /= stateActionDd.get(); } + + // Perform some sanity checks. + checkRewards(stateActionRewards.get(), "action rewards"); } // Then build the transition reward matrix. @@ -1279,12 +1278,12 @@ namespace storm { transitionRewardDd = transitions.notZero().template toAdd() * transitionRewardDd; } - // Perform some sanity checks. - checkRewards(transitionRewardDd); - // Add the rewards to the global transition reward matrix. transitionRewards.get() += transitionRewardDd; } + + // Perform some sanity checks. + checkRewards(transitionRewards.get(), "transition rewards"); // Scale transition rewards for DTMCs. if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { From d90c14b8f532b58c5e1c395c87fc91c84ec002c4 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 27 Aug 2020 17:35:45 +0200 Subject: [PATCH 05/33] Added progress information for LRA computations --- .../infinitehorizon/SparseInfiniteHorizonHelper.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.cpp index 3ff9611da..846c19a58 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.cpp @@ -17,6 +17,8 @@ #include "storm/utility/SignalHandler.h" #include "storm/utility/solver.h" #include "storm/utility/vector.h" +#include "storm/utility/Stopwatch.h" +#include "storm/utility/ProgressMeasurement.h" #include "storm/environment/solver/LongRunAverageSolverEnvironment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" @@ -133,13 +135,21 @@ namespace storm { createDecomposition(); // Compute the long-run average for all components in isolation. + // Set up some logging + std::string const componentString = (Nondeterministic ? std::string("Maximal end") : std::string("Bottom strongly connected")) + (_longRunComponentDecomposition->size() == 1 ? std::string(" component") : std::string(" components")); + storm::utility::ProgressMeasurement progress(componentString); + progress.setMaxCount( _longRunComponentDecomposition->size()); + progress.startNewMeasurement(0); + STORM_LOG_INFO("Computing long run average values for " << _longRunComponentDecomposition->size() << " " << componentString << " individually..."); std::vector componentLraValues; componentLraValues.reserve(_longRunComponentDecomposition->size()); for (auto const& c : *_longRunComponentDecomposition) { componentLraValues.push_back(computeLraForComponent(underlyingSolverEnvironment, stateRewardsGetter, actionRewardsGetter, c)); + progress.updateProgress(componentLraValues.size()); } // Solve the resulting SSP where end components are collapsed into single auxiliary states + STORM_LOG_INFO("Solving stochastic shortest path problem."); return buildAndSolveSsp(underlyingSolverEnvironment, componentLraValues); } From fb112ab191cc93509dedab406b2a78d0c763cf75 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 27 Aug 2020 17:36:37 +0200 Subject: [PATCH 06/33] Added support for modulo operators when building symbolic models in exact mode. --- resources/3rdparty/sylvan/src/storm_wrapper.cpp | 7 +++++-- resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp | 1 + resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp | 6 ++++++ src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp | 4 ++-- 4 files changed, 14 insertions(+), 4 deletions(-) diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_wrapper.cpp index 6d12a0825..5bfe580de 100644 --- a/resources/3rdparty/sylvan/src/storm_wrapper.cpp +++ b/resources/3rdparty/sylvan/src/storm_wrapper.cpp @@ -227,8 +227,11 @@ storm_rational_number_ptr storm_rational_number_mod(storm_rational_number_ptr a, storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; - - throw storm::exceptions::InvalidOperationException() << "Modulo not supported for rational numbers."; + if (carl::isInteger(srn_a) && carl::isInteger(srn_b)) { + storm::RationalNumber* result_srn = new storm::RationalNumber(carl::mod(carl::getNum(srn_a), carl::getNum(srn_b))); + return (storm_rational_number_ptr)result_srn; + } + throw storm::exceptions::InvalidOperationException() << "Modulo not supported for rational, non-integer numbers."; } storm_rational_number_ptr storm_rational_number_min(storm_rational_number_ptr a, storm_rational_number_ptr b) { diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp index d41976f5f..fc4ccf420 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp @@ -53,6 +53,7 @@ Mtbdd DivideRN(const Mtbdd &other) const; Mtbdd FloorRN() const; Mtbdd CeilRN() const; Mtbdd PowRN(const Mtbdd& other) const; +Mtbdd ModRN(const Mtbdd& other) const; Mtbdd MinimumRN() const; Mtbdd MaximumRN() const; diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp index 0420d112c..c622637cf 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp @@ -315,6 +315,12 @@ Mtbdd::PowRN(const Mtbdd& other) const { return sylvan_storm_rational_number_pow(mtbdd, other.mtbdd); } +Mtbdd +Mtbdd::ModRN(const Mtbdd& other) const { + LACE_ME; + return sylvan_storm_rational_number_mod(mtbdd, other.mtbdd); +} + Mtbdd Mtbdd::MinimumRN() const { LACE_ME; diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index 5a3cdc954..a7c33d59e 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -328,8 +328,8 @@ namespace storm { } template<> - InternalAdd InternalAdd::mod(InternalAdd const&) const { - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Operation (mod) not supported by rational numbers."); + InternalAdd InternalAdd::mod(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.ModRN(other.sylvanMtbdd)); } #ifdef STORM_HAVE_CARL From ee56f5b2f90e6b9802c6c377b1fcffb0eb3d6e81 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 1 Sep 2020 15:13:36 +0200 Subject: [PATCH 07/33] CMake Fixed version-info when the source code is not in a git repository. --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index cbab845cc..3d882f18c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -445,7 +445,7 @@ set(STORM_VERSION_APPENDIX "${CMAKE_MATCH_5}") # might be empty if (STORM_GIT_VERSION_STRING MATCHES "NOTFOUND") set(STORM_VERSION_SOURCE "VersionSource::Static") set(STORM_VERSION_COMMITS_AHEAD 0) - set(STORM_VERSION_DIRTY DirtyState:Unknown) + set(STORM_VERSION_DIRTY DirtyState::Unknown) include(version.cmake) message(WARNING "Storm - Git version information not available, statically assuming version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}.") else() From 9ce9ae9eeb5548100c53c96a45499e02b19f04e6 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 1 Sep 2020 16:12:16 +0200 Subject: [PATCH 08/33] OVI: Fixed too early termination. --- .../solver/IterativeMinMaxLinearEquationSolver.cpp | 9 +++++++++ src/storm/solver/NativeLinearEquationSolver.cpp | 6 ++++++ .../solver/helper/OptimisticValueIterationHelper.h | 11 +++++++---- 3 files changed, 22 insertions(+), 4 deletions(-) diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 90837a6b3..4f74b143e 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -360,6 +360,15 @@ namespace storm { template bool IterativeMinMaxLinearEquationSolver::solveEquationsOptimisticValueIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const { + if (!storm::utility::vector::hasNonZeroEntry(b)) { + // If all entries are zero, OVI might run in an endless loop. However, the result is easy in this case. + x.assign(x.size(), storm::utility::zero()); + if (this->isTrackSchedulerSet()) { + this->schedulerChoices = std::vector(x.size(), 0); + } + return true; + } + if (!this->multiplierA) { this->multiplierA = storm::solver::MultiplierFactory().create(env, *this->A); } diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index f06e1f311..a27988ba6 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -637,6 +637,12 @@ namespace storm { template bool NativeLinearEquationSolver::solveEquationsOptimisticValueIteration(Environment const& env, std::vector& x, std::vector const& b) const { + if (!storm::utility::vector::hasNonZeroEntry(b)) { + // If all entries are zero, OVI might run in an endless loop. However, the result is easy in this case. + x.assign(x.size(), storm::utility::zero()); + return true; + } + if (!this->multiplier) { this->multiplier = storm::solver::MultiplierFactory().create(env, *this->A); } diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h index fb646ce76..5542eb473 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.h +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h @@ -223,11 +223,14 @@ namespace storm { // From now on, we keep updating both bounds intervalIterationNeeded = true; } - } else if (newUpperBoundAlwaysHigherEqual && newUpperBoundAlwaysLowerEqual) { + // The following case below covers that bouth vectors (old and new) are equal. + // Theoretically, this means that the precise fixpoint has been reached. However, numerical instabilities can be tricky and this detection might be incorrect (see the haddad-monmege model). + // We therefore disable it. It is very unlikely that we guessed the right fixpoint anyway. + //} else if (newUpperBoundAlwaysHigherEqual && newUpperBoundAlwaysLowerEqual) { // In this case, the guessed upper bound is the precise fixpoint - status = SolverStatus::Converged; - std::swap(lowerX, auxVector); - break; + // status = SolverStatus::Converged; + // std::swap(lowerX, auxVector); + // break; } // At this point, the old upper bounds (auxVector) are not needed anymore. From 90d5da570cf7df0e9b324323124d52791477aa26 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 2 Sep 2020 11:04:09 +0200 Subject: [PATCH 09/33] Renamed portfolio engine to automatic engine. --- CHANGELOG.md | 3 +- src/storm-cli-utilities/model-handling.h | 40 +++++++++---------- src/storm/settings/modules/CoreSettings.cpp | 2 + .../{Portfolio.cpp => AutomaticSettings.cpp} | 28 ++++++------- .../{Portfolio.h => AutomaticSettings.h} | 4 +- src/storm/utility/Engine.cpp | 8 +++- src/storm/utility/Engine.h | 2 +- 7 files changed, 47 insertions(+), 40 deletions(-) rename src/storm/utility/{Portfolio.cpp => AutomaticSettings.cpp} (92%) rename src/storm/utility/{Portfolio.h => AutomaticSettings.h} (95%) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5976115a8..d9b1274da 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,7 +11,8 @@ Version 1.6.x ## Version 1.6.1 (??) - Prism program simplification improved. - Revamped implementation of long-run-average algorithms, including scheduler export for LRA properties on Markov automata. -- Support for step-bounded properties of the form ... [F[x,y] ... ] for DTMCs and MDPs (sparse engine). +- Support for step-bounded properties of the form ... [F[x,y] ... ] for DTMCs and MDPs (sparse engine). +- Renamed portfolio engine to automatic - `storm-dft`: Fix for relevant events when using symmetry reduction. - `storm-pomdp`: Fix for --transformsimple and --transformbinary when used with until formulae. - `storm-pomdp`: POMDPs can be parametric as well. diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index d5f27ec14..f630e67df 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -10,7 +10,7 @@ #include "storm/utility/macros.h" #include "storm/utility/NumberTraits.h" #include "storm/utility/Engine.h" -#include "storm/utility/Portfolio.h" +#include "storm/utility/AutomaticSettings.h" #include "storm/utility/initialize.h" #include "storm/utility/Stopwatch.h" @@ -178,30 +178,30 @@ namespace storm { bool isCompatible; }; - void getModelProcessingInformationPortfolio(SymbolicInput const& input, ModelProcessingInformation& mpi) { + void getModelProcessingInformationAutomatic(SymbolicInput const& input, ModelProcessingInformation& mpi) { auto hints = storm::settings::getModule(); - STORM_LOG_THROW(input.model.is_initialized(), storm::exceptions::InvalidArgumentException, "Portfolio engine requires a JANI input model."); - STORM_LOG_THROW(input.model->isJaniModel(), storm::exceptions::InvalidArgumentException, "Portfolio engine requires a JANI input model."); + STORM_LOG_THROW(input.model.is_initialized(), storm::exceptions::InvalidArgumentException, "Automatic engine requires a JANI input model."); + STORM_LOG_THROW(input.model->isJaniModel(), storm::exceptions::InvalidArgumentException, "Automatic engine requires a JANI input model."); std::vector const& properties = input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties; - STORM_LOG_THROW(!properties.empty(), storm::exceptions::InvalidArgumentException, "Portfolio engine requires a property."); - STORM_LOG_WARN_COND(properties.size() == 1, "Portfolio engine does not support decisions based on multiple properties. Only the first property will be considered."); + STORM_LOG_THROW(!properties.empty(), storm::exceptions::InvalidArgumentException, "Automatic engine requires a property."); + STORM_LOG_WARN_COND(properties.size() == 1, "Automatic engine does not support decisions based on multiple properties. Only the first property will be considered."); - storm::utility::Portfolio pf; + storm::utility::AutomaticSettings as; if (hints.isNumberStatesSet()) { - pf.predict(input.model->asJaniModel(), properties.front(), hints.getNumberStates()); + as.predict(input.model->asJaniModel(), properties.front(), hints.getNumberStates()); } else { - pf.predict(input.model->asJaniModel(), properties.front()); + as.predict(input.model->asJaniModel(), properties.front()); } - mpi.engine = pf.getEngine(); - if (pf.enableBisimulation()) { + mpi.engine = as.getEngine(); + if (as.enableBisimulation()) { mpi.applyBisimulation = true; } - if (pf.enableExact() && mpi.verificationValueType == ModelProcessingInformation::ValueType::FinitePrecision) { + if (as.enableExact() && mpi.verificationValueType == ModelProcessingInformation::ValueType::FinitePrecision) { mpi.verificationValueType = ModelProcessingInformation::ValueType::Exact; } - STORM_PRINT_AND_LOG( "Portfolio engine picked the following settings: " << std::endl + STORM_PRINT_AND_LOG( "Automatic engine picked the following settings: " << std::endl << "\tengine=" << mpi.engine << std::boolalpha << "\t bisimulation=" << mpi.applyBisimulation @@ -237,12 +237,12 @@ namespace storm { } auto originalVerificationValueType = mpi.verificationValueType; - // Since the remaining settings could depend on the ones above, we need apply the portfolio engine now. - bool usePortfolio = input.model.is_initialized() && mpi.engine == storm::utility::Engine::Portfolio; - if (usePortfolio) { + // Since the remaining settings could depend on the ones above, we need apply the automatic engine now. + bool useAutomatic = input.model.is_initialized() && mpi.engine == storm::utility::Engine::Automatic; + if (useAutomatic) { if (input.model->isJaniModel()) { // This can potentially overwrite the settings above, but will not overwrite settings that were explicitly set by the user (e.g. we will not disable bisimulation or disable exact arithmetic) - getModelProcessingInformationPortfolio(input, mpi); + getModelProcessingInformationAutomatic(input, mpi); } else { // Transform Prism to jani first STORM_LOG_ASSERT(input.model->isPrismProgram(), "Unexpected type of input."); @@ -255,7 +255,7 @@ namespace storm { janiInput.preprocessedProperties = std::move(modelAndProperties.second); } // This can potentially overwrite the settings above, but will not overwrite settings that were explicitly set by the user (e.g. we will not disable bisimulation or disable exact arithmetic) - getModelProcessingInformationPortfolio(janiInput, mpi); + getModelProcessingInformationAutomatic(janiInput, mpi); if (transformedJaniInput) { // We cache the transformation result. *transformedJaniInput = std::move(janiInput); @@ -279,9 +279,9 @@ namespace storm { }; mpi.isCompatible = checkCompatibleSettings(); if (!mpi.isCompatible) { - if (usePortfolio) { + if (useAutomatic) { bool useExact = mpi.verificationValueType != ModelProcessingInformation::ValueType::FinitePrecision; - STORM_LOG_WARN("The settings picked by the portfolio engine (engine=" << mpi.engine << ", bisim=" << mpi.applyBisimulation << ", exact=" << useExact << ") are incompatible with this model. Falling back to default settings."); + STORM_LOG_WARN("The settings picked by the automatic engine (engine=" << mpi.engine << ", bisim=" << mpi.applyBisimulation << ", exact=" << useExact << ") are incompatible with this model. Falling back to default settings."); mpi.engine = storm::utility::Engine::Sparse; mpi.applyBisimulation = false; mpi.verificationValueType = originalVerificationValueType; diff --git a/src/storm/settings/modules/CoreSettings.cpp b/src/storm/settings/modules/CoreSettings.cpp index d520f930b..d56081287 100644 --- a/src/storm/settings/modules/CoreSettings.cpp +++ b/src/storm/settings/modules/CoreSettings.cpp @@ -37,6 +37,8 @@ namespace storm { for (auto e : storm::utility::getEngines()) { engines.push_back(storm::utility::toString(e)); } + engines.push_back("portfolio"); // for backwards compatibility + this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(engines)).setDefaultValueString("sparse").build()).build()); diff --git a/src/storm/utility/Portfolio.cpp b/src/storm/utility/AutomaticSettings.cpp similarity index 92% rename from src/storm/utility/Portfolio.cpp rename to src/storm/utility/AutomaticSettings.cpp index f23ae66af..39a9aed7c 100644 --- a/src/storm/utility/Portfolio.cpp +++ b/src/storm/utility/AutomaticSettings.cpp @@ -1,4 +1,4 @@ -#include "storm/utility/Portfolio.h" +#include "storm/utility/AutomaticSettings.h" #include @@ -90,14 +90,14 @@ namespace storm { }; } - Portfolio::Portfolio() : engine(storm::utility::Engine::Unknown), useBisimulation(false), useExact(false) { + AutomaticSettings::AutomaticSettings() : engine(storm::utility::Engine::Unknown), useBisimulation(false), useExact(false) { // Intentionally left empty } - void Portfolio::predict(storm::jani::Model const& model, storm::jani::Property const& property) { + void AutomaticSettings::predict(storm::jani::Model const& model, storm::jani::Property const& property) { typedef pfinternal::PropertyType PropertyType; auto f = pfinternal::Features(model, property); - STORM_LOG_INFO("Portfolio engine using features " << f.toString() << "."); + STORM_LOG_INFO("Automatic engine using features " << f.toString() << "."); if (f.numVariables <= 12) { if (f.avgDomainSize <= 323.25) { @@ -218,54 +218,54 @@ namespace storm { } } - void Portfolio::predict(storm::jani::Model const& model, storm::jani::Property const& property, uint64_t) { + void AutomaticSettings::predict(storm::jani::Model const& model, storm::jani::Property const& property, uint64_t) { //typedef pfinternal::PropertyType PropertyType; //auto f = pfinternal::Features(model, property); //f.stateEstimate = stateEstimate; - //STORM_LOG_INFO("Portfolio engine using features " << f.toString() << "."); + //STORM_LOG_INFO("Automatic engine using features " << f.toString() << "."); // Right now, we do not make use of the state estimate, so we just ask the 'default' decision tree. predict(model, property); } - storm::utility::Engine Portfolio::getEngine() const { + storm::utility::Engine AutomaticSettings::getEngine() const { STORM_LOG_THROW(engine != storm::utility::Engine::Unknown, storm::exceptions::InvalidOperationException, "Tried to get the engine but apparently no prediction was done before."); return engine; } - bool Portfolio::enableBisimulation() const { + bool AutomaticSettings::enableBisimulation() const { return useBisimulation; } - bool Portfolio::enableExact() const { + bool AutomaticSettings::enableExact() const { return useExact; } - void Portfolio::sparse() { + void AutomaticSettings::sparse() { engine = storm::utility::Engine::Sparse; useBisimulation = false; useExact = false; } - void Portfolio::hybrid() { + void AutomaticSettings::hybrid() { engine = storm::utility::Engine::Hybrid; useBisimulation = false; useExact = false; } - void Portfolio::dd() { + void AutomaticSettings::dd() { engine = storm::utility::Engine::Dd; useBisimulation = false; useExact = false; } - void Portfolio::exact() { + void AutomaticSettings::exact() { engine = storm::utility::Engine::Sparse; useBisimulation = false; useExact = true; } - void Portfolio::ddbisim() { + void AutomaticSettings::ddbisim() { engine = storm::utility::Engine::DdSparse; useBisimulation = true; useExact = false; diff --git a/src/storm/utility/Portfolio.h b/src/storm/utility/AutomaticSettings.h similarity index 95% rename from src/storm/utility/Portfolio.h rename to src/storm/utility/AutomaticSettings.h index 472369bc7..2d3a7c7f7 100644 --- a/src/storm/utility/Portfolio.h +++ b/src/storm/utility/AutomaticSettings.h @@ -10,9 +10,9 @@ namespace storm { } namespace utility { - class Portfolio { + class AutomaticSettings { public: - Portfolio(); + AutomaticSettings(); /*! * Predicts "good" settings for the provided model checking query diff --git a/src/storm/utility/Engine.cpp b/src/storm/utility/Engine.cpp index 3c892c8b9..8eaecde4e 100644 --- a/src/storm/utility/Engine.cpp +++ b/src/storm/utility/Engine.cpp @@ -51,8 +51,8 @@ namespace storm { return "expl"; case Engine::AbstractionRefinement: return "abs"; - case Engine::Portfolio: - return "portfolio"; + case Engine::Automatic: + return "automatic"; case Engine::Unknown: return "UNKNOWN"; default: @@ -72,6 +72,10 @@ namespace storm { return e; } } + if (engineStr == "portfolio") { + STORM_LOG_WARN("The engine name \"portfolio\" is deprecated. The name of this engine has been changed to \"" << toString(Engine::Automatic) << "\"."); + return Engine::Automatic; + } STORM_LOG_ERROR("The engine '" << engineStr << "' was not found."); return Engine::Unknown; } diff --git a/src/storm/utility/Engine.h b/src/storm/utility/Engine.h index b193eb448..03dfd922a 100644 --- a/src/storm/utility/Engine.h +++ b/src/storm/utility/Engine.h @@ -30,7 +30,7 @@ namespace storm { /// An enumeration of all engines. enum class Engine { // The last one should always be 'Unknown' to make sure that the getEngines() method below works. - Sparse, Hybrid, Dd, DdSparse, Jit, Exploration, AbstractionRefinement, Portfolio, Unknown + Sparse, Hybrid, Dd, DdSparse, Jit, Exploration, AbstractionRefinement, Automatic, Unknown }; /*! From 6e2dab0e0bdac4d7052bb9a29e838da8de0e540e Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 2 Sep 2020 11:04:40 +0200 Subject: [PATCH 10/33] Silenced a warning in OVI code. --- src/storm/solver/helper/OptimisticValueIterationHelper.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h index 5542eb473..75adafb09 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.h +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h @@ -167,7 +167,7 @@ namespace storm { bool newUpperBoundAlwaysLowerEqual = true; if (noTerminationGuarantee) { bool cancelOuterScan = false; - for (uint64_t i = 0; i < upperX->size() & !cancelOuterScan; ++i) { + for (uint64_t i = 0; i < upperX->size() && !cancelOuterScan; ++i) { if ((*upperX)[i] < (*auxVector)[i]) { newUpperBoundAlwaysHigherEqual = false; for (++i; i < upperX->size(); ++i) { From 990d1c97596abe98e2f0f6b7c4622c6fdd24799f Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 2 Sep 2020 18:19:24 +0200 Subject: [PATCH 11/33] OVI: seperated implementation from header file. Use a separate helper for computing the upper bounds. --- .../IterativeMinMaxLinearEquationSolver.cpp | 8 +- .../solver/NativeLinearEquationSolver.cpp | 8 +- .../helper/OptimisticValueIterationHelper.cpp | 362 ++++++++++++++++++ .../helper/OptimisticValueIterationHelper.h | 362 ++++-------------- 4 files changed, 449 insertions(+), 291 deletions(-) create mode 100644 src/storm/solver/helper/OptimisticValueIterationHelper.cpp diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 4f74b143e..089ba266e 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -402,11 +402,12 @@ namespace storm { this->startMeasureProgress(); - - auto statusIters = storm::solver::helper::solveEquationsOptimisticValueIteration(env, lowerX, upperX, auxVector, + storm::solver::helper::OptimisticValueIterationHelper helper(*this->A); + auto statusIters = helper.solveEquationsOptimisticValueIteration(env, lowerX, upperX, auxVector, b, [&] (std::vector*& y, std::vector*& yPrime, ValueType const& precision, bool const& relative, uint64_t const& i, uint64_t const& maxI) { this->showProgressIterative(i); - return performValueIteration(env, dir, y, yPrime, b, precision, relative, guarantee, i, maxI, multiplicationStyle); + auto result = performValueIteration(env, dir, y, yPrime, b, precision, relative, guarantee, i, maxI, multiplicationStyle); + return std::make_pair(result.iterations, result.status); }, [&] (std::vector* y, std::vector* yPrime, uint64_t const& i) { this->showProgressIterative(i); @@ -423,6 +424,7 @@ namespace storm { env.solver().minMax().getRelativeTerminationCriterion(), storm::utility::convertNumber(env.solver().minMax().getPrecision()), env.solver().minMax().getMaximalNumberOfIterations(), + dir, relevantValues); auto two = storm::utility::convertNumber(2.0); storm::utility::vector::applyPointwise(*lowerX, *upperX, x, [&two] (ValueType const& a, ValueType const& b) -> ValueType { return (a + b) / two; }); diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index a27988ba6..9ca9683fc 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -675,11 +675,12 @@ namespace storm { std::vector* auxVector = this->cachedRowVector2.get(); this->startMeasureProgress(); - - auto statusIters = storm::solver::helper::solveEquationsOptimisticValueIteration(env, lowerX, upperX, auxVector, + storm::solver::helper::OptimisticValueIterationHelper helper(*this->A); + auto statusIters = helper.solveEquationsOptimisticValueIteration(env, lowerX, upperX, auxVector, b, [&] (std::vector*& y, std::vector*& yPrime, ValueType const& precision, bool const& relative, uint64_t const& i, uint64_t const& maxI) { this->showProgressIterative(i); - return performPowerIteration(env, y, yPrime, b, precision, relative, guarantee, i, maxI, multiplicationStyle); + auto result = performPowerIteration(env, y, yPrime, b, precision, relative, guarantee, i, maxI, multiplicationStyle); + return std::make_pair(result.iterations, result.status); }, [&] (std::vector* y, std::vector* yPrime, uint64_t const& i) { this->showProgressIterative(i); @@ -696,6 +697,7 @@ namespace storm { env.solver().native().getRelativeTerminationCriterion(), storm::utility::convertNumber(env.solver().native().getPrecision()), env.solver().native().getMaximalNumberOfIterations(), + boost::none, // No optimization dir relevantValues); auto two = storm::utility::convertNumber(2.0); storm::utility::vector::applyPointwise(*lowerX, *upperX, x, [&two] (ValueType const& a, ValueType const& b) -> ValueType { return (a + b) / two; }); diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.cpp b/src/storm/solver/helper/OptimisticValueIterationHelper.cpp new file mode 100644 index 000000000..d52d41d37 --- /dev/null +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.cpp @@ -0,0 +1,362 @@ +#include "OptimisticValueIterationHelper.h" + +#include "storm/utility/vector.h" +#include "storm/utility/SignalHandler.h" +#include "storm/environment/solver/OviSolverEnvironment.h" + +#include "storm/exceptions/NotSupportedException.h" + +#include "storm/utility/macros.h" + +namespace storm { + + namespace solver { + namespace helper { + namespace oviinternal { + + template + ValueType computeMaxAbsDiff(std::vector const& allOldValues, std::vector const& allNewValues, storm::storage::BitVector const& relevantValues) { + ValueType result = storm::utility::zero(); + for (auto value : relevantValues) { + result = storm::utility::max(result, storm::utility::abs(allNewValues[value] - allOldValues[value])); + } + return result; + } + + template + ValueType computeMaxAbsDiff(std::vector const& allOldValues, std::vector const& allNewValues) { + ValueType result = storm::utility::zero(); + for (uint64_t i = 0; i < allOldValues.size(); ++i) { + result = storm::utility::max(result, storm::utility::abs(allNewValues[i] - allOldValues[i])); + } + return result; + } + + template + ValueType computeMaxRelDiff(std::vector const& allOldValues, std::vector const& allNewValues, storm::storage::BitVector const& relevantValues) { + ValueType result = storm::utility::zero(); + for (auto const& i : relevantValues) { + STORM_LOG_ASSERT(!storm::utility::isZero(allNewValues[i]) || storm::utility::isZero(allOldValues[i]), "Unexpected entry in iteration vector."); + if (!storm::utility::isZero(allNewValues[i])) { + result = storm::utility::max(result, storm::utility::abs(allNewValues[i] - allOldValues[i]) / allNewValues[i]); + } + } + return result; + } + + template + ValueType computeMaxRelDiff(std::vector const& allOldValues, std::vector const& allNewValues) { + ValueType result = storm::utility::zero(); + for (uint64_t i = 0; i < allOldValues.size(); ++i) { + STORM_LOG_ASSERT(!storm::utility::isZero(allNewValues[i]) || storm::utility::isZero(allOldValues[i]), "Unexpected entry in iteration vector."); + if (!storm::utility::isZero(allNewValues[i])) { + result = storm::utility::max(result, storm::utility::abs(allNewValues[i] - allOldValues[i]) / allNewValues[i]); + } + } + return result; + } + + template + ValueType updateIterationPrecision(storm::Environment const& env, std::vector const& currentX, std::vector const& newX, bool const& relative, boost::optional const& relevantValues) { + auto factor = storm::utility::convertNumber(env.solver().ovi().getPrecisionUpdateFactor()); + bool useRelevant = relevantValues.is_initialized() && env.solver().ovi().useRelevantValuesForPrecisionUpdate(); + if (relative) { + return (useRelevant ? computeMaxRelDiff(newX, currentX, relevantValues.get()) : computeMaxRelDiff(newX, currentX)) * factor; + } else { + return (useRelevant ? computeMaxAbsDiff(newX, currentX, relevantValues.get()) : computeMaxAbsDiff(newX, currentX)) * factor; + } + } + + template + void guessUpperBoundRelative(std::vector const& x, std::vector &target, ValueType const& relativeBoundGuessingScaler) { + storm::utility::vector::applyPointwise(x, target, [&relativeBoundGuessingScaler] (ValueType const& argument) -> ValueType { return argument * relativeBoundGuessingScaler; }); + } + + template + void guessUpperBoundAbsolute(std::vector const& x, std::vector &target, ValueType const& precision) { + storm::utility::vector::applyPointwise(x, target, [&precision] (ValueType const& argument) -> ValueType { return argument + precision; }); + } + + template + UpperBoundIterator::UpperBoundIterator(storm::storage::SparseMatrix const& matrix) { + STORM_LOG_THROW(static_cast(std::numeric_limits::max()) > matrix.getRowCount() + 1, storm::exceptions::NotSupportedException, "Matrix dimensions too large."); + STORM_LOG_THROW(static_cast(std::numeric_limits::max()) > matrix.getEntryCount(), storm::exceptions::NotSupportedException, "Matrix dimensions too large."); + matrixValues.reserve(matrix.getNonzeroEntryCount()); + matrixColumns.reserve(matrix.getColumnCount()); + rowIndications.reserve(matrix.getRowCount() + 1); + rowIndications.push_back(0); + for (IndexType r = 0; r < static_cast(matrix.getRowCount()); ++r) { + for (auto const& entry : matrix.getRow(r)) { + matrixValues.push_back(entry.getValue()); + matrixColumns.push_back(entry.getColumn()); + } + rowIndications.push_back(matrixValues.size()); + } + if (!matrix.hasTrivialRowGrouping()) { + rowGroupIndices = &matrix.getRowGroupIndices(); + } + } + + template + typename UpperBoundIterator::IterateResult UpperBoundIterator::iterate(std::vector& x, std::vector const& b, bool takeMinOfOldAndNew) { + return iterateInternal(x, b, takeMinOfOldAndNew); + } + + template + typename UpperBoundIterator::IterateResult UpperBoundIterator::iterate(storm::solver::OptimizationDirection const& dir, std::vector& x, std::vector const& b, bool takeMinOfOldAndNew) { + if (minimize(dir)) { + return iterateInternal(x, b, takeMinOfOldAndNew); + } else { + return iterateInternal(x, b, takeMinOfOldAndNew); + } + } + + template + template + typename UpperBoundIterator::IterateResult UpperBoundIterator::iterateInternal(std::vector& x, std::vector const& b, bool takeMinOfOldAndNew) { + // For each row compare the new upper bound candidate with the old one + bool newUpperBoundAlwaysHigherEqual = true; + bool newUpperBoundAlwaysLowerEqual = true; + // Do a backwards gauss-seidel style iteration + for (IndexType i = x.size(); i > 0;) { + --i; + ValueType newXi = HasRowGroups ? multiplyRowGroup(i, b, x) : multiplyRow(i, b[i], x); + ValueType& oldXi = x[i]; + if (newXi > oldXi) { + newUpperBoundAlwaysLowerEqual = false; + if (!takeMinOfOldAndNew) { + oldXi = newXi; + } + } else if (newXi != oldXi) { + assert(newXi < oldXi); + newUpperBoundAlwaysHigherEqual = false; + oldXi = newXi; + } + } + // Return appropriate result + if (newUpperBoundAlwaysLowerEqual) { + if (newUpperBoundAlwaysHigherEqual) { + return IterateResult::Equal; + } else { + return IterateResult::AlwaysLowerOrEqual; + } + } else { + if (newUpperBoundAlwaysHigherEqual) { + return IterateResult::AlwaysHigherOrEqual; + } else { + return IterateResult::Incomparable; + } + } + } + + template + ValueType UpperBoundIterator::multiplyRow(IndexType const& rowIndex, ValueType const& bi, std::vector const& x) { + assert(rowIndex < rowIndications.size()); + ValueType xRes = bi; + + auto entryIt = matrixValues.begin() + rowIndications[rowIndex]; + auto entryItE = matrixValues.begin() + rowIndications[rowIndex + 1]; + auto colIt = matrixColumns.begin() + rowIndications[rowIndex]; + for (; entryIt != entryItE; ++entryIt, ++colIt) { + xRes += *entryIt * x[*colIt]; + } + return xRes; + } + + template + template + ValueType UpperBoundIterator::multiplyRowGroup(IndexType const& rowGroupIndex, std::vector const& b, std::vector const& x) { + STORM_LOG_ASSERT(rowGroupIndices != nullptr, "No row group indices available."); + auto row = (*rowGroupIndices)[rowGroupIndex]; + auto const& groupEnd = (*rowGroupIndices)[rowGroupIndex + 1]; + STORM_LOG_ASSERT(row < groupEnd, "Empty row group not expected."); + ValueType xRes = multiplyRow(row, b[row], x); + for (++row; row < groupEnd; ++row) { + ValueType xCur = multiplyRow(row, b[row], x); + xRes = minimize(Dir) ? std::min(xRes, xCur) : std::max(xRes, xCur); + } + return xRes; + } + } + + template + OptimisticValueIterationHelper::OptimisticValueIterationHelper(storm::storage::SparseMatrix const& matrix) : upperBoundIterator(matrix) { + // Intentionally left empty. + } + + template + std::pair OptimisticValueIterationHelper::solveEquationsOptimisticValueIteration(Environment const& env, std::vector* lowerX, std::vector* upperX, std::vector* auxVector, std::vector const& b, ValueIterationCallBackType const& valueIterationCallback, SingleIterationCallBackType const& singleIterationCallback, bool relative, ValueType precision, uint64_t maxOverallIterations, boost::optional dir, boost::optional relevantValues) { + STORM_LOG_ASSERT(lowerX->size() == upperX->size(), "Dimension missmatch."); + STORM_LOG_ASSERT(lowerX->size() == auxVector->size(), "Dimension missmatch."); + + // As we will shuffle pointers around, let's store the original positions here. + std::vector* initLowerX = lowerX; + std::vector* initUpperX = upperX; + std::vector* initAux = auxVector; + + uint64_t overallIterations = 0; + uint64_t lastValueIterationIterations = 0; + uint64_t currentVerificationIterations = 0; + uint64_t valueIterationInvocations = 0; + + // Get some parameters for the algorithm + // 2 + ValueType two = storm::utility::convertNumber(2.0); + // Use no termination guaranteed upper bound iteration method + bool noTerminationGuarantee = env.solver().ovi().useNoTerminationGuaranteeMinimumMethod(); + // Desired max difference between upperX and lowerX + ValueType doublePrecision = precision * two; + // Upper bound only iterations + uint64_t upperBoundOnlyIterations = env.solver().ovi().getUpperBoundOnlyIterations(); + ValueType relativeBoundGuessingScaler = (storm::utility::one() + storm::utility::convertNumber(env.solver().ovi().getUpperBoundGuessingFactor()) * precision); + // Initial precision for the value iteration calls + ValueType iterationPrecision = precision; + + SolverStatus status = SolverStatus::InProgress; + + while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { + + // Perform value iteration until convergence + ++valueIterationInvocations; + auto result = valueIterationCallback(lowerX, auxVector, iterationPrecision, relative, overallIterations, maxOverallIterations); + lastValueIterationIterations = result.first; + overallIterations += result.first; + + if (result.second != SolverStatus::Converged) { + status = result.second; + } else { + bool intervalIterationNeeded = false; + currentVerificationIterations = 0; + + if (relative) { + oviinternal::guessUpperBoundRelative(*lowerX, *upperX, relativeBoundGuessingScaler); + } else { + oviinternal::guessUpperBoundAbsolute(*lowerX, *upperX, precision); + } + + bool cancelGuess = false; + while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { + ++overallIterations; + ++currentVerificationIterations; + // Perform value iteration stepwise for lower bound and guessed upper bound + + // Upper bound iteration + auto upperBoundIterResult = dir ? upperBoundIterator.iterate(dir.get(), *upperX, b, !noTerminationGuarantee) : upperBoundIterator.iterate(*upperX, b, !noTerminationGuarantee); + + if (upperBoundIterResult == oviinternal::UpperBoundIterator::IterateResult::AlwaysHigherOrEqual) { + // All values moved up (and did not stay the same) + // That means the guess for an upper bound is actually a lower bound + iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues); + // We assume to have a single fixed point. We can thus safely set the new lower bound, to the wrongly guessed upper bound + // Set lowerX to the upper bound candidate + std::swap(lowerX, upperX); + break; + } else if (upperBoundIterResult == oviinternal::UpperBoundIterator::IterateResult::AlwaysLowerOrEqual) { + // All values moved down (and stayed not the same) + // This is a valid upper bound. We still need to check the precision. + // We can safely use twice the requested precision, as we calculate the center of both vectors + bool reachedPrecision; + if (relevantValues) { + reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, relevantValues.get(), doublePrecision, relative); + } else { + reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, doublePrecision, relative); + } + if (reachedPrecision) { + status = SolverStatus::Converged; + break; + } else { + // From now on, we keep updating both bounds + intervalIterationNeeded = true; + } + // The following case below covers that both vectors (old and new) are equal. + // Theoretically, this means that the precise fixpoint has been reached. However, numerical instabilities can be tricky and this detection might be incorrect (see the haddad-monmege model). + // We therefore disable it. It is very unlikely that we guessed the right fixpoint anyway. + //} else if (upperBoundIterResult == oviinternal::UpperBoundIterator::IterateResult::Equal) { + // In this case, the guessed upper bound is the precise fixpoint + // status = SolverStatus::Converged; + // std::swap(lowerX, auxVector); + // break; + } + + // Check whether we tried this guess for too long + ValueType scaledIterationCount = storm::utility::convertNumber(currentVerificationIterations) * storm::utility::convertNumber(env.solver().ovi().getMaxVerificationIterationFactor()); + if (!intervalIterationNeeded && scaledIterationCount >= storm::utility::convertNumber(lastValueIterationIterations)) { + cancelGuess = true; + // In this case we will make one more iteration on the lower bound (mainly to obtain a new iterationPrecision) + } + + // Lower bound iteration (only if needed) + if (cancelGuess || intervalIterationNeeded || currentVerificationIterations > upperBoundOnlyIterations) { + singleIterationCallback(lowerX, auxVector, overallIterations); + // At this point, auxVector contains the old values for the lower bound whereas lowerX contains the new ones. + + // Check whether the upper and lower bounds have crossed, i.e., the upper bound is smaller than the lower bound. + bool valuesCrossed = false; + for (uint64_t i = 0; i < lowerX->size(); ++i) { + if ((*upperX)[i] < (*lowerX)[i]) { + valuesCrossed = true; + break; + } + } + + if (cancelGuess || valuesCrossed) { + // A new guess is needed. + iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *lowerX, relative, relevantValues); + break; + } + } + } + if (storm::utility::resources::isTerminate()) { + status = SolverStatus::Aborted; + } + } + } // end while + + // Swap the results into the output vectors. + if (initLowerX == lowerX) { + // lowerX is already at the correct position. We still have to care for upperX + if (initUpperX != upperX) { + // UpperX is not at the correct position. It has to be at the auxVector + assert(initAux == upperX); + std::swap(*initUpperX, *initAux); + } + } else if (initUpperX == upperX) { + // UpperX is already at the correct position. + // We already know that lowerX is at the wrong position. It has to be at the auxVector + assert(initAux == lowerX); + std::swap(*initLowerX, *initAux); + } else if (initAux == auxVector) { + // We know that upperX and lowerX are swapped. + assert(initLowerX == upperX); + assert(initUpperX == lowerX); + std::swap(*initUpperX, *initLowerX); + } else { + // Now we know that all vectors are at the wrong position. There are only two possibilities left + if (initLowerX == upperX) { + assert(initUpperX == auxVector); + assert(initAux == lowerX); + std::swap(*initLowerX, *initAux); + std::swap(*initUpperX, *initAux); + } else { + assert(initLowerX == auxVector); + assert(initUpperX == lowerX); + assert (initAux == upperX); + std::swap(*initUpperX, *initAux); + std::swap(*initLowerX, *initAux); + } + } + + if (overallIterations > maxOverallIterations) { + status = SolverStatus::MaximalIterationsExceeded; + } + + return {status, overallIterations}; + } + + + template class OptimisticValueIterationHelper; + template class OptimisticValueIterationHelper; + } + } +} + diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h index 75adafb09..abf67dd3c 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.h +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h @@ -3,312 +3,104 @@ #include #include +#include "storm/storage/SparseMatrix.h" + #include "storm/solver/OptimizationDirection.h" #include "storm/solver/SolverStatus.h" -#include "storm/utility/vector.h" -#include "storm/utility/ProgressMeasurement.h" -#include "storm/utility/SignalHandler.h" #include "storm/storage/BitVector.h" -#include "storm/environment/solver/MinMaxSolverEnvironment.h" -#include "storm/environment/solver/OviSolverEnvironment.h" -#include "storm/utility/macros.h" namespace storm { + class Environment; namespace solver { namespace helper { namespace oviinternal { - template - ValueType computeMaxAbsDiff(std::vector const& allOldValues, std::vector const& allNewValues, storm::storage::BitVector const& relevantValues) { - ValueType result = storm::utility::zero(); - for (auto value : relevantValues) { - result = storm::utility::max(result, storm::utility::abs(allNewValues[value] - allOldValues[value])); - } - return result; - } - - template - ValueType computeMaxAbsDiff(std::vector const& allOldValues, std::vector const& allNewValues) { - ValueType result = storm::utility::zero(); - for (uint64_t i = 0; i < allOldValues.size(); ++i) { - result = storm::utility::max(result, storm::utility::abs(allNewValues[i] - allOldValues[i])); - } - return result; - } - - template - ValueType computeMaxRelDiff(std::vector const& allOldValues, std::vector const& allNewValues, storm::storage::BitVector const& relevantValues) { - ValueType result = storm::utility::zero(); - for (auto const& i : relevantValues) { - STORM_LOG_ASSERT(!storm::utility::isZero(allNewValues[i]) || storm::utility::isZero(allOldValues[i]), "Unexpected entry in iteration vector."); - if (!storm::utility::isZero(allNewValues[i])) { - result = storm::utility::max(result, storm::utility::abs(allNewValues[i] - allOldValues[i]) / allNewValues[i]); - } - } - return result; - } + template + class UpperBoundIterator { + public: + typedef uint32_t IndexType; + UpperBoundIterator(storm::storage::SparseMatrix const& matrix); + enum class IterateResult { + AlwaysHigherOrEqual, + AlwaysLowerOrEqual, + Equal, + Incomparable + }; + + IterateResult iterate(std::vector& x, std::vector const& b, bool takeMinOfOldAndNew); + IterateResult iterate(storm::solver::OptimizationDirection const& dir, std::vector& x, std::vector const& b, bool takeMinOfOldAndNew); - template - ValueType computeMaxRelDiff(std::vector const& allOldValues, std::vector const& allNewValues) { - ValueType result = storm::utility::zero(); - for (uint64_t i = 0; i < allOldValues.size(); ++i) { - STORM_LOG_ASSERT(!storm::utility::isZero(allNewValues[i]) || storm::utility::isZero(allOldValues[i]), "Unexpected entry in iteration vector."); - if (!storm::utility::isZero(allNewValues[i])) { - result = storm::utility::max(result, storm::utility::abs(allNewValues[i] - allOldValues[i]) / allNewValues[i]); - } - } - return result; - } - - template - ValueType updateIterationPrecision(storm::Environment const& env, std::vector const& currentX, std::vector const& newX, bool const& relative, boost::optional const& relevantValues) { - auto factor = storm::utility::convertNumber(env.solver().ovi().getPrecisionUpdateFactor()); - bool useRelevant = relevantValues.is_initialized() && env.solver().ovi().useRelevantValuesForPrecisionUpdate(); - if (relative) { - return (useRelevant ? computeMaxRelDiff(newX, currentX, relevantValues.get()) : computeMaxRelDiff(newX, currentX)) * factor; - } else { - return (useRelevant ? computeMaxAbsDiff(newX, currentX, relevantValues.get()) : computeMaxAbsDiff(newX, currentX)) * factor; - } - } - - template - void guessUpperBoundRelative(std::vector const& x, std::vector &target, ValueType const& relativeBoundGuessingScaler) { - storm::utility::vector::applyPointwise(x, target, [&relativeBoundGuessingScaler] (ValueType const& argument) -> ValueType { return argument * relativeBoundGuessingScaler; }); - } - - template - void guessUpperBoundAbsolute(std::vector const& x, std::vector &target, ValueType const& precision) { - storm::utility::vector::applyPointwise(x, target, [&precision] (ValueType const& argument) -> ValueType { return argument + precision; }); - } - + private: + + template + IterateResult iterateInternal(std::vector& x, std::vector const& b, bool takeMinOfOldAndNew); + ValueType multiplyRow(IndexType const& rowIndex, ValueType const& bi, std::vector const& x); + template + ValueType multiplyRowGroup(IndexType const& rowGroupIndex, std::vector const& b, std::vector const& x); + + std::vector matrixValues; + std::vector matrixColumns; + std::vector rowIndications; + std::vector const* rowGroupIndices; + }; } - /*! * Performs Optimistic value iteration. - * See https://arxiv.org/abs/1910.01100 for more information on this algorithm - * - * @tparam ValueType - * @tparam ValueType - * @param env - * @param lowerX Needs to be some arbitrary lower bound on the actual values initially - * @param upperX Does not need to be an upper bound initially - * @param auxVector auxiliary storage - * @param valueIterationCallback Function that should perform standard value iteration on the input vector - * @param singleIterationCallback Function that should perform a single value iteration step on the input vector e.g. ( x' = min/max(A*x + b)) - * @param relevantValues If given, we only check the precision at the states with the given indices. - * @return The status upon termination as well as the number of iterations Also, the maximum (relative/absolute) difference between lowerX and upperX will be 2*epsilon - * with precision parameters as given by the environment env. + * @see Hartmanns, Kaminski: Optimistic Value Iteration. https://doi.org/10.1007/978-3-030-53291-8\_26 */ - template - std::pair solveEquationsOptimisticValueIteration(Environment const& env, std::vector* lowerX, std::vector* upperX, std::vector* auxVector, ValueIterationCallback const& valueIterationCallback, SingleIterationCallback const& singleIterationCallback, bool relative, ValueType precision, uint64_t maxOverallIterations, boost::optional relevantValues = boost::none) { - STORM_LOG_ASSERT(lowerX->size() == upperX->size(), "Dimension missmatch."); - STORM_LOG_ASSERT(lowerX->size() == auxVector->size(), "Dimension missmatch."); - - // As we will shuffle pointers around, let's store the original positions here. - std::vector* initLowerX = lowerX; - std::vector* initUpperX = upperX; - std::vector* initAux = auxVector; - - uint64_t overallIterations = 0; - uint64_t lastValueIterationIterations = 0; - uint64_t currentVerificationIterations = 0; - uint64_t valueIterationInvocations = 0; - - // Get some parameters for the algorithm - // 2 - ValueType two = storm::utility::convertNumber(2.0); - // Use no termination guaranteed upper bound iteration method - bool noTerminationGuarantee = env.solver().ovi().useNoTerminationGuaranteeMinimumMethod(); - // Desired max difference between upperX and lowerX - ValueType doublePrecision = precision * two; - // Upper bound only iterations - uint64_t upperBoundOnlyIterations = env.solver().ovi().getUpperBoundOnlyIterations(); - ValueType relativeBoundGuessingScaler = (storm::utility::one() + storm::utility::convertNumber(env.solver().ovi().getUpperBoundGuessingFactor()) * precision); - // Initial precision for the value iteration calls - ValueType iterationPrecision = precision; + template + class OptimisticValueIterationHelper { + public: + OptimisticValueIterationHelper(storm::storage::SparseMatrix const& matrix); - SolverStatus status = SolverStatus::InProgress; - - while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { - - // Perform value iteration until convergence - ++valueIterationInvocations; - auto result = valueIterationCallback(lowerX, auxVector, iterationPrecision, relative, overallIterations, maxOverallIterations); - lastValueIterationIterations = result.iterations; - overallIterations += result.iterations; - - if (result.status != SolverStatus::Converged) { - status = result.status; - } else { - bool intervalIterationNeeded = false; - currentVerificationIterations = 0; - - if (relative) { - oviinternal::guessUpperBoundRelative(*lowerX, *upperX, relativeBoundGuessingScaler); - } else { - oviinternal::guessUpperBoundAbsolute(*lowerX, *upperX, precision); - } - - bool cancelGuess = false; - while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { - ++overallIterations; - ++currentVerificationIterations; - // Perform value iteration stepwise for lower bound and guessed upper bound - - // Upper bound iteration - singleIterationCallback(upperX, auxVector, overallIterations); - // At this point, auxVector contains the old values for the upper bound whereas upperX contains the new ones. - - // Compare the new upper bound candidate with the old one - bool newUpperBoundAlwaysHigherEqual = true; - bool newUpperBoundAlwaysLowerEqual = true; - if (noTerminationGuarantee) { - bool cancelOuterScan = false; - for (uint64_t i = 0; i < upperX->size() && !cancelOuterScan; ++i) { - if ((*upperX)[i] < (*auxVector)[i]) { - newUpperBoundAlwaysHigherEqual = false; - for (++i; i < upperX->size(); ++i) { - if ((*upperX)[i] > (*auxVector)[i]) { - newUpperBoundAlwaysLowerEqual = false; - cancelOuterScan = true; - break; - } - } - } else if ((*upperX)[i] != (*auxVector)[i]) { - newUpperBoundAlwaysLowerEqual = false; - for (++i; i < upperX->size(); ++i) { - if ((*upperX)[i] < (*auxVector)[i]) { - newUpperBoundAlwaysHigherEqual = false; - cancelOuterScan = true; - break; - } - } - } - } - } else { - for (uint64_t i = 0; i < upperX->size(); ++i) { - if ((*upperX)[i] < (*auxVector)[i]) { - newUpperBoundAlwaysHigherEqual = false; - } else if ((*upperX)[i] != (*auxVector)[i]) { - newUpperBoundAlwaysLowerEqual = false; - std::swap((*upperX)[i], (*auxVector)[i]); - } - } - } - - if (newUpperBoundAlwaysHigherEqual && !newUpperBoundAlwaysLowerEqual) { - // All values moved up or stayed the same - // That means the guess for an upper bound is actually a lower bound - iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues); - // We assume to have a single fixed point. We can thus safely set the new lower bound, to the wrongly guessed upper bound - // Set lowerX to the upper bound candidate - std::swap(lowerX, upperX); - break; - } else if (newUpperBoundAlwaysLowerEqual && !newUpperBoundAlwaysHigherEqual) { - // All values moved down or stayed the same and we have a maximum difference of twice the requested precision - // We can safely use twice the requested precision, as we calculate the center of both vectors - bool reachedPrecision; - if (relevantValues) { - reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, relevantValues.get(), doublePrecision, relative); - } else { - reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, doublePrecision, relative); - } - if (reachedPrecision) { - status = SolverStatus::Converged; - break; - } else { - // From now on, we keep updating both bounds - intervalIterationNeeded = true; - } - // The following case below covers that bouth vectors (old and new) are equal. - // Theoretically, this means that the precise fixpoint has been reached. However, numerical instabilities can be tricky and this detection might be incorrect (see the haddad-monmege model). - // We therefore disable it. It is very unlikely that we guessed the right fixpoint anyway. - //} else if (newUpperBoundAlwaysHigherEqual && newUpperBoundAlwaysLowerEqual) { - // In this case, the guessed upper bound is the precise fixpoint - // status = SolverStatus::Converged; - // std::swap(lowerX, auxVector); - // break; - } - // At this point, the old upper bounds (auxVector) are not needed anymore. - - // Check whether we tried this guess for too long - ValueType scaledIterationCount = storm::utility::convertNumber(currentVerificationIterations) * storm::utility::convertNumber(env.solver().ovi().getMaxVerificationIterationFactor()); - if (!intervalIterationNeeded && scaledIterationCount >= storm::utility::convertNumber(lastValueIterationIterations)) { - cancelGuess = true; - // In this case we will make one more iteration on the lower bound (mainly to obtain a new iterationPrecision) - } - - // Lower bound iteration (only if needed) - if (cancelGuess || intervalIterationNeeded || currentVerificationIterations > upperBoundOnlyIterations) { - singleIterationCallback(lowerX, auxVector, overallIterations); - // At this point, auxVector contains the old values for the lower bound whereas lowerX contains the new ones. - - // Check whether the upper and lower bounds have crossed, i.e., the upper bound is smaller than the lower bound. - bool valuesCrossed = false; - for (uint64_t i = 0; i < lowerX->size(); ++i) { - if ((*upperX)[i] < (*lowerX)[i]) { - valuesCrossed = true; - break; - } - } - - if (cancelGuess || valuesCrossed) { - // A new guess is needed. - iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *lowerX, relative, relevantValues); - break; - } - } - } - if (storm::utility::resources::isTerminate()) { - status = SolverStatus::Aborted; - } - } - } // end while + /*! + * Return type of value iteration callback. + * The first component shall be the number of performed iterations, the second component is the final convergence status. + */ + typedef std::pair ValueIterationReturnType; - // Swap the results into the output vectors. - if (initLowerX == lowerX) { - // lowerX is already at the correct position. We still have to care for upperX - if (initUpperX != upperX) { - // UpperX is not at the correct position. It has to be at the auxVector - assert(initAux == upperX); - std::swap(*initUpperX, *initAux); - } - } else if (initUpperX == upperX) { - // UpperX is already at the correct position. - // We already know that lowerX is at the wrong position. It has to be at the auxVector - assert(initAux == lowerX); - std::swap(*initLowerX, *initAux); - } else if (initAux == auxVector) { - // We know that upperX and lowerX are swapped. - assert(initLowerX == upperX); - assert(initUpperX == lowerX); - std::swap(*initUpperX, *initLowerX); - } else { - // Now we know that all vectors are at the wrong position. There are only two possibilities left - if (initLowerX == upperX) { - assert(initUpperX == auxVector); - assert(initAux == lowerX); - std::swap(*initLowerX, *initAux); - std::swap(*initUpperX, *initAux); - } else { - assert(initLowerX == auxVector); - assert(initUpperX == lowerX); - assert (initAux == upperX); - std::swap(*initUpperX, *initAux); - std::swap(*initLowerX, *initAux); - } - } + /*! + * Value iteration callback. Performs conventional value iteration for the given input. + * @pre y points to a vector that contains starting values + * @post y points to a vector that contains resulting values + * @param yPrime points to auxiliary storage + * @param precision is the target precision + * @param relative sets whether relative precision is considered + * @param maxI the maximal number of iterations to perform + */ + typedef std::function*& y, std::vector*& yPrime, ValueType const& precision, bool const& relative, uint64_t const& i, uint64_t const& maxI)> ValueIterationCallBackType; - if (overallIterations > maxOverallIterations) { - status = SolverStatus::MaximalIterationsExceeded; - } + /*! + * Should perform a single value iteration step (using conventional value iteration). + * @pre y points to a vector that contains starting values + * @post y points to a vector that contains resulting values + * @param yPrime points to auxiliary storage + * @param currI the current iteration (can be used to display progress within the callback) + */ + typedef std::function* y, std::vector* yPrime, uint64_t const& currI)> SingleIterationCallBackType; - return {status, overallIterations}; - } + /*! + * @param env + * @param lowerX Needs to be some arbitrary lower bound on the actual values initially + * @param upperX Does not need to be an upper bound initially + * @param auxVector auxiliary storage (same size as lowerX and upperX) + * @param b the values added to each matrix row (the b in A*x+b) + * @param valueIterationCallback Function that should perform standard value iteration on the input vector + * @param singleIterationCallback Function that should perform a single value iteration step on the input vector e.g. ( x' = min/max(A*x + b)) + * @param dir The optimization direction + * @param relevantValues If given, we only check the precision at the states with the given indices. + * @return The status upon termination as well as the number of iterations Also, the maximum (relative/absolute) difference between lowerX and upperX will be 2*epsilon + * with the provided precision parameters. + */ + std::pair solveEquationsOptimisticValueIteration(Environment const& env, std::vector* lowerX, std::vector* upperX, std::vector* auxVector, std::vector const& b, ValueIterationCallBackType const& valueIterationCallback, SingleIterationCallBackType const& singleIterationCallback, bool relative, ValueType precision, uint64_t maxOverallIterations, boost::optional dir, boost::optional relevantValues = boost::none); + + private: + oviinternal::UpperBoundIterator upperBoundIterator; + + }; } } } - From f45b56e72566e3b4727c61218834f374448a91e1 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 26 Aug 2020 16:56:09 -0700 Subject: [PATCH 12/33] convenience operation on prism programs --- src/storm/storage/prism/Module.cpp | 10 ++++++++++ src/storm/storage/prism/Module.h | 5 +++++ src/storm/storage/prism/Program.cpp | 10 +++++++++- src/storm/storage/prism/Program.h | 7 ++++++- 4 files changed, 30 insertions(+), 2 deletions(-) diff --git a/src/storm/storage/prism/Module.cpp b/src/storm/storage/prism/Module.cpp index 4f141e1aa..512985ded 100644 --- a/src/storm/storage/prism/Module.cpp +++ b/src/storm/storage/prism/Module.cpp @@ -114,6 +114,16 @@ namespace storm { bool Module::hasActionIndex(uint_fast64_t actionIndex) const { return this->actionIndicesToCommandIndexMap.find(actionIndex) != this->actionIndicesToCommandIndexMap.end(); } + + uint64_t Module::getNumberOfUnlabeledCommands() const { + uint64_t result = 0; + for (auto const& cmd : commands) { + if(!cmd.isLabeled()) { + result++; + } + } + return result; + } bool Module::isRenamedFromModule() const { return this->renamedFromModule != ""; diff --git a/src/storm/storage/prism/Module.h b/src/storm/storage/prism/Module.h index 202788816..138dfbe09 100644 --- a/src/storm/storage/prism/Module.h +++ b/src/storm/storage/prism/Module.h @@ -263,6 +263,11 @@ namespace storm { * Equips all of the modules' variables without initial values with initial values based on their type. */ void createMissingInitialValues(); + + /* + * Gets the number of commands without a label + */ + uint64_t getNumberOfUnlabeledCommands() const; /*! * Returns true, if an invariant was specified (only relevant for PTA models) diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index dfba08050..cdd41f7c3 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -508,7 +508,15 @@ namespace storm { std::map const& Program::getActionNameToIndexMapping() const { return actionToIndexMap; } - + + uint64_t Program::getNumberOfUnlabeledCommands() const { + uint64_t result = 0; + for (auto const& m : modules) { + result += m.getNumberOfUnlabeledCommands(); + } + return result; + } + bool Program::hasInitialConstruct() const { return static_cast(initialConstruct); } diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index 502cd2a46..0860dd913 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -462,7 +462,12 @@ namespace storm { * @return the index of the module and the (local) index of the found command */ std::pair getModuleCommandIndexByGlobalCommandIndex(uint_fast64_t globalCommandIndex) const; - + + /* + * Get total number of unlabeled commands + */ + uint64_t getNumberOfUnlabeledCommands() const; + /*! * Retrieves whether the program has reward models. * From 1b2a78e9ac70b96020b742ef0a58e85599bd5557 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 3 Sep 2020 13:55:22 +0200 Subject: [PATCH 13/33] Abstract equation solver: added getOptionalRelevantValues --- src/storm/solver/AbstractEquationSolver.cpp | 5 +++++ src/storm/solver/AbstractEquationSolver.h | 1 + 2 files changed, 6 insertions(+) diff --git a/src/storm/solver/AbstractEquationSolver.cpp b/src/storm/solver/AbstractEquationSolver.cpp index d8e3e7b91..c068e5d31 100644 --- a/src/storm/solver/AbstractEquationSolver.cpp +++ b/src/storm/solver/AbstractEquationSolver.cpp @@ -66,6 +66,11 @@ namespace storm { return relevantValues.get(); } + template + boost::optional const& AbstractEquationSolver::getOptionalRelevantValues() const { + return relevantValues; + } + template void AbstractEquationSolver::setRelevantValues(storm::storage::BitVector&& relevantValues) { this->relevantValues = std::move(relevantValues); diff --git a/src/storm/solver/AbstractEquationSolver.h b/src/storm/solver/AbstractEquationSolver.h index 8e303f042..0301ad42e 100644 --- a/src/storm/solver/AbstractEquationSolver.h +++ b/src/storm/solver/AbstractEquationSolver.h @@ -52,6 +52,7 @@ namespace storm { * Retrieves the relevant values (if there are any). */ storm::storage::BitVector const& getRelevantValues() const; + boost::optional const& getOptionalRelevantValues() const; /*! * Sets the relevant values. From 684c239f8087c6531986c008d0d85ac947150065 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 3 Sep 2020 13:56:26 +0200 Subject: [PATCH 14/33] Using the revamped optimistic value iteration helper also for the lower bound. --- .../IterativeMinMaxLinearEquationSolver.cpp | 58 +--- .../IterativeMinMaxLinearEquationSolver.h | 2 + .../solver/NativeLinearEquationSolver.cpp | 53 +-- src/storm/solver/NativeLinearEquationSolver.h | 2 + .../helper/OptimisticValueIterationHelper.cpp | 321 ++++++++++-------- .../helper/OptimisticValueIterationHelper.h | 56 ++- 6 files changed, 232 insertions(+), 260 deletions(-) diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 089ba266e..5e71c0503 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -2,7 +2,6 @@ #include #include "storm/solver/IterativeMinMaxLinearEquationSolver.h" -#include "storm/solver/helper/OptimisticValueIterationHelper.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/environment/solver/OviSolverEnvironment.h" @@ -369,63 +368,28 @@ namespace storm { return true; } - if (!this->multiplierA) { - this->multiplierA = storm::solver::MultiplierFactory().create(env, *this->A); - } - if (!auxiliaryRowGroupVector) { auxiliaryRowGroupVector = std::make_unique>(this->A->getRowGroupCount()); } - if (!auxiliaryRowGroupVector2) { - auxiliaryRowGroupVector2 = std::make_unique>(this->A->getRowGroupCount()); + if (!optimisticValueIterationHelper) { + optimisticValueIterationHelper = std::make_unique>(*this->A); } - // By default, we can not provide any guarantee - SolverGuarantee guarantee = SolverGuarantee::None; - // Get handle to multiplier. - storm::solver::Multiplier const &multiplier = *this->multiplierA; - // Allow aliased multiplications. - storm::solver::MultiplicationStyle multiplicationStyle = env.solver().minMax().getMultiplicationStyle(); - bool useGaussSeidelMultiplication = multiplicationStyle == storm::solver::MultiplicationStyle::GaussSeidel; - - boost::optional relevantValues; - if (this->hasRelevantValues()) { - relevantValues = this->getRelevantValues(); - } + storm::solver::helper::OptimisticValueIterationHelper helper(*this->A); // x has to start with a lower bound. this->createLowerBoundsVector(x); std::vector* lowerX = &x; std::vector* upperX = auxiliaryRowGroupVector.get(); - std::vector* auxVector = auxiliaryRowGroupVector2.get(); - this->startMeasureProgress(); - storm::solver::helper::OptimisticValueIterationHelper helper(*this->A); - auto statusIters = helper.solveEquationsOptimisticValueIteration(env, lowerX, upperX, auxVector, b, - [&] (std::vector*& y, std::vector*& yPrime, ValueType const& precision, bool const& relative, uint64_t const& i, uint64_t const& maxI) { - this->showProgressIterative(i); - auto result = performValueIteration(env, dir, y, yPrime, b, precision, relative, guarantee, i, maxI, multiplicationStyle); - return std::make_pair(result.iterations, result.status); - }, - [&] (std::vector* y, std::vector* yPrime, uint64_t const& i) { - this->showProgressIterative(i); - if (useGaussSeidelMultiplication) { - // Copy over the current vectors so we can modify them in-place. - // This is necessary as we want to compare the new values with the current ones. - *yPrime = *y; - multiplier.multiplyAndReduceGaussSeidel(env, dir, *y, &b); - } else { - multiplier.multiplyAndReduce(env, dir, *y, &b, *yPrime); - std::swap(y, yPrime); - } - }, - env.solver().minMax().getRelativeTerminationCriterion(), - storm::utility::convertNumber(env.solver().minMax().getPrecision()), - env.solver().minMax().getMaximalNumberOfIterations(), - dir, - relevantValues); + auto statusIters = helper.solveEquations(env, lowerX, upperX, b, + env.solver().minMax().getRelativeTerminationCriterion(), + storm::utility::convertNumber(env.solver().minMax().getPrecision()), + env.solver().minMax().getMaximalNumberOfIterations(), + dir, + this->getOptionalRelevantValues()); auto two = storm::utility::convertNumber(2.0); storm::utility::vector::applyPointwise(*lowerX, *upperX, x, [&two] (ValueType const& a, ValueType const& b) -> ValueType { return (a + b) / two; }); @@ -434,8 +398,7 @@ namespace storm { // If requested, we store the scheduler for retrieval. if (this->isTrackSchedulerSet()) { this->schedulerChoices = std::vector(this->A->getRowGroupCount()); - this->multiplierA->multiplyAndReduce(env, dir, x, &b, *auxiliaryRowGroupVector.get(), &this->schedulerChoices.get()); - this->multiplierA->multiplyAndReduce(env, dir, x, &b, *auxiliaryRowGroupVector.get(), &this->schedulerChoices.get()); + this->A->multiplyAndReduce(dir, this->A->getRowGroupIndices(), x, &b, *auxiliaryRowGroupVector.get(), &this->schedulerChoices.get()); } if (!this->isCachingEnabled()) { @@ -1109,6 +1072,7 @@ namespace storm { auxiliaryRowGroupVector.reset(); auxiliaryRowGroupVector2.reset(); soundValueIterationHelper.reset(); + optimisticValueIterationHelper.reset(); StandardMinMaxLinearEquationSolver::clearCache(); } diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h index 6582caefa..be268f35f 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h @@ -8,6 +8,7 @@ #include "storm/solver/Multiplier.h" #include "storm/solver/StandardMinMaxLinearEquationSolver.h" #include "storm/solver/helper/SoundValueIterationHelper.h" +#include "storm/solver/helper/OptimisticValueIterationHelper.h" #include "storm/solver/SolverStatus.h" @@ -85,6 +86,7 @@ namespace storm { mutable std::unique_ptr> auxiliaryRowGroupVector; // A.rowGroupCount() entries mutable std::unique_ptr> auxiliaryRowGroupVector2; // A.rowGroupCount() entries mutable std::unique_ptr> soundValueIterationHelper; + mutable std::unique_ptr> optimisticValueIterationHelper; }; diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index 9ca9683fc..82bf7d5ec 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -643,62 +643,26 @@ namespace storm { return true; } - if (!this->multiplier) { - this->multiplier = storm::solver::MultiplierFactory().create(env, *this->A); - } - if (!this->cachedRowVector) { this->cachedRowVector = std::make_unique>(this->A->getRowCount()); } - if (!this->cachedRowVector2) { - this->cachedRowVector2 = std::make_unique>(this->A->getRowCount()); + if (!optimisticValueIterationHelper) { + optimisticValueIterationHelper = std::make_unique>(*this->A); } - // By default, we can not provide any guarantee - SolverGuarantee guarantee = SolverGuarantee::None; - // Get handle to multiplier. - storm::solver::Multiplier const &multiplier = *this->multiplier; - // Allow aliased multiplications. - storm::solver::MultiplicationStyle multiplicationStyle = env.solver().native().getPowerMethodMultiplicationStyle(); - bool useGaussSeidelMultiplication = multiplicationStyle == storm::solver::MultiplicationStyle::GaussSeidel; - - boost::optional relevantValues; - if (this->hasRelevantValues()) { - relevantValues = this->getRelevantValues(); - } - // x has to start with a lower bound. this->createLowerBoundsVector(x); std::vector* lowerX = &x; std::vector* upperX = this->cachedRowVector.get(); - std::vector* auxVector = this->cachedRowVector2.get(); - this->startMeasureProgress(); storm::solver::helper::OptimisticValueIterationHelper helper(*this->A); - auto statusIters = helper.solveEquationsOptimisticValueIteration(env, lowerX, upperX, auxVector, b, - [&] (std::vector*& y, std::vector*& yPrime, ValueType const& precision, bool const& relative, uint64_t const& i, uint64_t const& maxI) { - this->showProgressIterative(i); - auto result = performPowerIteration(env, y, yPrime, b, precision, relative, guarantee, i, maxI, multiplicationStyle); - return std::make_pair(result.iterations, result.status); - }, - [&] (std::vector* y, std::vector* yPrime, uint64_t const& i) { - this->showProgressIterative(i); - if (useGaussSeidelMultiplication) { - // Copy over the current vectors so we can modify them in-place. - // This is necessary as we want to compare the new values with the current ones. - *yPrime = *y; - multiplier.multiplyGaussSeidel(env, *y, &b); - } else { - multiplier.multiply(env, *y, &b, *yPrime); - std::swap(y, yPrime); - } - }, - env.solver().native().getRelativeTerminationCriterion(), - storm::utility::convertNumber(env.solver().native().getPrecision()), - env.solver().native().getMaximalNumberOfIterations(), - boost::none, // No optimization dir - relevantValues); + auto statusIters = helper.solveEquations(env, lowerX, upperX, b, + env.solver().native().getRelativeTerminationCriterion(), + storm::utility::convertNumber(env.solver().native().getPrecision()), + env.solver().native().getMaximalNumberOfIterations(), + boost::none, // No optimization dir + this->getOptionalRelevantValues()); auto two = storm::utility::convertNumber(2.0); storm::utility::vector::applyPointwise(*lowerX, *upperX, x, [&two] (ValueType const& a, ValueType const& b) -> ValueType { return (a + b) / two; }); this->logIterations(statusIters.first == SolverStatus::Converged, statusIters.first == SolverStatus::TerminatedEarly, statusIters.second); @@ -1066,6 +1030,7 @@ namespace storm { walkerChaeData.reset(); multiplier.reset(); soundValueIterationHelper.reset(); + optimisticValueIterationHelper.reset(); LinearEquationSolver::clearCache(); } diff --git a/src/storm/solver/NativeLinearEquationSolver.h b/src/storm/solver/NativeLinearEquationSolver.h index d551cd931..93c627a86 100644 --- a/src/storm/solver/NativeLinearEquationSolver.h +++ b/src/storm/solver/NativeLinearEquationSolver.h @@ -9,6 +9,7 @@ #include "storm/solver/NativeMultiplier.h" #include "storm/solver/SolverStatus.h" #include "storm/solver/helper/SoundValueIterationHelper.h" +#include "storm/solver/helper/OptimisticValueIterationHelper.h" #include "storm/utility/NumberTraits.h" @@ -96,6 +97,7 @@ namespace storm { // cached auxiliary data mutable std::unique_ptr> cachedRowVector2; // A.getRowCount() rows mutable std::unique_ptr> soundValueIterationHelper; + mutable std::unique_ptr> optimisticValueIterationHelper; struct JacobiDecomposition { JacobiDecomposition(Environment const& env, storm::storage::SparseMatrix const& A); diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.cpp b/src/storm/solver/helper/OptimisticValueIterationHelper.cpp index d52d41d37..28644d5de 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.cpp +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.cpp @@ -35,7 +35,7 @@ namespace storm { template ValueType computeMaxRelDiff(std::vector const& allOldValues, std::vector const& allNewValues, storm::storage::BitVector const& relevantValues) { ValueType result = storm::utility::zero(); - for (auto const& i : relevantValues) { + for (auto i : relevantValues) { STORM_LOG_ASSERT(!storm::utility::isZero(allNewValues[i]) || storm::utility::isZero(allOldValues[i]), "Unexpected entry in iteration vector."); if (!storm::utility::isZero(allNewValues[i])) { result = storm::utility::max(result, storm::utility::abs(allNewValues[i] - allOldValues[i]) / allNewValues[i]); @@ -48,7 +48,7 @@ namespace storm { ValueType computeMaxRelDiff(std::vector const& allOldValues, std::vector const& allNewValues) { ValueType result = storm::utility::zero(); for (uint64_t i = 0; i < allOldValues.size(); ++i) { - STORM_LOG_ASSERT(!storm::utility::isZero(allNewValues[i]) || storm::utility::isZero(allOldValues[i]), "Unexpected entry in iteration vector."); + STORM_LOG_WARN_COND(!storm::utility::isZero(allNewValues[i]) || storm::utility::isZero(allOldValues[i]), "Unexpected entry in iteration vector."); if (!storm::utility::isZero(allNewValues[i])) { result = storm::utility::max(result, storm::utility::abs(allNewValues[i] - allOldValues[i]) / allNewValues[i]); } @@ -57,14 +57,9 @@ namespace storm { } template - ValueType updateIterationPrecision(storm::Environment const& env, std::vector const& currentX, std::vector const& newX, bool const& relative, boost::optional const& relevantValues) { + ValueType updateIterationPrecision(storm::Environment const& env, ValueType const& diff) { auto factor = storm::utility::convertNumber(env.solver().ovi().getPrecisionUpdateFactor()); - bool useRelevant = relevantValues.is_initialized() && env.solver().ovi().useRelevantValuesForPrecisionUpdate(); - if (relative) { - return (useRelevant ? computeMaxRelDiff(newX, currentX, relevantValues.get()) : computeMaxRelDiff(newX, currentX)) * factor; - } else { - return (useRelevant ? computeMaxAbsDiff(newX, currentX, relevantValues.get()) : computeMaxAbsDiff(newX, currentX)) * factor; - } + return factor * diff; } template @@ -78,7 +73,7 @@ namespace storm { } template - UpperBoundIterator::UpperBoundIterator(storm::storage::SparseMatrix const& matrix) { + IterationHelper::IterationHelper(storm::storage::SparseMatrix const& matrix) { STORM_LOG_THROW(static_cast(std::numeric_limits::max()) > matrix.getRowCount() + 1, storm::exceptions::NotSupportedException, "Matrix dimensions too large."); STORM_LOG_THROW(static_cast(std::numeric_limits::max()) > matrix.getEntryCount(), storm::exceptions::NotSupportedException, "Matrix dimensions too large."); matrixValues.reserve(matrix.getNonzeroEntryCount()); @@ -97,23 +92,120 @@ namespace storm { } } + + template + ValueType IterationHelper::singleIterationWithDiff(std::vector& x, std::vector const& b, bool computeRelativeDiff) { + return singleIterationWithDiffInternal(x, b, computeRelativeDiff); + } + + template + ValueType IterationHelper::singleIterationWithDiff(storm::solver::OptimizationDirection const& dir, std::vector& x, std::vector const& b, bool computeRelativeDiff) { + if (minimize(dir)) { + return singleIterationWithDiffInternal(x, b, computeRelativeDiff); + } else { + return singleIterationWithDiffInternal(x, b, computeRelativeDiff); + } + } + template - typename UpperBoundIterator::IterateResult UpperBoundIterator::iterate(std::vector& x, std::vector const& b, bool takeMinOfOldAndNew) { - return iterateInternal(x, b, takeMinOfOldAndNew); + template + ValueType IterationHelper::singleIterationWithDiffInternal(std::vector& x, std::vector const& b, bool computeRelativeDiff) { + STORM_LOG_ASSERT(x.size() > 0, "Empty equation system not expected."); + ValueType diff = storm::utility::zero(); + + IndexType i = x.size(); + while (i > 0) { + --i; + ValueType newXi = HasRowGroups ? multiplyRowGroup(i, b, x) : multiplyRow(i, b[i], x); + ValueType& oldXi = x[i]; + if (computeRelativeDiff) { + if (storm::utility::isZero(newXi)) { + if (storm::utility::isZero(oldXi)) { + // this operation has no effect: + // diff = std::max(diff, storm::utility::zero()); + } else { + diff = std::max(diff, storm::utility::one()); + } + } else { + diff = std::max(diff, storm::utility::abs((newXi - oldXi) / newXi)); + } + } else { + diff = std::max(diff, storm::utility::abs(newXi - oldXi)); + } + oldXi = std::move(newXi); + } + return diff; + } + + template + uint64_t IterationHelper::repeatedIterate(storm::solver::OptimizationDirection const& dir, std::vector& x, std::vector const& b, ValueType precision, bool relative) { + if (minimize(dir)) { + return repeatedIterateInternal(x, b, precision, relative); + } else { + return repeatedIterateInternal(x, b, precision, relative); + } + } + + template + uint64_t IterationHelper::repeatedIterate(std::vector& x, const std::vector& b, ValueType precision, bool relative) { + return repeatedIterateInternal(x, b, precision, relative); + } + + template + template + uint64_t IterationHelper::repeatedIterateInternal(std::vector& x, std::vector const& b, ValueType precision, bool relative) { + // Do a backwards gauss-seidel style iteration + bool convergence = true; + IndexType i = x.size(); + while (i > 0) { + --i; + ValueType newXi = HasRowGroups ? multiplyRowGroup(i, b, x) : multiplyRow(i, b[i], x); + ValueType& oldXi = x[i]; + // Check if we converged + if (relative) { + if (storm::utility::isZero(oldXi)) { + if (!storm::utility::isZero(newXi)) { + convergence = false; + break; + } + } else if (storm::utility::abs((newXi - oldXi) / oldXi) > precision) { + convergence = false; + break; + } + } else { + if (storm::utility::abs((newXi - oldXi)) > precision) { + convergence = false; + break; + } + } + } + if (!convergence) { + // we now know that we did not converge. We still need to set the remaining values + while (i > 0) { + --i; + x[i] = HasRowGroups ? multiplyRowGroup(i, b, x) : multiplyRow(i, b[i], x); + } + } + return convergence; } template - typename UpperBoundIterator::IterateResult UpperBoundIterator::iterate(storm::solver::OptimizationDirection const& dir, std::vector& x, std::vector const& b, bool takeMinOfOldAndNew) { + typename IterationHelper::IterateResult IterationHelper::iterateUpper(storm::solver::OptimizationDirection const& dir, std::vector& x, std::vector const& b, bool takeMinOfOldAndNew) { if (minimize(dir)) { - return iterateInternal(x, b, takeMinOfOldAndNew); + return iterateUpperInternal(x, b, takeMinOfOldAndNew); } else { - return iterateInternal(x, b, takeMinOfOldAndNew); + return iterateUpperInternal(x, b, takeMinOfOldAndNew); } } + template + typename IterationHelper::IterateResult IterationHelper::iterateUpper(std::vector& x, std::vector const& b, bool takeMinOfOldAndNew) { + return iterateUpperInternal(x, b, takeMinOfOldAndNew); + } + template template - typename UpperBoundIterator::IterateResult UpperBoundIterator::iterateInternal(std::vector& x, std::vector const& b, bool takeMinOfOldAndNew) { + typename IterationHelper::IterateResult IterationHelper::iterateUpperInternal(std::vector& x, std::vector const& b, bool takeMinOfOldAndNew) { // For each row compare the new upper bound candidate with the old one bool newUpperBoundAlwaysHigherEqual = true; bool newUpperBoundAlwaysLowerEqual = true; @@ -150,7 +242,7 @@ namespace storm { } template - ValueType UpperBoundIterator::multiplyRow(IndexType const& rowIndex, ValueType const& bi, std::vector const& x) { + ValueType IterationHelper::multiplyRow(IndexType const& rowIndex, ValueType const& bi, std::vector const& x) { assert(rowIndex < rowIndications.size()); ValueType xRes = bi; @@ -165,7 +257,7 @@ namespace storm { template template - ValueType UpperBoundIterator::multiplyRowGroup(IndexType const& rowGroupIndex, std::vector const& b, std::vector const& x) { + ValueType IterationHelper::multiplyRowGroup(IndexType const& rowGroupIndex, std::vector const& b, std::vector const& x) { STORM_LOG_ASSERT(rowGroupIndices != nullptr, "No row group indices available."); auto row = (*rowGroupIndices)[rowGroupIndex]; auto const& groupEnd = (*rowGroupIndices)[rowGroupIndex + 1]; @@ -180,24 +272,21 @@ namespace storm { } template - OptimisticValueIterationHelper::OptimisticValueIterationHelper(storm::storage::SparseMatrix const& matrix) : upperBoundIterator(matrix) { + OptimisticValueIterationHelper::OptimisticValueIterationHelper(storm::storage::SparseMatrix const& matrix) : iterationHelper(matrix) { // Intentionally left empty. } template - std::pair OptimisticValueIterationHelper::solveEquationsOptimisticValueIteration(Environment const& env, std::vector* lowerX, std::vector* upperX, std::vector* auxVector, std::vector const& b, ValueIterationCallBackType const& valueIterationCallback, SingleIterationCallBackType const& singleIterationCallback, bool relative, ValueType precision, uint64_t maxOverallIterations, boost::optional dir, boost::optional relevantValues) { + std::pair OptimisticValueIterationHelper::solveEquations(Environment const& env, std::vector* lowerX, std::vector* upperX, std::vector const& b, bool relative, ValueType precision, uint64_t maxOverallIterations, boost::optional dir, boost::optional const& relevantValues) { STORM_LOG_ASSERT(lowerX->size() == upperX->size(), "Dimension missmatch."); - STORM_LOG_ASSERT(lowerX->size() == auxVector->size(), "Dimension missmatch."); // As we will shuffle pointers around, let's store the original positions here. std::vector* initLowerX = lowerX; std::vector* initUpperX = upperX; - std::vector* initAux = auxVector; uint64_t overallIterations = 0; uint64_t lastValueIterationIterations = 0; uint64_t currentVerificationIterations = 0; - uint64_t valueIterationInvocations = 0; // Get some parameters for the algorithm // 2 @@ -215,135 +304,101 @@ namespace storm { SolverStatus status = SolverStatus::InProgress; while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { - // Perform value iteration until convergence - ++valueIterationInvocations; - auto result = valueIterationCallback(lowerX, auxVector, iterationPrecision, relative, overallIterations, maxOverallIterations); - lastValueIterationIterations = result.first; - overallIterations += result.first; + lastValueIterationIterations = dir ? iterationHelper.repeatedIterate(dir.get(), *lowerX, b, precision, relative) : iterationHelper.repeatedIterate(*lowerX, b, precision, relative); + overallIterations += lastValueIterationIterations; - if (result.second != SolverStatus::Converged) { - status = result.second; - } else { - bool intervalIterationNeeded = false; - currentVerificationIterations = 0; + bool intervalIterationNeeded = false; + currentVerificationIterations = 0; - if (relative) { - oviinternal::guessUpperBoundRelative(*lowerX, *upperX, relativeBoundGuessingScaler); - } else { - oviinternal::guessUpperBoundAbsolute(*lowerX, *upperX, precision); - } + if (relative) { + oviinternal::guessUpperBoundRelative(*lowerX, *upperX, relativeBoundGuessingScaler); + } else { + oviinternal::guessUpperBoundAbsolute(*lowerX, *upperX, precision); + } - bool cancelGuess = false; - while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { - ++overallIterations; - ++currentVerificationIterations; - // Perform value iteration stepwise for lower bound and guessed upper bound + bool cancelGuess = false; + while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { + ++overallIterations; + ++currentVerificationIterations; + // Perform value iteration stepwise for lower bound and guessed upper bound - // Upper bound iteration - auto upperBoundIterResult = dir ? upperBoundIterator.iterate(dir.get(), *upperX, b, !noTerminationGuarantee) : upperBoundIterator.iterate(*upperX, b, !noTerminationGuarantee); + // Upper bound iteration + auto upperBoundIterResult = dir ? iterationHelper.iterateUpper(dir.get(), *upperX, b, !noTerminationGuarantee) : iterationHelper.iterateUpper(*upperX, b, !noTerminationGuarantee); - if (upperBoundIterResult == oviinternal::UpperBoundIterator::IterateResult::AlwaysHigherOrEqual) { - // All values moved up (and did not stay the same) - // That means the guess for an upper bound is actually a lower bound - iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues); - // We assume to have a single fixed point. We can thus safely set the new lower bound, to the wrongly guessed upper bound - // Set lowerX to the upper bound candidate - std::swap(lowerX, upperX); - break; - } else if (upperBoundIterResult == oviinternal::UpperBoundIterator::IterateResult::AlwaysLowerOrEqual) { - // All values moved down (and stayed not the same) - // This is a valid upper bound. We still need to check the precision. - // We can safely use twice the requested precision, as we calculate the center of both vectors - bool reachedPrecision; - if (relevantValues) { - reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, relevantValues.get(), doublePrecision, relative); - } else { - reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, doublePrecision, relative); - } - if (reachedPrecision) { - status = SolverStatus::Converged; - break; - } else { - // From now on, we keep updating both bounds - intervalIterationNeeded = true; - } - // The following case below covers that both vectors (old and new) are equal. - // Theoretically, this means that the precise fixpoint has been reached. However, numerical instabilities can be tricky and this detection might be incorrect (see the haddad-monmege model). - // We therefore disable it. It is very unlikely that we guessed the right fixpoint anyway. - //} else if (upperBoundIterResult == oviinternal::UpperBoundIterator::IterateResult::Equal) { - // In this case, the guessed upper bound is the precise fixpoint - // status = SolverStatus::Converged; - // std::swap(lowerX, auxVector); - // break; + if (upperBoundIterResult == oviinternal::IterationHelper::IterateResult::AlwaysHigherOrEqual) { + // All values moved up (and did not stay the same) + // That means the guess for an upper bound is actually a lower bound + auto diff = dir ? iterationHelper.singleIterationWithDiff(dir.get(), *upperX, b, relative) : iterationHelper.singleIterationWithDiff(*upperX, b, relative); + iterationPrecision = oviinternal::updateIterationPrecision(env, diff); + // We assume to have a single fixed point. We can thus safely set the new lower bound, to the wrongly guessed upper bound + // Set lowerX to the upper bound candidate + std::swap(lowerX, upperX); + break; + } else if (upperBoundIterResult == oviinternal::IterationHelper::IterateResult::AlwaysLowerOrEqual) { + // All values moved down (and stayed not the same) + // This is a valid upper bound. We still need to check the precision. + // We can safely use twice the requested precision, as we calculate the center of both vectors + bool reachedPrecision; + if (relevantValues) { + reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, relevantValues.get(), doublePrecision, relative); + } else { + reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, doublePrecision, relative); } - - // Check whether we tried this guess for too long - ValueType scaledIterationCount = storm::utility::convertNumber(currentVerificationIterations) * storm::utility::convertNumber(env.solver().ovi().getMaxVerificationIterationFactor()); - if (!intervalIterationNeeded && scaledIterationCount >= storm::utility::convertNumber(lastValueIterationIterations)) { - cancelGuess = true; - // In this case we will make one more iteration on the lower bound (mainly to obtain a new iterationPrecision) + if (reachedPrecision) { + status = SolverStatus::Converged; + break; + } else { + // From now on, we keep updating both bounds + intervalIterationNeeded = true; } + // The following case below covers that both vectors (old and new) are equal. + // Theoretically, this means that the precise fixpoint has been reached. However, numerical instabilities can be tricky and this detection might be incorrect (see the haddad-monmege model). + // We therefore disable it. It is very unlikely that we guessed the right fixpoint anyway. + //} else if (upperBoundIterResult == oviinternal::IterationHelper::IterateResult::Equal) { + // In this case, the guessed upper bound is the precise fixpoint + // status = SolverStatus::Converged; + // break; + } - // Lower bound iteration (only if needed) - if (cancelGuess || intervalIterationNeeded || currentVerificationIterations > upperBoundOnlyIterations) { - singleIterationCallback(lowerX, auxVector, overallIterations); - // At this point, auxVector contains the old values for the lower bound whereas lowerX contains the new ones. + // Check whether we tried this guess for too long + ValueType scaledIterationCount = storm::utility::convertNumber(currentVerificationIterations) * storm::utility::convertNumber(env.solver().ovi().getMaxVerificationIterationFactor()); + if (!intervalIterationNeeded && scaledIterationCount >= storm::utility::convertNumber(lastValueIterationIterations)) { + cancelGuess = true; + // In this case we will make one more iteration on the lower bound (mainly to obtain a new iterationPrecision) + } - // Check whether the upper and lower bounds have crossed, i.e., the upper bound is smaller than the lower bound. - bool valuesCrossed = false; - for (uint64_t i = 0; i < lowerX->size(); ++i) { - if ((*upperX)[i] < (*lowerX)[i]) { - valuesCrossed = true; - break; - } - } + // Lower bound iteration (only if needed) + if (cancelGuess || intervalIterationNeeded || currentVerificationIterations > upperBoundOnlyIterations) { + auto diff = dir ? iterationHelper.singleIterationWithDiff(dir.get(), *lowerX, b, relative) : iterationHelper.singleIterationWithDiff(*lowerX, b, relative); - if (cancelGuess || valuesCrossed) { - // A new guess is needed. - iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *lowerX, relative, relevantValues); + // Check whether the upper and lower bounds have crossed, i.e., the upper bound is smaller than the lower bound. + bool valuesCrossed = false; + for (uint64_t i = 0; i < lowerX->size(); ++i) { + if ((*upperX)[i] < (*lowerX)[i]) { + valuesCrossed = true; break; } } + + if (cancelGuess || valuesCrossed) { + // A new guess is needed. + iterationPrecision = oviinternal::updateIterationPrecision(env, diff); + break; + } } - if (storm::utility::resources::isTerminate()) { - status = SolverStatus::Aborted; - } + } + if (storm::utility::resources::isTerminate()) { + status = SolverStatus::Aborted; } } // end while - // Swap the results into the output vectors. - if (initLowerX == lowerX) { - // lowerX is already at the correct position. We still have to care for upperX - if (initUpperX != upperX) { - // UpperX is not at the correct position. It has to be at the auxVector - assert(initAux == upperX); - std::swap(*initUpperX, *initAux); - } - } else if (initUpperX == upperX) { - // UpperX is already at the correct position. - // We already know that lowerX is at the wrong position. It has to be at the auxVector - assert(initAux == lowerX); - std::swap(*initLowerX, *initAux); - } else if (initAux == auxVector) { - // We know that upperX and lowerX are swapped. - assert(initLowerX == upperX); + // Swap the results into the output vectors (if necessary). + assert(initLowerX != lowerX || (initLowerX == lowerX && initUpperX == upperX)); + if (initLowerX != lowerX) { assert(initUpperX == lowerX); - std::swap(*initUpperX, *initLowerX); - } else { - // Now we know that all vectors are at the wrong position. There are only two possibilities left - if (initLowerX == upperX) { - assert(initUpperX == auxVector); - assert(initAux == lowerX); - std::swap(*initLowerX, *initAux); - std::swap(*initUpperX, *initAux); - } else { - assert(initLowerX == auxVector); - assert(initUpperX == lowerX); - assert (initAux == upperX); - std::swap(*initUpperX, *initAux); - std::swap(*initLowerX, *initAux); - } + assert(initLowerX == upperX); + lowerX->swap(*upperX); } if (overallIterations > maxOverallIterations) { diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h index abf67dd3c..d559d508d 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.h +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h @@ -18,10 +18,10 @@ namespace storm { namespace oviinternal { template - class UpperBoundIterator { + class IterationHelper { public: typedef uint32_t IndexType; - UpperBoundIterator(storm::storage::SparseMatrix const& matrix); + IterationHelper(storm::storage::SparseMatrix const& matrix); enum class IterateResult { AlwaysHigherOrEqual, AlwaysLowerOrEqual, @@ -29,13 +29,26 @@ namespace storm { Incomparable }; - IterateResult iterate(std::vector& x, std::vector const& b, bool takeMinOfOldAndNew); - IterateResult iterate(storm::solver::OptimizationDirection const& dir, std::vector& x, std::vector const& b, bool takeMinOfOldAndNew); + /// performs a single iteration and returns the maximal difference between the iterations as well as the index where this difference happened + ValueType singleIterationWithDiff(std::vector& x, std::vector const& b, bool computeRelativeDiff); + ValueType singleIterationWithDiff(storm::solver::OptimizationDirection const& dir, std::vector& x, std::vector const& b, bool computeRelativeDiff); + + /// returns the number of performed iterations + uint64_t repeatedIterate(std::vector& x, std::vector const& b, ValueType precision, bool relative); + uint64_t repeatedIterate(storm::solver::OptimizationDirection const& dir, std::vector& x, std::vector const& b, ValueType precision, bool relative); + + /// Performs a single iteration for the upper bound + IterateResult iterateUpper(std::vector& x, std::vector const& b, bool takeMinOfOldAndNew); + IterateResult iterateUpper(storm::solver::OptimizationDirection const& dir, std::vector& x, std::vector const& b, bool takeMinOfOldAndNew); private: template - IterateResult iterateInternal(std::vector& x, std::vector const& b, bool takeMinOfOldAndNew); + ValueType singleIterationWithDiffInternal(std::vector& x, std::vector const& b, bool computeRelativeDiff); + template + uint64_t repeatedIterateInternal(std::vector& x, std::vector const& b, ValueType precision, bool relative); + template + IterateResult iterateUpperInternal(std::vector& x, std::vector const& b, bool takeMinOfOldAndNew); ValueType multiplyRow(IndexType const& rowIndex, ValueType const& bi, std::vector const& x); template ValueType multiplyRowGroup(IndexType const& rowGroupIndex, std::vector const& b, std::vector const& x); @@ -56,49 +69,20 @@ namespace storm { public: OptimisticValueIterationHelper(storm::storage::SparseMatrix const& matrix); - /*! - * Return type of value iteration callback. - * The first component shall be the number of performed iterations, the second component is the final convergence status. - */ - typedef std::pair ValueIterationReturnType; - - /*! - * Value iteration callback. Performs conventional value iteration for the given input. - * @pre y points to a vector that contains starting values - * @post y points to a vector that contains resulting values - * @param yPrime points to auxiliary storage - * @param precision is the target precision - * @param relative sets whether relative precision is considered - * @param maxI the maximal number of iterations to perform - */ - typedef std::function*& y, std::vector*& yPrime, ValueType const& precision, bool const& relative, uint64_t const& i, uint64_t const& maxI)> ValueIterationCallBackType; - - /*! - * Should perform a single value iteration step (using conventional value iteration). - * @pre y points to a vector that contains starting values - * @post y points to a vector that contains resulting values - * @param yPrime points to auxiliary storage - * @param currI the current iteration (can be used to display progress within the callback) - */ - typedef std::function* y, std::vector* yPrime, uint64_t const& currI)> SingleIterationCallBackType; - /*! * @param env * @param lowerX Needs to be some arbitrary lower bound on the actual values initially * @param upperX Does not need to be an upper bound initially - * @param auxVector auxiliary storage (same size as lowerX and upperX) * @param b the values added to each matrix row (the b in A*x+b) - * @param valueIterationCallback Function that should perform standard value iteration on the input vector - * @param singleIterationCallback Function that should perform a single value iteration step on the input vector e.g. ( x' = min/max(A*x + b)) * @param dir The optimization direction * @param relevantValues If given, we only check the precision at the states with the given indices. * @return The status upon termination as well as the number of iterations Also, the maximum (relative/absolute) difference between lowerX and upperX will be 2*epsilon * with the provided precision parameters. */ - std::pair solveEquationsOptimisticValueIteration(Environment const& env, std::vector* lowerX, std::vector* upperX, std::vector* auxVector, std::vector const& b, ValueIterationCallBackType const& valueIterationCallback, SingleIterationCallBackType const& singleIterationCallback, bool relative, ValueType precision, uint64_t maxOverallIterations, boost::optional dir, boost::optional relevantValues = boost::none); + std::pair solveEquations(Environment const& env, std::vector* lowerX, std::vector* upperX, std::vector const& b, bool relative, ValueType precision, uint64_t maxOverallIterations, boost::optional dir, boost::optional const& relevantValues); private: - oviinternal::UpperBoundIterator upperBoundIterator; + oviinternal::IterationHelper iterationHelper; }; } From d135bc8ecb0821cef7dfeab47f7e6907eb0de5b1 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 3 Sep 2020 14:22:15 +0200 Subject: [PATCH 15/33] cmake: Workaround for the FATAL_ERROR that occurred whenever building shipped carl was aborted (bypassing github issue #62). --- resources/3rdparty/CMakeLists.txt | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index d939ab369..170e72033 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -260,14 +260,26 @@ if (NOT STORM_FORCE_SHIPPED_CARL) find_package(carl QUIET) endif() endif() + +set(STORM_SHIPPED_CARL OFF) if(carl_FOUND AND NOT STORM_FORCE_SHIPPED_CARL) get_target_property(carlLOCATION lib_carl LOCATION) if("${carlLOCATION}" STREQUAL "carlLOCATION-NOTFOUND") - message(FATAL_ERROR "Library location for carl is not found, did you build carl?") + if(EXISTS ${STORM_3RDPARTY_BINARY_DIR}/carl) + message(WARNING "Storm - Library for carl location is not found but the directory ${STORM_3RDPARTY_BINARY_DIR}/carl exists. Will (re-)try to build a shipped version of carl.") + set(STORM_SHIPPED_CARL ON) + else() + message(FATAL_ERROR "Library location for carl is not found, did you build carl?") + endif() elseif(EXISTS ${carlLOCATION}) #empty on purpose else() - message(FATAL_ERROR "File ${carlLOCATION} does not exist, did you build carl?") + if(EXISTS ${STORM_3RDPARTY_BINARY_DIR}/carl) + message(WARNING "Storm - File ${carlLOCATION} does not exist but the directory ${STORM_3RDPARTY_BINARY_DIR}/carl exists. Will (re-)try to build a shipped version of carl.") + set(STORM_SHIPPED_CARL ON) + else() + message(FATAL_ERROR "File ${carlLOCATION} does not exist, did you build carl?") + endif() endif() if("${carl_VERSION_MAJOR}" STREQUAL "${CARL_C14VERSION}") message(STATUS "Storm - Found carl using master14 branch.") @@ -276,14 +288,16 @@ if(carl_FOUND AND NOT STORM_FORCE_SHIPPED_CARL) message(FATAL_ERROR "Carl outdated, require ${CARL_MINVERSION}, have ${carl_VERSION}") endif() - set(STORM_SHIPPED_CARL OFF) set(STORM_HAVE_CARL ON) message(STATUS "Storm - Use system version of carl.") message(STATUS "Storm - Linking with preinstalled carl ${carl_VERSION} (include: ${carl_INCLUDE_DIR}, library ${carl_LIBRARIES}, CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}, CARL_USE_GINAC: ${CARL_USE_GINAC}).") set(STORM_HAVE_CLN ${CARL_USE_CLN_NUMBERS}) set(STORM_HAVE_GINAC ${CARL_USE_GINAC}) else() - set(STORM_SHIPPED_CARL ON) + set(STORM_SHIPPED_CARL ON) +endif() + +if (STORM_SHIPPED_CARL) # The first external project will be built at *configure stage* message(STATUS "Carl - Start of config process") file(MAKE_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download) From 45803c547e096f3ecf9f37a7ed09d78093b08b4e Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 3 Sep 2020 16:59:04 +0200 Subject: [PATCH 16/33] storm-pars: Fixed an issue in the instantiation model checkers where maybestates were cached incorrectly. --- .../SparseDtmcInstantiationModelChecker.cpp | 68 +++++++++++----- .../SparseMdpInstantiationModelChecker.cpp | 80 +++++++++++-------- src/storm/modelchecker/CheckTask.h | 8 ++ 3 files changed, 100 insertions(+), 56 deletions(-) diff --git a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp index 5de3d8fd3..9ea15c4f9 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp +++ b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp @@ -42,8 +42,31 @@ namespace storm { this->currentCheckTask->setHint(std::make_shared>()); } ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); - std::unique_ptr result; + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // Perform purely qualitative analysis once + std::vector qualitativeResult; + if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { + auto newCheckTask = *this->currentCheckTask; + newCheckTask.setQualitative(true); + newCheckTask.setOnlyInitialStatesRelevant(false); + qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); + } else { + auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()); + newCheckTask.setQualitative(true); + newCheckTask.setOnlyInitialStatesRelevant(false); + qualitativeResult = modelChecker.computeProbabilities(env, newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); + } + std::cout << storm::utility::vector::toString(qualitativeResult) << std::endl; + storm::storage::BitVector maybeStates = storm::utility::vector::filter(qualitativeResult, + [] (ConstantType const& value) -> bool { return !(storm::utility::isZero(value) || storm::utility::isOne(value)); }); + std::cout < result; // Check the formula and store the result as a hint for the next call. // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { @@ -56,15 +79,6 @@ namespace storm { hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); } - if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { - // Extract the maybe states from the current result. - assert(hint.hasResultHint()); - storm::storage::BitVector maybeStates = ~storm::utility::vector::filter(hint.getResultHint(), - [] (ConstantType const& value) -> bool { return storm::utility::isZero(value) || storm::utility::isOne(value); }); - hint.setMaybeStates(std::move(maybeStates)); - hint.setComputeOnlyMaybeStates(true); - } - return result; } @@ -75,6 +89,28 @@ namespace storm { this->currentCheckTask->setHint(std::make_shared>()); } ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); + + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // Perform purely qualitative analysis once + std::vector qualitativeResult; + if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { + auto newCheckTask = *this->currentCheckTask; + newCheckTask.setQualitative(true); + newCheckTask.setOnlyInitialStatesRelevant(false); + qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); + } else { + auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()); + newCheckTask.setQualitative(true); + newCheckTask.setOnlyInitialStatesRelevant(false); + qualitativeResult = modelChecker.computeRewards(env, this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); + } + storm::storage::BitVector maybeStates = storm::utility::vector::filter(qualitativeResult, + [] (ConstantType const& value) -> bool { return !(storm::utility::isZero(value) || storm::utility::isInfinity(value)); }); + hint.setMaybeStates(std::move(maybeStates)); + hint.setResultHint(std::move(qualitativeResult)); + hint.setComputeOnlyMaybeStates(true); + } + std::unique_ptr result; // Check the formula and store the result as a hint for the next call. @@ -89,18 +125,6 @@ namespace storm { this->currentCheckTask->getHint().template asExplicitModelCheckerHint().setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); } - if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { - // Extract the maybe states from the current result. - assert(hint.hasResultHint()); - storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint()); - // We need to exclude the target states from the maybe states. - // Note that we can not consider the states with reward zero since a valuation might set a reward to zero - std::unique_ptr subFormulaResult = modelChecker.check(env, this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()); - maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); - hint.setMaybeStates(std::move(maybeStates)); - hint.setComputeOnlyMaybeStates(true); - } - return result; } diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp index 3dc4866d3..0f1e8b9ac 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp +++ b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp @@ -47,8 +47,31 @@ namespace storm { this->currentCheckTask->setHint(std::make_shared>()); } ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); - std::unique_ptr result; + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // Perform purely qualitative analysis once + std::vector qualitativeResult; + if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { + auto newCheckTask = *this->currentCheckTask; + newCheckTask.setQualitative(true); + newCheckTask.setOnlyInitialStatesRelevant(false); + qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); + } else { + auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()); + newCheckTask.setQualitative(true); + newCheckTask.setOnlyInitialStatesRelevant(false); + qualitativeResult = modelChecker.computeProbabilities(env, newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); + } + std::cout << storm::utility::vector::toString(qualitativeResult) << std::endl; + storm::storage::BitVector maybeStates = storm::utility::vector::filter(qualitativeResult, + [] (ConstantType const& value) -> bool { return !(storm::utility::isZero(value) || storm::utility::isOne(value)); }); + std::cout < result; // Check the formula and store the result as a hint for the next call. // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { @@ -65,21 +88,6 @@ namespace storm { hint.setSchedulerHint(std::move(dynamic_cast&>(scheduler))); } - if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { - // Extract the maybe states from the current result. - assert(hint.hasResultHint()); - storm::storage::BitVector maybeStates = ~storm::utility::vector::filter(hint.getResultHint(), - [] (ConstantType const& value) -> bool { return storm::utility::isZero(value) || storm::utility::isOne(value); }); - hint.setMaybeStates(std::move(maybeStates)); - hint.setComputeOnlyMaybeStates(true); - - // Check if there can be end components within the maybestates - if (storm::solver::minimize(this->currentCheckTask->getOptimizationDirection()) || - storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) { - hint.setNoEndComponentsInMaybeStates(true); - } - } - return result; } @@ -92,8 +100,29 @@ namespace storm { this->currentCheckTask->setHint(std::make_shared>()); } ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); - std::unique_ptr result; + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // Perform purely qualitative analysis once + std::vector qualitativeResult; + if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { + auto newCheckTask = *this->currentCheckTask; + newCheckTask.setQualitative(true); + newCheckTask.setOnlyInitialStatesRelevant(false); + qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); + } else { + auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()); + newCheckTask.setQualitative(true); + newCheckTask.setOnlyInitialStatesRelevant(false); + qualitativeResult = modelChecker.computeRewards(env, this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); + } + storm::storage::BitVector maybeStates = storm::utility::vector::filter(qualitativeResult, + [] (ConstantType const& value) -> bool { return !(storm::utility::isZero(value) || storm::utility::isInfinity(value)); }); + hint.setMaybeStates(std::move(maybeStates)); + hint.setResultHint(std::move(qualitativeResult)); + hint.setComputeOnlyMaybeStates(true); + } + + std::unique_ptr result; // Check the formula and store the result as a hint for the next call. // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { @@ -110,23 +139,6 @@ namespace storm { hint.setSchedulerHint(std::move(dynamic_cast&>(scheduler))); } - if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { - // Extract the maybe states from the current result. - assert(hint.hasResultHint()); - storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint()); - // We need to exclude the target states from the maybe states. - // Note that we can not consider the states with reward zero since a valuation might set a reward to zero - std::unique_ptr subFormulaResult = modelChecker.check(env, this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()); - maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); - hint.setMaybeStates(std::move(maybeStates)); - hint.setComputeOnlyMaybeStates(true); - - // Check if there can be end components within the maybestates - if (storm::solver::maximize(this->currentCheckTask->getOptimizationDirection()) || - storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) { - hint.setNoEndComponentsInMaybeStates(true); - } - } return result; } diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h index 45f2a9bc3..898795fda 100644 --- a/src/storm/modelchecker/CheckTask.h +++ b/src/storm/modelchecker/CheckTask.h @@ -207,6 +207,14 @@ namespace storm { bool isQualitativeSet() const { return qualitative; } + + /*! + * sets whether the computation only needs to be performed qualitatively, because the values will only + * be compared to 0/1. + */ + void setQualitative(bool value) { + qualitative = value; + } /*! * Sets whether to produce schedulers (if supported). From 84c0d777723e8e01f76291c4894f3c828f776d3b Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 3 Sep 2020 17:03:24 +0200 Subject: [PATCH 17/33] storm-pars fixed the fix... --- .../instantiation/SparseMdpInstantiationModelChecker.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp index 0f1e8b9ac..38860ef77 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp +++ b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp @@ -55,11 +55,13 @@ namespace storm { auto newCheckTask = *this->currentCheckTask; newCheckTask.setQualitative(true); newCheckTask.setOnlyInitialStatesRelevant(false); + newCheckTask.setProduceSchedulers(false); qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); } else { auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()); newCheckTask.setQualitative(true); newCheckTask.setOnlyInitialStatesRelevant(false); + newCheckTask.setProduceSchedulers(false); qualitativeResult = modelChecker.computeProbabilities(env, newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); } std::cout << storm::utility::vector::toString(qualitativeResult) << std::endl; @@ -108,11 +110,13 @@ namespace storm { auto newCheckTask = *this->currentCheckTask; newCheckTask.setQualitative(true); newCheckTask.setOnlyInitialStatesRelevant(false); + newCheckTask.setProduceSchedulers(false); qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); } else { auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()); newCheckTask.setQualitative(true); newCheckTask.setOnlyInitialStatesRelevant(false); + newCheckTask.setProduceSchedulers(false); qualitativeResult = modelChecker.computeRewards(env, this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); } storm::storage::BitVector maybeStates = storm::utility::vector::filter(qualitativeResult, From 18d9ba0f3881ca504aa400ca40c8b74bb34ac448 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 3 Sep 2020 20:49:47 +0200 Subject: [PATCH 18/33] ovi: fixed using incorrect precision --- src/storm/solver/helper/OptimisticValueIterationHelper.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.cpp b/src/storm/solver/helper/OptimisticValueIterationHelper.cpp index 28644d5de..a9f8c663f 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.cpp +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.cpp @@ -305,7 +305,7 @@ namespace storm { while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { // Perform value iteration until convergence - lastValueIterationIterations = dir ? iterationHelper.repeatedIterate(dir.get(), *lowerX, b, precision, relative) : iterationHelper.repeatedIterate(*lowerX, b, precision, relative); + lastValueIterationIterations = dir ? iterationHelper.repeatedIterate(dir.get(), *lowerX, b, iterationPrecision, relative) : iterationHelper.repeatedIterate(*lowerX, b, iterationPrecision, relative); overallIterations += lastValueIterationIterations; bool intervalIterationNeeded = false; From 169f9201b23b8a35958e1457cd2016dc0d8399e1 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 4 Sep 2020 10:45:16 +0200 Subject: [PATCH 19/33] ovi: Fixed heuristic for canceling a guess. --- src/storm/settings/modules/OviSolverSettings.cpp | 2 +- src/storm/solver/helper/OptimisticValueIterationHelper.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/settings/modules/OviSolverSettings.cpp b/src/storm/settings/modules/OviSolverSettings.cpp index 931aa1af8..bc474b798 100644 --- a/src/storm/settings/modules/OviSolverSettings.cpp +++ b/src/storm/settings/modules/OviSolverSettings.cpp @@ -25,7 +25,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, useRelevantValuesForPrecisionUpdateOptionName, false, "Sets whether the precision of the inner value iteration is only based on the relevant values (i.e. initial states).").setIsAdvanced().build()); - this->addOption(storm::settings::OptionBuilder(moduleName, maxVerificationIterationFactorOptionName, false, "Controls how many verification iterations are performed before guessing a new upper bound.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("factor", "The factor.").setDefaultValueDouble(0.1).addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, maxVerificationIterationFactorOptionName, false, "Controls how many verification iterations are performed before guessing a new upper bound.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("factor", "The factor.").setDefaultValueDouble(1.0).addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, upperBoundGuessingFactorOptionName, false, "Sets with which factor the precision is multiplied to guess the upper bound.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("factor", "The factor.").setDefaultValueDouble(1.0).addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build()); diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.cpp b/src/storm/solver/helper/OptimisticValueIterationHelper.cpp index a9f8c663f..076782e40 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.cpp +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.cpp @@ -363,7 +363,7 @@ namespace storm { // Check whether we tried this guess for too long ValueType scaledIterationCount = storm::utility::convertNumber(currentVerificationIterations) * storm::utility::convertNumber(env.solver().ovi().getMaxVerificationIterationFactor()); - if (!intervalIterationNeeded && scaledIterationCount >= storm::utility::convertNumber(lastValueIterationIterations)) { + if (!intervalIterationNeeded && scaledIterationCount * iterationPrecision >= storm::utility::one()) { cancelGuess = true; // In this case we will make one more iteration on the lower bound (mainly to obtain a new iterationPrecision) } From c5f698f9f7f579a3d181d9c3607340ce83dd740e Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 4 Sep 2020 10:46:13 +0200 Subject: [PATCH 20/33] ovi: removed unused option for only taking relevant values when updating the precision --- src/storm/environment/solver/OviSolverEnvironment.cpp | 5 ----- src/storm/environment/solver/OviSolverEnvironment.h | 2 -- src/storm/settings/modules/OviSolverSettings.cpp | 6 ------ src/storm/settings/modules/OviSolverSettings.h | 3 --- 4 files changed, 16 deletions(-) diff --git a/src/storm/environment/solver/OviSolverEnvironment.cpp b/src/storm/environment/solver/OviSolverEnvironment.cpp index fe6a21a12..382b27a54 100644 --- a/src/storm/environment/solver/OviSolverEnvironment.cpp +++ b/src/storm/environment/solver/OviSolverEnvironment.cpp @@ -11,7 +11,6 @@ namespace storm { auto const& oviSettings = storm::settings::getModule(); precisionUpdateFactor = storm::utility::convertNumber(oviSettings.getPrecisionUpdateFactor()); maxVerificationIterationFactor = storm::utility::convertNumber(oviSettings.getMaxVerificationIterationFactor()); - relevantValuesForPrecisionUpdate = oviSettings.useRelevantValuesForPrecisionUpdate(); upperBoundGuessingFactor = storm::utility::convertNumber(oviSettings.getUpperBoundGuessingFactor()); upperBoundOnlyIterations = oviSettings.getUpperBoundOnlyIterations(); noTerminationGuaranteeMinimumMethod = oviSettings.useNoTerminationGuaranteeMinimumMethod(); @@ -29,10 +28,6 @@ namespace storm { return maxVerificationIterationFactor; } - bool OviSolverEnvironment::useRelevantValuesForPrecisionUpdate() const { - return relevantValuesForPrecisionUpdate; - } - storm::RationalNumber OviSolverEnvironment::getUpperBoundGuessingFactor() const { return upperBoundGuessingFactor; } diff --git a/src/storm/environment/solver/OviSolverEnvironment.h b/src/storm/environment/solver/OviSolverEnvironment.h index 0875bad9a..207717982 100644 --- a/src/storm/environment/solver/OviSolverEnvironment.h +++ b/src/storm/environment/solver/OviSolverEnvironment.h @@ -14,7 +14,6 @@ namespace storm { storm::RationalNumber getPrecisionUpdateFactor() const; storm::RationalNumber getMaxVerificationIterationFactor() const; - bool useRelevantValuesForPrecisionUpdate() const; storm::RationalNumber getUpperBoundGuessingFactor() const; uint64_t getUpperBoundOnlyIterations() const; bool useNoTerminationGuaranteeMinimumMethod() const; @@ -22,7 +21,6 @@ namespace storm { private: storm::RationalNumber precisionUpdateFactor; storm::RationalNumber maxVerificationIterationFactor; - bool relevantValuesForPrecisionUpdate; storm::RationalNumber upperBoundGuessingFactor; uint64_t upperBoundOnlyIterations; bool noTerminationGuaranteeMinimumMethod; diff --git a/src/storm/settings/modules/OviSolverSettings.cpp b/src/storm/settings/modules/OviSolverSettings.cpp index bc474b798..d6331cd3f 100644 --- a/src/storm/settings/modules/OviSolverSettings.cpp +++ b/src/storm/settings/modules/OviSolverSettings.cpp @@ -23,8 +23,6 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, precisionUpdateFactorOptionName, false, "Sets with which factor the precision of the inner value iteration is updated.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("factor", "The factor.").setDefaultValueDouble(0.4).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, useRelevantValuesForPrecisionUpdateOptionName, false, "Sets whether the precision of the inner value iteration is only based on the relevant values (i.e. initial states).").setIsAdvanced().build()); - this->addOption(storm::settings::OptionBuilder(moduleName, maxVerificationIterationFactorOptionName, false, "Controls how many verification iterations are performed before guessing a new upper bound.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("factor", "The factor.").setDefaultValueDouble(1.0).addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, upperBoundGuessingFactorOptionName, false, "Sets with which factor the precision is multiplied to guess the upper bound.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("factor", "The factor.").setDefaultValueDouble(1.0).addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build()); @@ -42,10 +40,6 @@ namespace storm { return this->getOption(maxVerificationIterationFactorOptionName).getArgumentByName("factor").getValueAsDouble(); } - bool OviSolverSettings::useRelevantValuesForPrecisionUpdate() const { - return this->getOption(useRelevantValuesForPrecisionUpdateOptionName).getHasOptionBeenSet(); - } - double OviSolverSettings::getUpperBoundGuessingFactor() const { return this->getOption(upperBoundGuessingFactorOptionName).getArgumentByName("factor").getValueAsDouble(); } diff --git a/src/storm/settings/modules/OviSolverSettings.h b/src/storm/settings/modules/OviSolverSettings.h index 70c1c4f0f..1b033121a 100644 --- a/src/storm/settings/modules/OviSolverSettings.h +++ b/src/storm/settings/modules/OviSolverSettings.h @@ -19,8 +19,6 @@ namespace storm { double getMaxVerificationIterationFactor() const; - bool useRelevantValuesForPrecisionUpdate() const; - double getUpperBoundGuessingFactor() const; uint64_t getUpperBoundOnlyIterations() const; @@ -33,7 +31,6 @@ namespace storm { private: static const std::string precisionUpdateFactorOptionName; static const std::string maxVerificationIterationFactorOptionName; - static const std::string useRelevantValuesForPrecisionUpdateOptionName; static const std::string upperBoundGuessingFactorOptionName; static const std::string upperBoundOnlyIterationsOptionName; static const std::string useNoTerminationGuaranteeMinimumMethodOptionName; From cb39cc5c15cedc2c94dc933c2cfd056ae86f96e5 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 4 Sep 2020 10:47:48 +0200 Subject: [PATCH 21/33] Optimistic value iteration helper: Removed unused code. --- .../helper/OptimisticValueIterationHelper.cpp | 42 ------------------- 1 file changed, 42 deletions(-) diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.cpp b/src/storm/solver/helper/OptimisticValueIterationHelper.cpp index 076782e40..df89bcaa5 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.cpp +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.cpp @@ -14,48 +14,6 @@ namespace storm { namespace helper { namespace oviinternal { - template - ValueType computeMaxAbsDiff(std::vector const& allOldValues, std::vector const& allNewValues, storm::storage::BitVector const& relevantValues) { - ValueType result = storm::utility::zero(); - for (auto value : relevantValues) { - result = storm::utility::max(result, storm::utility::abs(allNewValues[value] - allOldValues[value])); - } - return result; - } - - template - ValueType computeMaxAbsDiff(std::vector const& allOldValues, std::vector const& allNewValues) { - ValueType result = storm::utility::zero(); - for (uint64_t i = 0; i < allOldValues.size(); ++i) { - result = storm::utility::max(result, storm::utility::abs(allNewValues[i] - allOldValues[i])); - } - return result; - } - - template - ValueType computeMaxRelDiff(std::vector const& allOldValues, std::vector const& allNewValues, storm::storage::BitVector const& relevantValues) { - ValueType result = storm::utility::zero(); - for (auto i : relevantValues) { - STORM_LOG_ASSERT(!storm::utility::isZero(allNewValues[i]) || storm::utility::isZero(allOldValues[i]), "Unexpected entry in iteration vector."); - if (!storm::utility::isZero(allNewValues[i])) { - result = storm::utility::max(result, storm::utility::abs(allNewValues[i] - allOldValues[i]) / allNewValues[i]); - } - } - return result; - } - - template - ValueType computeMaxRelDiff(std::vector const& allOldValues, std::vector const& allNewValues) { - ValueType result = storm::utility::zero(); - for (uint64_t i = 0; i < allOldValues.size(); ++i) { - STORM_LOG_WARN_COND(!storm::utility::isZero(allNewValues[i]) || storm::utility::isZero(allOldValues[i]), "Unexpected entry in iteration vector."); - if (!storm::utility::isZero(allNewValues[i])) { - result = storm::utility::max(result, storm::utility::abs(allNewValues[i] - allOldValues[i]) / allNewValues[i]); - } - } - return result; - } - template ValueType updateIterationPrecision(storm::Environment const& env, ValueType const& diff) { auto factor = storm::utility::convertNumber(env.solver().ovi().getPrecisionUpdateFactor()); From 50c3a28305676ea68eb0380e2545622c319f34ea Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 4 Sep 2020 10:57:43 +0200 Subject: [PATCH 22/33] Fixed spacing in ovi code. --- src/storm/solver/helper/OptimisticValueIterationHelper.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.cpp b/src/storm/solver/helper/OptimisticValueIterationHelper.cpp index df89bcaa5..296dd2ceb 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.cpp +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.cpp @@ -50,7 +50,6 @@ namespace storm { } } - template ValueType IterationHelper::singleIterationWithDiff(std::vector& x, std::vector const& b, bool computeRelativeDiff) { return singleIterationWithDiffInternal(x, b, computeRelativeDiff); @@ -232,7 +231,7 @@ namespace storm { template OptimisticValueIterationHelper::OptimisticValueIterationHelper(storm::storage::SparseMatrix const& matrix) : iterationHelper(matrix) { // Intentionally left empty. - } + } template std::pair OptimisticValueIterationHelper::solveEquations(Environment const& env, std::vector* lowerX, std::vector* upperX, std::vector const& b, bool relative, ValueType precision, uint64_t maxOverallIterations, boost::optional dir, boost::optional const& relevantValues) { From 871a28d6f6ea0fc6a4b65437bcfb31b998f64059 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 4 Sep 2020 10:59:37 +0200 Subject: [PATCH 23/33] Fixed compiling OviSettings --- src/storm/settings/modules/OviSolverSettings.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/storm/settings/modules/OviSolverSettings.cpp b/src/storm/settings/modules/OviSolverSettings.cpp index d6331cd3f..4d8311737 100644 --- a/src/storm/settings/modules/OviSolverSettings.cpp +++ b/src/storm/settings/modules/OviSolverSettings.cpp @@ -14,7 +14,6 @@ namespace storm { const std::string OviSolverSettings::moduleName = "ovi"; const std::string OviSolverSettings::precisionUpdateFactorOptionName = "precision-update-factor"; const std::string OviSolverSettings::maxVerificationIterationFactorOptionName = "max-verification-iter-factor"; - const std::string OviSolverSettings::useRelevantValuesForPrecisionUpdateOptionName = "use-relevant-values"; const std::string OviSolverSettings::upperBoundGuessingFactorOptionName = "upper-bound-factor"; const std::string OviSolverSettings::upperBoundOnlyIterationsOptionName = "check-upper-only-iter"; const std::string OviSolverSettings::useNoTerminationGuaranteeMinimumMethodOptionName = "no-termination-guarantee"; From a04085e8482fdeb3bebeab8e24cd2ad1fddc110e Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 4 Sep 2020 11:50:10 +0200 Subject: [PATCH 24/33] Added cmake option exclude_tests_from_all so that we can run make install without building the tests. --- CMakeLists.txt | 3 +++ src/CMakeLists.txt | 7 +++++-- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 3d882f18c..edf9fa3e3 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -61,6 +61,9 @@ export_option(STORM_USE_CLN_RF) option(BUILD_SHARED_LIBS "Build the Storm library dynamically" OFF) option(STORM_DEBUG_CUDD "Build CUDD in debug mode." OFF) MARK_AS_ADVANCED(STORM_DEBUG_CUDD) +option(STORM_EXCLUDE_TESTS_FROM_ALL "If set, tests will not be compiled by default" OFF ) +export_option(STORM_EXCLUDE_TESTS_FROM_ALL) +MARK_AS_ADVANCED(STORM_EXCLUDE_TESTS_FROM_ALL) set(BOOST_ROOT "" CACHE STRING "A hint to the root directory of Boost (optional).") set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optional).") set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).") diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 24a213e76..2f0e8ac34 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -23,7 +23,10 @@ add_subdirectory(storm-pomdp-cli) add_subdirectory(storm-conv) add_subdirectory(storm-conv-cli) - -add_subdirectory(test) +if (STORM_EXCLUDE_TESTS_FROM_ALL) + add_subdirectory(test EXCLUDE_FROM_ALL) +else() + add_subdirectory(test) +endif() set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) From 7f03d1e6710e47c7daa52960338db3b34686a183 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Fri, 4 Sep 2020 14:44:52 +0200 Subject: [PATCH 25/33] Remove debug info --- .../instantiation/SparseDtmcInstantiationModelChecker.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp index 9ea15c4f9..85c5ce466 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp +++ b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp @@ -60,7 +60,6 @@ namespace storm { std::cout << storm::utility::vector::toString(qualitativeResult) << std::endl; storm::storage::BitVector maybeStates = storm::utility::vector::filter(qualitativeResult, [] (ConstantType const& value) -> bool { return !(storm::utility::isZero(value) || storm::utility::isOne(value)); }); - std::cout < Date: Fri, 4 Sep 2020 14:53:53 +0200 Subject: [PATCH 26/33] Storm Version 1.6.1 --- CHANGELOG.md | 2 +- version.cmake | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index d9b1274da..f9a228274 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,7 +8,7 @@ The releases of major and minor versions contain an overview of changes since th Version 1.6.x ------------- -## Version 1.6.1 (??) +## Version 1.6.1 (2020/09) - Prism program simplification improved. - Revamped implementation of long-run-average algorithms, including scheduler export for LRA properties on Markov automata. - Support for step-bounded properties of the form ... [F[x,y] ... ] for DTMCs and MDPs (sparse engine). diff --git a/version.cmake b/version.cmake index 801d8403c..ef412f960 100644 --- a/version.cmake +++ b/version.cmake @@ -1,4 +1,4 @@ set(STORM_VERSION_MAJOR 1) set(STORM_VERSION_MINOR 6) -set(STORM_VERSION_PATCH 0) +set(STORM_VERSION_PATCH 1) From 50d7ee6e8daeeabde352724e4f76e73d3f1bbacf Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Fri, 4 Sep 2020 15:46:34 +0200 Subject: [PATCH 27/33] Remove debug info --- .../instantiation/SparseDtmcInstantiationModelChecker.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp index 85c5ce466..6c743422a 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp +++ b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp @@ -57,7 +57,6 @@ namespace storm { newCheckTask.setOnlyInitialStatesRelevant(false); qualitativeResult = modelChecker.computeProbabilities(env, newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); } - std::cout << storm::utility::vector::toString(qualitativeResult) << std::endl; storm::storage::BitVector maybeStates = storm::utility::vector::filter(qualitativeResult, [] (ConstantType const& value) -> bool { return !(storm::utility::isZero(value) || storm::utility::isOne(value)); }); hint.setMaybeStates(std::move(maybeStates)); From 2c4e4b29e6b4ebbb38850e81e4564b6be4f453e2 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 4 Sep 2020 16:14:53 +0200 Subject: [PATCH 28/33] Updated documentation for new release. --- doc/checklist_new_release.md | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/doc/checklist_new_release.md b/doc/checklist_new_release.md index dcb1351a1..2735ca46d 100644 --- a/doc/checklist_new_release.md +++ b/doc/checklist_new_release.md @@ -34,11 +34,18 @@ Note that in most cases a simultaneous release of [carl](https://github.com/smtr 6. [Add new release](https://github.com/moves-rwth/storm/releases/new) in GitHub. 7. Update `stable` branch: + ```console git checkout stable - git merge master + git rebase master git push origin stable ``` + Note: Rebasing might fail if `stable` is ahead of `master` (e.g. because of merge commits). In this case we can do: + ```console + git checkout stable + git reset --hard master + git push --force origin stable + ``` 8. Update [Homebrew formula](https://github.com/moves-rwth/homebrew-storm). From 42ceed59c6f58f793913cfc7b802418767576326 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 4 Sep 2020 16:16:16 +0200 Subject: [PATCH 29/33] Removed debug output. --- .../instantiation/SparseMdpInstantiationModelChecker.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp index 38860ef77..6bbbaa158 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp +++ b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp @@ -64,10 +64,8 @@ namespace storm { newCheckTask.setProduceSchedulers(false); qualitativeResult = modelChecker.computeProbabilities(env, newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); } - std::cout << storm::utility::vector::toString(qualitativeResult) << std::endl; storm::storage::BitVector maybeStates = storm::utility::vector::filter(qualitativeResult, [] (ConstantType const& value) -> bool { return !(storm::utility::isZero(value) || storm::utility::isOne(value)); }); - std::cout < Date: Fri, 4 Sep 2020 16:23:20 +0200 Subject: [PATCH 30/33] Storm version 1.6.2 --- CHANGELOG.md | 2 +- version.cmake | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f9a228274..43b7c547a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,7 +8,7 @@ The releases of major and minor versions contain an overview of changes since th Version 1.6.x ------------- -## Version 1.6.1 (2020/09) +## Version 1.6.2 (2020/09) - Prism program simplification improved. - Revamped implementation of long-run-average algorithms, including scheduler export for LRA properties on Markov automata. - Support for step-bounded properties of the form ... [F[x,y] ... ] for DTMCs and MDPs (sparse engine). diff --git a/version.cmake b/version.cmake index ef412f960..4fcf2a030 100644 --- a/version.cmake +++ b/version.cmake @@ -1,4 +1,4 @@ set(STORM_VERSION_MAJOR 1) set(STORM_VERSION_MINOR 6) -set(STORM_VERSION_PATCH 1) +set(STORM_VERSION_PATCH 2) From 41089dee26ced3f6bbae44d15661a20b1974969e Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 7 Sep 2020 13:44:09 +0200 Subject: [PATCH 31/33] Throw exception in ParameterRegion if number of variables is too high --- src/storm-pars/storage/ParameterRegion.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/storm-pars/storage/ParameterRegion.cpp b/src/storm-pars/storage/ParameterRegion.cpp index 68d6e94dc..71030ff4d 100644 --- a/src/storm-pars/storage/ParameterRegion.cpp +++ b/src/storm-pars/storage/ParameterRegion.cpp @@ -1,7 +1,10 @@ #include "storm-pars/storage/ParameterRegion.h" +#include + #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/OutOfRangeException.h" #include "storm/utility/constants.h" namespace storm { @@ -88,6 +91,7 @@ namespace storm { template std::vector::Valuation> ParameterRegion::getVerticesOfRegion(std::set const& consideredVariables) const { std::size_t const numOfVariables = consideredVariables.size(); + STORM_LOG_THROW(numOfVariables <= std::numeric_limits::digits, storm::exceptions::OutOfRangeException, "Number of variables " << numOfVariables << " is too high."); std::size_t const numOfVertices = std::pow(2, numOfVariables); std::vector resultingVector(numOfVertices); From 6dcfd281867d5c360352ab2be98c420d4cdb9c0d Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 8 Sep 2020 17:14:32 +0200 Subject: [PATCH 32/33] Fixed dot output of BDDs in sylvan. --- resources/3rdparty/sylvan/src/sylvan_mtbdd.c | 57 ++++++++++++-------- 1 file changed, 34 insertions(+), 23 deletions(-) diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c index 964b538be..2397c9932 100755 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c @@ -3044,30 +3044,39 @@ mtbdd_leaf_to_str(MTBDD leaf, char *buf, size_t buflen) */ static void -mtbdd_fprintdot_rec(FILE *out, MTBDD mtbdd) +mtbdd_fprintdot_rec(FILE *out, MTBDD mtbdd, int *mtbdd_true_marked, int *mtbdd_false_marked) { - mtbddnode_t n = MTBDD_GETNODE(mtbdd); // also works for mtbdd_false - if (mtbddnode_getmark(n)) return; - mtbddnode_setmark(n, 1); - - if (mtbdd == mtbdd_true || mtbdd == mtbdd_false) { - fprintf(out, "0 [shape=box, style=filled, label=\"F\"];\n"); - } else if (mtbddnode_isleaf(n)) { - fprintf(out, "%" PRIu64 " [shape=box, style=filled, label=\"", MTBDD_STRIPMARK(mtbdd)); - mtbdd_fprint_leaf(out, mtbdd); - fprintf(out, "\"];\n"); + if (mtbdd == mtbdd_true) { + if (*mtbdd_true_marked) return; + *mtbdd_true_marked = 1; + fprintf(out, "%" PRIu64 " [shape=box, style=filled, label=\"T\"];\n", mtbdd); + } else if (mtbdd == mtbdd_false) { + if (*mtbdd_false_marked) return; + *mtbdd_false_marked = 1; + fprintf(out, "%" PRIu64 " [shape=box, style=filled, label=\"F\"];\n", mtbdd); } else { - fprintf(out, "%" PRIu64 " [label=\"%" PRIu32 "\"];\n", - MTBDD_STRIPMARK(mtbdd), mtbddnode_getvariable(n)); - - mtbdd_fprintdot_rec(out, mtbddnode_getlow(n)); - mtbdd_fprintdot_rec(out, mtbddnode_gethigh(n)); - - fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=dashed];\n", - MTBDD_STRIPMARK(mtbdd), mtbddnode_getlow(n)); - fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=solid dir=both arrowtail=%s];\n", - MTBDD_STRIPMARK(mtbdd), MTBDD_STRIPMARK(mtbddnode_gethigh(n)), - mtbddnode_getcomp(n) ? "dot" : "none"); + mtbddnode_t n = MTBDD_GETNODE(mtbdd); // also works for mtbdd_false + if (mtbddnode_getmark(n)) return; + mtbddnode_setmark(n, 1); + if (mtbddnode_isleaf(n)) { + fprintf(out, "%" PRIu64 " [shape=box, style=filled, label=\"", MTBDD_STRIPMARK(mtbdd)); + mtbdd_fprint_leaf(out, mtbdd); + fprintf(out, "\"];\n"); + } else { + fprintf(out, "%" PRIu64 " [label=\"%" PRIu32 "\"];\n", + MTBDD_STRIPMARK(mtbdd), mtbddnode_getvariable(n)); + + mtbdd_fprintdot_rec(out, mtbddnode_getlow(n), mtbdd_true_marked, mtbdd_false_marked); + mtbdd_fprintdot_rec(out, mtbddnode_gethigh(n), mtbdd_true_marked, mtbdd_false_marked); + + fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=dashed];\n", + MTBDD_STRIPMARK(mtbdd), + (mtbddnode_getlow(n) == mtbdd_true || mtbddnode_getlow(n) == mtbdd_false) ? mtbddnode_getlow(n) : MTBDD_STRIPMARK(mtbddnode_getlow(n))); + fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=solid dir=both arrowtail=%s];\n", + MTBDD_STRIPMARK(mtbdd), + (mtbddnode_gethigh(n) == mtbdd_true || mtbddnode_gethigh(n) == mtbdd_false) ? mtbddnode_gethigh(n) : MTBDD_STRIPMARK(mtbddnode_gethigh(n)), + mtbddnode_getcomp(n) ? "dot" : "none"); + } } } @@ -3082,7 +3091,9 @@ mtbdd_fprintdot(FILE *out, MTBDD mtbdd) fprintf(out, "root -> %" PRIu64 " [style=solid dir=both arrowtail=%s];\n", MTBDD_STRIPMARK(mtbdd), MTBDD_HASMARK(mtbdd) ? "dot" : "none"); - mtbdd_fprintdot_rec(out, mtbdd); + int mtbdd_true_marked = 0; + int mtbdd_false_marked = 0; + mtbdd_fprintdot_rec(out, mtbdd, &mtbdd_true_marked, &mtbdd_false_marked); mtbdd_unmark_rec(mtbdd); fprintf(out, "}\n"); From 6902a3c8f82a37069d8c6b9bbfa41a4cf879be7a Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 8 Sep 2020 18:47:42 +0200 Subject: [PATCH 33/33] Revert "Fixed dot output of BDDs in sylvan." This reverts commit 6dcfd281867d5c360352ab2be98c420d4cdb9c0d. --- resources/3rdparty/sylvan/src/sylvan_mtbdd.c | 57 ++++++++------------ 1 file changed, 23 insertions(+), 34 deletions(-) diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c index 2397c9932..964b538be 100755 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c @@ -3044,39 +3044,30 @@ mtbdd_leaf_to_str(MTBDD leaf, char *buf, size_t buflen) */ static void -mtbdd_fprintdot_rec(FILE *out, MTBDD mtbdd, int *mtbdd_true_marked, int *mtbdd_false_marked) +mtbdd_fprintdot_rec(FILE *out, MTBDD mtbdd) { - if (mtbdd == mtbdd_true) { - if (*mtbdd_true_marked) return; - *mtbdd_true_marked = 1; - fprintf(out, "%" PRIu64 " [shape=box, style=filled, label=\"T\"];\n", mtbdd); - } else if (mtbdd == mtbdd_false) { - if (*mtbdd_false_marked) return; - *mtbdd_false_marked = 1; - fprintf(out, "%" PRIu64 " [shape=box, style=filled, label=\"F\"];\n", mtbdd); + mtbddnode_t n = MTBDD_GETNODE(mtbdd); // also works for mtbdd_false + if (mtbddnode_getmark(n)) return; + mtbddnode_setmark(n, 1); + + if (mtbdd == mtbdd_true || mtbdd == mtbdd_false) { + fprintf(out, "0 [shape=box, style=filled, label=\"F\"];\n"); + } else if (mtbddnode_isleaf(n)) { + fprintf(out, "%" PRIu64 " [shape=box, style=filled, label=\"", MTBDD_STRIPMARK(mtbdd)); + mtbdd_fprint_leaf(out, mtbdd); + fprintf(out, "\"];\n"); } else { - mtbddnode_t n = MTBDD_GETNODE(mtbdd); // also works for mtbdd_false - if (mtbddnode_getmark(n)) return; - mtbddnode_setmark(n, 1); - if (mtbddnode_isleaf(n)) { - fprintf(out, "%" PRIu64 " [shape=box, style=filled, label=\"", MTBDD_STRIPMARK(mtbdd)); - mtbdd_fprint_leaf(out, mtbdd); - fprintf(out, "\"];\n"); - } else { - fprintf(out, "%" PRIu64 " [label=\"%" PRIu32 "\"];\n", - MTBDD_STRIPMARK(mtbdd), mtbddnode_getvariable(n)); - - mtbdd_fprintdot_rec(out, mtbddnode_getlow(n), mtbdd_true_marked, mtbdd_false_marked); - mtbdd_fprintdot_rec(out, mtbddnode_gethigh(n), mtbdd_true_marked, mtbdd_false_marked); - - fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=dashed];\n", - MTBDD_STRIPMARK(mtbdd), - (mtbddnode_getlow(n) == mtbdd_true || mtbddnode_getlow(n) == mtbdd_false) ? mtbddnode_getlow(n) : MTBDD_STRIPMARK(mtbddnode_getlow(n))); - fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=solid dir=both arrowtail=%s];\n", - MTBDD_STRIPMARK(mtbdd), - (mtbddnode_gethigh(n) == mtbdd_true || mtbddnode_gethigh(n) == mtbdd_false) ? mtbddnode_gethigh(n) : MTBDD_STRIPMARK(mtbddnode_gethigh(n)), - mtbddnode_getcomp(n) ? "dot" : "none"); - } + fprintf(out, "%" PRIu64 " [label=\"%" PRIu32 "\"];\n", + MTBDD_STRIPMARK(mtbdd), mtbddnode_getvariable(n)); + + mtbdd_fprintdot_rec(out, mtbddnode_getlow(n)); + mtbdd_fprintdot_rec(out, mtbddnode_gethigh(n)); + + fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=dashed];\n", + MTBDD_STRIPMARK(mtbdd), mtbddnode_getlow(n)); + fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=solid dir=both arrowtail=%s];\n", + MTBDD_STRIPMARK(mtbdd), MTBDD_STRIPMARK(mtbddnode_gethigh(n)), + mtbddnode_getcomp(n) ? "dot" : "none"); } } @@ -3091,9 +3082,7 @@ mtbdd_fprintdot(FILE *out, MTBDD mtbdd) fprintf(out, "root -> %" PRIu64 " [style=solid dir=both arrowtail=%s];\n", MTBDD_STRIPMARK(mtbdd), MTBDD_HASMARK(mtbdd) ? "dot" : "none"); - int mtbdd_true_marked = 0; - int mtbdd_false_marked = 0; - mtbdd_fprintdot_rec(out, mtbdd, &mtbdd_true_marked, &mtbdd_false_marked); + mtbdd_fprintdot_rec(out, mtbdd); mtbdd_unmark_rec(mtbdd); fprintf(out, "}\n");