From 0370729768171cf4f5e4455e69d03a92dedae5d9 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 3 Aug 2026 21:13:30 +0200 Subject: [PATCH 1/8] cleanup in state elimination --- src/storm/environment/SubEnvironment.cpp | 1 + .../solver/AllSolverEnvironments.h | 1 + .../environment/solver/SolverEnvironment.cpp | 8 ++ .../environment/solver/SolverEnvironment.h | 4 + .../SparseDtmcEliminationModelChecker.cpp | 98 +++++++++---------- .../SparseDtmcEliminationModelChecker.h | 21 ++-- .../settings/modules/EliminationSettings.cpp | 24 ++--- .../settings/modules/EliminationSettings.h | 17 +--- .../EliminationLinearEquationSolver.cpp | 17 ++-- .../stateelimination/EliminationMethod.h | 14 +++ .../stateelimination/EliminationOrder.h | 14 +++ .../stateelimination/EliminatorBase.cpp | 4 +- .../StateEliminationUtility.cpp} | 70 ++++++------- .../StateEliminationUtility.h} | 29 +++--- .../stateelimination/StateEliminator.cpp | 4 +- 15 files changed, 168 insertions(+), 158 deletions(-) create mode 100644 src/storm/solver/stateelimination/EliminationMethod.h create mode 100644 src/storm/solver/stateelimination/EliminationOrder.h rename src/storm/{utility/stateelimination.cpp => solver/stateelimination/StateEliminationUtility.cpp} (83%) rename src/storm/{utility/stateelimination.h => solver/stateelimination/StateEliminationUtility.h} (76%) diff --git a/src/storm/environment/SubEnvironment.cpp b/src/storm/environment/SubEnvironment.cpp index d187483e1b..d2031b9c08 100644 --- a/src/storm/environment/SubEnvironment.cpp +++ b/src/storm/environment/SubEnvironment.cpp @@ -53,6 +53,7 @@ template class SubEnvironment; template class SubEnvironment; template class SubEnvironment; +template class SubEnvironment; template class SubEnvironment; template class SubEnvironment; template class SubEnvironment; diff --git a/src/storm/environment/solver/AllSolverEnvironments.h b/src/storm/environment/solver/AllSolverEnvironments.h index b925fd282b..0bfd96453e 100644 --- a/src/storm/environment/solver/AllSolverEnvironments.h +++ b/src/storm/environment/solver/AllSolverEnvironments.h @@ -1,6 +1,7 @@ #pragma once #include "storm/environment/solver/EigenSolverEnvironment.h" +#include "storm/environment/solver/EliminationSolverEnvironment.h" #include "storm/environment/solver/GameSolverEnvironment.h" #include "storm/environment/solver/GmmxxSolverEnvironment.h" #include "storm/environment/solver/LongRunAverageSolverEnvironment.h" diff --git a/src/storm/environment/solver/SolverEnvironment.cpp b/src/storm/environment/solver/SolverEnvironment.cpp index 8d4814f96a..78720c8b51 100644 --- a/src/storm/environment/solver/SolverEnvironment.cpp +++ b/src/storm/environment/solver/SolverEnvironment.cpp @@ -96,6 +96,14 @@ TopologicalSolverEnvironment const& SolverEnvironment::topological() const { return topologicalSolverEnvironment.get(); } +EliminationSolverEnvironment& SolverEnvironment::elimination() { + return eliminationSolverEnvironment.get(); +} + +EliminationSolverEnvironment const& SolverEnvironment::elimination() const { + return eliminationSolverEnvironment.get(); +} + OviSolverEnvironment& SolverEnvironment::ovi() { return oviSolverEnvironment.get(); } diff --git a/src/storm/environment/solver/SolverEnvironment.h b/src/storm/environment/solver/SolverEnvironment.h index 2a39903d66..1ea3d9d792 100644 --- a/src/storm/environment/solver/SolverEnvironment.h +++ b/src/storm/environment/solver/SolverEnvironment.h @@ -21,6 +21,7 @@ class MultiplierEnvironment; class GameSolverEnvironment; class TopologicalSolverEnvironment; class OviSolverEnvironment; +class EliminationSolverEnvironment; class SolverEnvironment { public: @@ -47,6 +48,8 @@ class SolverEnvironment { GameSolverEnvironment const& game() const; TopologicalSolverEnvironment& topological(); TopologicalSolverEnvironment const& topological() const; + EliminationSolverEnvironment& elimination(); + EliminationSolverEnvironment const& elimination() const; bool isForceSoundness() const; void setForceSoundness(bool value); @@ -73,6 +76,7 @@ class SolverEnvironment { SubEnvironment minMaxSolverEnvironment; SubEnvironment multiplierEnvironment; SubEnvironment oviSolverEnvironment; + SubEnvironment eliminationSolverEnvironment; storm::solver::EquationSolverType linearEquationSolverType; bool linearEquationSolverTypeSetFromDefault; diff --git a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 2c9c2aeb2b..d49c986dc9 100644 --- a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -5,31 +5,30 @@ #include #include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/environment/solver/EliminationSolverEnvironment.h" +#include "storm/environment/solver/SolverEnvironment.h" #include "storm/exceptions/IllegalArgumentException.h" #include "storm/exceptions/InvalidPropertyException.h" #include "storm/logic/FragmentSpecification.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/EliminationSettings.h" #include "storm/solver/stateelimination/ConditionalStateEliminator.h" #include "storm/solver/stateelimination/DynamicStatePriorityQueue.h" #include "storm/solver/stateelimination/MultiValueStateEliminator.h" #include "storm/solver/stateelimination/PrioritizedStateEliminator.h" +#include "storm/solver/stateelimination/StateEliminationUtility.h" #include "storm/solver/stateelimination/StaticStatePriorityQueue.h" #include "storm/storage/StronglyConnectedComponentDecomposition.h" #include "storm/utility/constants.h" #include "storm/utility/graph.h" #include "storm/utility/macros.h" -#include "storm/utility/stateelimination.h" #include "storm/utility/vector.h" namespace storm { namespace modelchecker { -using namespace storm::utility::stateelimination; - template SparseDtmcEliminationModelChecker::SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model) : SparsePropositionalModelChecker(model) { @@ -100,8 +99,8 @@ std::unique_ptr SparseDtmcEliminationModelChecker stateValues(maybeStates.size(), storm::utility::zero()); storm::utility::vector::setVectorValues(stateValues, psiStates, storm::utility::one()); - result = - computeLongRunValues(transitionMatrix, backwardTransitions, initialStates, maybeStates, checkTask.isOnlyInitialStatesRelevantSet(), stateValues); + result = computeLongRunValues(env, transitionMatrix, backwardTransitions, initialStates, maybeStates, checkTask.isOnlyInitialStatesRelevantSet(), + stateValues); } // Construct check result based on whether we have computed values for all states or just the initial states. @@ -165,7 +164,7 @@ std::unique_ptr SparseDtmcEliminationModelChecker SparseDtmcEliminationModelChecker std::vector::SolutionType> -SparseDtmcEliminationModelChecker::computeLongRunValues(storm::storage::SparseMatrix const& transitionMatrix, +SparseDtmcEliminationModelChecker::computeLongRunValues(Environment const& env, + storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& maybeStates, @@ -205,11 +205,10 @@ SparseDtmcEliminationModelChecker::computeLongRunValues(sto std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now(); - storm::settings::modules::EliminationSettings::EliminationOrder order = - storm::settings::getModule().getEliminationOrder(); + EliminationOrder order = env.solver().elimination().getOrder(); boost::optional> distanceBasedPriorities; if (eliminationOrderNeedsDistances(order)) { - distanceBasedPriorities = getDistanceBasedPriorities(transitionMatrix, backwardTransitions, initialStates, stateValues, + distanceBasedPriorities = getDistanceBasedPriorities(order, transitionMatrix, backwardTransitions, initialStates, stateValues, eliminationOrderNeedsForwardDistances(order), eliminationOrderNeedsReversedDistances(order)); } @@ -239,7 +238,7 @@ SparseDtmcEliminationModelChecker::computeLongRunValues(sto // First, we eliminate all states in BSCCs (except for the representative states). std::shared_ptr priorityQueue = - createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, stateValues, regularStatesInBsccs); + createStatePriorityQueue(order, distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, stateValues, regularStatesInBsccs); storm::solver::stateelimination::MultiValueStateEliminator stateEliminator(flexibleMatrix, flexibleBackwardTransitions, priorityQueue, stateValues, averageTimeInStates); @@ -301,7 +300,7 @@ SparseDtmcEliminationModelChecker::computeLongRunValues(sto // We only need to eliminate the remaining states if there was some BSCC that has a non-zero value, i.e. // that consists of maybe states. if (!relevantBsccs.empty()) { - performOrdinaryStateElimination(flexibleMatrix, flexibleBackwardTransitions, remainingStates, initialStates, computeResultsForInitialStatesOnly, + performOrdinaryStateElimination(env, flexibleMatrix, flexibleBackwardTransitions, remainingStates, initialStates, computeResultsForInitialStatesOnly, stateValues, distanceBasedPriorities); } @@ -457,13 +456,13 @@ std::unique_ptr SparseDtmcEliminationModelCheckertemplate asExplicitQualitativeCheckResult().getTruthValuesVector(); storm::storage::BitVector const& psiStates = rightResultPointer->template asExplicitQualitativeCheckResult().getTruthValuesVector(); - return computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), - phiStates, psiStates, checkTask.isOnlyInitialStatesRelevantSet()); + return computeUntilProbabilities(env, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), + this->getModel().getInitialStates(), phiStates, psiStates, checkTask.isOnlyInitialStatesRelevantSet()); } template std::unique_ptr SparseDtmcEliminationModelChecker::computeUntilProbabilities( - storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, + Environment const& env, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly) { // Then, compute the subset of states that has a probability of 0 or 1, respectively. @@ -506,7 +505,7 @@ std::unique_ptr SparseDtmcEliminationModelChecker submatrix = probabilityMatrix.getSubmatrix(false, maybeStates, maybeStates); storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); - std::vector subresult = computeReachabilityValues(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, + std::vector subresult = computeReachabilityValues(env, submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, computeForInitialStatesOnly, oneStepProbabilities); storm::utility::vector::setVectorValues(result, maybeStates, subresult); } @@ -542,7 +541,7 @@ std::unique_ptr SparseDtmcEliminationModelCheckergetModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), targetStates, + env, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), targetStates, [&](uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { return rewardModel.getTotalRewardVector(numberOfRows, transitionMatrix, maybeStates); }, @@ -551,11 +550,11 @@ std::unique_ptr SparseDtmcEliminationModelChecker std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards( - storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, + Environment const& env, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector& stateRewardValues, bool computeForInitialStatesOnly) { return computeReachabilityRewards( - probabilityMatrix, backwardTransitions, initialStates, targetStates, + env, probabilityMatrix, backwardTransitions, initialStates, targetStates, [&](uint_fast64_t numberOfRows, storm::storage::SparseMatrix const&, storm::storage::BitVector const& maybeStates) { std::vector result(numberOfRows); storm::utility::vector::selectVectorValues(result, maybeStates, stateRewardValues); @@ -566,7 +565,7 @@ std::unique_ptr SparseDtmcEliminationModelChecker std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards( - storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, + Environment const& env, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, @@ -615,7 +614,7 @@ std::unique_ptr SparseDtmcEliminationModelChecker stateRewardValues = totalStateRewardVectorGetter(submatrix.getRowCount(), probabilityMatrix, maybeStates); std::vector subresult = - computeReachabilityValues(submatrix, stateRewardValues, submatrixTransposed, newInitialStates, computeForInitialStatesOnly, + computeReachabilityValues(env, submatrix, stateRewardValues, submatrixTransposed, newInitialStates, computeForInitialStatesOnly, probabilityMatrix.getConstrainedRowSumVector(maybeStates, targetStates)); storm::utility::vector::setVectorValues(result, maybeStates, subresult); } @@ -651,10 +650,6 @@ std::unique_ptr SparseDtmcEliminationModelCheckertemplate asExplicitQualitativeCheckResult().getTruthValuesVector(); storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); - // Do some sanity checks to establish some required properties. - // STORM_LOG_WARN_COND(storm::settings::getModule().getEliminationMethod() == - // storm::settings::modules::EliminationSettings::EliminationMethod::State, "The chosen elimination method is not available for computing conditional - // probabilities. Falling back to regular state elimination."); STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::IllegalArgumentException, @@ -722,10 +717,9 @@ std::unique_ptr SparseDtmcEliminationModelChecker> distanceBasedPriorities; - storm::settings::modules::EliminationSettings::EliminationOrder order = - storm::settings::getModule().getEliminationOrder(); + EliminationOrder order = env.solver().elimination().getOrder(); if (eliminationOrderNeedsDistances(order)) { - distanceBasedPriorities = getDistanceBasedPriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities, + distanceBasedPriorities = getDistanceBasedPriorities(order, submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities, eliminationOrderNeedsForwardDistances(order), eliminationOrderNeedsReversedDistances(order)); } @@ -733,7 +727,7 @@ std::unique_ptr SparseDtmcEliminationModelChecker flexibleBackwardTransitions(submatrixTransposed, true); std::shared_ptr statePriorities = - createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, statesToEliminate); + createStatePriorityQueue(order, distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, statesToEliminate); STORM_LOG_INFO("Computing conditional probilities.\n"); uint_fast64_t numberOfStatesToEliminate = statePriorities->size(); @@ -883,11 +877,11 @@ void SparseDtmcEliminationModelChecker::performPrioritizedS template void SparseDtmcEliminationModelChecker::performOrdinaryStateElimination( - storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, + Environment const& env, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities) { std::shared_ptr statePriorities = - createStatePriorityQueue(distanceBasedPriorities, transitionMatrix, backwardTransitions, values, subsystem); + createStatePriorityQueue(env.solver().elimination().getOrder(), distanceBasedPriorities, transitionMatrix, backwardTransitions, values, subsystem); std::size_t numberOfStatesToEliminate = statePriorities->size(); STORM_LOG_DEBUG("Eliminating " << numberOfStatesToEliminate << " states using the state elimination technique.\n"); @@ -897,19 +891,19 @@ void SparseDtmcEliminationModelChecker::performOrdinaryStat template uint_fast64_t SparseDtmcEliminationModelChecker::performHybridStateElimination( - storm::storage::SparseMatrix const& forwardTransitions, storm::storage::FlexibleSparseMatrix& transitionMatrix, + Environment const& env, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities) { // When using the hybrid technique, we recursively treat the SCCs up to some size. std::vector entryStateQueue; STORM_LOG_DEBUG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique.\n"); - uint_fast64_t maximalDepth = treatScc(transitionMatrix, values, initialStates, subsystem, initialStates, forwardTransitions, backwardTransitions, false, 0, - storm::settings::getModule().getMaximalSccSize(), entryStateQueue, - computeResultsForInitialStatesOnly, distanceBasedPriorities); + uint_fast64_t maximalDepth = treatScc(env, transitionMatrix, values, initialStates, subsystem, initialStates, forwardTransitions, backwardTransitions, + false, 0, env.solver().elimination().getMaximalSccSize(), entryStateQueue, computeResultsForInitialStatesOnly, + distanceBasedPriorities); // If the entry states were to be eliminated last, we need to do so now. - if (storm::settings::getModule().isEliminateEntryStatesLastSet()) { + if (env.solver().elimination().isEliminateEntryStatesLastSet()) { STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step."); std::vector sortedStates(entryStateQueue.begin(), entryStateQueue.end()); std::shared_ptr queuePriorities = std::make_shared(sortedStates); @@ -921,7 +915,8 @@ uint_fast64_t SparseDtmcEliminationModelChecker::performHyb template std::vector::ValueType> -SparseDtmcEliminationModelChecker::computeReachabilityValues(storm::storage::SparseMatrix const& transitionMatrix, +SparseDtmcEliminationModelChecker::computeReachabilityValues(Environment const& env, + storm::storage::SparseMatrix const& transitionMatrix, std::vector& values, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, @@ -931,24 +926,21 @@ SparseDtmcEliminationModelChecker::computeReachabilityValue storm::storage::FlexibleSparseMatrix flexibleMatrix(transitionMatrix); storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(backwardTransitions); - storm::settings::modules::EliminationSettings::EliminationOrder order = - storm::settings::getModule().getEliminationOrder(); + EliminationOrder order = env.solver().elimination().getOrder(); boost::optional> distanceBasedPriorities; if (eliminationOrderNeedsDistances(order)) { - distanceBasedPriorities = getDistanceBasedPriorities(transitionMatrix, backwardTransitions, initialStates, oneStepProbabilitiesToTarget, + distanceBasedPriorities = getDistanceBasedPriorities(order, transitionMatrix, backwardTransitions, initialStates, oneStepProbabilitiesToTarget, eliminationOrderNeedsForwardDistances(order), eliminationOrderNeedsReversedDistances(order)); } // Create a bit vector that represents the subsystem of states we still have to eliminate. storm::storage::BitVector subsystem = storm::storage::BitVector(transitionMatrix.getRowCount(), true); - if (storm::settings::getModule().getEliminationMethod() == - storm::settings::modules::EliminationSettings::EliminationMethod::State) { - performOrdinaryStateElimination(flexibleMatrix, flexibleBackwardTransitions, subsystem, initialStates, computeResultsForInitialStatesOnly, values, + if (env.solver().elimination().getMethod() == EliminationMethod::State) { + performOrdinaryStateElimination(env, flexibleMatrix, flexibleBackwardTransitions, subsystem, initialStates, computeResultsForInitialStatesOnly, values, distanceBasedPriorities); - } else if (storm::settings::getModule().getEliminationMethod() == - storm::settings::modules::EliminationSettings::EliminationMethod::Hybrid) { - uint64_t maximalDepth = performHybridStateElimination(transitionMatrix, flexibleMatrix, flexibleBackwardTransitions, subsystem, initialStates, + } else if (env.solver().elimination().getMethod() == EliminationMethod::Hybrid) { + uint64_t maximalDepth = performHybridStateElimination(env, transitionMatrix, flexibleMatrix, flexibleBackwardTransitions, subsystem, initialStates, computeResultsForInitialStatesOnly, values, distanceBasedPriorities); STORM_LOG_TRACE("Maximal depth of decomposition was " << maximalDepth << "."); } @@ -966,7 +958,7 @@ SparseDtmcEliminationModelChecker::computeReachabilityValue template uint_fast64_t SparseDtmcEliminationModelChecker::treatScc( - storm::storage::FlexibleSparseMatrix& matrix, std::vector& values, storm::storage::BitVector const& entryStates, + Environment const& env, storm::storage::FlexibleSparseMatrix& matrix, std::vector& values, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& initialStates, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, bool computeResultsForInitialStatesOnly, @@ -999,7 +991,7 @@ uint_fast64_t SparseDtmcEliminationModelChecker::treatScc( } std::shared_ptr statePriorities = - createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, statesInTrivialSccs); + createStatePriorityQueue(env.solver().elimination().getOrder(), distanceBasedPriorities, matrix, backwardTransitions, values, statesInTrivialSccs); STORM_LOG_TRACE("Eliminating " << statePriorities->size() << " trivial SCCs."); performPrioritizedStateElimination(statePriorities, matrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly); STORM_LOG_TRACE("Eliminated all trivial SCCs."); @@ -1024,16 +1016,16 @@ uint_fast64_t SparseDtmcEliminationModelChecker::treatScc( // Recursively descend in SCC-hierarchy. uint_fast64_t depth = - treatScc(matrix, values, entryStates, newSccAsBitVector, initialStates, forwardTransitions, backwardTransitions, - eliminateEntryStates || !storm::settings::getModule().isEliminateEntryStatesLastSet(), - level + 1, maximalSccSize, entryStateQueue, computeResultsForInitialStatesOnly, distanceBasedPriorities); + treatScc(env, matrix, values, entryStates, newSccAsBitVector, initialStates, forwardTransitions, backwardTransitions, + eliminateEntryStates || !env.solver().elimination().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, entryStateQueue, + computeResultsForInitialStatesOnly, distanceBasedPriorities); maximalDepth = std::max(maximalDepth, depth); } } else { // In this case, we perform simple state elimination in the current SCC. STORM_LOG_TRACE("SCC of size " << scc.getNumberOfSetBits() << " is small enough to be eliminated directly."); std::shared_ptr statePriorities = - createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, scc & ~entryStates); + createStatePriorityQueue(env.solver().elimination().getOrder(), distanceBasedPriorities, matrix, backwardTransitions, values, scc & ~entryStates); performPrioritizedStateElimination(statePriorities, matrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly); STORM_LOG_TRACE("Eliminated all states of SCC."); } diff --git a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 8b70af8ea4..5ab7215579 100644 --- a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -53,31 +53,34 @@ class SparseDtmcEliminationModelChecker : public SparsePropositionalModelChecker CheckTask const& checkTask) override; // Static helper methods - static std::unique_ptr computeUntilProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, + static std::unique_ptr computeUntilProbabilities(Environment const& env, + storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly); - static std::unique_ptr computeReachabilityRewards(storm::storage::SparseMatrix const& probabilityMatrix, + static std::unique_ptr computeReachabilityRewards(Environment const& env, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector& stateRewardValues, bool computeForInitialStatesOnly); private: - static std::vector computeLongRunValues(storm::storage::SparseMatrix const& transitionMatrix, + static std::vector computeLongRunValues(Environment const& env, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& maybeStates, bool computeResultsForInitialStatesOnly, std::vector& stateValues); static std::unique_ptr computeReachabilityRewards( - storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, - storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, + Environment const& env, storm::storage::SparseMatrix const& probabilityMatrix, + storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, + storm::storage::BitVector const& targetStates, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, bool computeForInitialStatesOnly); - static std::vector computeReachabilityValues(storm::storage::SparseMatrix const& transitionMatrix, std::vector& values, + static std::vector computeReachabilityValues(Environment const& env, storm::storage::SparseMatrix const& transitionMatrix, + std::vector& values, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector const& oneStepProbabilitiesToTarget); @@ -87,20 +90,20 @@ class SparseDtmcEliminationModelChecker : public SparsePropositionalModelChecker storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly); - static void performOrdinaryStateElimination(storm::storage::FlexibleSparseMatrix& transitionMatrix, + static void performOrdinaryStateElimination(Environment const& env, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities); - static uint_fast64_t performHybridStateElimination(storm::storage::SparseMatrix const& forwardTransitions, + static uint_fast64_t performHybridStateElimination(Environment const& env, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities); - static uint_fast64_t treatScc(storm::storage::FlexibleSparseMatrix& matrix, std::vector& values, + static uint_fast64_t treatScc(Environment const& env, storm::storage::FlexibleSparseMatrix& matrix, std::vector& values, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& initialStates, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, diff --git a/src/storm/settings/modules/EliminationSettings.cpp b/src/storm/settings/modules/EliminationSettings.cpp index d9ad5f24c5..76b0b71f01 100644 --- a/src/storm/settings/modules/EliminationSettings.cpp +++ b/src/storm/settings/modules/EliminationSettings.cpp @@ -56,35 +56,35 @@ EliminationSettings::EliminationSettings() : ModuleSettings(moduleName) { .build()); } -EliminationSettings::EliminationMethod EliminationSettings::getEliminationMethod() const { +storm::solver::stateelimination::EliminationMethod EliminationSettings::getEliminationMethod() const { std::string eliminationMethodAsString = this->getOption(eliminationMethodOptionName).getArgumentByName("name").getValueAsString(); if (eliminationMethodAsString == "state") { - return EliminationMethod::State; + return storm::solver::stateelimination::EliminationMethod::State; } else if (eliminationMethodAsString == "hybrid") { - return EliminationMethod::Hybrid; + return storm::solver::stateelimination::EliminationMethod::Hybrid; } else { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal elimination method selected."); } } -EliminationSettings::EliminationOrder EliminationSettings::getEliminationOrder() const { +storm::solver::stateelimination::EliminationOrder EliminationSettings::getEliminationOrder() const { std::string eliminationOrderAsString = this->getOption(eliminationOrderOptionName).getArgumentByName("name").getValueAsString(); if (eliminationOrderAsString == "fw") { - return EliminationOrder::Forward; + return storm::solver::stateelimination::EliminationOrder::Forward; } else if (eliminationOrderAsString == "fwrev") { - return EliminationOrder::ForwardReversed; + return storm::solver::stateelimination::EliminationOrder::ForwardReversed; } else if (eliminationOrderAsString == "bw") { - return EliminationOrder::Backward; + return storm::solver::stateelimination::EliminationOrder::Backward; } else if (eliminationOrderAsString == "bwrev") { - return EliminationOrder::BackwardReversed; + return storm::solver::stateelimination::EliminationOrder::BackwardReversed; } else if (eliminationOrderAsString == "rand") { - return EliminationOrder::Random; + return storm::solver::stateelimination::EliminationOrder::Random; } else if (eliminationOrderAsString == "spen") { - return EliminationOrder::StaticPenalty; + return storm::solver::stateelimination::EliminationOrder::StaticPenalty; } else if (eliminationOrderAsString == "dpen") { - return EliminationOrder::DynamicPenalty; + return storm::solver::stateelimination::EliminationOrder::DynamicPenalty; } else if (eliminationOrderAsString == "regex") { - return EliminationOrder::RegularExpression; + return storm::solver::stateelimination::EliminationOrder::RegularExpression; } else { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal elimination order selected."); } diff --git a/src/storm/settings/modules/EliminationSettings.h b/src/storm/settings/modules/EliminationSettings.h index 7bac9cbb94..d73c22f767 100644 --- a/src/storm/settings/modules/EliminationSettings.h +++ b/src/storm/settings/modules/EliminationSettings.h @@ -2,6 +2,9 @@ #include "storm/settings/modules/ModuleSettings.h" +#include "storm/solver/stateelimination/EliminationMethod.h" +#include "storm/solver/stateelimination/EliminationOrder.h" + namespace storm { namespace settings { namespace modules { @@ -11,16 +14,6 @@ namespace modules { */ class EliminationSettings : public ModuleSettings { public: - /*! - * An enum that contains all available state elimination orders. - */ - enum class EliminationOrder { Forward, ForwardReversed, Backward, BackwardReversed, Random, StaticPenalty, DynamicPenalty, RegularExpression }; - - /*! - * An enum that contains all available elimination methods. - */ - enum class EliminationMethod { State, Scc, Hybrid }; - /*! * Creates a new set of parametric model checking settings. */ @@ -31,14 +24,14 @@ class EliminationSettings : public ModuleSettings { * * @return The selected elimination method. */ - EliminationMethod getEliminationMethod() const; + storm::solver::stateelimination::EliminationMethod getEliminationMethod() const; /*! * Retrieves the selected elimination order. * * @return The selected elimination order. */ - EliminationOrder getEliminationOrder() const; + storm::solver::stateelimination::EliminationOrder getEliminationOrder() const; /*! * Retrieves whether the option to eliminate entry states in the very end is set. diff --git a/src/storm/solver/EliminationLinearEquationSolver.cpp b/src/storm/solver/EliminationLinearEquationSolver.cpp index 0e4f950497..ef40b53e4d 100644 --- a/src/storm/solver/EliminationLinearEquationSolver.cpp +++ b/src/storm/solver/EliminationLinearEquationSolver.cpp @@ -3,20 +3,19 @@ #include #include "storm/adapters/RationalFunctionAdapter.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/EliminationSettings.h" +#include "storm/environment/solver/EliminationSolverEnvironment.h" +#include "storm/environment/solver/SolverEnvironment.h" #include "storm/solver/stateelimination/PrioritizedStateEliminator.h" +#include "storm/solver/stateelimination/StateEliminationUtility.h" #include "storm/solver/stateelimination/StatePriorityQueue.h" #include "storm/utility/graph.h" #include "storm/utility/macros.h" -#include "storm/utility/stateelimination.h" #include "storm/utility/vector.h" namespace storm { namespace solver { using namespace stateelimination; -using namespace storm::utility::stateelimination; template EliminationLinearEquationSolver::EliminationLinearEquationSolver() { @@ -68,21 +67,19 @@ bool EliminationLinearEquationSolver::internalSolveEquations(Environm boost::optional> distanceBasedPriorities; - // TODO: get the order from the environment - storm::settings::modules::EliminationSettings::EliminationOrder order = - storm::settings::getModule().getEliminationOrder(); + EliminationOrder order = env.solver().elimination().getOrder(); if (eliminationOrderNeedsDistances(order)) { // Since we have no initial states at this point, we determine a representative of every BSCC regarding // the backward transitions, because this means that every row is reachable from this set of rows, which // we require to make sure we cover every row. storm::storage::BitVector initialRows = storm::utility::graph::getBsccCover(backwardTransitions); - distanceBasedPriorities = getDistanceBasedPriorities(transitionMatrix, backwardTransitions, initialRows, b, + distanceBasedPriorities = getDistanceBasedPriorities(order, transitionMatrix, backwardTransitions, initialRows, b, eliminationOrderNeedsForwardDistances(order), eliminationOrderNeedsReversedDistances(order)); } - std::shared_ptr priorityQueue = - createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, b, storm::storage::BitVector(x.size(), true)); + std::shared_ptr priorityQueue = createStatePriorityQueue( + order, distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, b, storm::storage::BitVector(x.size(), true)); // Create a state eliminator to perform the actual elimination. PrioritizedStateEliminator eliminator(flexibleMatrix, flexibleBackwardTransitions, priorityQueue, x); diff --git a/src/storm/solver/stateelimination/EliminationMethod.h b/src/storm/solver/stateelimination/EliminationMethod.h new file mode 100644 index 0000000000..ec3f845622 --- /dev/null +++ b/src/storm/solver/stateelimination/EliminationMethod.h @@ -0,0 +1,14 @@ +#pragma once + +namespace storm { +namespace solver { +namespace stateelimination { + +/*! + * An enum that contains all available elimination methods. + */ +enum class EliminationMethod { State, Scc, Hybrid }; + +} // namespace stateelimination +} // namespace solver +} // namespace storm diff --git a/src/storm/solver/stateelimination/EliminationOrder.h b/src/storm/solver/stateelimination/EliminationOrder.h new file mode 100644 index 0000000000..ff6910bc89 --- /dev/null +++ b/src/storm/solver/stateelimination/EliminationOrder.h @@ -0,0 +1,14 @@ +#pragma once + +namespace storm { +namespace solver { +namespace stateelimination { + +/*! + * An enum that contains all available state elimination orders. + */ +enum class EliminationOrder { Forward, ForwardReversed, Backward, BackwardReversed, Random, StaticPenalty, DynamicPenalty, RegularExpression }; + +} // namespace stateelimination +} // namespace solver +} // namespace storm diff --git a/src/storm/solver/stateelimination/EliminatorBase.cpp b/src/storm/solver/stateelimination/EliminatorBase.cpp index b951dea7aa..79368bebe9 100644 --- a/src/storm/solver/stateelimination/EliminatorBase.cpp +++ b/src/storm/solver/stateelimination/EliminatorBase.cpp @@ -2,16 +2,14 @@ #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/InvalidStateException.h" +#include "storm/solver/stateelimination/StateEliminationUtility.h" #include "storm/utility/constants.h" #include "storm/utility/macros.h" -#include "storm/utility/stateelimination.h" namespace storm { namespace solver { namespace stateelimination { -using namespace storm::utility::stateelimination; - template EliminatorBase::EliminatorBase(storm::storage::FlexibleSparseMatrix& matrix, storm::storage::FlexibleSparseMatrix& transposedMatrix) diff --git a/src/storm/utility/stateelimination.cpp b/src/storm/solver/stateelimination/StateEliminationUtility.cpp similarity index 83% rename from src/storm/utility/stateelimination.cpp rename to src/storm/solver/stateelimination/StateEliminationUtility.cpp index 9098bc754e..101fa081c0 100644 --- a/src/storm/utility/stateelimination.cpp +++ b/src/storm/solver/stateelimination/StateEliminationUtility.cpp @@ -1,11 +1,10 @@ -#include "storm/utility/stateelimination.h" +#include "storm/solver/stateelimination/StateEliminationUtility.h" #include #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/InvalidSettingsException.h" #include "storm/exceptions/InvalidStateException.h" -#include "storm/settings/SettingsManager.h" #include "storm/solver/stateelimination/DynamicStatePriorityQueue.h" #include "storm/solver/stateelimination/StatePriorityQueue.h" #include "storm/solver/stateelimination/StaticStatePriorityQueue.h" @@ -16,34 +15,28 @@ #include "storm/utility/macros.h" namespace storm { -namespace utility { +namespace solver { namespace stateelimination { -bool eliminationOrderNeedsDistances(storm::settings::modules::EliminationSettings::EliminationOrder const& order) { - return order == storm::settings::modules::EliminationSettings::EliminationOrder::Forward || - order == storm::settings::modules::EliminationSettings::EliminationOrder::ForwardReversed || - order == storm::settings::modules::EliminationSettings::EliminationOrder::Backward || - order == storm::settings::modules::EliminationSettings::EliminationOrder::BackwardReversed; +bool eliminationOrderNeedsDistances(EliminationOrder const& order) { + return order == EliminationOrder::Forward || order == EliminationOrder::ForwardReversed || order == EliminationOrder::Backward || + order == EliminationOrder::BackwardReversed; } -bool eliminationOrderNeedsForwardDistances(storm::settings::modules::EliminationSettings::EliminationOrder const& order) { - return order == storm::settings::modules::EliminationSettings::EliminationOrder::Forward || - order == storm::settings::modules::EliminationSettings::EliminationOrder::ForwardReversed; +bool eliminationOrderNeedsForwardDistances(EliminationOrder const& order) { + return order == EliminationOrder::Forward || order == EliminationOrder::ForwardReversed; } -bool eliminationOrderNeedsReversedDistances(storm::settings::modules::EliminationSettings::EliminationOrder const& order) { - return order == storm::settings::modules::EliminationSettings::EliminationOrder::ForwardReversed || - order == storm::settings::modules::EliminationSettings::EliminationOrder::BackwardReversed; +bool eliminationOrderNeedsReversedDistances(EliminationOrder const& order) { + return order == EliminationOrder::ForwardReversed || order == EliminationOrder::BackwardReversed; } -bool eliminationOrderIsPenaltyBased(storm::settings::modules::EliminationSettings::EliminationOrder const& order) { - return order == storm::settings::modules::EliminationSettings::EliminationOrder::StaticPenalty || - order == storm::settings::modules::EliminationSettings::EliminationOrder::DynamicPenalty || - order == storm::settings::modules::EliminationSettings::EliminationOrder::RegularExpression; +bool eliminationOrderIsPenaltyBased(EliminationOrder const& order) { + return order == EliminationOrder::StaticPenalty || order == EliminationOrder::DynamicPenalty || order == EliminationOrder::RegularExpression; } -bool eliminationOrderIsStatic(storm::settings::modules::EliminationSettings::EliminationOrder const& order) { - return eliminationOrderNeedsDistances(order) || order == storm::settings::modules::EliminationSettings::EliminationOrder::StaticPenalty; +bool eliminationOrderIsStatic(EliminationOrder const& order) { + return eliminationOrderNeedsDistances(order) || order == EliminationOrder::StaticPenalty; } template @@ -97,19 +90,16 @@ uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state } template -std::shared_ptr createStatePriorityQueue(boost::optional> const& distanceBasedStatePriorities, +std::shared_ptr createStatePriorityQueue(EliminationOrder const& order, + boost::optional> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities, storm::storage::BitVector const& states) { STORM_LOG_TRACE("Creating state priority queue for states " << states); - // Get the settings to customize the priority queue. - storm::settings::modules::EliminationSettings::EliminationOrder order = - storm::settings::getModule().getEliminationOrder(); - std::vector sortedStates(states.begin(), states.end()); - if (order == storm::settings::modules::EliminationSettings::EliminationOrder::Random) { + if (order == EliminationOrder::Random) { std::random_device randomDevice; std::mt19937 generator(randomDevice()); std::shuffle(sortedStates.begin(), sortedStates.end(), generator); @@ -126,7 +116,7 @@ std::shared_ptr createStatePriorityQueue(boost::optional> statePenalties(sortedStates.size()); typename DynamicStatePriorityQueue::PenaltyFunctionType penaltyFunction = - order == storm::settings::modules::EliminationSettings::EliminationOrder::RegularExpression ? computeStatePenaltyRegularExpression + order == EliminationOrder::RegularExpression ? computeStatePenaltyRegularExpression : computeStatePenalty; for (uint_fast64_t index = 0; index < sortedStates.size(); ++index) { statePenalties[index] = @@ -164,7 +154,7 @@ std::shared_ptr createStatePriorityQueue(std::vector -std::vector getDistanceBasedPriorities(storm::storage::SparseMatrix const& transitionMatrix, +std::vector getDistanceBasedPriorities(EliminationOrder const& order, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward, bool reverse) { @@ -176,10 +166,7 @@ std::vector getDistanceBasedPriorities(storm::storage::SparseMatr std::vector distances = getStateDistances(transitionMatrix, transitionMatrixTransposed, initialStates, oneStepProbabilities, - storm::settings::getModule().getEliminationOrder() == - storm::settings::modules::EliminationSettings::EliminationOrder::Forward || - storm::settings::getModule().getEliminationOrder() == - storm::settings::modules::EliminationSettings::EliminationOrder::ForwardReversed); + order == EliminationOrder::Forward || order == EliminationOrder::ForwardReversed); // In case of the forward or backward ordering, we can sort the states according to the distances. if (forward ^ reverse) { @@ -225,7 +212,8 @@ std::vector getStateDistances(storm::storage::SparseMatrix createStatePriorityQueue(boost::optional> const& distanceBasedStatePriorities, +template std::shared_ptr createStatePriorityQueue(EliminationOrder const& order, + boost::optional> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities, storm::storage::BitVector const& states); @@ -237,7 +225,7 @@ template uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::spar storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); -template std::vector getDistanceBasedPriorities(storm::storage::SparseMatrix const& transitionMatrix, +template std::vector getDistanceBasedPriorities(EliminationOrder const& order, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward, bool reverse); @@ -247,7 +235,8 @@ template std::vector getStateDistances(storm::storage::SparseMatr bool forward); template uint_fast64_t estimateComplexity(storm::RationalNumber const& value); -template std::shared_ptr createStatePriorityQueue(boost::optional> const& distanceBasedStatePriorities, +template std::shared_ptr createStatePriorityQueue(EliminationOrder const& order, + boost::optional> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities, @@ -260,7 +249,8 @@ template uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::spar storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); -template std::vector getDistanceBasedPriorities(storm::storage::SparseMatrix const& transitionMatrix, +template std::vector getDistanceBasedPriorities(EliminationOrder const& order, + storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward, bool reverse); @@ -269,7 +259,8 @@ template std::vector getStateDistances(storm::storage::SparseMatr storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward); -template std::shared_ptr createStatePriorityQueue(boost::optional> const& distanceBasedStatePriorities, +template std::shared_ptr createStatePriorityQueue(EliminationOrder const& order, + boost::optional> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities, @@ -282,7 +273,8 @@ template uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::spar storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); -template std::vector getDistanceBasedPriorities(storm::storage::SparseMatrix const& transitionMatrix, +template std::vector getDistanceBasedPriorities(EliminationOrder const& order, + storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward, bool reverse); @@ -291,5 +283,5 @@ template std::vector getStateDistances(storm::storage::SparseMatr storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward); } // namespace stateelimination -} // namespace utility +} // namespace solver } // namespace storm diff --git a/src/storm/utility/stateelimination.h b/src/storm/solver/stateelimination/StateEliminationUtility.h similarity index 76% rename from src/storm/utility/stateelimination.h rename to src/storm/solver/stateelimination/StateEliminationUtility.h index b8793baa69..e4dc43e921 100644 --- a/src/storm/utility/stateelimination.h +++ b/src/storm/solver/stateelimination/StateEliminationUtility.h @@ -5,16 +5,10 @@ #include #include "storm/adapters/RationalFunctionForward.h" -#include "storm/settings/modules/EliminationSettings.h" +#include "storm/solver/stateelimination/EliminationOrder.h" #include "storm/storage/sparse/StateType.h" namespace storm { -namespace solver { -namespace stateelimination { -class StatePriorityQueue; -} -} // namespace solver - namespace storage { class BitVector; @@ -25,16 +19,16 @@ template class SparseMatrix; } // namespace storage -namespace utility { +namespace solver { namespace stateelimination { -using namespace storm::solver::stateelimination; +class StatePriorityQueue; -bool eliminationOrderNeedsDistances(storm::settings::modules::EliminationSettings::EliminationOrder const& order); -bool eliminationOrderNeedsForwardDistances(storm::settings::modules::EliminationSettings::EliminationOrder const& order); -bool eliminationOrderNeedsReversedDistances(storm::settings::modules::EliminationSettings::EliminationOrder const& order); -bool eliminationOrderIsPenaltyBased(storm::settings::modules::EliminationSettings::EliminationOrder const& order); -bool eliminationOrderIsStatic(storm::settings::modules::EliminationSettings::EliminationOrder const& order); +bool eliminationOrderNeedsDistances(EliminationOrder const& order); +bool eliminationOrderNeedsForwardDistances(EliminationOrder const& order); +bool eliminationOrderNeedsReversedDistances(EliminationOrder const& order); +bool eliminationOrderIsPenaltyBased(EliminationOrder const& order); +bool eliminationOrderIsStatic(EliminationOrder const& order); template uint_fast64_t estimateComplexity(ValueType const& value); @@ -54,7 +48,8 @@ uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state std::vector const& oneStepProbabilities); template -std::shared_ptr createStatePriorityQueue(boost::optional> const& stateDistances, +std::shared_ptr createStatePriorityQueue(EliminationOrder const& order, + boost::optional> const& stateDistances, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities, storm::storage::BitVector const& states); @@ -63,7 +58,7 @@ std::shared_ptr createStatePriorityQueue(storm::storage::Bit std::shared_ptr createStatePriorityQueue(std::vector const& states); template -std::vector getDistanceBasedPriorities(storm::storage::SparseMatrix const& transitionMatrix, +std::vector getDistanceBasedPriorities(EliminationOrder const& order, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward, bool reverse); @@ -74,5 +69,5 @@ std::vector getStateDistances(storm::storage::SparseMatrix const& oneStepProbabilities, bool forward); } // namespace stateelimination -} // namespace utility +} // namespace solver } // namespace storm diff --git a/src/storm/solver/stateelimination/StateEliminator.cpp b/src/storm/solver/stateelimination/StateEliminator.cpp index bd3dce7358..be62c14f33 100644 --- a/src/storm/solver/stateelimination/StateEliminator.cpp +++ b/src/storm/solver/stateelimination/StateEliminator.cpp @@ -2,15 +2,13 @@ #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/IllegalArgumentException.h" +#include "storm/solver/stateelimination/StateEliminationUtility.h" #include "storm/utility/macros.h" -#include "storm/utility/stateelimination.h" namespace storm { namespace solver { namespace stateelimination { -using namespace storm::utility::stateelimination; - template StateEliminator::StateEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions) From 73496db8916b4765b1a010f739ed3937fec0ca98 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 3 Aug 2026 21:38:23 +0200 Subject: [PATCH 2/8] format --- .../solver/EliminationSolverEnvironment.cpp | 53 +++++++++++++++ .../solver/EliminationSolverEnvironment.h | 29 ++++++++ .../SparseDtmcEliminationModelChecker.cpp | 66 +++++++++---------- .../SparseDtmcEliminationModelChecker.h | 6 +- .../StateEliminationUtility.cpp | 8 +-- .../StateEliminationUtility.h | 3 +- 6 files changed, 120 insertions(+), 45 deletions(-) create mode 100644 src/storm/environment/solver/EliminationSolverEnvironment.cpp create mode 100644 src/storm/environment/solver/EliminationSolverEnvironment.h diff --git a/src/storm/environment/solver/EliminationSolverEnvironment.cpp b/src/storm/environment/solver/EliminationSolverEnvironment.cpp new file mode 100644 index 0000000000..c9f5e61288 --- /dev/null +++ b/src/storm/environment/solver/EliminationSolverEnvironment.cpp @@ -0,0 +1,53 @@ +#include "storm/environment/solver/EliminationSolverEnvironment.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/EliminationSettings.h" + +namespace storm { + +EliminationSolverEnvironment::EliminationSolverEnvironment() { + auto const& eliminationSettings = storm::settings::getModule(); + + order = eliminationSettings.getEliminationOrder(); + method = eliminationSettings.getEliminationMethod(); + maximalSccSize = eliminationSettings.getMaximalSccSize(); + eliminateEntryStatesLast = eliminationSettings.isEliminateEntryStatesLastSet(); +} + +EliminationSolverEnvironment::~EliminationSolverEnvironment() { + // Intentionally left empty +} + +storm::solver::stateelimination::EliminationOrder const& EliminationSolverEnvironment::getOrder() const { + return order; +} + +void EliminationSolverEnvironment::setOrder(storm::solver::stateelimination::EliminationOrder value) { + order = value; +} + +storm::solver::stateelimination::EliminationMethod const& EliminationSolverEnvironment::getMethod() const { + return method; +} + +void EliminationSolverEnvironment::setMethod(storm::solver::stateelimination::EliminationMethod value) { + method = value; +} + +uint64_t const& EliminationSolverEnvironment::getMaximalSccSize() const { + return maximalSccSize; +} + +void EliminationSolverEnvironment::setMaximalSccSize(uint64_t value) { + maximalSccSize = value; +} + +bool const& EliminationSolverEnvironment::isEliminateEntryStatesLastSet() const { + return eliminateEntryStatesLast; +} + +void EliminationSolverEnvironment::setEliminateEntryStatesLast(bool value) { + eliminateEntryStatesLast = value; +} + +} // namespace storm diff --git a/src/storm/environment/solver/EliminationSolverEnvironment.h b/src/storm/environment/solver/EliminationSolverEnvironment.h new file mode 100644 index 0000000000..bb247fe392 --- /dev/null +++ b/src/storm/environment/solver/EliminationSolverEnvironment.h @@ -0,0 +1,29 @@ +#pragma once + +#include "storm/environment/solver/SolverEnvironment.h" +#include "storm/solver/stateelimination/EliminationMethod.h" +#include "storm/solver/stateelimination/EliminationOrder.h" + +namespace storm { + +class EliminationSolverEnvironment { + public: + EliminationSolverEnvironment(); + ~EliminationSolverEnvironment(); + + storm::solver::stateelimination::EliminationOrder const& getOrder() const; + void setOrder(storm::solver::stateelimination::EliminationOrder value); + storm::solver::stateelimination::EliminationMethod const& getMethod() const; + void setMethod(storm::solver::stateelimination::EliminationMethod value); + uint64_t const& getMaximalSccSize() const; + void setMaximalSccSize(uint64_t value); + bool const& isEliminateEntryStatesLastSet() const; + void setEliminateEntryStatesLast(bool value); + + private: + storm::solver::stateelimination::EliminationOrder order; + storm::solver::stateelimination::EliminationMethod method; + uint64_t maximalSccSize; + bool eliminateEntryStatesLast; +}; +} // namespace storm diff --git a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index d49c986dc9..0e226c6445 100644 --- a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -462,9 +462,9 @@ std::unique_ptr SparseDtmcEliminationModelChecker std::unique_ptr SparseDtmcEliminationModelChecker::computeUntilProbabilities( - Environment const& env, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, - storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, - bool computeForInitialStatesOnly) { + Environment const& env, storm::storage::SparseMatrix const& probabilityMatrix, + storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, + storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly) { // Then, compute the subset of states that has a probability of 0 or 1, respectively. std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates); @@ -550,9 +550,9 @@ std::unique_ptr SparseDtmcEliminationModelChecker std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards( - Environment const& env, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, - storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector& stateRewardValues, - bool computeForInitialStatesOnly) { + Environment const& env, storm::storage::SparseMatrix const& probabilityMatrix, + storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, + storm::storage::BitVector const& targetStates, std::vector& stateRewardValues, bool computeForInitialStatesOnly) { return computeReachabilityRewards( env, probabilityMatrix, backwardTransitions, initialStates, targetStates, [&](uint_fast64_t numberOfRows, storm::storage::SparseMatrix const&, storm::storage::BitVector const& maybeStates) { @@ -565,8 +565,9 @@ std::unique_ptr SparseDtmcEliminationModelChecker std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards( - Environment const& env, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, - storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, + Environment const& env, storm::storage::SparseMatrix const& probabilityMatrix, + storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, + storm::storage::BitVector const& targetStates, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, bool computeForInitialStatesOnly) { @@ -877,9 +878,10 @@ void SparseDtmcEliminationModelChecker::performPrioritizedS template void SparseDtmcEliminationModelChecker::performOrdinaryStateElimination( - Environment const& env, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, - storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, - std::vector& values, boost::optional> const& distanceBasedPriorities) { + Environment const& env, storm::storage::FlexibleSparseMatrix& transitionMatrix, + storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, + storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, + boost::optional> const& distanceBasedPriorities) { std::shared_ptr statePriorities = createStatePriorityQueue(env.solver().elimination().getOrder(), distanceBasedPriorities, transitionMatrix, backwardTransitions, values, subsystem); @@ -891,16 +893,16 @@ void SparseDtmcEliminationModelChecker::performOrdinaryStat template uint_fast64_t SparseDtmcEliminationModelChecker::performHybridStateElimination( - Environment const& env, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::FlexibleSparseMatrix& transitionMatrix, - storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, - storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, - boost::optional> const& distanceBasedPriorities) { + Environment const& env, storm::storage::SparseMatrix const& forwardTransitions, + storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, + storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, + std::vector& values, boost::optional> const& distanceBasedPriorities) { // When using the hybrid technique, we recursively treat the SCCs up to some size. std::vector entryStateQueue; STORM_LOG_DEBUG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique.\n"); - uint_fast64_t maximalDepth = treatScc(env, transitionMatrix, values, initialStates, subsystem, initialStates, forwardTransitions, backwardTransitions, - false, 0, env.solver().elimination().getMaximalSccSize(), entryStateQueue, computeResultsForInitialStatesOnly, - distanceBasedPriorities); + uint_fast64_t maximalDepth = + treatScc(env, transitionMatrix, values, initialStates, subsystem, initialStates, forwardTransitions, backwardTransitions, false, 0, + env.solver().elimination().getMaximalSccSize(), entryStateQueue, computeResultsForInitialStatesOnly, distanceBasedPriorities); // If the entry states were to be eliminated last, we need to do so now. if (env.solver().elimination().isEliminateEntryStatesLastSet()) { @@ -915,13 +917,10 @@ uint_fast64_t SparseDtmcEliminationModelChecker::performHyb template std::vector::ValueType> -SparseDtmcEliminationModelChecker::computeReachabilityValues(Environment const& env, - storm::storage::SparseMatrix const& transitionMatrix, - std::vector& values, - storm::storage::SparseMatrix const& backwardTransitions, - storm::storage::BitVector const& initialStates, - bool computeResultsForInitialStatesOnly, - std::vector const& oneStepProbabilitiesToTarget) { +SparseDtmcEliminationModelChecker::computeReachabilityValues( + Environment const& env, storm::storage::SparseMatrix const& transitionMatrix, std::vector& values, + storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, + std::vector const& oneStepProbabilitiesToTarget) { // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. storm::storage::FlexibleSparseMatrix flexibleMatrix(transitionMatrix); storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(backwardTransitions); @@ -958,11 +957,11 @@ SparseDtmcEliminationModelChecker::computeReachabilityValue template uint_fast64_t SparseDtmcEliminationModelChecker::treatScc( - Environment const& env, storm::storage::FlexibleSparseMatrix& matrix, std::vector& values, storm::storage::BitVector const& entryStates, - storm::storage::BitVector const& scc, storm::storage::BitVector const& initialStates, storm::storage::SparseMatrix const& forwardTransitions, - storm::storage::FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, - std::vector& entryStateQueue, bool computeResultsForInitialStatesOnly, - boost::optional> const& distanceBasedPriorities) { + Environment const& env, storm::storage::FlexibleSparseMatrix& matrix, std::vector& values, + storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& initialStates, + storm::storage::SparseMatrix const& forwardTransitions, storm::storage::FlexibleSparseMatrix& backwardTransitions, + bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, + bool computeResultsForInitialStatesOnly, boost::optional> const& distanceBasedPriorities) { uint_fast64_t maximalDepth = level; // If the SCCs are large enough, we try to split them further. @@ -1015,10 +1014,9 @@ uint_fast64_t SparseDtmcEliminationModelChecker::treatScc( } // Recursively descend in SCC-hierarchy. - uint_fast64_t depth = - treatScc(env, matrix, values, entryStates, newSccAsBitVector, initialStates, forwardTransitions, backwardTransitions, - eliminateEntryStates || !env.solver().elimination().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, entryStateQueue, - computeResultsForInitialStatesOnly, distanceBasedPriorities); + uint_fast64_t depth = treatScc(env, matrix, values, entryStates, newSccAsBitVector, initialStates, forwardTransitions, backwardTransitions, + eliminateEntryStates || !env.solver().elimination().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, + entryStateQueue, computeResultsForInitialStatesOnly, distanceBasedPriorities); maximalDepth = std::max(maximalDepth, depth); } } else { diff --git a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 5ab7215579..2793d5b450 100644 --- a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -53,8 +53,7 @@ class SparseDtmcEliminationModelChecker : public SparsePropositionalModelChecker CheckTask const& checkTask) override; // Static helper methods - static std::unique_ptr computeUntilProbabilities(Environment const& env, - storm::storage::SparseMatrix const& probabilityMatrix, + static std::unique_ptr computeUntilProbabilities(Environment const& env, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly); @@ -80,8 +79,7 @@ class SparseDtmcEliminationModelChecker : public SparsePropositionalModelChecker bool computeForInitialStatesOnly); static std::vector computeReachabilityValues(Environment const& env, storm::storage::SparseMatrix const& transitionMatrix, - std::vector& values, - storm::storage::SparseMatrix const& backwardTransitions, + std::vector& values, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector const& oneStepProbabilitiesToTarget); diff --git a/src/storm/solver/stateelimination/StateEliminationUtility.cpp b/src/storm/solver/stateelimination/StateEliminationUtility.cpp index 101fa081c0..078ce40308 100644 --- a/src/storm/solver/stateelimination/StateEliminationUtility.cpp +++ b/src/storm/solver/stateelimination/StateEliminationUtility.cpp @@ -116,8 +116,7 @@ std::shared_ptr createStatePriorityQueue(EliminationOrder co } else if (eliminationOrderIsPenaltyBased(order)) { std::vector> statePenalties(sortedStates.size()); typename DynamicStatePriorityQueue::PenaltyFunctionType penaltyFunction = - order == EliminationOrder::RegularExpression ? computeStatePenaltyRegularExpression - : computeStatePenalty; + order == EliminationOrder::RegularExpression ? computeStatePenaltyRegularExpression : computeStatePenalty; for (uint_fast64_t index = 0; index < sortedStates.size(); ++index) { statePenalties[index] = std::make_pair(sortedStates[index], penaltyFunction(sortedStates[index], transitionMatrix, backwardTransitions, oneStepProbabilities)); @@ -164,9 +163,8 @@ std::vector getDistanceBasedPriorities(EliminationOrder const& or states[index] = index; } - std::vector distances = - getStateDistances(transitionMatrix, transitionMatrixTransposed, initialStates, oneStepProbabilities, - order == EliminationOrder::Forward || order == EliminationOrder::ForwardReversed); + std::vector distances = getStateDistances(transitionMatrix, transitionMatrixTransposed, initialStates, oneStepProbabilities, + order == EliminationOrder::Forward || order == EliminationOrder::ForwardReversed); // In case of the forward or backward ordering, we can sort the states according to the distances. if (forward ^ reverse) { diff --git a/src/storm/solver/stateelimination/StateEliminationUtility.h b/src/storm/solver/stateelimination/StateEliminationUtility.h index e4dc43e921..f103f1252f 100644 --- a/src/storm/solver/stateelimination/StateEliminationUtility.h +++ b/src/storm/solver/stateelimination/StateEliminationUtility.h @@ -48,8 +48,7 @@ uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state std::vector const& oneStepProbabilities); template -std::shared_ptr createStatePriorityQueue(EliminationOrder const& order, - boost::optional> const& stateDistances, +std::shared_ptr createStatePriorityQueue(EliminationOrder const& order, boost::optional> const& stateDistances, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities, storm::storage::BitVector const& states); From f7aa0df5275a17d218d1b74915ac1572f9e8172b Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 3 Aug 2026 21:45:45 +0200 Subject: [PATCH 3/8] update --- .../reachability/SparseDtmcEliminationModelChecker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 0e226c6445..6b87af50e2 100644 --- a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -13,7 +13,7 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/EliminationSettings.h" +#include "storm/settings/modules/CoreSettings.h" #include "storm/solver/stateelimination/ConditionalStateEliminator.h" #include "storm/solver/stateelimination/DynamicStatePriorityQueue.h" #include "storm/solver/stateelimination/MultiValueStateEliminator.h" From 9658c5273bd0bfd3fc03d2ea9ee327b35f3ce7bd Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 4 Aug 2026 16:50:14 +0200 Subject: [PATCH 4/8] monotonicity revamped --- .../region/monotonicity/AssumptionChecker.cpp | 76 ++-- .../region/monotonicity/AssumptionChecker.h | 15 +- .../region/monotonicity/AssumptionMaker.cpp | 58 ++- .../region/monotonicity/AssumptionMaker.h | 31 +- .../monotonicity/MonotonicityHelper.cpp | 144 +++--- .../region/monotonicity/MonotonicityHelper.h | 58 +-- .../region/monotonicity/Order.cpp | 186 ++++---- .../modelchecker/region/monotonicity/Order.h | 22 + .../OrderBasedMonotonicityBackend.cpp | 6 +- .../region/monotonicity/OrderExtender.cpp | 423 +++++++++--------- .../region/monotonicity/OrderExtender.h | 37 +- .../monotonicity/AssumptionCheckerTest.cpp | 128 ++---- .../monotonicity/AssumptionMakerTest.cpp | 39 +- .../region/monotonicity/OrderTest.cpp | 88 ++++ 14 files changed, 661 insertions(+), 650 deletions(-) diff --git a/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.cpp b/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.cpp index ce31150bb4..6494e342f8 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.cpp @@ -9,8 +9,6 @@ #include "storm/solver/Z3SmtSolver.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/RationalFunctionToExpression.h" -#include "storm/storage/expressions/SimpleValuation.h" -#include "storm/storage/expressions/VariableExpression.h" #include "storm/utility/solver.h" namespace storm { @@ -73,22 +71,21 @@ AssumptionChecker::AssumptionChecker(std::shared_ptr -AssumptionStatus AssumptionChecker::validateAssumption(uint_fast64_t val1, uint_fast64_t val2, - std::shared_ptr assumption, - std::shared_ptr order, storage::ParameterRegion region, +AssumptionStatus AssumptionChecker::validateAssumption(Assumption const& assumption, std::shared_ptr order, + storage::ParameterRegion region, std::vector const minValues, std::vector const maxValues) const { // First check if based on sample points the assumption can be discharged - assert(val1 == std::stoull(assumption->getFirstOperand()->asVariableExpression().getVariableName())); - assert(val2 == std::stoull(assumption->getSecondOperand()->asVariableExpression().getVariableName())); AssumptionStatus result = AssumptionStatus::UNKNOWN; if (useSamples) { result = checkOnSamples(assumption); } - assert(result != AssumptionStatus::VALID); + STORM_LOG_ASSERT(result != AssumptionStatus::VALID, "Sample-based checking should never conclude VALID by itself."); if (minValues.size() != 0) { - if (assumption->getRelationType() == expressions::RelationType::Greater) { + auto const val1 = assumption.state1; + auto const val2 = assumption.state2; + if (assumption.relation == expressions::RelationType::Greater) { if (minValues[val1] > maxValues[val2]) { return AssumptionStatus::VALID; } else if (minValues[val1] == maxValues[val2] && minValues[val1] == maxValues[val1] && minValues[val2] == maxValues[val2]) { @@ -109,31 +106,20 @@ AssumptionStatus AssumptionChecker::validateAssumption( if (result == AssumptionStatus::UNKNOWN) { // If result from sample checking was unknown, the assumption might hold - std::set vars = std::set({}); - assumption->gatherVariables(vars); - - STORM_LOG_THROW( - assumption->getRelationType() == expressions::RelationType::Greater || assumption->getRelationType() == expressions::RelationType::Equal, - exceptions::NotSupportedException, "Only Greater Or Equal assumptions supported"); - result = validateAssumptionSMTSolver(val1, val2, assumption, order, region, minValues, maxValues); + STORM_LOG_THROW(assumption.relation == expressions::RelationType::Greater || assumption.relation == expressions::RelationType::Equal, + exceptions::NotSupportedException, "Only Greater Or Equal assumptions supported"); + result = validateAssumptionSMTSolver(assumption, order, region, minValues, maxValues); } return result; } template -AssumptionStatus AssumptionChecker::checkOnSamples(std::shared_ptr assumption) const { +AssumptionStatus AssumptionChecker::checkOnSamples(Assumption const& assumption) const { auto result = AssumptionStatus::UNKNOWN; - std::set vars = std::set({}); - assumption->gatherVariables(vars); - for (auto values : samples) { - auto valuation = expressions::SimpleValuation(assumption->getManager().getSharedPointer()); - for (auto var : vars) { - auto index = std::stoi(var.getName()); - valuation.setRationalValue(var, utility::convertNumber(values[index])); - } - - assert(assumption->hasBooleanType()); - if (!assumption->evaluateAsBool(&valuation)) { + for (auto const& values : samples) { + bool holds = assumption.relation == expressions::RelationType::Greater ? values[assumption.state1] > values[assumption.state2] + : values[assumption.state1] == values[assumption.state2]; + if (!holds) { result = AssumptionStatus::INVALID; break; } @@ -142,19 +128,19 @@ AssumptionStatus AssumptionChecker::checkOnSamples(std: } template -AssumptionStatus AssumptionChecker::validateAssumptionSMTSolver( - uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr assumption, std::shared_ptr order, - storage::ParameterRegion region, std::vector const minValues, std::vector const maxValues) const { - std::shared_ptr smtSolverFactory = std::make_shared(); +AssumptionStatus AssumptionChecker::validateAssumptionSMTSolver(Assumption const& assumption, std::shared_ptr order, + storage::ParameterRegion region, + std::vector const minValues, + std::vector const maxValues) const { std::shared_ptr manager(new expressions::ExpressionManager()); AssumptionStatus result = AssumptionStatus::UNKNOWN; - auto var1 = assumption->getFirstOperand()->asVariableExpression().getVariableName(); - auto var2 = assumption->getSecondOperand()->asVariableExpression().getVariableName(); + uint_fast64_t val1 = assumption.state1; + uint_fast64_t val2 = assumption.state2; auto row1 = matrix.getRow(val1); auto row2 = matrix.getRow(val2); bool orderKnown = true; - // if the state with number var1 (var2) occurs in the successors of the state with number var2 (var1) we need to add var1 == expr1 (var2 == expr2) to the + // if the state with number val1 (val2) occurs in the successors of the state with number val2 (val1) we need to add val1 == expr1 (val2 == expr2) to the // bounds bool addVar1 = false; bool addVar2 = false; @@ -165,7 +151,7 @@ AssumptionStatus AssumptionChecker::validateAssumptionS std::set topVariables; std::set bottomVariables; for (auto itr1 = row1.begin(); orderKnown && itr1 != row1.end(); ++itr1) { - addVar2 |= std::to_string(itr1->getColumn()) == var2; + addVar2 |= itr1->getColumn() == val2; auto varname1 = "s" + std::to_string(itr1->getColumn()); if (!manager->hasVariable(varname1)) { if (order->isTopState(itr1->getColumn())) { @@ -178,7 +164,7 @@ AssumptionStatus AssumptionChecker::validateAssumptionS } for (auto itr2 = row2.begin(); orderKnown && itr2 != row2.end(); ++itr2) { - addVar1 |= std::to_string(itr2->getColumn()) == var1; + addVar1 |= itr2->getColumn() == val1; if (itr1->getColumn() != itr2->getColumn()) { auto varname2 = "s" + std::to_string(itr2->getColumn()); if (!manager->hasVariable(varname2)) { @@ -248,10 +234,10 @@ AssumptionStatus AssumptionChecker::validateAssumptionS // It is the negation of actual assumption expressions::Expression exprToCheck; - if (assumption->getRelationType() == expressions::RelationType::Greater) { + if (assumption.relation == expressions::RelationType::Greater) { exprToCheck = expr1 <= expr2; } else { - assert(assumption->getRelationType() == expressions::RelationType::Equal); + STORM_LOG_ASSERT(assumption.relation == expressions::RelationType::Equal, "Only Greater and Equal assumptions are supported."); exprToCheck = expr1 != expr2; } @@ -259,10 +245,10 @@ AssumptionStatus AssumptionChecker::validateAssumptionS // Bounds for the state probabilities and parameters expressions::Expression exprBounds = manager->boolean(true); if (addVar1) { - exprBounds = exprBounds && (manager->getVariable("s" + var1) == expr1); + exprBounds = exprBounds && (manager->getVariable("s" + std::to_string(val1)) == expr1); } if (addVar2) { - exprBounds = exprBounds && (manager->getVariable("s" + var2) == expr2); + exprBounds = exprBounds && (manager->getVariable("s" + std::to_string(val2)) == expr2); } for (auto var : variables) { if (find(stateVariables.begin(), stateVariables.end(), var) != stateVariables.end()) { @@ -297,7 +283,6 @@ AssumptionStatus AssumptionChecker::validateAssumptionS if (s.check() == solver::SmtSolver::CheckResult::Unsat) { return AssumptionStatus::INVALID; } - assert(s.check() != solver::SmtSolver::CheckResult::Unsat); s.add(exprToCheck); auto smtRes = s.check(); @@ -312,13 +297,10 @@ AssumptionStatus AssumptionChecker::validateAssumptionS } template -AssumptionStatus AssumptionChecker::validateAssumption(std::shared_ptr assumption, - std::shared_ptr order, +AssumptionStatus AssumptionChecker::validateAssumption(Assumption const& assumption, std::shared_ptr order, storage::ParameterRegion region) const { - auto var1 = std::stoi(assumption->getFirstOperand()->asVariableExpression().getVariableName()); - auto var2 = std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName()); std::vector vals; - return validateAssumption(var1, var2, assumption, order, region, vals, vals); + return validateAssumption(assumption, order, region, vals, vals); } template class AssumptionChecker; diff --git a/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.h b/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.h index 3d7bf04084..18d23bd7c4 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.h +++ b/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.h @@ -1,5 +1,6 @@ #pragma once +#include "Assumption.h" #include "Order.h" #include "storm-pars/storage/ParameterRegion.h" #include "storm/environment/Environment.h" @@ -7,7 +8,6 @@ #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" #include "storm/storage/SparseMatrix.h" -#include "storm/storage/expressions/BinaryRelationExpression.h" namespace storm { namespace analysis { @@ -69,11 +69,9 @@ class AssumptionChecker { * @param region The region of the considered model. * @return AssumptionStatus::VALID, or AssumptionStatus::UNKNOWN, or AssumptionStatus::INVALID */ - AssumptionStatus validateAssumption(uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr assumption, - std::shared_ptr order, storage::ParameterRegion region, std::vector const minValues, - std::vector const maxValue) const; - AssumptionStatus validateAssumption(std::shared_ptr assumption, std::shared_ptr order, - storage::ParameterRegion region) const; + AssumptionStatus validateAssumption(Assumption const& assumption, std::shared_ptr order, storage::ParameterRegion region, + std::vector const minValues, std::vector const maxValue) const; + AssumptionStatus validateAssumption(Assumption const& assumption, std::shared_ptr order, storage::ParameterRegion region) const; private: bool useSamples; @@ -82,11 +80,10 @@ class AssumptionChecker { storage::SparseMatrix matrix; - AssumptionStatus validateAssumptionSMTSolver(uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr assumption, - std::shared_ptr order, storage::ParameterRegion region, + AssumptionStatus validateAssumptionSMTSolver(Assumption const& assumption, std::shared_ptr order, storage::ParameterRegion region, std::vector const minValues, std::vector const maxValue) const; - AssumptionStatus checkOnSamples(std::shared_ptr assumption) const; + AssumptionStatus checkOnSamples(Assumption const& assumption) const; }; } // namespace analysis } // namespace storm diff --git a/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.cpp b/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.cpp index 135450a0bd..64c7668624 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.cpp @@ -6,15 +6,11 @@ namespace storm { namespace analysis { template AssumptionMaker::AssumptionMaker(storage::SparseMatrix matrix) : assumptionChecker(matrix) { - numberOfStates = matrix.getColumnCount(); - expressionManager = std::make_shared(expressions::ExpressionManager()); - for (uint_fast64_t i = 0; i < this->numberOfStates; ++i) { - expressionManager->declareRationalVariable(std::to_string(i)); - } + // Intentionally left empty. } template -std::map, AssumptionStatus> AssumptionMaker::createAndCheckAssumptions( +std::vector> AssumptionMaker::createAndCheckAssumptions( uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr order, storage::ParameterRegion region) const { auto vec1 = std::vector(); auto vec2 = std::vector(); @@ -22,49 +18,51 @@ std::map, AssumptionStatu } template -std::map, AssumptionStatus> AssumptionMaker::createAndCheckAssumptions( +std::vector> AssumptionMaker::createAndCheckAssumptions( uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr order, storage::ParameterRegion region, std::vector const minValues, std::vector const maxValues) const { - std::map, AssumptionStatus> result; + std::vector> result; STORM_LOG_INFO("Creating assumptions for " << val1 << " and " << val2); - assert(order->compare(val1, val2) == Order::UNKNOWN); + STORM_LOG_ASSERT(order->compare(val1, val2) == Order::UNKNOWN, "Expected the given pair to indeed be unordered."); auto assumption = createAndCheckAssumption(val1, val2, expressions::RelationType::Greater, order, region, minValues, maxValues); if (assumption.second != AssumptionStatus::INVALID) { - result.insert(assumption); + result.push_back(assumption); if (assumption.second == AssumptionStatus::VALID) { - assert(createAndCheckAssumption(val2, val1, expressions::RelationType::Greater, order, region, minValues, maxValues).second != - AssumptionStatus::VALID && - createAndCheckAssumption(val1, val2, expressions::RelationType::Equal, order, region, minValues, maxValues).second != - AssumptionStatus::VALID); + STORM_LOG_ASSERT(createAndCheckAssumption(val2, val1, expressions::RelationType::Greater, order, region, minValues, maxValues).second != + AssumptionStatus::VALID && + createAndCheckAssumption(val1, val2, expressions::RelationType::Equal, order, region, minValues, maxValues).second != + AssumptionStatus::VALID, + "At most one of the three candidate assumptions may be valid."); STORM_LOG_INFO("Assumption " << assumption.first << "is valid\n"); return result; } } - assert(order->compare(val1, val2) == Order::UNKNOWN); + STORM_LOG_ASSERT(order->compare(val1, val2) == Order::UNKNOWN, "Expected the given pair to indeed be unordered."); assumption = createAndCheckAssumption(val2, val1, expressions::RelationType::Greater, order, region, minValues, maxValues); if (assumption.second != AssumptionStatus::INVALID) { if (assumption.second == AssumptionStatus::VALID) { result.clear(); - result.insert(assumption); - assert(createAndCheckAssumption(val1, val2, expressions::RelationType::Equal, order, region, minValues, maxValues).second != - AssumptionStatus::VALID); + result.push_back(assumption); + STORM_LOG_ASSERT(createAndCheckAssumption(val1, val2, expressions::RelationType::Equal, order, region, minValues, maxValues).second != + AssumptionStatus::VALID, + "At most one of the three candidate assumptions may be valid."); STORM_LOG_INFO("Assumption " << assumption.first << "is valid\n"); return result; } - result.insert(assumption); + result.push_back(assumption); } - assert(order->compare(val1, val2) == Order::UNKNOWN); + STORM_LOG_ASSERT(order->compare(val1, val2) == Order::UNKNOWN, "Expected the given pair to indeed be unordered."); assumption = createAndCheckAssumption(val1, val2, expressions::RelationType::Equal, order, region, minValues, maxValues); if (assumption.second != AssumptionStatus::INVALID) { if (assumption.second == AssumptionStatus::VALID) { result.clear(); - result.insert(assumption); + result.push_back(assumption); STORM_LOG_INFO("Assumption " << assumption.first << "is valid\n"); return result; } - result.insert(assumption); + result.push_back(assumption); } - assert(order->compare(val1, val2) == Order::UNKNOWN); + STORM_LOG_ASSERT(order->compare(val1, val2) == Order::UNKNOWN, "Expected the given pair to indeed be unordered."); STORM_LOG_INFO("None of the assumptions is valid, number of possible assumptions: " << result.size() << '\n'); return result; } @@ -82,17 +80,13 @@ void AssumptionMaker::setSampleValues(std::vector -std::pair, AssumptionStatus> AssumptionMaker::createAndCheckAssumption( +std::pair AssumptionMaker::createAndCheckAssumption( uint_fast64_t val1, uint_fast64_t val2, expressions::RelationType relationType, std::shared_ptr order, storage::ParameterRegion region, std::vector const minValues, std::vector const maxValues) const { - assert(val1 != val2); - expressions::Variable var1 = expressionManager->getVariable(std::to_string(val1)); - expressions::Variable var2 = expressionManager->getVariable(std::to_string(val2)); - auto assumption = std::make_shared( - expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), var1.getExpression().getBaseExpressionPointer(), - var2.getExpression().getBaseExpressionPointer(), relationType)); - AssumptionStatus validationResult = assumptionChecker.validateAssumption(val1, val2, assumption, order, region, minValues, maxValues); - return std::pair, AssumptionStatus>(assumption, validationResult); + STORM_LOG_ASSERT(val1 != val2, "An assumption must relate two distinct states."); + Assumption assumption{val1, val2, relationType}; + AssumptionStatus validationResult = assumptionChecker.validateAssumption(assumption, order, region, minValues, maxValues); + return {assumption, validationResult}; } template class AssumptionMaker; diff --git a/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h b/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h index d261cea620..633b16d8cc 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h +++ b/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h @@ -1,19 +1,17 @@ #pragma once +#include "Assumption.h" #include "AssumptionChecker.h" #include "Order.h" #include "storm/storage/SparseMatrix.h" -#include "storm/storage/expressions/BinaryRelationExpression.h" -#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/storage/expressions/BinaryRelationType.h" namespace storm { namespace analysis { template class AssumptionMaker { - typedef std::shared_ptr AssumptionType; - public: /*! * Constructs AssumptionMaker based on the matrix of the model. @@ -31,13 +29,15 @@ class AssumptionMaker { * @param val2 Second state number. * @param order The order on which the assumptions are checked. * @param region The region for the parameters. - * @return Map with at most three assumptions, and the validation. + * @return At most three (assumption, status) candidates, in the order they were tried + * (val1 > val2, val2 > val1, val1 == val2). */ - std::map, AssumptionStatus> createAndCheckAssumptions( - uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr order, storage::ParameterRegion region) const; - std::map, AssumptionStatus> createAndCheckAssumptions( - uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr order, storage::ParameterRegion region, - std::vector const minValues, std::vector const maxValue) const; + std::vector> createAndCheckAssumptions(uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr order, + storage::ParameterRegion region) const; + std::vector> createAndCheckAssumptions(uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr order, + storage::ParameterRegion region, + std::vector const minValues, + std::vector const maxValue) const; /*! * Initializes the given number of sample points for a given model, formula and region. @@ -58,15 +58,12 @@ class AssumptionMaker { void setSampleValues(std::vector> const& samples); private: - std::pair, AssumptionStatus> createAndCheckAssumption( - uint_fast64_t val1, uint_fast64_t val2, expressions::RelationType relationType, std::shared_ptr order, - storage::ParameterRegion region, std::vector const minValues, std::vector const maxValue) const; + std::pair createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, expressions::RelationType relationType, + std::shared_ptr order, storage::ParameterRegion region, + std::vector const minValues, + std::vector const maxValue) const; AssumptionChecker assumptionChecker; - - std::shared_ptr expressionManager; - - uint_fast64_t numberOfStates; }; } // namespace analysis } // namespace storm diff --git a/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.cpp b/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.cpp index 4e7ca1de6d..def16a9b88 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.cpp @@ -61,7 +61,7 @@ MonotonicityHelper::MonotonicityHelper(std::shared_ptr< checkSamples = false; } - this->extender = new analysis::OrderExtender(model, formulas[0]); + this->extender = std::make_unique>(model, formulas[0]); for (uint_fast64_t i = 0; i < matrix.getRowCount(); ++i) { std::set occurringVariables; @@ -78,7 +78,7 @@ MonotonicityHelper::MonotonicityHelper(std::shared_ptr< /*** Public methods ***/ template std::map, std::pair::VariableType>>, - std::vector>>> + std::vector>> MonotonicityHelper::checkMonotonicityInBuild(std::ostream& outfile, bool usePLA, std::string dotOutfileName) { if (usePLA) { storm::utility::Stopwatch plaWatch(true); @@ -110,7 +110,7 @@ MonotonicityHelper::checkMonotonicityInBuild(std::ostre << " "; first = false; } - outfile << *assumption; + outfile << assumption; } if (!first) { outfile << '\n'; @@ -177,21 +177,13 @@ void MonotonicityHelper::createOrder() { auto monRes = std::make_shared>(MonotonicityResult()); criticalTuple = extender->toOrder(region, monRes); // Continue based on not (yet) sorted states - std::map, std::vector>> result; - auto val1 = std::get<1>(criticalTuple); auto val2 = std::get<2>(criticalTuple); auto numberOfStates = model->getNumberOfStates(); - std::vector> assumptions; + std::vector assumptions; if (val1 == numberOfStates && val2 == numberOfStates) { - auto resAssumptionPair = - std::pair>, std::vector>>(monRes, - assumptions); - monResults.insert( - std::pair, - std::pair>, std::vector>>>( - std::get<0>(criticalTuple), resAssumptionPair)); + monResults.insert({std::get<0>(criticalTuple), {monRes, assumptions}}); } else if (val1 != numberOfStates && val2 != numberOfStates) { extendOrderWithAssumptions(std::get<0>(criticalTuple), val1, val2, assumptions, monRes); } else { @@ -201,74 +193,90 @@ void MonotonicityHelper::createOrder() { template void MonotonicityHelper::extendOrderWithAssumptions(std::shared_ptr order, uint_fast64_t val1, uint_fast64_t val2, - std::vector> assumptions, + std::vector assumptions, std::shared_ptr> monRes) { - std::map, std::vector>> result; - if (order->isInvalid()) { - // We don't add anything as the order we created with assumptions turns out to be invalid - STORM_LOG_INFO(" The order was invalid, so we stop here"); - return; - } - auto numberOfStates = model->getNumberOfStates(); - if (val1 == numberOfStates || val2 == numberOfStates) { - assert(val1 == val2); - assert(order->getNumberOfAddedStates() == order->getNumberOfStates()); - auto resAssumptionPair = - std::pair>, std::vector>>(monRes, - assumptions); - monResults.insert( - std::pair, - std::pair>, std::vector>>>( - std::move(order), std::move(resAssumptionPair))); - } else { + // Explicit worklist instead of recursion: each unresolved (val1, val2) pair can spawn up to + // three independent branches (one per candidate assumption), and pathological pMCs can chain + // enough of these to overflow the C++ call stack if done recursively. The branches are pushed + // in reverse so popping (LIFO) visits them in the same left-to-right order the original + // recursion did; that's not required for correctness (branches share no mutable state) but + // keeps behavior close to before while validating this change. + struct PendingBranch { + std::shared_ptr order; + uint_fast64_t val1; + uint_fast64_t val2; + std::vector assumptions; + std::shared_ptr> monRes; + }; + std::vector worklist; + worklist.push_back({std::move(order), val1, val2, std::move(assumptions), std::move(monRes)}); + + auto const numberOfStates = model->getNumberOfStates(); + while (!worklist.empty()) { + PendingBranch current = std::move(worklist.back()); + worklist.pop_back(); + + if (current.order->isInvalid()) { + // We don't add anything as the order we created with assumptions turns out to be invalid + STORM_LOG_INFO(" The order was invalid, so we stop here"); + continue; + } + if (current.val1 == numberOfStates || current.val2 == numberOfStates) { + assert(current.val1 == current.val2); + assert(current.order->getNumberOfAddedStates() == current.order->getNumberOfStates()); + monResults.insert({current.order, {current.monRes, current.assumptions}}); + continue; + } + // Make the three assumptions - STORM_LOG_INFO("Creating assumptions for " << val1 << " and " << val2 << ". "); - auto newAssumptions = assumptionMaker.createAndCheckAssumptions(val1, val2, order, region); + STORM_LOG_INFO("Creating assumptions for " << current.val1 << " and " << current.val2 << ". "); + auto newAssumptions = assumptionMaker.createAndCheckAssumptions(current.val1, current.val2, current.order, region); assert(newAssumptions.size() <= 3); - auto itr = newAssumptions.begin(); - if (newAssumptions.size() == 0) { - monRes = std::make_shared>(MonotonicityResult()); + + if (newAssumptions.empty()) { + auto fallbackMonRes = std::make_shared>(MonotonicityResult()); for (auto& entry : occuringStatesAtVariable) { for (auto& state : entry.second) { - extender->checkParOnStateMonRes(state, order, entry.first, monRes); - if (monRes->getMonotonicity(entry.first) == Monotonicity::Unknown) { + extender->checkParOnStateMonRes(state, current.order, entry.first, fallbackMonRes); + if (fallbackMonRes->getMonotonicity(entry.first) == Monotonicity::Unknown) { break; } } - monRes->setDoneForVar(entry.first); + fallbackMonRes->setDoneForVar(entry.first); } - monResults.insert({order, {monRes, assumptions}}); + monResults.insert({current.order, {fallbackMonRes, current.assumptions}}); STORM_LOG_INFO(" None of the assumptions were valid, we stop exploring the current order"); - } else { - STORM_LOG_INFO(" Created " << newAssumptions.size() << " assumptions, we continue extending the current order"); + continue; } + STORM_LOG_INFO(" Created " << newAssumptions.size() << " assumptions, we continue extending the current order"); - while (itr != newAssumptions.end()) { - auto assumption = *itr; - ++itr; - if (assumption.second != AssumptionStatus::INVALID) { - if (itr != newAssumptions.end()) { - // We make a copy of the order and the assumptions - auto orderCopy = order->copy(); - auto assumptionsCopy = std::vector>(assumptions); - auto monResCopy = monRes->copy(); - - if (assumption.second == AssumptionStatus::UNKNOWN) { - // only add assumption to the set of assumptions if it is unknown whether it holds or not - assumptionsCopy.push_back(std::move(assumption.first)); - } - auto criticalTuple = extender->extendOrder(orderCopy, region, monResCopy, assumption.first); - extendOrderWithAssumptions(std::get<0>(criticalTuple), std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptionsCopy, monResCopy); - } else { - // It is the last one, so we don't need to create a copy. - if (assumption.second == AssumptionStatus::UNKNOWN) { - // only add assumption to the set of assumptions if it is unknown whether it holds or not - assumptions.push_back(std::move(assumption.first)); - } - auto criticalTuple = extender->extendOrder(order, region, monRes, assumption.first); - extendOrderWithAssumptions(std::get<0>(criticalTuple), std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptions, monRes); - } + // Prepare branches in forward order, exactly mirroring the original recursion's execution + // order: candidates 0..size-2 each get an independent copy of current.order/monRes (so + // extending one cannot affect another), while the last candidate reuses + // current.order/monRes in place. That in-place mutation must happen last, after every + // other candidate has already taken its copy from the still-pristine original. + std::vector preparedBranches; + preparedBranches.reserve(newAssumptions.size()); + for (size_t i = 0; i < newAssumptions.size(); ++i) { + auto const& assumption = newAssumptions[i]; + bool const isLastCandidate = (i == newAssumptions.size() - 1); + + std::shared_ptr branchOrder = isLastCandidate ? current.order : current.order->copy(); + std::shared_ptr> branchMonRes = isLastCandidate ? current.monRes : current.monRes->copy(); + std::vector branchAssumptions = current.assumptions; + + if (assumption.second == AssumptionStatus::UNKNOWN) { + // only add assumption to the set of assumptions if it is unknown whether it holds or not + branchAssumptions.push_back(assumption.first); } + auto criticalTuple = extender->extendOrder(branchOrder, region, branchMonRes, assumption.first); + preparedBranches.push_back( + {std::get<0>(criticalTuple), std::get<1>(criticalTuple), std::get<2>(criticalTuple), std::move(branchAssumptions), branchMonRes}); + } + // Push in reverse so the first-prepared branch ends up on top of the stack and is explored + // first, matching the original left-to-right visitation order. + for (auto it = preparedBranches.rbegin(); it != preparedBranches.rend(); ++it) { + worklist.push_back(std::move(*it)); } } } diff --git a/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.h b/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.h index 07d2eadbf7..d25e2f5076 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.h +++ b/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.h @@ -1,6 +1,7 @@ #pragma once #include +#include "Assumption.h" #include "AssumptionMaker.h" #include "LocalMonotonicityResult.h" #include "MonotonicityResult.h" @@ -16,7 +17,6 @@ #include "storm/solver/Z3SmtSolver.h" #include "storm/storage/SparseMatrix.h" -#include "storm/storage/expressions/BinaryRelationExpression.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/RationalFunctionToExpression.h" @@ -57,47 +57,7 @@ class MonotonicityHelper { * @return pair of bools, >= 0 and <= 0 */ static std::pair checkDerivative(ValueType derivative, storage::ParameterRegion reg) { - bool monIncr = false; - bool monDecr = false; - - if (derivative.isZero()) { - monIncr = true; - monDecr = true; - } else if (derivative.isConstant()) { - monIncr = derivative.constantPart() >= 0; - monDecr = derivative.constantPart() <= 0; - } else { - std::shared_ptr smtSolverFactory = std::make_shared(); - std::shared_ptr manager(new expressions::ExpressionManager()); - solver::Z3SmtSolver s(*manager); - std::set variables = derivative.gatherVariables(); - - expressions::Expression exprBounds = manager->boolean(true); - for (auto variable : variables) { - auto managerVariable = manager->declareRationalVariable(variable.name()); - auto lb = utility::convertNumber(reg.getLowerBoundary(variable)); - auto ub = utility::convertNumber(reg.getUpperBoundary(variable)); - exprBounds = exprBounds && manager->rational(lb) < managerVariable && managerVariable < manager->rational(ub); - } - - auto converter = expressions::RationalFunctionToExpression(manager); - - // < 0, so not monotone increasing. If this is unsat, then it should be monotone increasing. - expressions::Expression exprToCheck = converter.toExpression(derivative) < manager->rational(0); - s.add(exprBounds); - s.add(exprToCheck); - monIncr = s.check() == solver::SmtSolver::CheckResult::Unsat; - - // > 0, so not monotone decreasing. If this is unsat it should be monotone decreasing. - exprToCheck = converter.toExpression(derivative) > manager->rational(0); - s.reset(); - s.add(exprBounds); - s.add(exprToCheck); - monDecr = s.check() == solver::SmtSolver::CheckResult::Unsat; - } - assert(!(monIncr && monDecr) || derivative.isZero()); - - return std::pair(monIncr, monDecr); + return MonotonicityChecker::checkDerivative(derivative, reg); } /*! @@ -107,9 +67,8 @@ class MonotonicityHelper { * @param dotOutfileName Name for the files of the dot outputs should they be generated * @return Map which maps each order to its Reachability Order and used assumptions. */ - std::map, - std::pair>, std::vector>>> - checkMonotonicityInBuild(std::ostream& outfile, bool usePLA = false, std::string dotOutfileName = "dotOutput"); + std::map, std::pair>, std::vector>> checkMonotonicityInBuild( + std::ostream& outfile, bool usePLA = false, std::string dotOutfileName = "dotOutput"); /*! * Builds Reachability Orders for the given model and simultaneously uses them to check for Monotonicity. @@ -125,8 +84,7 @@ class MonotonicityHelper { void checkMonotonicityOnSamples(std::shared_ptr> model, uint_fast64_t numberOfSamples); - void extendOrderWithAssumptions(std::shared_ptr order, uint_fast64_t val1, uint_fast64_t val2, - std::vector> assumptions, + void extendOrderWithAssumptions(std::shared_ptr order, uint_fast64_t val1, uint_fast64_t val2, std::vector assumptions, std::shared_ptr> monRes); std::shared_ptr model; @@ -143,11 +101,9 @@ class MonotonicityHelper { std::map> occuringStatesAtVariable; - std::map, - std::pair>, std::vector>>> - monResults; + std::map, std::pair>, std::vector>> monResults; - OrderExtender* extender; + std::unique_ptr> extender; ConstantType precision; diff --git a/src/storm-pars/modelchecker/region/monotonicity/Order.cpp b/src/storm-pars/modelchecker/region/monotonicity/Order.cpp index 81a8d084ee..e1b813e71e 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/Order.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/Order.cpp @@ -27,8 +27,9 @@ Order::Order(storm::storage::BitVector const& topStates, storm::storage::BitVect this->nodes[i] = bottom; numberOfAddedStates++; } - assert(numberOfAddedStates <= numberOfStates); - assert(doneStates.getNumberOfSetBits() == (topStates.getNumberOfSetBits() + bottomStates.getNumberOfSetBits())); + STORM_LOG_ASSERT(numberOfAddedStates <= numberOfStates, "More states were added to the order than it has room for."); + STORM_LOG_ASSERT(doneStates.getNumberOfSetBits() == (topStates.getNumberOfSetBits() + bottomStates.getNumberOfSetBits()), + "Number of done states does not match the number of given top and bottom states."); if (numberOfAddedStates == numberOfStates) { doneBuilding = doneStates.full(); } @@ -50,10 +51,10 @@ Order::Order(uint_fast64_t topState, uint_fast64_t bottomState, uint_fast64_t nu this->bottom->states.insert(bottomState); this->nodes[bottomState] = bottom; this->numberOfAddedStates = 2; - assert(numberOfAddedStates <= numberOfStates); + STORM_LOG_ASSERT(numberOfAddedStates <= numberOfStates, "More states were added to the order than it has room for."); this->statesSorted = statesSorted; - assert(doneStates.getNumberOfSetBits() == 2); + STORM_LOG_ASSERT(doneStates.getNumberOfSetBits() == 2, "Expected exactly the given top and bottom state to be done."); if (numberOfAddedStates == numberOfStates) { doneBuilding = doneStates.full(); } @@ -63,10 +64,70 @@ Order::Order() { this->invalid = false; } +Order::Order(Order const& other) + : invalid(other.invalid), + doneBuilding(other.doneBuilding), + onlyBottomTopOrder(other.onlyBottomTopOrder), + doneStates(other.doneStates), + trivialStates(other.trivialStates), + nodes(other.numberOfStates, nullptr), + statesToHandle(other.statesToHandle), + top(nullptr), + bottom(nullptr), + numberOfStates(other.numberOfStates), + numberOfAddedStates(other.numberOfAddedStates), + statesSorted(other.statesSorted) { + storm::storage::BitVector seenStates(numberOfStates, false); + for (uint_fast64_t state = 0; state < numberOfStates; ++state) { + Node* oldNode = other.nodes.at(state); + if (oldNode != nullptr && !seenStates[*(oldNode->states.begin())]) { + Node* newNode = allocateNode(); + if (oldNode == other.top) { + top = newNode; + } else if (oldNode == other.bottom) { + bottom = newNode; + } + newNode->statesAbove = oldNode->statesAbove; + for (auto const& i : oldNode->states) { + newNode->states.insert(i); + seenStates.set(i); + nodes[i] = newNode; + } + } + } +} + +Order& Order::operator=(Order other) { + swap(*this, other); + return *this; +} + +void swap(Order& first, Order& second) noexcept { + using std::swap; + swap(first.invalid, second.invalid); + swap(first.doneBuilding, second.doneBuilding); + swap(first.onlyBottomTopOrder, second.onlyBottomTopOrder); + swap(first.doneStates, second.doneStates); + swap(first.trivialStates, second.trivialStates); + swap(first.nodes, second.nodes); + swap(first.nodeStorage, second.nodeStorage); + swap(first.statesToHandle, second.statesToHandle); + swap(first.top, second.top); + swap(first.bottom, second.bottom); + swap(first.numberOfStates, second.numberOfStates); + swap(first.numberOfAddedStates, second.numberOfAddedStates); + swap(first.statesSorted, second.statesSorted); +} + +Order::Node* Order::allocateNode() { + nodeStorage.push_back(std::make_unique()); + return nodeStorage.back().get(); +} + /*** Modifying the order ***/ void Order::add(uint_fast64_t state) { - assert(nodes[state] == nullptr); + STORM_LOG_ASSERT(nodes[state] == nullptr, "State " << state << " is already in the order."); addBetween(state, top, bottom); addStateToHandle(state); } @@ -74,8 +135,8 @@ void Order::add(uint_fast64_t state) { void Order::addAbove(uint_fast64_t state, Node* node) { STORM_LOG_INFO("Add " << state << " above " << *node->states.begin() << '\n'); - assert(nodes[state] == nullptr); - Node* newNode = new Node(); + STORM_LOG_ASSERT(nodes[state] == nullptr, "State " << state << " is already in the order."); + Node* newNode = allocateNode(); nodes[state] = newNode; newNode->states.insert(state); @@ -94,8 +155,8 @@ void Order::addAbove(uint_fast64_t state, Node* node) { void Order::addBelow(uint_fast64_t state, Node* node) { STORM_LOG_INFO("Add " << state << " below " << *node->states.begin() << '\n'); - assert(nodes[state] == nullptr); - Node* newNode = new Node(); + STORM_LOG_ASSERT(nodes[state] == nullptr, "State " << state << " is already in the order."); + Node* newNode = allocateNode(); nodes[state] = newNode; newNode->states.insert(state); newNode->statesAbove = storm::storage::BitVector((node->statesAbove)); @@ -108,17 +169,17 @@ void Order::addBelow(uint_fast64_t state, Node* node) { if (numberOfAddedStates == numberOfStates) { doneBuilding = doneStates.full(); } - assert(numberOfAddedStates <= numberOfStates); + STORM_LOG_ASSERT(numberOfAddedStates <= numberOfStates, "More states were added to the order than it has room for."); } void Order::addBetween(uint_fast64_t state, Node* above, Node* below) { STORM_LOG_INFO("Add " << state << " between (above) " << *above->states.begin() << " and " << *below->states.begin() << '\n'); - assert(compare(above, below) == ABOVE); - assert(above != nullptr && below != nullptr); + STORM_LOG_ASSERT(compare(above, below) == ABOVE, "Expected the first node/state to be above the second."); + STORM_LOG_ASSERT(above != nullptr && below != nullptr, "Both nodes must exist."); if (nodes[state] == nullptr) { // State is not in the order yet - Node* newNode = new Node(); + Node* newNode = allocateNode(); nodes[state] = newNode; newNode->states.insert(state); @@ -132,7 +193,7 @@ void Order::addBetween(uint_fast64_t state, Node* above, Node* below) { if (numberOfAddedStates == numberOfStates) { doneBuilding = doneStates.full(); } - assert(numberOfAddedStates <= numberOfStates); + STORM_LOG_ASSERT(numberOfAddedStates <= numberOfStates, "More states were added to the order than it has room for."); } else { // State is in the order already, so we add the new relations addRelationNodes(above, nodes[state]); @@ -141,20 +202,21 @@ void Order::addBetween(uint_fast64_t state, Node* above, Node* below) { } void Order::addBetween(uint_fast64_t state, uint_fast64_t above, uint_fast64_t below) { - assert(compare(above, below) == ABOVE); - assert(getNode(below)->states.find(below) != getNode(below)->states.end()); - assert(getNode(above)->states.find(above) != getNode(above)->states.end()); + // No compare(above, below) == ABOVE check here: addBetween(state, Node*, Node*) below checks + // that itself (and is also called directly by other sites, so it can't drop that check). + STORM_LOG_ASSERT(getNode(below)->states.find(below) != getNode(below)->states.end(), "State " << below << " is not in its own node."); + STORM_LOG_ASSERT(getNode(above)->states.find(above) != getNode(above)->states.end(), "State " << above << " is not in its own node."); addBetween(state, getNode(above), getNode(below)); } void Order::addRelation(uint_fast64_t above, uint_fast64_t below, bool allowMerge) { - assert(getNode(above) != nullptr && getNode(below) != nullptr); + STORM_LOG_ASSERT(getNode(above) != nullptr && getNode(below) != nullptr, "Both states must already be in the order."); addRelationNodes(getNode(above), getNode(below), allowMerge); } void Order::addRelationNodes(Order::Node* above, Order::Node* below, bool allowMerge) { - assert(allowMerge || compare(above, below) != BELOW); + STORM_LOG_ASSERT(allowMerge || compare(above, below) != BELOW, "The first node/state is already known to be below the second."); STORM_LOG_INFO("Add relation between (above) " << *above->states.begin() << " and " << *below->states.begin() << '\n'); @@ -168,7 +230,7 @@ void Order::addRelationNodes(Order::Node* above, Order::Node* below, bool allowM for (auto const& state : above->states) { below->statesAbove.set(state); } - assert(compare(above, below) == ABOVE); + STORM_LOG_ASSERT(compare(above, below) == ABOVE, "Expected the first node/state to be above the second."); } void Order::addToNode(uint_fast64_t state, Node* node) { @@ -182,7 +244,7 @@ void Order::addToNode(uint_fast64_t state, Node* node) { if (numberOfAddedStates == numberOfStates) { doneBuilding = doneStates.full(); } - assert(numberOfAddedStates <= numberOfStates); + STORM_LOG_ASSERT(numberOfAddedStates <= numberOfStates, "More states were added to the order than it has room for."); } else { // State is in the order already, so we merge the nodes @@ -216,7 +278,13 @@ bool Order::mergeNodes(storm::analysis::Order::Node* node1, storm::analysis::Ord } } for (uint_fast64_t i = 0; i < numberOfStates; ++i) { + if (nodes[i] == nullptr) { + continue; + } for (uint_fast64_t j = i + 1; j < numberOfStates; ++j) { + if (nodes[j] == nullptr) { + continue; + } auto comp1 = compare(i, j); auto comp2 = compare(j, i); if (!((comp1 == BELOW && comp2 == ABOVE) || (comp1 == ABOVE && comp2 == BELOW) || (comp1 == UNKNOWN && comp2 == UNKNOWN) || @@ -272,7 +340,10 @@ Order::NodeComparison Order::compare(Node* node1, Node* node2, NodeComparison hy return comp; } if ((hypothesis == UNKNOWN || hypothesis == ABOVE) && above(node1, node2)) { - assert(!above(node2, node1)); + // Deliberately no assertion here that above(node2, node1) doesn't also hold: mergeNodes's + // own O(n^2) revalidation loop calls compare(i, j) and compare(j, i) on every pair + // specifically to detect and gracefully reject merges that would produce this kind of + // mutual-above inconsistency; that detection must be allowed to complete undisturbed. return ABOVE; } @@ -296,7 +367,8 @@ Order::Node* Order::getBottom() const { } bool Order::getDoneBuilding() const { - assert(!doneStates.full() || numberOfAddedStates == numberOfStates); + STORM_LOG_ASSERT(!doneStates.full() || numberOfAddedStates == numberOfStates, + "All states are marked done, but not all states have been added to the order."); return doneStates.full(); } @@ -344,7 +416,7 @@ bool Order::isOnlyBottomTopOrder() const { } std::vector Order::sortStates(std::vector* states) { - assert(states != nullptr); + STORM_LOG_ASSERT(states != nullptr, "States to sort must be given."); uint_fast64_t numberOfStatesToSort = states->size(); std::vector result; // Go over all states @@ -377,7 +449,7 @@ std::vector Order::sortStates(std::vector* states) while (result.size() < numberOfStatesToSort) { result.push_back(numberOfStates); } - assert(result.size() == numberOfStatesToSort); + STORM_LOG_ASSERT(result.size() == numberOfStatesToSort, "Not all states could be sorted (or padded with the sentinel value)."); return result; } @@ -425,17 +497,18 @@ std::pair, std::vector> O } } if (!unknown && oneUnknown) { - assert(statesSorted.size() == states.size()); + STORM_LOG_ASSERT(statesSorted.size() == states.size(), "Expected all but the single unresolved state to have been sorted."); s2 = numberOfStates; } - assert(s1 == numberOfStates || (s1 != numberOfStates && s2 == numberOfStates && statesSorted.size() == states.size()) || - (s1 != numberOfStates && s2 != numberOfStates && statesSorted.size() < states.size())); + STORM_LOG_ASSERT(s1 == numberOfStates || (s1 != numberOfStates && s2 == numberOfStates && statesSorted.size() == states.size()) || + (s1 != numberOfStates && s2 != numberOfStates && statesSorted.size() < states.size()), + "Inconsistent result: (s1, s2) and the number of sorted states must agree on how far sorting got."); return {{s1, s2}, statesSorted}; } std::pair, std::vector> Order::sortStatesUnorderedPair(const std::vector* states) { - assert(states != nullptr); + STORM_LOG_ASSERT(states != nullptr, "States to sort must be given."); [[maybe_unused]] uint_fast64_t numberOfStatesToSort = states->size(); std::vector result; // Go over all states @@ -465,7 +538,7 @@ std::pair, std::vector> O } } - assert(result.size() == numberOfStatesToSort); + STORM_LOG_ASSERT(result.size() == numberOfStatesToSort, "Not all states could be sorted."); return {{numberOfStates, numberOfStates}, std::move(result)}; } @@ -502,54 +575,15 @@ std::vector Order::sortStates(storm::storage::BitVector* states) while (result.size() < numberOfStatesToSort) { result.push_back(numberOfStates); } - assert(result.size() == numberOfStatesToSort); + STORM_LOG_ASSERT(result.size() == numberOfStatesToSort, "Not all states could be sorted (or padded with the sentinel value)."); return result; } /*** Checking on helpfunctionality for building of order ***/ std::shared_ptr Order::copy() const { - assert(!isInvalid()); - std::shared_ptr copiedOrder = std::make_shared(); - copiedOrder->nodes = std::vector(numberOfStates, nullptr); - copiedOrder->onlyBottomTopOrder = this->isOnlyBottomTopOrder(); - copiedOrder->numberOfStates = this->getNumberOfStates(); - copiedOrder->statesSorted = std::vector(this->statesSorted); - copiedOrder->statesToHandle = std::vector(this->statesToHandle); - copiedOrder->trivialStates = storm::storage::BitVector(trivialStates); - copiedOrder->doneStates = storm::storage::BitVector(doneStates); - copiedOrder->numberOfAddedStates = this->numberOfAddedStates; - copiedOrder->doneBuilding = this->doneBuilding; - - auto seenStates = storm::storage::BitVector(numberOfStates, false); - // copy nodes - for (uint_fast64_t state = 0; state < numberOfStates; ++state) { - Node* oldNode = nodes.at(state); - if (oldNode != nullptr) { - if (!seenStates[*(oldNode->states.begin())]) { - Node* newNode = new Node(); - if (oldNode == this->getTop()) { - copiedOrder->top = newNode; - } else if (oldNode == this->getBottom()) { - copiedOrder->bottom = newNode; - } - newNode->statesAbove = storm::storage::BitVector(oldNode->statesAbove); - for (size_t i = 0; i < oldNode->statesAbove.size(); ++i) { - assert(newNode->statesAbove[i] == oldNode->statesAbove[i]); - } - for (auto const& i : oldNode->states) { - assert(!seenStates[i]); - newNode->states.insert(i); - seenStates.set(i); - copiedOrder->nodes[i] = newNode; - } - } - } else { - assert(copiedOrder->nodes[state] == nullptr); - } - } - - return copiedOrder; + STORM_LOG_ASSERT(!isInvalid(), "Cannot copy an invalid order."); + return std::make_shared(*this); } /*** Setters ***/ @@ -655,7 +689,7 @@ void Order::init(uint_fast64_t numberOfStates, storage::Decompositioninvalid = false; this->nodes = std::vector(numberOfStates, nullptr); this->doneStates = storm::storage::BitVector(numberOfStates, false); - assert(doneStates.getNumberOfSetBits() == 0); + STORM_LOG_ASSERT(doneStates.getNumberOfSetBits() == 0, "A freshly initialized order must not have any done states yet."); if (decomposition.size() == 0) { this->trivialStates = storm::storage::BitVector(numberOfStates, true); } else { @@ -666,8 +700,8 @@ void Order::init(uint_fast64_t numberOfStates, storage::Decompositiontop = new Node(); - this->bottom = new Node(); + this->top = allocateNode(); + this->bottom = allocateNode(); this->top->statesAbove = storm::storage::BitVector(numberOfStates, false); this->bottom->statesAbove = storm::storage::BitVector(numberOfStates, false); this->doneBuilding = doneBuilding; @@ -761,7 +795,7 @@ std::pair Order::getNextStateNumber() { } std::pair Order::getStateToHandle() { - assert(existsStateToHandle()); + STORM_LOG_ASSERT(existsStateToHandle(), "No state to handle exists."); auto state = statesToHandle.back(); statesToHandle.pop_back(); return {state, false}; diff --git a/src/storm-pars/modelchecker/region/monotonicity/Order.h b/src/storm-pars/modelchecker/region/monotonicity/Order.h index 219b14fd43..5a8d5f151c 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/Order.h +++ b/src/storm-pars/modelchecker/region/monotonicity/Order.h @@ -57,6 +57,18 @@ class Order { */ Order(); + /*! + * Constructs a deep copy of the given Order. Every Node is reallocated; no state is shared + * with other. + */ + Order(Order const& other); + + Order(Order&&) noexcept = default; + + Order& operator=(Order other); + + friend void swap(Order& first, Order& second) noexcept; + /*! * Adds state between the top and bottom node of the order. * @@ -318,6 +330,12 @@ class Order { void init(uint_fast64_t numberOfStates, storage::Decomposition, bool doneBuilding = false); + /*! + * Allocates a new Node owned by this Order (in nodeStorage) and returns an observer pointer to + * it. + */ + Node* allocateNode(); + std::string nodeName(Node n) const; std::string nodeLabel(Node n) const; @@ -333,6 +351,10 @@ class Order { std::vector nodes; + // Sole owner of every Node allocated for this Order; `nodes`, `top` and `bottom` are + // non-owning observer pointers into this storage. + std::vector> nodeStorage; + std::vector statesToHandle; Node* top; diff --git a/src/storm-pars/modelchecker/region/monotonicity/OrderBasedMonotonicityBackend.cpp b/src/storm-pars/modelchecker/region/monotonicity/OrderBasedMonotonicityBackend.cpp index 568bb2f4e9..5c656c3df3 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/OrderBasedMonotonicityBackend.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/OrderBasedMonotonicityBackend.cpp @@ -102,7 +102,7 @@ void OrderBasedMonotonicityBackend::initializeMono if (useBounds) { STORM_LOG_ASSERT(plaBoundFunction, "PLA bound function not registered."); orderExtender->setMaxValuesInit(plaBoundFunction(env, region, storm::solver::OptimizationDirection::Maximize)); - orderExtender->setMaxValuesInit(plaBoundFunction(env, region, storm::solver::OptimizationDirection::Minimize)); + orderExtender->setMinValuesInit(plaBoundFunction(env, region, storm::solver::OptimizationDirection::Minimize)); } typename MonotonicityAnnotation::OrderBasedMonotonicityAnnotation annotation; annotation.stateOrder = detail::extendOrder(*this->orderExtender, nullptr, region.region); @@ -128,11 +128,9 @@ void OrderBasedMonotonicityBackend::updateMonotoni // Copy order only if it will potentially change and if it is shared with another region bool const changeOrder = !annotation->stateOrder->getDoneBuilding() && orderExtender->isHope(annotation->stateOrder); if (changeOrder && annotation->stateOrder.use_count() > 1) { - // TODO: orderExtender currently uses shared_ptr which likely interferes with the use_count() > 1 check above // TODO: Make sure that only annotated regions own the order auto newOrder = annotation->stateOrder->copy(); - orderExtender->setUnknownStates(annotation->stateOrder, newOrder); - orderExtender->copyMinMax(annotation->stateOrder, newOrder); + orderExtender->copyContext(annotation->stateOrder, newOrder); annotation->stateOrder = newOrder; } if (changeOrder) { diff --git a/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp b/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp index a57d2d9ead..b633f2f446 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp @@ -26,7 +26,7 @@ OrderExtender::OrderExtender(std::shared_ptrmatrix = model->getTransitionMatrix(); this->numberOfStates = this->model->getNumberOfStates(); this->formula = formula; - this->assumptionMaker = new analysis::AssumptionMaker(matrix); + this->assumptionMaker = std::make_unique>(matrix); } template @@ -36,13 +36,22 @@ OrderExtender::OrderExtender(storm::storage::BitVector this->matrix = matrix; this->model = nullptr; this->monotonicityChecker = MonotonicityChecker(matrix); + this->numberOfStates = matrix.getColumnCount(); + + this->bottomTopOrder = computeInitialOrder(topStates, bottomStates, matrix, /*addStatesWithDirectBoundaryTransition=*/true); + this->assumptionMaker = std::make_unique>(matrix); +} + +template +std::shared_ptr OrderExtender::computeInitialOrder(storm::storage::BitVector const& topStates, + storm::storage::BitVector const& bottomStates, + storm::storage::SparseMatrix const& matrix, + bool addStatesWithDirectBoundaryTransition) { storm::storage::StronglyConnectedComponentDecompositionOptions options; options.forceTopologicalSort(); - this->numberOfStates = matrix.getColumnCount(); std::vector firstStates; - storm::storage::BitVector subStates(topStates.size(), true); for (auto state : topStates) { firstStates.push_back(state); @@ -59,7 +68,7 @@ OrderExtender::OrderExtender(storm::storage::BitVector } auto statesSorted = storm::utility::graph::getTopologicalSort(matrix.transpose(), firstStates); - this->bottomTopOrder = std::make_shared(topStates, bottomStates, numberOfStates, std::move(decomposition), std::move(statesSorted)); + auto order = std::make_shared(topStates, bottomStates, numberOfStates, std::move(decomposition), std::move(statesSorted)); // Build stateMap for (uint_fast64_t state = 0; state < numberOfStates; ++state) { @@ -70,8 +79,8 @@ OrderExtender::OrderExtender(storm::storage::BitVector for (auto& entry : matrix.getRow(state)) { // ignore self-loops when there are more transitions if (state != entry.getColumn() || row.getNumberOfEntries() == 1) { - if (!subStates[entry.getColumn()] && !bottomTopOrder->contains(state)) { - bottomTopOrder->add(state); + if (addStatesWithDirectBoundaryTransition && !subStates[entry.getColumn()] && !order->contains(state)) { + order->add(state); } stateMap[state].push_back(entry.getColumn()); } @@ -87,19 +96,19 @@ OrderExtender::OrderExtender(storm::storage::BitVector occuringVariablesAtState.push_back(std::move(occurringVariables)); } - this->assumptionMaker = new analysis::AssumptionMaker(matrix); + return order; } template std::shared_ptr OrderExtender::getBottomTopOrder() { if (bottomTopOrder == nullptr) { - assert(model != nullptr); + STORM_LOG_ASSERT(model != nullptr, "Cannot lazily build the bottom-top order without a model."); STORM_LOG_THROW(matrix.getRowCount() == matrix.getColumnCount(), exceptions::NotSupportedException, "Creating order not supported for non-square matrix"); modelchecker::SparsePropositionalModelChecker> propositionalChecker(*model); storage::BitVector phiStates; storage::BitVector psiStates; - assert(formula->isProbabilityOperatorFormula()); + STORM_LOG_ASSERT(formula->isProbabilityOperatorFormula(), "Expected a probability operator formula."); if (formula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { phiStates = propositionalChecker.check(formula->asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula()) ->template asExplicitQualitativeCheckResult() @@ -108,7 +117,7 @@ std::shared_ptr OrderExtender::getBottomTopOrder ->template asExplicitQualitativeCheckResult() .getTruthValuesVector(); } else { - assert(formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()); + STORM_LOG_ASSERT(formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula(), "Expected an eventually formula."); phiStates = storage::BitVector(numberOfStates, true); psiStates = propositionalChecker.check(formula->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()) ->template asExplicitQualitativeCheckResult() @@ -122,89 +131,57 @@ std::shared_ptr OrderExtender::getBottomTopOrder STORM_LOG_THROW(topStates.begin() != topStates.end(), exceptions::NotSupportedException, "Formula yields to no 1 states"); STORM_LOG_THROW(bottomStates.begin() != bottomStates.end(), exceptions::NotSupportedException, "Formula yields to no zero states"); - auto& matrix = this->model->getTransitionMatrix(); - std::vector firstStates; - - storm::storage::BitVector subStates(topStates.size(), true); - for (auto state : topStates) { - firstStates.push_back(state); - subStates.set(state, false); - } - for (auto state : bottomStates) { - firstStates.push_back(state); - subStates.set(state, false); - } - cyclic = storm::utility::graph::hasCycle(matrix, subStates); - storm::storage::StronglyConnectedComponentDecomposition decomposition; - if (cyclic) { - storm::storage::StronglyConnectedComponentDecompositionOptions options; - options.forceTopologicalSort(); - decomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, options); - } - auto statesSorted = storm::utility::graph::getTopologicalSort(matrix.transpose(), firstStates); - bottomTopOrder = std::make_shared(topStates, bottomStates, numberOfStates, std::move(decomposition), std::move(statesSorted)); - - // Build stateMap - for (uint_fast64_t state = 0; state < numberOfStates; ++state) { - auto const& row = matrix.getRow(state); - stateMap[state] = std::vector(); - std::set occurringVariables; - - for (auto& entry : matrix.getRow(state)) { - // ignore self-loops when there are more transitions - if (state != entry.getColumn() || row.getNumberOfEntries() == 1) { - // if (!subStates[entry.getColumn()] && !bottomTopOrder->contains(state)) { - // bottomTopOrder->add(state); - // } - stateMap[state].push_back(entry.getColumn()); - } - storm::utility::parametric::gatherOccurringVariables(entry.getValue(), occurringVariables); - } - if (occurringVariables.empty()) { - nonParametricStates.insert(state); - } - for (auto& var : occurringVariables) { - occuringStatesAtVariable[var].push_back(state); - } - occuringVariablesAtState.push_back(std::move(occurringVariables)); - } + // Unlike the BitVector-matrix constructor, this path does not pre-add states with a direct + // transition to a top/bottom state to the order ahead of the main construction loop. + bottomTopOrder = computeInitialOrder(topStates, bottomStates, this->model->getTransitionMatrix(), /*addStatesWithDirectBoundaryTransition=*/false); } if (minValuesInit && maxValuesInit) { - continueExtending[bottomTopOrder] = true; - usePLA[bottomTopOrder] = true; - minValues[bottomTopOrder] = std::move(minValuesInit.get()); - maxValues[bottomTopOrder] = std::move(maxValuesInit.get()); + auto& ctx = context(bottomTopOrder); + ctx.continueExtending = true; + ctx.usePLA = true; + ctx.minValues = std::move(minValuesInit.get()); + ctx.maxValues = std::move(maxValuesInit.get()); } else { - usePLA[bottomTopOrder] = false; + context(bottomTopOrder).usePLA = false; } return bottomTopOrder; } +template +typename OrderExtender::Context& OrderExtender::context(std::shared_ptr const& order) { + auto result = contexts.try_emplace(order); + if (result.second) { + result.first->second.unknownStates = {numberOfStates, numberOfStates}; + } + return result.first->second; +} + +template +typename OrderExtender::Context const& OrderExtender::contextAt(std::shared_ptr const& order) const { + auto it = contexts.find(order); + STORM_LOG_ASSERT(it != contexts.end(), "No context set for this order."); + return it->second; +} + template std::tuple, uint_fast64_t, uint_fast64_t> OrderExtender::toOrder( storage::ParameterRegion region, std::shared_ptr> monRes) { - return this->extendOrder(nullptr, region, monRes, nullptr); + return this->extendOrder(nullptr, region, monRes, std::nullopt); } template -void OrderExtender::handleAssumption(std::shared_ptr order, - std::shared_ptr assumption) const { - assert(assumption != nullptr); - assert(assumption->getFirstOperand()->isVariable() && assumption->getSecondOperand()->isVariable()); - - expressions::Variable var1 = assumption->getFirstOperand()->asVariableExpression().getVariable(); - expressions::Variable var2 = assumption->getSecondOperand()->asVariableExpression().getVariable(); - auto const& val1 = std::stoul(var1.getName(), nullptr, 0); - auto const& val2 = std::stoul(var2.getName(), nullptr, 0); +void OrderExtender::handleAssumption(std::shared_ptr order, Assumption const& assumption) const { + uint_fast64_t val1 = assumption.state1; + uint_fast64_t val2 = assumption.state2; - assert(order->compare(val1, val2) == Order::UNKNOWN); + STORM_LOG_ASSERT(order->compare(val1, val2) == Order::UNKNOWN, "The assumption's states are already ordered; handling it again is redundant."); Order::Node* n1 = order->getNode(val1); Order::Node* n2 = order->getNode(val2); - if (assumption->getRelationType() == expressions::RelationType::Equal) { + if (assumption.relation == expressions::RelationType::Equal) { if (n1 != nullptr && n2 != nullptr) { order->mergeNodes(n1, n2); } else if (n1 != nullptr) { @@ -216,7 +193,7 @@ void OrderExtender::handleAssumption(std::shared_ptraddToNode(val2, order->getNode(val1)); } } else { - assert(assumption->getRelationType() == expressions::RelationType::Greater); + STORM_LOG_ASSERT(assumption.relation == expressions::RelationType::Greater, "Only Equal and Greater assumptions are supported."); if (n1 != nullptr && n2 != nullptr) { order->addRelationNodes(n1, n2); } else if (n1 != nullptr) { @@ -233,13 +210,14 @@ void OrderExtender::handleAssumption(std::shared_ptr std::tuple, uint_fast64_t, uint_fast64_t> OrderExtender::extendOrder( std::shared_ptr order, storm::storage::ParameterRegion region, std::shared_ptr> monRes, - std::shared_ptr assumption) { + std::optional assumption) { this->region = region; if (order == nullptr) { order = getBottomTopOrder(); - if (usePLA[order]) { - auto& min = minValues[order]; - auto& max = maxValues[order]; + auto& initialContext = context(order); + if (initialContext.usePLA) { + auto& min = initialContext.minValues; + auto& max = initialContext.maxValues; // Try to make the order as complete as possible based on pla results auto& statesSorted = order->getStatesSorted(); auto itr = statesSorted.begin(); @@ -275,9 +253,11 @@ std::tuple, uint_fast64_t, uint_fast64_t> OrderExtenderaddToNode(state1, order->getNode(state2)); } else if (!order->contains(state2)) { order->addToNode(state2, order->getNode(state1)); - } else { - order->merge(state1, state2); - assert(!order->isInvalid()); + } else if (!order->merge(state1, state2)) { + // The PLA-bound-based conclusion that state1 and state2 are equal + // contradicts what the order already knows about them. Bail out here + // rather than continuing to build on top of an inconsistent order. + return std::make_tuple(order, numberOfStates, numberOfStates); } } else { all = false; @@ -290,54 +270,68 @@ std::tuple, uint_fast64_t, uint_fast64_t> OrderExtender std::tuple, uint_fast64_t, uint_fast64_t> OrderExtender::extendOrder( - std::shared_ptr order, std::shared_ptr> monRes, std::shared_ptr assumption) { - if (assumption != nullptr) { + std::shared_ptr order, std::shared_ptr> monRes, std::optional assumption) { + if (assumption.has_value()) { STORM_LOG_INFO("Handling assumption " << *assumption << '\n'); - handleAssumption(order, assumption); + handleAssumption(order, *assumption); + if (order->isInvalid()) { + // The assumption led to a mathematically inconsistent order (a merge of two states that + // should stay distinct). Bail out here rather than continuing to build on top of it. + return std::make_tuple(order, numberOfStates, numberOfStates); + } } auto currentStateMode = getNextState(order, numberOfStates, false); while (currentStateMode.first != numberOfStates) { - assert(currentStateMode.first < numberOfStates); + STORM_LOG_ASSERT(currentStateMode.first < numberOfStates, "Expected a valid state, not the sentinel value."); auto& currentState = currentStateMode.first; auto& successors = stateMap[currentState]; std::pair result = {numberOfStates, numberOfStates}; if (successors.size() == 1) { - assert(order->contains(successors[0])); + STORM_LOG_ASSERT(order->contains(successors[0]), "The single successor of a state must already be in the order."); handleOneSuccessor(order, currentState, successors[0]); } else if (!successors.empty()) { if (order->isOnlyBottomTopOrder()) { order->add(currentState); if (!order->isTrivial(currentState)) { // This state is part of an scc, therefore, we could do forward reasoning here - result = extendByForwardReasoning(order, currentState, successors, assumption != nullptr); + result = extendByForwardReasoning(order, currentState, successors, assumption.has_value()); } else { result = {numberOfStates, numberOfStates}; } } else { - result = extendNormal(order, currentState, successors, assumption != nullptr); + result = extendNormal(order, currentState, successors, assumption.has_value()); } } + if (order->isInvalid()) { + // A merge performed while extending this state (directly, or via forward/backward + // reasoning) produced a mathematically inconsistent order. Bail out here rather than + // continuing to build on top of it. + return std::make_tuple(order, numberOfStates, numberOfStates); + } + if (result.first == numberOfStates) { // We did extend the order - assert(result.second == numberOfStates); - assert(order->sortStates(&successors).size() == successors.size()); - assert(order->contains(currentState) && order->getNode(currentState) != nullptr); + STORM_LOG_ASSERT(result.second == numberOfStates, "Expected both entries of result to be the sentinel value."); + STORM_LOG_ASSERT(order->sortStates(&successors).size() == successors.size(), "Expected all successors to be sortable at this point."); + STORM_LOG_ASSERT(order->contains(currentState) && order->getNode(currentState) != nullptr, + "The current state should have been placed in the order."); if (monRes != nullptr) { for (auto& param : occuringVariablesAtState[currentState]) { @@ -347,12 +341,15 @@ std::tuple, uint_fast64_t, uint_fast64_t> OrderExtendercompare(result.first, result.second) == Order::UNKNOWN); - assert(order->compare(result.second, result.first) == Order::UNKNOWN); + STORM_LOG_ASSERT(result.first < numberOfStates, "Expected a valid state, not the sentinel value."); + STORM_LOG_ASSERT(result.second < numberOfStates, "Expected a valid state, not the sentinel value."); + STORM_LOG_ASSERT(order->compare(result.first, result.second) == Order::UNKNOWN, "Expected the unresolved pair to indeed be unordered."); + STORM_LOG_ASSERT(order->compare(result.second, result.first) == Order::UNKNOWN, "Expected the unresolved pair to indeed be unordered."); // Try to add states based on min/max and assumptions, only if we are not in statesToHandle mode if (currentStateMode.second && extendByAssumption(order, result.first, result.second)) { + if (order->isInvalid()) { + return std::make_tuple(order, numberOfStates, numberOfStates); + } continue; } // We couldn't extend the order @@ -372,15 +369,18 @@ std::tuple, uint_fast64_t, uint_fast64_t> OrderExtenderaddStateSorted(currentState); - continueExtending[order] = false; + context(order).continueExtending = false; return {order, result.first, result.second}; } } } - assert(order->sortStates(&successors).size() == successors.size()); + // No postcondition check here: every path through the else-branch above either `continue`s + // or `return`s, so this point is only ever reached via the success branch, which already + // checked (at line ~332) that successors are sortable, with nothing since then that could + // have changed that. } - assert(order->getDoneBuilding()); + STORM_LOG_ASSERT(order->getDoneBuilding(), "Expected the order to be fully built at this point."); if (monRes != nullptr) { // monotonicity result for the in-build checking of monotonicity monRes->setDone(); @@ -396,7 +396,8 @@ std::pair OrderExtender:: // Try to extend the order for this scc return extendByForwardReasoning(order, currentState, successors, allowMerge); } else { - assert(order->isTrivial(currentState) || !order->contains(currentState)); + STORM_LOG_ASSERT(order->isTrivial(currentState) || !order->contains(currentState), + "A non-trivial (SCC) state that is already in the order should use forward reasoning, not backward reasoning."); // Do backward reasoning, all successor states must be in the order return extendByBackwardReasoning(order, currentState, successors, allowMerge); } @@ -404,7 +405,7 @@ std::pair OrderExtender:: template void OrderExtender::handleOneSuccessor(std::shared_ptr order, uint_fast64_t currentState, uint_fast64_t successor) { - assert(order->contains(successor)); + STORM_LOG_ASSERT(order->contains(successor), "The successor must already be in the order."); if (currentState != successor) { if (order->contains(currentState)) { order->merge(currentState, successor); @@ -419,13 +420,14 @@ std::pair OrderExtender:: uint_fast64_t currentState, std::vector const& successors, bool allowMerge) { - assert(!order->isOnlyBottomTopOrder()); - assert(successors.size() > 1); + STORM_LOG_ASSERT(!order->isOnlyBottomTopOrder(), "Backward reasoning requires the order to have grown beyond just top and bottom."); + STORM_LOG_ASSERT(successors.size() > 1, "Backward reasoning is only needed for states with more than one successor."); - bool pla = (usePLA.find(order) != usePLA.end() && usePLA.at(order)); + auto& ctx = context(order); + bool pla = ctx.usePLA; std::vector sortedSuccs; - if (pla && (continueExtending.find(order) == continueExtending.end() || continueExtending.at(order))) { + if (pla && ctx.continueExtending) { for (auto& state1 : successors) { if (sortedSuccs.size() == 0) { sortedSuccs.push_back(state1); @@ -447,7 +449,7 @@ std::pair OrderExtender:: added = true; break; } else if (compareRes == Order::NodeComparison::UNKNOWN) { - continueExtending[order] = false; + ctx.continueExtending = false; return {state1, state2}; } } @@ -473,13 +475,13 @@ std::pair OrderExtender:: } } else { if (!order->contains(sortedSuccs[0])) { - assert(order->isBottomState(sortedSuccs[sortedSuccs.size() - 1])); - assert(sortedSuccs.size() == 2); + STORM_LOG_ASSERT(order->isBottomState(sortedSuccs[sortedSuccs.size() - 1]), "Expected the other successor to be a bottom state."); + STORM_LOG_ASSERT(sortedSuccs.size() == 2, "Expected exactly two successors in this case."); order->addAbove(sortedSuccs[0], order->getBottom()); } if (!order->contains(sortedSuccs[sortedSuccs.size() - 1])) { - assert(order->isTopState(sortedSuccs[0])); - assert(sortedSuccs.size() == 2); + STORM_LOG_ASSERT(order->isTopState(sortedSuccs[0]), "Expected the other successor to be a top state."); + STORM_LOG_ASSERT(sortedSuccs.size() == 2, "Expected exactly two successors in this case."); order->addBelow(sortedSuccs[sortedSuccs.size() - 1], order->getTop()); } // sortedSuccs[0] is highest @@ -490,8 +492,9 @@ std::pair OrderExtender:: order->addRelation(currentState, sortedSuccs[sortedSuccs.size() - 1], allowMerge); } } - assert(order->contains(currentState) && order->compare(order->getNode(currentState), order->getBottom()) == Order::ABOVE && - order->compare(order->getNode(currentState), order->getTop()) == Order::BELOW); + STORM_LOG_ASSERT(order->contains(currentState) && order->compare(order->getNode(currentState), order->getBottom()) == Order::ABOVE && + order->compare(order->getNode(currentState), order->getTop()) == Order::BELOW, + "The current state should have ended up strictly between top and bottom in the order."); return {numberOfStates, numberOfStates}; } @@ -500,13 +503,13 @@ std::pair OrderExtender:: uint_fast64_t currentState, std::vector const& successors, bool allowMerge) { - assert(successors.size() > 1); - assert(order->contains(currentState)); - assert(cyclic); + STORM_LOG_ASSERT(successors.size() > 1, "Forward reasoning is only needed for states with more than one successor."); + STORM_LOG_ASSERT(order->contains(currentState), "The current state must already be in the order before doing forward reasoning on it."); + STORM_LOG_ASSERT(cyclic, "Forward reasoning is only applicable to cyclic pMCs."); std::vector statesSorted; statesSorted.push_back(currentState); - bool pla = (usePLA.find(order) != usePLA.end() && usePLA.at(order)); + bool pla = context(order).usePLA; // Go over all states bool oneUnknown = false; bool unknown = false; @@ -554,12 +557,12 @@ std::pair OrderExtender:: } } if (!unknown && oneUnknown) { - assert(statesSorted.size() == successors.size()); + STORM_LOG_ASSERT(statesSorted.size() == successors.size(), "Expected all but the single unresolved successor to have been sorted."); s2 = numberOfStates; } if (s1 == numberOfStates) { - assert(statesSorted.size() == successors.size() + 1); + STORM_LOG_ASSERT(statesSorted.size() == successors.size() + 1, "Expected all successors (plus the current state) to have been sorted."); // all could be sorted, no need to do anything } else if (s2 == numberOfStates) { if (!order->contains(s1)) { @@ -568,19 +571,27 @@ std::pair OrderExtender:: if (statesSorted[0] == currentState) { order->addRelation(s1, statesSorted[0], allowMerge); - assert((order->compare(s1, statesSorted[0]) == Order::ABOVE) || - (allowMerge && (order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::SAME))); + // Fallback checks statesSorted[0]: that's the element the addRelation call just above + // related (and, if allowMerge applies, may have merged) s1 with. + STORM_LOG_ASSERT((order->compare(s1, statesSorted[0]) == Order::ABOVE) || + (allowMerge && (order->compare(s1, statesSorted[0]) == Order::SAME)), + "Expected s1 to end up above (or, if merged, equal to) statesSorted[0]."); order->addRelation(s1, statesSorted[statesSorted.size() - 1], allowMerge); - assert((order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::ABOVE) || - (allowMerge && (order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::SAME))); + STORM_LOG_ASSERT((order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::ABOVE) || + (allowMerge && (order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::SAME)), + "Expected s1 to end up above (or, if merged, equal to) the lowest sorted successor."); order->addStateToHandle(s1); } else if (statesSorted[statesSorted.size() - 1] == currentState) { order->addRelation(statesSorted[0], s1, allowMerge); - assert((order->compare(s1, statesSorted[0]) == Order::BELOW) || - (allowMerge && (order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::SAME))); + // Fallback checks statesSorted[0]: that's the element the addRelation call just above + // related (and, if allowMerge applies, may have merged) s1 with. + STORM_LOG_ASSERT((order->compare(s1, statesSorted[0]) == Order::BELOW) || + (allowMerge && (order->compare(s1, statesSorted[0]) == Order::SAME)), + "Expected s1 to end up below (or, if merged, equal to) statesSorted[0]."); order->addRelation(statesSorted[statesSorted.size() - 1], s1, allowMerge); - assert((order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::BELOW) || - (allowMerge && (order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::SAME))); + STORM_LOG_ASSERT((order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::BELOW) || + (allowMerge && (order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::SAME)), + "Expected s1 to end up below (or, if merged, equal to) the highest sorted successor."); order->addStateToHandle(s1); } else { bool continueSearch = true; @@ -602,17 +613,18 @@ std::pair OrderExtender:: } else { return {s1, s2}; } - assert(order->contains(currentState) && order->compare(order->getNode(currentState), order->getBottom()) == Order::ABOVE && - order->compare(order->getNode(currentState), order->getTop()) == Order::BELOW); + STORM_LOG_ASSERT(order->contains(currentState) && order->compare(order->getNode(currentState), order->getBottom()) == Order::ABOVE && + order->compare(order->getNode(currentState), order->getTop()) == Order::BELOW, + "The current state should have ended up strictly between top and bottom in the order."); return {numberOfStates, numberOfStates}; } template bool OrderExtender::extendByAssumption(std::shared_ptr order, uint_fast64_t state1, uint_fast64_t state2) { - bool usePLANow = usePLA.find(order) != usePLA.end() && usePLA[order]; - assert(order->compare(state1, state2) == Order::UNKNOWN); - auto assumptions = usePLANow ? assumptionMaker->createAndCheckAssumptions(state1, state2, order, region, minValues[order], maxValues[order]) - : assumptionMaker->createAndCheckAssumptions(state1, state2, order, region); + auto& ctx = context(order); + STORM_LOG_ASSERT(order->compare(state1, state2) == Order::UNKNOWN, "Expected the given pair to indeed be unordered."); + auto assumptions = ctx.usePLA ? assumptionMaker->createAndCheckAssumptions(state1, state2, order, region, ctx.minValues, ctx.maxValues) + : assumptionMaker->createAndCheckAssumptions(state1, state2, order, region); if (assumptions.size() == 1 && assumptions.begin()->second == AssumptionStatus::VALID) { handleAssumption(order, assumptions.begin()->first); // Assumptions worked, we continue @@ -624,15 +636,19 @@ bool OrderExtender::extendByAssumption(std::shared_ptr< template Order::NodeComparison OrderExtender::addStatesBasedOnMinMax(std::shared_ptr order, uint_fast64_t state1, uint_fast64_t state2) const { - assert(order->compareFast(state1, state2) == Order::UNKNOWN); - assert(minValues.find(order) != minValues.end()); - std::vector const& mins = minValues.at(order); - std::vector const& maxs = maxValues.at(order); + STORM_LOG_ASSERT(order->compareFast(state1, state2) == Order::UNKNOWN, "Expected the given pair to indeed be unordered."); + auto const& ctx = contextAt(order); + std::vector const& mins = ctx.minValues; + std::vector const& maxs = ctx.maxValues; if (mins[state1] == maxs[state1] && mins[state2] == maxs[state2] && mins[state1] == mins[state2]) { if (order->contains(state1)) { if (order->contains(state2)) { - order->merge(state1, state2); - assert(!order->isInvalid()); + if (!order->merge(state1, state2)) { + // The min/max-based conclusion that state1 and state2 are equal contradicts + // what the order already knows about them; treat it as unresolved rather than + // silently building on top of an inconsistent order. + return Order::UNKNOWN; + } } else { order->addToNode(state2, order->getNode(state1)); } @@ -646,8 +662,8 @@ Order::NodeComparison OrderExtender::addStatesBasedOnMi if (!order->contains(state2)) { order->add(state2); } - assert(order->compare(state1, state2) != Order::BELOW); - assert(order->compare(state1, state2) != Order::SAME); + STORM_LOG_ASSERT(order->compare(state1, state2) != Order::BELOW, "min/max values say state1 is above state2, contradicting the order."); + STORM_LOG_ASSERT(order->compare(state1, state2) != Order::SAME, "min/max values say state1 is strictly above state2, contradicting the order."); order->addRelation(state1, state2); return Order::ABOVE; @@ -659,8 +675,8 @@ Order::NodeComparison OrderExtender::addStatesBasedOnMi if (!order->contains(state2)) { order->add(state2); } - assert(order->compare(state2, state1) != Order::BELOW); - assert(order->compare(state2, state1) != Order::SAME); + STORM_LOG_ASSERT(order->compare(state2, state1) != Order::BELOW, "min/max values say state2 is above state1, contradicting the order."); + STORM_LOG_ASSERT(order->compare(state2, state1) != Order::SAME, "min/max values say state2 is strictly above state1, contradicting the order."); order->addRelation(state2, state1); return Order::BELOW; } else { @@ -696,82 +712,70 @@ void OrderExtender::initializeMinMaxValues(storage::Par plaModelChecker.check(env, annotatedRegion, solver::OptimizationDirection::Maximize)->template asExplicitQuantitativeCheckResult(); minValuesInit = minCheck.getValueVector(); maxValuesInit = maxCheck.getValueVector(); - assert(minValuesInit->size() == numberOfStates); - assert(maxValuesInit->size() == numberOfStates); + STORM_LOG_ASSERT(minValuesInit->size() == numberOfStates, "Expected one lower bound per state."); + STORM_LOG_ASSERT(maxValuesInit->size() == numberOfStates, "Expected one upper bound per state."); } } template void OrderExtender::setMinMaxValues(std::shared_ptr order, std::vector&& minValues, std::vector&& maxValues) { - assert(minValues.size() == numberOfStates); - assert(maxValues.size() == numberOfStates); - usePLA[order] = true; - if (unknownStatesMap.find(order) != unknownStatesMap.end()) { - auto& unknownStates = unknownStatesMap[order]; - if (unknownStates.first != numberOfStates) { - continueExtending[order] = - minValues[unknownStates.first] >= maxValues[unknownStates.second] || minValues[unknownStates.second] >= maxValues[unknownStates.first]; - } else { - continueExtending[order] = true; - } + STORM_LOG_ASSERT(minValues.size() == numberOfStates, "Expected one lower bound per state."); + STORM_LOG_ASSERT(maxValues.size() == numberOfStates, "Expected one upper bound per state."); + auto& ctx = context(order); + ctx.usePLA = true; + if (ctx.unknownStates.first != numberOfStates) { + ctx.continueExtending = + minValues[ctx.unknownStates.first] >= maxValues[ctx.unknownStates.second] || minValues[ctx.unknownStates.second] >= maxValues[ctx.unknownStates.first]; } else { - continueExtending[order] = true; + ctx.continueExtending = true; } - this->minValues[order] = std::move(minValues); - this->maxValues[order] = std::move(maxValues); + ctx.minValues = std::move(minValues); + ctx.maxValues = std::move(maxValues); } template void OrderExtender::setMinValues(std::shared_ptr order, std::vector&& minValues) { - assert(minValues.size() == numberOfStates); - auto& maxValues = this->maxValues[order]; - usePLA[order] = this->maxValues.find(order) != this->maxValues.end(); - if (maxValues.size() == 0) { - continueExtending[order] = false; - } else if (unknownStatesMap.find(order) != unknownStatesMap.end()) { - auto& unknownStates = unknownStatesMap[order]; - if (unknownStates.first != numberOfStates) { - continueExtending[order] = - minValues[unknownStates.first] >= maxValues[unknownStates.second] || minValues[unknownStates.second] >= maxValues[unknownStates.first]; - } else { - continueExtending[order] = true; - } + STORM_LOG_ASSERT(minValues.size() == numberOfStates, "Expected one lower bound per state."); + auto& ctx = context(order); + // usePLA becomes true unconditionally here (unlike setMaxValues, which checks whether the other + // bound is already known): accessing ctx.maxValues below always makes it "known", even if empty. + ctx.usePLA = true; + if (ctx.maxValues.size() == 0) { + ctx.continueExtending = false; + } else if (ctx.unknownStates.first != numberOfStates) { + ctx.continueExtending = minValues[ctx.unknownStates.first] >= ctx.maxValues[ctx.unknownStates.second] || + minValues[ctx.unknownStates.second] >= ctx.maxValues[ctx.unknownStates.first]; } else { - continueExtending[order] = true; + ctx.continueExtending = true; } - this->minValues[order] = std::move(minValues); + ctx.minValues = std::move(minValues); } template void OrderExtender::setMaxValues(std::shared_ptr order, std::vector&& maxValues) { - assert(maxValues.size() == numberOfStates); - usePLA[order] = this->minValues.find(order) != this->minValues.end(); - auto& minValues = this->minValues[order]; - if (minValues.size() == 0) { - continueExtending[order] = false; - } else if (unknownStatesMap.find(order) != unknownStatesMap.end()) { - auto& unknownStates = unknownStatesMap[order]; - if (unknownStates.first != numberOfStates) { - continueExtending[order] = - minValues[unknownStates.first] >= maxValues[unknownStates.second] || minValues[unknownStates.second] >= maxValues[unknownStates.first]; - } else { - continueExtending[order] = true; - } + STORM_LOG_ASSERT(maxValues.size() == numberOfStates, "Expected one upper bound per state."); + auto& ctx = context(order); + ctx.usePLA = !ctx.minValues.empty(); + if (ctx.minValues.size() == 0) { + ctx.continueExtending = false; + } else if (ctx.unknownStates.first != numberOfStates) { + ctx.continueExtending = ctx.minValues[ctx.unknownStates.first] >= maxValues[ctx.unknownStates.second] || + ctx.minValues[ctx.unknownStates.second] >= maxValues[ctx.unknownStates.first]; } else { - continueExtending[order] = true; + ctx.continueExtending = true; } - this->maxValues[order] = std::move(maxValues); // maxCheck->asExplicitQuantitativeCheckResult().getValueVector(); + ctx.maxValues = std::move(maxValues); } template void OrderExtender::setMinValuesInit(std::vector&& minValues) { - assert(minValues.size() == numberOfStates); + STORM_LOG_ASSERT(minValues.size() == numberOfStates, "Expected one lower bound per state."); this->minValuesInit = std::move(minValues); } template void OrderExtender::setMaxValuesInit(std::vector&& maxValues) { - assert(maxValues.size() == numberOfStates); + STORM_LOG_ASSERT(maxValues.size() == numberOfStates, "Expected one upper bound per state."); this->maxValuesInit = std::move(maxValues); // maxCheck->asExplicitQuantitativeCheckResult().getValueVector(); } @@ -785,33 +789,23 @@ void OrderExtender::checkParOnStateMonRes(uint_fast64_t template void OrderExtender::setUnknownStates(std::shared_ptr order, uint_fast64_t state1, uint_fast64_t state2) { - assert(state1 != numberOfStates && state2 != numberOfStates); - unknownStatesMap[order] = {state1, state2}; + STORM_LOG_ASSERT(state1 != numberOfStates && state2 != numberOfStates, "Expected two actual states, not the sentinel value."); + context(order).unknownStates = {state1, state2}; } template std::pair OrderExtender::getUnknownStates(std::shared_ptr order) const { - if (unknownStatesMap.find(order) != unknownStatesMap.end()) { - return unknownStatesMap.at(order); + auto it = contexts.find(order); + if (it != contexts.end()) { + return it->second.unknownStates; } return {numberOfStates, numberOfStates}; } template -void OrderExtender::setUnknownStates(std::shared_ptr orderOriginal, std::shared_ptr orderCopy) { - assert(unknownStatesMap.find(orderCopy) == unknownStatesMap.end()); - unknownStatesMap.insert({orderCopy, {unknownStatesMap[orderOriginal].first, unknownStatesMap[orderOriginal].second}}); -} - -template -void OrderExtender::copyMinMax(std::shared_ptr orderOriginal, std::shared_ptr orderCopy) { - usePLA[orderCopy] = usePLA[orderOriginal]; - if (usePLA[orderCopy]) { - minValues[orderCopy] = minValues[orderOriginal]; - assert(maxValues.find(orderOriginal) != maxValues.end()); - maxValues[orderCopy] = maxValues[orderOriginal]; - } - continueExtending[orderCopy] = continueExtending[orderOriginal]; +void OrderExtender::copyContext(std::shared_ptr orderOriginal, std::shared_ptr orderCopy) { + STORM_LOG_ASSERT(contexts.find(orderCopy) == contexts.end(), "The copy must not already have a context set."); + contexts[orderCopy] = contextAt(orderOriginal); } template @@ -833,11 +827,10 @@ std::pair OrderExtender::getNextSt template bool OrderExtender::isHope(std::shared_ptr order) { - assert(unknownStatesMap.find(order) != unknownStatesMap.end()); - assert(!order->getDoneBuilding()); + STORM_LOG_ASSERT(contexts.find(order) != contexts.end(), "Expected a context to be set for this order."); + STORM_LOG_ASSERT(!order->getDoneBuilding(), "Asking for hope on an order that is already fully built is meaningless."); // First check if bounds helped us - bool yesThereIsHope = continueExtending[order]; - return yesThereIsHope; + return context(order).continueExtending; } template MonotonicityChecker& OrderExtender::getMonotoncityChecker() { diff --git a/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.h b/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.h index b552abd947..aed1bdaf79 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.h +++ b/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.h @@ -1,12 +1,12 @@ #pragma once #include +#include #include "storm/logic/Formula.h" #include "storm/models/sparse/Model.h" -#include "storm/storage/expressions/BinaryRelationExpression.h" -#include "storm/storage/expressions/VariableExpression.h" #include "storm/utility/Stopwatch.h" +#include "storm-pars/modelchecker/region/monotonicity/Assumption.h" #include "storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h" #include "storm-pars/modelchecker/region/monotonicity/MonotonicityChecker.h" #include "storm-pars/modelchecker/region/monotonicity/MonotonicityResult.h" @@ -63,7 +63,7 @@ class OrderExtender { std::tuple, uint_fast64_t, uint_fast64_t> extendOrder(std::shared_ptr order, storm::storage::ParameterRegion region, std::shared_ptr> monRes = nullptr, - std::shared_ptr assumption = nullptr); + std::optional assumption = std::nullopt); void setMinMaxValues(std::shared_ptr order, std::vector&& minValues, std::vector&& maxValues); void setMinValues(std::shared_ptr order, std::vector&& minValues); @@ -74,8 +74,7 @@ class OrderExtender { void setUnknownStates(std::shared_ptr order, uint_fast64_t state1, uint_fast64_t state2); std::pair getUnknownStates(std::shared_ptr order) const; - void setUnknownStates(std::shared_ptr orderOriginal, std::shared_ptr orderCopy); - void copyMinMax(std::shared_ptr orderOriginal, std::shared_ptr orderCopy); + void copyContext(std::shared_ptr orderOriginal, std::shared_ptr orderCopy); void initializeMinMaxValues(storage::ParameterRegion region); void checkParOnStateMonRes(uint_fast64_t s, std::shared_ptr order, typename OrderExtender::VariableType param, std::shared_ptr> monResult); @@ -89,7 +88,7 @@ class OrderExtender { Order::NodeComparison addStatesBasedOnMinMax(std::shared_ptr order, uint_fast64_t state1, uint_fast64_t state2) const; std::tuple, uint_fast64_t, uint_fast64_t> extendOrder(std::shared_ptr order, std::shared_ptr> monRes, - std::shared_ptr assumption = nullptr); + std::optional assumption = std::nullopt); std::pair extendNormal(std::shared_ptr order, uint_fast64_t currentState, std::vector const& successors, bool allowMerge); std::pair extendByBackwardReasoning(std::shared_ptr order, uint_fast64_t currentState, @@ -99,26 +98,38 @@ class OrderExtender { bool extendByAssumption(std::shared_ptr order, uint_fast64_t state1, uint_fast64_t state2); void handleOneSuccessor(std::shared_ptr order, uint_fast64_t currentState, uint_fast64_t successor); - void handleAssumption(std::shared_ptr order, std::shared_ptr assumption) const; + void handleAssumption(std::shared_ptr order, Assumption const& assumption) const; std::pair getNextState(std::shared_ptr order, uint_fast64_t stateNumber, bool done); + std::shared_ptr computeInitialOrder(storm::storage::BitVector const& topStates, storm::storage::BitVector const& bottomStates, + storm::storage::SparseMatrix const& matrix, bool addStatesWithDirectBoundaryTransition); std::shared_ptr getBottomTopOrder(); std::shared_ptr bottomTopOrder = nullptr; - std::map, std::vector> minValues; + // Per-in-progress-order bookkeeping used while extending an order (PLA bounds, whether PLA is + // usable/worth continuing, and the pair of states this order got stuck on, if any). Keyed by + // weak_ptr rather than shared_ptr so that this bookkeeping does not itself keep an order alive + // or inflate its use_count() while it is still being extended. + struct Context { + std::vector minValues; + std::vector maxValues; + bool usePLA = false; + bool continueExtending = true; + std::pair unknownStates; + }; + Context& context(std::shared_ptr const& order); + Context const& contextAt(std::shared_ptr const& order) const; + std::map, Context, std::owner_less>> contexts; + boost::optional> minValuesInit; boost::optional> maxValuesInit; - std::map, std::vector> maxValues; storage::SparseMatrix matrix; std::shared_ptr> model; std::map> stateMap; - std::map, std::pair> unknownStatesMap; - std::map, bool> usePLA; - std::map, bool> continueExtending; bool cyclic; std::shared_ptr formula; @@ -127,7 +138,7 @@ class OrderExtender { uint_fast64_t numberOfStates; - analysis::AssumptionMaker* assumptionMaker; + std::unique_ptr> assumptionMaker; boost::container::flat_set nonParametricStates; diff --git a/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionCheckerTest.cpp b/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionCheckerTest.cpp index 96428dc0a6..5dbaeaa28a 100644 --- a/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionCheckerTest.cpp +++ b/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionCheckerTest.cpp @@ -18,8 +18,6 @@ #include "storm/logic/Formulas.h" #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "storm/storage/StronglyConnectedComponentDecomposition.h" -#include "storm/storage/expressions/BinaryRelationExpression.h" -#include "storm/storage/expressions/ExpressionManager.h" #include "storm/utility/graph.h" class AssumptionCheckerTest : public ::testing::Test { @@ -58,9 +56,6 @@ TEST_F(AssumptionCheckerTest, Brp_no_bisimulation) { auto region = storm::api::parseRegion("0.00001 <= pK <= 0.00001, 0.00001 <= pL <= 0.99999", vars); auto checker = storm::analysis::AssumptionChecker(dtmc->getTransitionMatrix()); - auto expressionManager = std::make_shared(storm::expressions::ExpressionManager()); - expressionManager->declareRationalVariable("7"); - expressionManager->declareRationalVariable("5"); storm::storage::BitVector above(193); above.set(0); storm::storage::BitVector below(193); @@ -73,35 +68,23 @@ TEST_F(AssumptionCheckerTest, Brp_no_bisimulation) { auto statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); auto dummyOrder = std::shared_ptr(new storm::analysis::Order(above, below, 193, decomposition, statesSorted)); - auto assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + storm::analysis::Assumption assumption{7, 5, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.validateAssumption(assumption, dummyOrder, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{5, 7, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.validateAssumption(assumption, dummyOrder, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal)); + assumption = storm::analysis::Assumption{7, 5, storm::expressions::RelationType::Equal}; EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.validateAssumption(assumption, dummyOrder, region)); checker.initializeCheckingOnSamples(formulas[0], dtmc, region, 3); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{7, 5, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.validateAssumption(assumption, dummyOrder, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{5, 7, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyOrder, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal)); + assumption = storm::analysis::Assumption{7, 5, storm::expressions::RelationType::Equal}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyOrder, region)); } @@ -132,9 +115,6 @@ TEST_F(AssumptionCheckerTest, Simple1) { auto checker = storm::analysis::AssumptionChecker(dtmc->getTransitionMatrix()); - auto expressionManager = std::make_shared(storm::expressions::ExpressionManager()); - expressionManager->declareRationalVariable("1"); - expressionManager->declareRationalVariable("2"); storm::storage::StronglyConnectedComponentDecompositionOptions options; options.forceTopologicalSort(); auto decomposition = storm::storage::StronglyConnectedComponentDecomposition(model->getTransitionMatrix(), options); @@ -147,35 +127,23 @@ TEST_F(AssumptionCheckerTest, Simple1) { auto order = std::shared_ptr(new storm::analysis::Order(above, below, 5, decomposition, statesSorted)); // Validating - auto assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + storm::analysis::Assumption assumption{1, 2, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{2, 1, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Equal}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); region = storm::api::parseRegion("0.51 <= p <= 0.99", vars); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{2, 1, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Equal}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); } @@ -206,10 +174,6 @@ TEST_F(AssumptionCheckerTest, Casestudy1) { auto checker = storm::analysis::AssumptionChecker(dtmc->getTransitionMatrix()); - auto expressionManager = std::make_shared(storm::expressions::ExpressionManager()); - expressionManager->declareRationalVariable("1"); - expressionManager->declareRationalVariable("2"); - storm::storage::BitVector above(5); above.set(3); storm::storage::BitVector below(5); @@ -222,35 +186,23 @@ TEST_F(AssumptionCheckerTest, Casestudy1) { auto order = std::shared_ptr(new storm::analysis::Order(above, below, 5, decomposition, statesSorted)); // Validating - auto assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + storm::analysis::Assumption assumption{1, 2, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{2, 1, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Equal}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); checker.initializeCheckingOnSamples(formulas[0], dtmc, region, 3); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{2, 1, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Equal}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); } @@ -281,10 +233,6 @@ TEST_F(AssumptionCheckerTest, Casestudy2) { auto checker = storm::analysis::AssumptionChecker(dtmc->getTransitionMatrix()); - auto expressionManager = std::make_shared(storm::expressions::ExpressionManager()); - expressionManager->declareRationalVariable("1"); - expressionManager->declareRationalVariable("2"); - storm::storage::BitVector above(6); above.set(4); storm::storage::BitVector below(6); @@ -298,19 +246,13 @@ TEST_F(AssumptionCheckerTest, Casestudy2) { order->add(3); // Checking on samples and validate - auto assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + storm::analysis::Assumption assumption{1, 2, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{2, 1, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Equal}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); } @@ -341,10 +283,6 @@ TEST_F(AssumptionCheckerTest, Casestudy3) { auto checker = storm::analysis::AssumptionChecker(dtmc->getTransitionMatrix()); - auto expressionManager = std::make_shared(storm::expressions::ExpressionManager()); - expressionManager->declareRationalVariable("1"); - expressionManager->declareRationalVariable("2"); - // Order storm::storage::BitVector above(5); above.set(3); @@ -356,35 +294,23 @@ TEST_F(AssumptionCheckerTest, Casestudy3) { auto statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); auto order = std::shared_ptr(new storm::analysis::Order(above, below, 5, decomposition, statesSorted)); - auto assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + storm::analysis::Assumption assumption{1, 2, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{2, 1, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Equal}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); checker.initializeCheckingOnSamples(formulas[0], dtmc, region, 3); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{2, 1, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Equal}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); } diff --git a/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionMakerTest.cpp b/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionMakerTest.cpp index a16c0ddcc8..f2dc8d02de 100644 --- a/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionMakerTest.cpp +++ b/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionMakerTest.cpp @@ -65,20 +65,29 @@ TEST_F(AssumptionMakerTest, Brp_without_bisimulation) { for (auto res : result) { EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, res.second); - EXPECT_EQ(true, res.first->getFirstOperand()->isVariable()); - EXPECT_EQ(true, res.first->getSecondOperand()->isVariable()); } + // Regression test: when more than one candidate survives, they must be returned in construction + // order (val1 > val2, val2 > val1, val1 == val2), not e.g. heap-address order of some internal + // representation. + EXPECT_EQ(183ul, result[0].first.state1); + EXPECT_EQ(186ul, result[0].first.state2); + EXPECT_EQ(storm::expressions::RelationType::Greater, result[0].first.relation); + EXPECT_EQ(186ul, result[1].first.state1); + EXPECT_EQ(183ul, result[1].first.state2); + EXPECT_EQ(storm::expressions::RelationType::Greater, result[1].first.relation); + EXPECT_EQ(183ul, result[2].first.state1); + EXPECT_EQ(186ul, result[2].first.state2); + EXPECT_EQ(storm::expressions::RelationType::Equal, result[2].first.relation); + assumptionMaker.initializeCheckingOnSamples(formulas[0], model, region, 10); result = assumptionMaker.createAndCheckAssumptions(std::get<1>(criticalTuple), std::get<2>(criticalTuple), std::get<0>(criticalTuple), region); EXPECT_EQ(1ul, result.size()); auto itr = result.begin(); EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, itr->second); - EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); - EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); - EXPECT_EQ("186", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); - EXPECT_EQ("183", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); - EXPECT_EQ(storm::expressions::RelationType::Greater, itr->first->getRelationType()); + EXPECT_EQ(186ul, itr->first.state1); + EXPECT_EQ(183ul, itr->first.state2); + EXPECT_EQ(storm::expressions::RelationType::Greater, itr->first.relation); } TEST_F(AssumptionMakerTest, Simple1) { @@ -127,11 +136,9 @@ TEST_F(AssumptionMakerTest, Simple1) { EXPECT_EQ(1ul, result.size()); auto itr = result.begin(); EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, itr->second); - EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); - EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); - EXPECT_EQ("1", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); - EXPECT_EQ("2", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); - EXPECT_EQ(storm::expressions::RelationType::Greater, itr->first->getRelationType()); + EXPECT_EQ(1ul, itr->first.state1); + EXPECT_EQ(2ul, itr->first.state2); + EXPECT_EQ(storm::expressions::RelationType::Greater, itr->first.relation); } TEST_F(AssumptionMakerTest, Casestudy1) { @@ -173,9 +180,7 @@ TEST_F(AssumptionMakerTest, Casestudy1) { EXPECT_EQ(1ul, result.size()); auto itr = result.begin(); EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, itr->second); - EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); - EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); - EXPECT_EQ("1", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); - EXPECT_EQ("2", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); - EXPECT_EQ(storm::expressions::RelationType::Greater, itr->first->getRelationType()); + EXPECT_EQ(1ul, itr->first.state1); + EXPECT_EQ(2ul, itr->first.state2); + EXPECT_EQ(storm::expressions::RelationType::Greater, itr->first.relation); } diff --git a/src/test/storm-pars/modelchecker/region/monotonicity/OrderTest.cpp b/src/test/storm-pars/modelchecker/region/monotonicity/OrderTest.cpp index 7c6c5c8e5d..db6fe869e7 100644 --- a/src/test/storm-pars/modelchecker/region/monotonicity/OrderTest.cpp +++ b/src/test/storm-pars/modelchecker/region/monotonicity/OrderTest.cpp @@ -152,6 +152,53 @@ TEST(OrderTest, copy_order) { EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(5, 6)); } +TEST(OrderTest, copy_is_deep) { + // Regression test: Order's copy constructor must deep-copy every Node, not alias the + // original's nodes. Mutating one Order (adding states, merging nodes) must not affect the + // other. + auto numberOfStates = 7; + auto above = storm::storage::BitVector(numberOfStates); + above.set(0); + auto below = storm::storage::BitVector(numberOfStates); + below.set(1); + storm::storage::SparseMatrixBuilder matrixBuilder(2, 2, 2); + matrixBuilder.addNextValue(0, 0, storm::RationalFunction(1)); + matrixBuilder.addNextValue(1, 1, storm::RationalFunction(1)); + storm::storage::StronglyConnectedComponentDecompositionOptions options; + options.forceTopologicalSort(); + auto matrix = matrixBuilder.build(); + auto decomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, options); + auto statesSorted = storm::utility::graph::getTopologicalSort(matrix); + auto order = storm::analysis::Order(above, below, numberOfStates, decomposition, statesSorted); + order.add(2); + order.add(3); + order.addToNode(4, order.getNode(2)); + + auto orderCopy = storm::analysis::Order(order); + + // Mutating the copy (adding a new state) must not be visible in the original. + orderCopy.addBetween(5, orderCopy.getNode(0), orderCopy.getNode(3)); + EXPECT_TRUE(orderCopy.contains(5)); + EXPECT_FALSE(order.contains(5)); + + // Mutating the original (adding a different state) must not be visible in the copy. + order.addBetween(6, order.getNode(0), order.getNode(3)); + EXPECT_TRUE(order.contains(6)); + EXPECT_FALSE(orderCopy.contains(6)); + + // Merging nodes in the copy must not merge the corresponding nodes in the original: states 2 + // and 3 stay unrelated in the original, even after they are merged in the copy. + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(2, 3)); + orderCopy.mergeNodes(orderCopy.getNode(2), orderCopy.getNode(3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, orderCopy.compare(2, 3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(2, 3)); + + // Node pointers themselves must not be shared between the two Orders. + EXPECT_NE(order.getNode(0), orderCopy.getNode(0)); + EXPECT_NE(order.getTop(), orderCopy.getTop()); + EXPECT_NE(order.getBottom(), orderCopy.getBottom()); +} + TEST(OrderTest, merge_nodes) { auto numberOfStates = 7; auto above = storm::storage::BitVector(numberOfStates); @@ -192,6 +239,47 @@ TEST(OrderTest, merge_nodes) { EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1, 5)); } +TEST(OrderTest, merge_nodes_inconsistent) { + // Regression test: forcing a merge that contradicts an already-established chain of relations + // must be reported gracefully (mergeNodes returns false, isInvalid() becomes true) rather than + // crashing on an internal assertion when a later compare() call discovers the resulting cycle. + auto numberOfStates = 6; + auto above = storm::storage::BitVector(numberOfStates); + above.set(0); + auto below = storm::storage::BitVector(numberOfStates); + below.set(1); + storm::storage::SparseMatrixBuilder matrixBuilder(2, 2, 2); + matrixBuilder.addNextValue(0, 0, storm::RationalFunction(1)); + matrixBuilder.addNextValue(1, 1, storm::RationalFunction(1)); + storm::storage::StronglyConnectedComponentDecompositionOptions options; + options.forceTopologicalSort(); + auto matrix = matrixBuilder.build(); + auto decomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, options); + auto statesSorted = storm::utility::graph::getTopologicalSort(matrix); + auto order = storm::analysis::Order(above, below, numberOfStates, decomposition, statesSorted); + + // Build a strict chain: top(0) > 3 > 4 > 5 > 2 > bottom(1). + order.add(2); + order.addBetween(3, order.getNode(0), order.getNode(2)); + order.addBetween(4, order.getNode(3), order.getNode(2)); + order.addBetween(5, order.getNode(4), order.getNode(2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(3, 2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(3, 4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(4, 5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(5, 2)); + + // Forcing 3 and 2 to be equal directly contradicts 3 > 4 > 5 > 2: mergeNodes must refuse this + // (returning false, marking the order invalid) instead of leaving the order in a state where a + // later compare() call would discover a state both above and below another. + EXPECT_FALSE(order.mergeNodes(order.getNode(3), order.getNode(2))); + EXPECT_TRUE(order.isInvalid()); + + // Further compare() calls on the now-invalid order must not crash. + EXPECT_NO_FATAL_FAILURE(order.compare(4, 5)); + EXPECT_NO_FATAL_FAILURE(order.compare(3, 4)); + EXPECT_NO_FATAL_FAILURE(order.compare(0, 1)); +} + TEST(OrderTest, sort_states) { auto numberOfStates = 7; auto above = storm::storage::BitVector(numberOfStates); From 6385b40c80bad805e7b79abd33a8ad3f3543f9dd Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 4 Aug 2026 17:03:59 +0200 Subject: [PATCH 5/8] format --- .../region/monotonicity/AssumptionChecker.cpp | 6 +-- .../region/monotonicity/AssumptionMaker.cpp | 14 +++--- .../region/monotonicity/AssumptionMaker.h | 5 +-- .../monotonicity/MonotonicityHelper.cpp | 4 +- .../region/monotonicity/Order.cpp | 8 ++-- .../region/monotonicity/OrderExtender.cpp | 44 +++++++++---------- 6 files changed, 39 insertions(+), 42 deletions(-) diff --git a/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.cpp b/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.cpp index 6494e342f8..1768434c62 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.cpp @@ -129,9 +129,9 @@ AssumptionStatus AssumptionChecker::checkOnSamples(Assu template AssumptionStatus AssumptionChecker::validateAssumptionSMTSolver(Assumption const& assumption, std::shared_ptr order, - storage::ParameterRegion region, - std::vector const minValues, - std::vector const maxValues) const { + storage::ParameterRegion region, + std::vector const minValues, + std::vector const maxValues) const { std::shared_ptr manager(new expressions::ExpressionManager()); AssumptionStatus result = AssumptionStatus::UNKNOWN; uint_fast64_t val1 = assumption.state1; diff --git a/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.cpp b/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.cpp index 64c7668624..ef3b1000b0 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.cpp @@ -29,10 +29,10 @@ std::vector> AssumptionMaker> AssumptionMaker createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, expressions::RelationType relationType, - std::shared_ptr order, storage::ParameterRegion region, - std::vector const minValues, - std::vector const maxValue) const; + std::shared_ptr order, storage::ParameterRegion region, + std::vector const minValues, std::vector const maxValue) const; AssumptionChecker assumptionChecker; }; diff --git a/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.cpp b/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.cpp index def16a9b88..0a8ba7b1e4 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.cpp @@ -77,8 +77,8 @@ MonotonicityHelper::MonotonicityHelper(std::shared_ptr< /*** Public methods ***/ template -std::map, std::pair::VariableType>>, - std::vector>> +std::map, + std::pair::VariableType>>, std::vector>> MonotonicityHelper::checkMonotonicityInBuild(std::ostream& outfile, bool usePLA, std::string dotOutfileName) { if (usePLA) { storm::utility::Stopwatch plaWatch(true); diff --git a/src/storm-pars/modelchecker/region/monotonicity/Order.cpp b/src/storm-pars/modelchecker/region/monotonicity/Order.cpp index e1b813e71e..2ad65c8417 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/Order.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/Order.cpp @@ -29,7 +29,7 @@ Order::Order(storm::storage::BitVector const& topStates, storm::storage::BitVect } STORM_LOG_ASSERT(numberOfAddedStates <= numberOfStates, "More states were added to the order than it has room for."); STORM_LOG_ASSERT(doneStates.getNumberOfSetBits() == (topStates.getNumberOfSetBits() + bottomStates.getNumberOfSetBits()), - "Number of done states does not match the number of given top and bottom states."); + "Number of done states does not match the number of given top and bottom states."); if (numberOfAddedStates == numberOfStates) { doneBuilding = doneStates.full(); } @@ -368,7 +368,7 @@ Order::Node* Order::getBottom() const { bool Order::getDoneBuilding() const { STORM_LOG_ASSERT(!doneStates.full() || numberOfAddedStates == numberOfStates, - "All states are marked done, but not all states have been added to the order."); + "All states are marked done, but not all states have been added to the order."); return doneStates.full(); } @@ -501,8 +501,8 @@ std::pair, std::vector> O s2 = numberOfStates; } STORM_LOG_ASSERT(s1 == numberOfStates || (s1 != numberOfStates && s2 == numberOfStates && statesSorted.size() == states.size()) || - (s1 != numberOfStates && s2 != numberOfStates && statesSorted.size() < states.size()), - "Inconsistent result: (s1, s2) and the number of sorted states must agree on how far sorting got."); + (s1 != numberOfStates && s2 != numberOfStates && statesSorted.size() < states.size()), + "Inconsistent result: (s1, s2) and the number of sorted states must agree on how far sorting got."); return {{s1, s2}, statesSorted}; } diff --git a/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp b/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp index b633f2f446..4eac4693d6 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp @@ -45,9 +45,9 @@ OrderExtender::OrderExtender(storm::storage::BitVector template std::shared_ptr OrderExtender::computeInitialOrder(storm::storage::BitVector const& topStates, - storm::storage::BitVector const& bottomStates, - storm::storage::SparseMatrix const& matrix, - bool addStatesWithDirectBoundaryTransition) { + storm::storage::BitVector const& bottomStates, + storm::storage::SparseMatrix const& matrix, + bool addStatesWithDirectBoundaryTransition) { storm::storage::StronglyConnectedComponentDecompositionOptions options; options.forceTopologicalSort(); @@ -331,7 +331,7 @@ std::tuple, uint_fast64_t, uint_fast64_t> OrderExtendersortStates(&successors).size() == successors.size(), "Expected all successors to be sortable at this point."); STORM_LOG_ASSERT(order->contains(currentState) && order->getNode(currentState) != nullptr, - "The current state should have been placed in the order."); + "The current state should have been placed in the order."); if (monRes != nullptr) { for (auto& param : occuringVariablesAtState[currentState]) { @@ -397,7 +397,7 @@ std::pair OrderExtender:: return extendByForwardReasoning(order, currentState, successors, allowMerge); } else { STORM_LOG_ASSERT(order->isTrivial(currentState) || !order->contains(currentState), - "A non-trivial (SCC) state that is already in the order should use forward reasoning, not backward reasoning."); + "A non-trivial (SCC) state that is already in the order should use forward reasoning, not backward reasoning."); // Do backward reasoning, all successor states must be in the order return extendByBackwardReasoning(order, currentState, successors, allowMerge); } @@ -493,8 +493,8 @@ std::pair OrderExtender:: } } STORM_LOG_ASSERT(order->contains(currentState) && order->compare(order->getNode(currentState), order->getBottom()) == Order::ABOVE && - order->compare(order->getNode(currentState), order->getTop()) == Order::BELOW, - "The current state should have ended up strictly between top and bottom in the order."); + order->compare(order->getNode(currentState), order->getTop()) == Order::BELOW, + "The current state should have ended up strictly between top and bottom in the order."); return {numberOfStates, numberOfStates}; } @@ -573,25 +573,23 @@ std::pair OrderExtender:: order->addRelation(s1, statesSorted[0], allowMerge); // Fallback checks statesSorted[0]: that's the element the addRelation call just above // related (and, if allowMerge applies, may have merged) s1 with. - STORM_LOG_ASSERT((order->compare(s1, statesSorted[0]) == Order::ABOVE) || - (allowMerge && (order->compare(s1, statesSorted[0]) == Order::SAME)), - "Expected s1 to end up above (or, if merged, equal to) statesSorted[0]."); + STORM_LOG_ASSERT((order->compare(s1, statesSorted[0]) == Order::ABOVE) || (allowMerge && (order->compare(s1, statesSorted[0]) == Order::SAME)), + "Expected s1 to end up above (or, if merged, equal to) statesSorted[0]."); order->addRelation(s1, statesSorted[statesSorted.size() - 1], allowMerge); STORM_LOG_ASSERT((order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::ABOVE) || - (allowMerge && (order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::SAME)), - "Expected s1 to end up above (or, if merged, equal to) the lowest sorted successor."); + (allowMerge && (order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::SAME)), + "Expected s1 to end up above (or, if merged, equal to) the lowest sorted successor."); order->addStateToHandle(s1); } else if (statesSorted[statesSorted.size() - 1] == currentState) { order->addRelation(statesSorted[0], s1, allowMerge); // Fallback checks statesSorted[0]: that's the element the addRelation call just above // related (and, if allowMerge applies, may have merged) s1 with. - STORM_LOG_ASSERT((order->compare(s1, statesSorted[0]) == Order::BELOW) || - (allowMerge && (order->compare(s1, statesSorted[0]) == Order::SAME)), - "Expected s1 to end up below (or, if merged, equal to) statesSorted[0]."); + STORM_LOG_ASSERT((order->compare(s1, statesSorted[0]) == Order::BELOW) || (allowMerge && (order->compare(s1, statesSorted[0]) == Order::SAME)), + "Expected s1 to end up below (or, if merged, equal to) statesSorted[0]."); order->addRelation(statesSorted[statesSorted.size() - 1], s1, allowMerge); STORM_LOG_ASSERT((order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::BELOW) || - (allowMerge && (order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::SAME)), - "Expected s1 to end up below (or, if merged, equal to) the highest sorted successor."); + (allowMerge && (order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::SAME)), + "Expected s1 to end up below (or, if merged, equal to) the highest sorted successor."); order->addStateToHandle(s1); } else { bool continueSearch = true; @@ -614,8 +612,8 @@ std::pair OrderExtender:: return {s1, s2}; } STORM_LOG_ASSERT(order->contains(currentState) && order->compare(order->getNode(currentState), order->getBottom()) == Order::ABOVE && - order->compare(order->getNode(currentState), order->getTop()) == Order::BELOW, - "The current state should have ended up strictly between top and bottom in the order."); + order->compare(order->getNode(currentState), order->getTop()) == Order::BELOW, + "The current state should have ended up strictly between top and bottom in the order."); return {numberOfStates, numberOfStates}; } @@ -725,8 +723,8 @@ void OrderExtender::setMinMaxValues(std::shared_ptr= maxValues[ctx.unknownStates.second] || minValues[ctx.unknownStates.second] >= maxValues[ctx.unknownStates.first]; + ctx.continueExtending = minValues[ctx.unknownStates.first] >= maxValues[ctx.unknownStates.second] || + minValues[ctx.unknownStates.second] >= maxValues[ctx.unknownStates.first]; } else { ctx.continueExtending = true; } @@ -745,7 +743,7 @@ void OrderExtender::setMinValues(std::shared_ptr ctx.continueExtending = false; } else if (ctx.unknownStates.first != numberOfStates) { ctx.continueExtending = minValues[ctx.unknownStates.first] >= ctx.maxValues[ctx.unknownStates.second] || - minValues[ctx.unknownStates.second] >= ctx.maxValues[ctx.unknownStates.first]; + minValues[ctx.unknownStates.second] >= ctx.maxValues[ctx.unknownStates.first]; } else { ctx.continueExtending = true; } @@ -761,7 +759,7 @@ void OrderExtender::setMaxValues(std::shared_ptr ctx.continueExtending = false; } else if (ctx.unknownStates.first != numberOfStates) { ctx.continueExtending = ctx.minValues[ctx.unknownStates.first] >= maxValues[ctx.unknownStates.second] || - ctx.minValues[ctx.unknownStates.second] >= maxValues[ctx.unknownStates.first]; + ctx.minValues[ctx.unknownStates.second] >= maxValues[ctx.unknownStates.first]; } else { ctx.continueExtending = true; } From 95119936b336ea2a501ac17e5a09d42c1fc94691 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 5 Aug 2026 00:27:55 +0200 Subject: [PATCH 6/8] missing files and style fix --- .../region/monotonicity/Assumption.cpp | 14 +++++++++++ .../region/monotonicity/Assumption.h | 24 +++++++++++++++++++ .../region/monotonicity/AssumptionChecker.h | 7 +++--- .../region/monotonicity/AssumptionMaker.h | 8 +++---- .../region/monotonicity/MonotonicityHelper.h | 12 +++++----- .../region/monotonicity/OrderExtender.cpp | 2 +- 6 files changed, 53 insertions(+), 14 deletions(-) create mode 100644 src/storm-pars/modelchecker/region/monotonicity/Assumption.cpp create mode 100644 src/storm-pars/modelchecker/region/monotonicity/Assumption.h diff --git a/src/storm-pars/modelchecker/region/monotonicity/Assumption.cpp b/src/storm-pars/modelchecker/region/monotonicity/Assumption.cpp new file mode 100644 index 0000000000..966f668cd6 --- /dev/null +++ b/src/storm-pars/modelchecker/region/monotonicity/Assumption.cpp @@ -0,0 +1,14 @@ +#include "storm-pars/modelchecker/region/monotonicity/Assumption.h" + +#include "storm/utility/macros.h" + +namespace storm { +namespace analysis { + +std::ostream& operator<<(std::ostream& out, Assumption const& assumption) { + out << "s" << assumption.state1 << (assumption.relation == storm::expressions::RelationType::Greater ? " > s" : " = s") << assumption.state2; + return out; +} + +} // namespace analysis +} // namespace storm diff --git a/src/storm-pars/modelchecker/region/monotonicity/Assumption.h b/src/storm-pars/modelchecker/region/monotonicity/Assumption.h new file mode 100644 index 0000000000..cb14a41876 --- /dev/null +++ b/src/storm-pars/modelchecker/region/monotonicity/Assumption.h @@ -0,0 +1,24 @@ +#pragma once + +#include +#include + +#include "storm/storage/expressions/BinaryRelationType.h" + +namespace storm { +namespace analysis { + +/*! + * A candidate relation between two states of a reachability order: either state1 > state2 + * (Greater) or state1 == state2 (Equal). Only these two relation types are supported. + */ +struct Assumption { + uint64_t state1; + uint64_t state2; + storm::expressions::RelationType relation; +}; + +std::ostream& operator<<(std::ostream& out, Assumption const& assumption); + +} // namespace analysis +} // namespace storm diff --git a/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.h b/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.h index 18d23bd7c4..255ac2e21f 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.h +++ b/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.h @@ -1,14 +1,15 @@ #pragma once -#include "Assumption.h" -#include "Order.h" -#include "storm-pars/storage/ParameterRegion.h" #include "storm/environment/Environment.h" #include "storm/logic/Formula.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" #include "storm/storage/SparseMatrix.h" +#include "storm-pars/modelchecker/region/monotonicity/Assumption.h" +#include "storm-pars/modelchecker/region/monotonicity/Order.h" +#include "storm-pars/storage/ParameterRegion.h" + namespace storm { namespace analysis { /*! diff --git a/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h b/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h index 9d52f87bdb..09ca0b9baa 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h +++ b/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h @@ -1,12 +1,12 @@ #pragma once -#include "Assumption.h" -#include "AssumptionChecker.h" -#include "Order.h" - #include "storm/storage/SparseMatrix.h" #include "storm/storage/expressions/BinaryRelationType.h" +#include "storm-pars/modelchecker/region/monotonicity/Assumption.h" +#include "storm-pars/modelchecker/region/monotonicity/AssumptionChecker.h" +#include "storm-pars/modelchecker/region/monotonicity/Order.h" + namespace storm { namespace analysis { diff --git a/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.h b/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.h index d25e2f5076..0142b6caea 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.h +++ b/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.h @@ -1,12 +1,6 @@ #pragma once #include -#include "Assumption.h" -#include "AssumptionMaker.h" -#include "LocalMonotonicityResult.h" -#include "MonotonicityResult.h" -#include "Order.h" -#include "OrderExtender.h" #include "storm/logic/Formula.h" @@ -23,6 +17,12 @@ #include "storm/utility/constants.h" #include "storm-pars/api/region.h" +#include "storm-pars/modelchecker/region/monotonicity/Assumption.h" +#include "storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h" +#include "storm-pars/modelchecker/region/monotonicity/LocalMonotonicityResult.h" +#include "storm-pars/modelchecker/region/monotonicity/MonotonicityResult.h" +#include "storm-pars/modelchecker/region/monotonicity/Order.h" +#include "storm-pars/modelchecker/region/monotonicity/OrderExtender.h" namespace storm { namespace analysis { diff --git a/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp b/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp index 4eac4693d6..493d514d85 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp @@ -1,4 +1,4 @@ -#include "OrderExtender.h" +#include "storm-pars/modelchecker/region/monotonicity/OrderExtender.h" #include #include "storm/exceptions/NotSupportedException.h" From 1d39a7377daa85c5154d902e2b008b0f6a9779ad Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 5 Aug 2026 10:15:29 +0200 Subject: [PATCH 7/8] cut some crap --- .../monotonicity/MonotonicityHelper.cpp | 23 ++++++++----------- .../region/monotonicity/Order.cpp | 9 +++----- .../region/monotonicity/OrderExtender.cpp | 4 ---- .../region/monotonicity/OrderExtender.h | 4 ++-- 4 files changed, 15 insertions(+), 25 deletions(-) diff --git a/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.cpp b/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.cpp index 0a8ba7b1e4..077c6ed808 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.cpp @@ -195,12 +195,10 @@ template void MonotonicityHelper::extendOrderWithAssumptions(std::shared_ptr order, uint_fast64_t val1, uint_fast64_t val2, std::vector assumptions, std::shared_ptr> monRes) { - // Explicit worklist instead of recursion: each unresolved (val1, val2) pair can spawn up to - // three independent branches (one per candidate assumption), and pathological pMCs can chain - // enough of these to overflow the C++ call stack if done recursively. The branches are pushed - // in reverse so popping (LIFO) visits them in the same left-to-right order the original - // recursion did; that's not required for correctness (branches share no mutable state) but - // keeps behavior close to before while validating this change. + // Algorithm 2 spawns up to three branches per unresolved (val1, val2) pair, one per candidate + // assumption. The worklist keeps this iterative so that pMCs chaining many such ambiguities + // cannot overflow the call stack. Branches are pushed in reverse so popping (LIFO) visits + // them depth-first, left to right. struct PendingBranch { std::shared_ptr order; uint_fast64_t val1; @@ -250,11 +248,10 @@ void MonotonicityHelper::extendOrderWithAssumptions(std } STORM_LOG_INFO(" Created " << newAssumptions.size() << " assumptions, we continue extending the current order"); - // Prepare branches in forward order, exactly mirroring the original recursion's execution - // order: candidates 0..size-2 each get an independent copy of current.order/monRes (so - // extending one cannot affect another), while the last candidate reuses - // current.order/monRes in place. That in-place mutation must happen last, after every - // other candidate has already taken its copy from the still-pristine original. + // Candidates 0..size-2 each get an independent copy of current.order/monRes, so extending + // one cannot affect another; the last candidate reuses current.order/monRes in place. + // That in-place mutation must happen last, after every other candidate has already taken + // its copy from the still-pristine original. std::vector preparedBranches; preparedBranches.reserve(newAssumptions.size()); for (size_t i = 0; i < newAssumptions.size(); ++i) { @@ -273,8 +270,8 @@ void MonotonicityHelper::extendOrderWithAssumptions(std preparedBranches.push_back( {std::get<0>(criticalTuple), std::get<1>(criticalTuple), std::get<2>(criticalTuple), std::move(branchAssumptions), branchMonRes}); } - // Push in reverse so the first-prepared branch ends up on top of the stack and is explored - // first, matching the original left-to-right visitation order. + // Pushed in reverse so the first-prepared branch ends up on top of the stack and is + // explored first, i.e., depth-first, left to right. for (auto it = preparedBranches.rbegin(); it != preparedBranches.rend(); ++it) { worklist.push_back(std::move(*it)); } diff --git a/src/storm-pars/modelchecker/region/monotonicity/Order.cpp b/src/storm-pars/modelchecker/region/monotonicity/Order.cpp index 2ad65c8417..8bec99b8d3 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/Order.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/Order.cpp @@ -202,8 +202,6 @@ void Order::addBetween(uint_fast64_t state, Node* above, Node* below) { } void Order::addBetween(uint_fast64_t state, uint_fast64_t above, uint_fast64_t below) { - // No compare(above, below) == ABOVE check here: addBetween(state, Node*, Node*) below checks - // that itself (and is also called directly by other sites, so it can't drop that check). STORM_LOG_ASSERT(getNode(below)->states.find(below) != getNode(below)->states.end(), "State " << below << " is not in its own node."); STORM_LOG_ASSERT(getNode(above)->states.find(above) != getNode(above)->states.end(), "State " << above << " is not in its own node."); @@ -340,10 +338,9 @@ Order::NodeComparison Order::compare(Node* node1, Node* node2, NodeComparison hy return comp; } if ((hypothesis == UNKNOWN || hypothesis == ABOVE) && above(node1, node2)) { - // Deliberately no assertion here that above(node2, node1) doesn't also hold: mergeNodes's - // own O(n^2) revalidation loop calls compare(i, j) and compare(j, i) on every pair - // specifically to detect and gracefully reject merges that would produce this kind of - // mutual-above inconsistency; that detection must be allowed to complete undisturbed. + // This does not require !above(node2, node1): mergeNodes calls compare() on every + // pair in both directions to detect exactly that antisymmetry violation and reject + // the merge, so this function must tolerate it transiently rather than fail here. return ABOVE; } diff --git a/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp b/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp index 493d514d85..65951f9bcc 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp @@ -374,10 +374,6 @@ std::tuple, uint_fast64_t, uint_fast64_t> OrderExtendergetDoneBuilding(), "Expected the order to be fully built at this point."); diff --git a/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.h b/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.h index aed1bdaf79..27d802057b 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.h +++ b/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.h @@ -109,8 +109,8 @@ class OrderExtender { // Per-in-progress-order bookkeeping used while extending an order (PLA bounds, whether PLA is // usable/worth continuing, and the pair of states this order got stuck on, if any). Keyed by - // weak_ptr rather than shared_ptr so that this bookkeeping does not itself keep an order alive - // or inflate its use_count() while it is still being extended. + // weak_ptr so this bookkeeping neither keeps an order alive nor inflates its use_count() + // while the order is still being extended. struct Context { std::vector minValues; std::vector maxValues; From a170ba88d3d8ebd05c6b6df383187eb0b57295a6 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 8 Aug 2026 20:13:11 +0200 Subject: [PATCH 8/8] Assert Greater/Equal relation in Assumption checkOnSamples and operator<< Both silently treated any non-Greater relation as Equal, per Copilot review comments. --- src/storm-pars/modelchecker/region/monotonicity/Assumption.cpp | 2 ++ .../modelchecker/region/monotonicity/AssumptionChecker.cpp | 2 ++ 2 files changed, 4 insertions(+) diff --git a/src/storm-pars/modelchecker/region/monotonicity/Assumption.cpp b/src/storm-pars/modelchecker/region/monotonicity/Assumption.cpp index 966f668cd6..436234668a 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/Assumption.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/Assumption.cpp @@ -6,6 +6,8 @@ namespace storm { namespace analysis { std::ostream& operator<<(std::ostream& out, Assumption const& assumption) { + STORM_LOG_ASSERT(assumption.relation == storm::expressions::RelationType::Greater || assumption.relation == storm::expressions::RelationType::Equal, + "Only Greater or Equal assumptions are supported."); out << "s" << assumption.state1 << (assumption.relation == storm::expressions::RelationType::Greater ? " > s" : " = s") << assumption.state2; return out; } diff --git a/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.cpp b/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.cpp index 9fa6c5f10e..68042435c1 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.cpp @@ -115,6 +115,8 @@ AssumptionStatus AssumptionChecker::validateAssumption( template AssumptionStatus AssumptionChecker::checkOnSamples(Assumption const& assumption) const { + STORM_LOG_ASSERT(assumption.relation == expressions::RelationType::Greater || assumption.relation == expressions::RelationType::Equal, + "Only Greater or Equal assumptions are supported."); auto result = AssumptionStatus::UNKNOWN; for (auto const& values : samples) { bool holds = assumption.relation == expressions::RelationType::Greater ? values[assumption.state1] > values[assumption.state2]