From c7bdf7fa516f04437b342eeed21348658c4f5b16 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 13 Aug 2026 11:46:04 +0200 Subject: [PATCH 1/4] Fix clang-tidy.sh path resolution for relative arguments --- resources/scripts/clang-tidy.sh | 48 ++++++++++++++++++++++++++------- 1 file changed, 39 insertions(+), 9 deletions(-) diff --git a/resources/scripts/clang-tidy.sh b/resources/scripts/clang-tidy.sh index 7bed3b9b41..a57fd2a155 100755 --- a/resources/scripts/clang-tidy.sh +++ b/resources/scripts/clang-tidy.sh @@ -23,7 +23,8 @@ Selection: ...HEAD plus untracked files. ... Only check the given files. Arguments are treated as literal paths (matched as a substring of the recorded - absolute path), relative to the repository root or absolute. + absolute path), relative to the current directory or + absolute. (neither) Check the whole code base (the default). Options: @@ -81,22 +82,49 @@ is_source_file() { is_cpp_file "$1" || is_header_file "$1" } -# Reads newline-separated repository-relative paths from stdin and fills the -# globals $files (displayable) and $regex (escaped absolute paths, '|'-joined). +# Collapse redundant '.' and '..' path segments lexically, without resolving +# symlinks, so that paths such as "$root/../src/foo.h" produce the same +# absolute path as recorded in the compilation database. +normalize_path() { + local path=$1 out="/" seg + local -a parts + IFS='/' read -r -a parts <<< "$path" + for seg in "${parts[@]}"; do + case "$seg" in + ''|'.') : ;; + '..') out=${out%/*} ;; + *) out="${out%/}/$seg" ;; + esac + done + printf '%s' "${out:-/}" +} + +# Reads newline-separated paths from stdin and fills the globals $files +# (displayable) and $regex (escaped absolute paths, '|'-joined). +# Relative paths are resolved against the current directory ($1 = "cwd", for +# explicit file arguments) or against the repository root ($1 = "repo", for +# the repo-relative paths produced by git). files=() regex="" has_cpp=0 has_header=0 build_file_lists() { - local root file escaped + local mode=$1 root file abs escaped root=$(git_ rev-parse --show-toplevel) || die "not inside a git repository" while IFS= read -r file; do [ -z "$file" ] && continue is_source_file "$file" || continue case "$file" in - /*) escaped=$(escape_regex "$file") ;; - *) escaped=$(escape_regex "$root/$file") ;; + /*) abs=$file ;; + *) + if [ "$mode" = "cwd" ]; then + abs="$PWD/$file" + else + abs="$root/$file" + fi + ;; esac + escaped=$(escape_regex "$(normalize_path "$abs")") regex="${regex:+$regex|}${escaped}" files+=("$file") is_cpp_file "$file" && has_cpp=1 @@ -208,7 +236,7 @@ fi echo "Using run-clang-tidy executable: $run_clang_tidy_bin" if [ "$git_ref_mode" -eq 1 ]; then - build_file_lists < <(changed_files "$git_ref") + build_file_lists repo < <(changed_files "$git_ref") if [ "${#files[@]}" -eq 0 ]; then echo "No source files changed relative to $git_ref; nothing to check." exit 0 @@ -216,7 +244,7 @@ if [ "$git_ref_mode" -eq 1 ]; then echo "Checking ${#files[@]} file(s) changed relative to $git_ref:" printf ' %s\n' "${files[@]}" elif [ "$#" -gt 0 ]; then - build_file_lists < <(printf '%s\n' "$@") + build_file_lists cwd < <(printf '%s\n' "$@") if [ "${#files[@]}" -eq 0 ]; then echo "No source files selected; nothing to check." exit 0 @@ -239,7 +267,9 @@ args=() if [ "$dry_run" -eq 1 ]; then printf 'PYTHONUNBUFFERED=1 %s' "$run_clang_tidy_bin" - printf ' %q' "${args[@]}" + for a in "${args[@]}"; do + printf ' %q' "$a" + done if [ "${#files[@]}" -gt 0 ]; then printf ' %q' "$regex" fi From 744d030676d4e318989013e21a1a8bb37d0acb36 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 14 Aug 2026 13:28:14 +0200 Subject: [PATCH 2/4] Clang-tidy: enable bugprone checks with no current warnings --- .clang-tidy | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/.clang-tidy b/.clang-tidy index 5123c5e488..0a34e24793 100644 --- a/.clang-tidy +++ b/.clang-tidy @@ -2,18 +2,18 @@ # Disable everything first, then enable individual checks. Checks: >- -*, + bugprone-dangling-handle, + bugprone-infinite-loop, + bugprone-misplaced-widening-cast, + bugprone-signed-char-misuse, + bugprone-unused-return-value, + bugprone-virtual-near-miss, readability-braces-around-statements # Candidate checks that are not (yet) enabled: # bugprone-branch-clone, # bugprone-copy-constructor-init, -# bugprone-dangling-handle, -# bugprone-infinite-loop, -# bugprone-misplaced-widening-cast, # bugprone-redundant-expression, -# bugprone-signed-char-misuse, -# bugprone-unused-return-value, # bugprone-use-after-move, -# bugprone-virtual-near-miss, # clang-analyzer-core.*, # clang-analyzer-cplusplus.*, # clang-analyzer-deadcode.*, From 155dad591ae17261b809ee7a07b4ad07a6646ad4 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 14 Aug 2026 13:21:34 +0200 Subject: [PATCH 3/4] Fixed bugs revealed by clang-tidy bugprone-use-after-move --- .clang-tidy | 2 +- .../generator/DftNextStateGenerator.cpp | 2 ++ .../monotonicity/MonotonicityResult.cpp | 12 +++++--- ...SparseDeterministicVisitingTimesHelper.cpp | 5 ++-- .../prctl/helper/SparseDtmcPrctlHelper.cpp | 4 ++- .../prctl/helper/SparseMdpPrctlHelper.cpp | 30 +++++++++++-------- src/storm/models/sparse/Ctmc.cpp | 2 ++ src/storm/models/sparse/MarkovAutomaton.cpp | 2 ++ src/storm/models/sparse/Model.cpp | 2 +- src/storm/models/sparse/Smg.cpp | 2 ++ .../models/sparse/StochasticTwoPlayerGame.cpp | 4 ++- .../storage/jani/visitor/JSONExporter.cpp | 10 +++---- .../SparseModelMemoryProduct.cpp | 2 +- .../storage/valuations/ValuationsStorage.cpp | 4 +-- .../prctl/dtmc/DtmcPrctlModelCheckerTest.cpp | 3 +- 15 files changed, 54 insertions(+), 32 deletions(-) diff --git a/.clang-tidy b/.clang-tidy index 0a34e24793..e080291abf 100644 --- a/.clang-tidy +++ b/.clang-tidy @@ -7,13 +7,13 @@ Checks: >- bugprone-misplaced-widening-cast, bugprone-signed-char-misuse, bugprone-unused-return-value, + bugprone-use-after-move, bugprone-virtual-near-miss, readability-braces-around-statements # Candidate checks that are not (yet) enabled: # bugprone-branch-clone, # bugprone-copy-constructor-init, # bugprone-redundant-expression, -# bugprone-use-after-move, # clang-analyzer-core.*, # clang-analyzer-cplusplus.*, # clang-analyzer-deadcode.*, diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 5f9bd249a1..ba9cde8207 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -130,6 +130,8 @@ storm::generator::StateBehavior DftNextStateGeneratorname()); } result.addChoice(std::move(choice)); + // Start a fresh choice for the next conflicting dependency. + choice = storm::generator::Choice(0, !exploreDependencies); // Handle premature stop for dependencies if (!iterFailable.isConflictingDependency()) { diff --git a/src/storm-pars/modelchecker/region/monotonicity/MonotonicityResult.cpp b/src/storm-pars/modelchecker/region/monotonicity/MonotonicityResult.cpp index f2df02f460..a77c5f2b31 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/MonotonicityResult.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/MonotonicityResult.cpp @@ -18,7 +18,7 @@ MonotonicityResult::MonotonicityResult() { template void MonotonicityResult::addMonotonicityResult(VariableType var, MonotonicityResult::Monotonicity mon) { - monotonicityResult.insert(std::pair::Monotonicity>(std::move(var), std::move(mon))); + monotonicityResult.insert(std::pair::Monotonicity>(std::move(var), mon)); } template @@ -27,7 +27,7 @@ void MonotonicityResult::updateMonotonicityResult(VariableType var if (force) { STORM_LOG_ASSERT(mon == MonotonicityResult::Monotonicity::Not, "Expected Not monotonicity for force."); if (monotonicityResult.find(var) == monotonicityResult.end()) { - addMonotonicityResult(std::move(var), std::move(mon)); + addMonotonicityResult(std::move(var), mon); } else { monotonicityResult[var] = mon; } @@ -36,8 +36,10 @@ void MonotonicityResult::updateMonotonicityResult(VariableType var mon = MonotonicityResult::Monotonicity::Unknown; } + bool unknownMon = false; if (monotonicityResult.find(var) == monotonicityResult.end()) { - addMonotonicityResult(std::move(var), std::move(mon)); + addMonotonicityResult(std::move(var), mon); + unknownMon = (mon == MonotonicityResult::Monotonicity::Unknown); } else { auto monRes = monotonicityResult[var]; if (monRes == MonotonicityResult::Monotonicity::Unknown || monRes == mon || @@ -45,11 +47,13 @@ void MonotonicityResult::updateMonotonicityResult(VariableType var return; } else if (mon == MonotonicityResult::Monotonicity::Unknown || monRes == MonotonicityResult::Monotonicity::Constant) { monotonicityResult[var] = mon; + unknownMon = (mon == MonotonicityResult::Monotonicity::Unknown); } else { monotonicityResult[var] = MonotonicityResult::Monotonicity::Unknown; + unknownMon = true; } } - if (monotonicityResult[var] == MonotonicityResult::Monotonicity::Unknown) { + if (unknownMon) { setAllMonotonicity(false); setSomewhereMonotonicity(false); } else { diff --git a/src/storm/modelchecker/helper/indefinitehorizon/visitingtimes/SparseDeterministicVisitingTimesHelper.cpp b/src/storm/modelchecker/helper/indefinitehorizon/visitingtimes/SparseDeterministicVisitingTimesHelper.cpp index 611baef01f..3f6da0c00f 100644 --- a/src/storm/modelchecker/helper/indefinitehorizon/visitingtimes/SparseDeterministicVisitingTimesHelper.cpp +++ b/src/storm/modelchecker/helper/indefinitehorizon/visitingtimes/SparseDeterministicVisitingTimesHelper.cpp @@ -471,6 +471,8 @@ std::vector SparseDeterministicVisitingTimesHelper::comput } // Get the solver object and satisfy requirements + // The solver consumes the matrix, so the acyclic check must be performed before moving it. + bool const hasCycles = storm::utility::graph::hasCycle(sccMatrix); auto solver = linearEquationSolverFactory.create(env, std::move(sccMatrix)); solver->setLowerBound(storm::utility::zero()); auto req = solver->getRequirements(env); @@ -483,8 +485,7 @@ std::vector SparseDeterministicVisitingTimesHelper::comput } if (req.acyclic().isCritical()) { - STORM_LOG_THROW(!storm::utility::graph::hasCycle(sccMatrix), storm::exceptions::UnmetRequirementException, - "The solver requires an acyclic model, but the model is not acyclic."); + STORM_LOG_THROW(!hasCycles, storm::exceptions::UnmetRequirementException, "The solver requires an acyclic model, but the model is not acyclic."); req.clearAcyclic(); } diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 4e4a217ae4..2e9e9b98c1 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -141,10 +141,12 @@ std::vector computeRobustValuesForMaybeStates(Environment const& e // Set up the solver. storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; + // The goal is consumed by the solver configuration, so capture what is needed first. + auto const uncertaintyResolutionMode = goal.getUncertaintyResolutionMode(); std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver( env, std::move(goal), minMaxLinearEquationSolverFactory, std::move(submatrix), convert(OptimizationDirection::Maximize)); // default to maximize for IDTMCs; does not affect the result - solver->setUncertaintyResolutionMode(goal.getUncertaintyResolutionMode()); + solver->setUncertaintyResolutionMode(uncertaintyResolutionMode); solver->setHasUniqueSolution(computeReward); // As we check for graph-preservation, in case of rewards on IDTMCs, we have a unique solution solver->setHasNoEndComponents(false); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 5182fc9c2f..084bb836dc 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -436,12 +436,14 @@ MaybeStateResult computeValuesForMaybeStates(Environment const& en : std::vector(submatrix.getRowGroupCount(), hint.hasLowerResultBound() ? hint.getLowerResultBound() : storm::utility::zero()); + // Capture the uncertainty resolution mode before the goal is consumed by the solver configuration. + auto const uncertaintyResolutionMode = goal.getUncertaintyResolutionMode(); // Set up the solver. storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(env, std::move(goal), minMaxLinearEquationSolverFactory, std::move(submatrix)); solver->setRequirementsChecked(); - solver->setUncertaintyResolutionMode(goal.getUncertaintyResolutionMode()); + solver->setUncertaintyResolutionMode(uncertaintyResolutionMode); solver->setHasUniqueSolution(hint.hasUniqueSolution()); solver->setHasNoEndComponents(hint.hasNoEndComponents()); if (hint.hasLowerResultBound()) { @@ -578,14 +580,13 @@ void extractSchedulerChoices(storm::storage::Scheduler& scheduler, } template -void extendScheduler(storm::storage::Scheduler& scheduler, storm::solver::SolveGoal const& goal, - QualitativeStateSetsUntilProbabilities const& qualitativeStateSets, storm::storage::SparseMatrix const& transitionMatrix, - storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, - storm::storage::BitVector const& psiStates) { +void extendScheduler(storm::storage::Scheduler& scheduler, bool minimize, QualitativeStateSetsUntilProbabilities const& qualitativeStateSets, + storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // Finally, if we need to produce a scheduler, we also need to figure out the parts of the scheduler for // the states with probability 1 or 0 (depending on whether we maximize or minimize). // We also need to define some arbitrary choice for the remaining states to obtain a fully defined scheduler. - if (goal.minimize()) { + if (minimize) { storm::utility::graph::computeSchedulerProb0E(qualitativeStateSets.statesWithProbability0, transitionMatrix, scheduler); for (auto prob1State : qualitativeStateSets.statesWithProbability1) { scheduler.setChoice(0, prob1State); @@ -704,6 +705,8 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper> scheduler; if (produceScheduler) { @@ -778,7 +781,7 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper -void extendScheduler(storm::storage::Scheduler& scheduler, storm::solver::SolveGoal const& goal, - QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, storm::storage::SparseMatrix const& transitionMatrix, - storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, - std::function const& zeroRewardChoicesGetter) { +void extendScheduler(storm::storage::Scheduler& scheduler, bool minimize, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, + storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, + storm::storage::BitVector const& targetStates, std::function const& zeroRewardChoicesGetter) { // Finally, if we need to produce a scheduler, we also need to figure out the parts of the scheduler for // the states with reward zero/infinity. - if (goal.minimize()) { + if (minimize) { storm::utility::graph::computeSchedulerProb1E(qualitativeStateSets.rewardZeroStates, transitionMatrix, backwardTransitions, qualitativeStateSets.rewardZeroStates, targetStates, scheduler, zeroRewardChoicesGetter()); for (auto state : qualitativeStateSets.infinityStates) { @@ -1374,6 +1376,8 @@ MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper SparseMdpPrctlHelper::Ctmc(storm::storage::sparse::ModelComponents Ctmc::Ctmc(storm::storage::sparse::ModelComponents&& components) : DeterministicModel(storm::models::ModelType::Ctmc, std::move(components)) { + // NOLINTBEGIN(bugprone-use-after-move) The base constructor only consumes the base-relevant fields of components. if (components.exitRates) { exitRates = std::move(components.exitRates.get()); } else { @@ -53,6 +54,7 @@ Ctmc::Ctmc(storm::storage::sparse::ModelComponentsgetTransitionMatrix().scaleRowsInPlace(exitRates); } + // NOLINTEND(bugprone-use-after-move) } template diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index c5fd21397e..6f0deb7f04 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -51,6 +51,7 @@ MarkovAutomaton::MarkovAutomaton(storm::storage::spa template MarkovAutomaton::MarkovAutomaton(storm::storage::sparse::ModelComponents&& components) : NondeterministicModel(ModelType::MarkovAutomaton, std::move(components)), + // NOLINTBEGIN(bugprone-use-after-move) The base constructor only consumes the base-relevant fields of components. markovianStates(std::move(components.markovianStates.get())) { if (components.exitRates) { exitRates = std::move(components.exitRates.get()); @@ -59,6 +60,7 @@ MarkovAutomaton::MarkovAutomaton(storm::storage::spa if (components.rateTransitions) { this->turnRatesToProbabilities(); } + // NOLINTEND(bugprone-use-after-move) closed = this->checkIsClosed(); } diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index 7bd2a879da..2b3d92208f 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -585,7 +585,7 @@ void Model::writeJsonToStream(std::ostream& outStrea } } if (!choiceRewardsJson.empty()) { - choiceRewardsJson["rew"] = std::move(choiceRewardsJson); + choiceJson["rew"] = std::move(choiceRewardsJson); } storm::json successors; for (auto const& entry : transitionMatrix.getRow(choiceIndex)) { diff --git a/src/storm/models/sparse/Smg.cpp b/src/storm/models/sparse/Smg.cpp index c381e135b7..c15a9fc80a 100644 --- a/src/storm/models/sparse/Smg.cpp +++ b/src/storm/models/sparse/Smg.cpp @@ -23,11 +23,13 @@ Smg::Smg(storm::storage::sparse::ModelComponents Smg::Smg(storm::storage::sparse::ModelComponents&& components) : NondeterministicModel(ModelType::Smg, std::move(components)), + // NOLINTBEGIN(bugprone-use-after-move) The base constructor only consumes the base-relevant fields of components. statePlayerIndications(std::move(components.statePlayerIndications.get())) { if (components.playerNameToIndexMap) { playerNameToIndexMap = std::move(components.playerNameToIndexMap.get()); } // Otherwise the map remains empty. + // NOLINTEND(bugprone-use-after-move) } template diff --git a/src/storm/models/sparse/StochasticTwoPlayerGame.cpp b/src/storm/models/sparse/StochasticTwoPlayerGame.cpp index c85bc0b163..1ea7c17012 100644 --- a/src/storm/models/sparse/StochasticTwoPlayerGame.cpp +++ b/src/storm/models/sparse/StochasticTwoPlayerGame.cpp @@ -37,7 +37,9 @@ StochasticTwoPlayerGame::StochasticTwoPlayerGame( template StochasticTwoPlayerGame::StochasticTwoPlayerGame(storm::storage::sparse::ModelComponents&& components) - : NondeterministicModel(ModelType::S2pg, std::move(components)), player1Matrix(std::move(components.player1Matrix.get())) { + : NondeterministicModel(ModelType::S2pg, std::move(components)), + // NOLINTNEXTLINE(bugprone-use-after-move) The base constructor only consumes the base-relevant fields of components. + player1Matrix(std::move(components.player1Matrix.get())) { // Intentionally left empty } diff --git a/src/storm/storage/jani/visitor/JSONExporter.cpp b/src/storm/storage/jani/visitor/JSONExporter.cpp index 921cfd2a4f..40cc6079b0 100644 --- a/src/storm/storage/jani/visitor/JSONExporter.cpp +++ b/src/storm/storage/jani/visitor/JSONExporter.cpp @@ -1068,11 +1068,11 @@ ExportJsonType buildLValue(storm::jani::LValue const& lValue, std::vector> Sparse if (model.isOfType(storm::models::ModelType::Ctmc)) { components.rateTransitions = true; } else if (model.isOfType(storm::models::ModelType::Mdp)) { - if (!preserveModelType && matrix.hasTrivialRowGrouping()) { + if (!preserveModelType && components.transitionMatrix.hasTrivialRowGrouping()) { targetModelType = storm::models::ModelType::Dtmc; } } else if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) { diff --git a/src/storm/storage/valuations/ValuationsStorage.cpp b/src/storm/storage/valuations/ValuationsStorage.cpp index 34433973fb..29d30c5121 100644 --- a/src/storm/storage/valuations/ValuationsStorage.cpp +++ b/src/storm/storage/valuations/ValuationsStorage.cpp @@ -161,7 +161,7 @@ ValuationsStorage::ValuationsStorage(uint64_t const numEntities, std::vectorstringMapping.push_back(0); } STORM_LOG_ASSERT(hasStringVariable || this->stringMapping.empty(), "Non-empty string mapping given but there is no string variable."); - STORM_LOG_ASSERT(stringMapping.empty() || this->stringMapping.back() == strings.size(), + STORM_LOG_ASSERT(this->stringMapping.empty() || this->stringMapping.back() == this->strings.size(), "String mapping should end with the total size of the string data."); // Enable quick access to the right byte span for each entity. @@ -185,7 +185,7 @@ ValuationsStorage::ValuationsStorage(uint64_t const numEntities, std::vectorvariableClasses.front().sizeInBytes == 0 || this->valuations.size() % this->variableClasses.front().sizeInBytes == 0, "Valuation data size is not a multiple of the unique valuation size."); STORM_LOG_ASSERT(numEntities * this->variableClasses.front().sizeInBytes == this->valuations.size(), - "Valuation data size (" << valuations.size() << ") does not match number of entities (" << this->numEntities + "Valuation data size (" << this->valuations.size() << ") does not match number of entities (" << this->numEntities << ") times valuation size (" << this->variableClasses.front().sizeInBytes << ")."); } } diff --git a/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp index a205617a87..5db1c76006 100644 --- a/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp @@ -828,7 +828,8 @@ TEST(DtmcPrctlModelCheckerTest, AllUntilProbabilities) { phiStates.set(6); psiStates.set(1); - result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeAllUntilProbabilities(env, std::move(goal), matrix, initialStates, phiStates, + storm::solver::SolveGoal goal2(*model, tasks[0]); + result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeAllUntilProbabilities(env, std::move(goal2), matrix, initialStates, phiStates, psiStates); EXPECT_NEAR(1, result[0], 1e-6); From ff008fe72e96cdfe41a54052353ac09649a8cd3b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 17 Aug 2026 13:51:45 +0200 Subject: [PATCH 4/4] Suggestion from tquatmann --- .../SparseDeterministicVisitingTimesHelper.cpp | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/storm/modelchecker/helper/indefinitehorizon/visitingtimes/SparseDeterministicVisitingTimesHelper.cpp b/src/storm/modelchecker/helper/indefinitehorizon/visitingtimes/SparseDeterministicVisitingTimesHelper.cpp index 3f6da0c00f..fe36910561 100644 --- a/src/storm/modelchecker/helper/indefinitehorizon/visitingtimes/SparseDeterministicVisitingTimesHelper.cpp +++ b/src/storm/modelchecker/helper/indefinitehorizon/visitingtimes/SparseDeterministicVisitingTimesHelper.cpp @@ -472,10 +472,16 @@ std::vector SparseDeterministicVisitingTimesHelper::comput // Get the solver object and satisfy requirements // The solver consumes the matrix, so the acyclic check must be performed before moving it. - bool const hasCycles = storm::utility::graph::hasCycle(sccMatrix); + auto req = linearEquationSolverFactory.getRequirements(env); + if (req.acyclic().isCritical()) { + // The solver consumes the matrix, so the acyclic check must be performed before moving it. + STORM_LOG_THROW(!storm::utility::graph::hasCycle(sccMatrix), storm::exceptions::UnmetRequirementException, + "The solver requires an acyclic model, but the model is not acyclic."); + req.clearAcyclic(); + } auto solver = linearEquationSolverFactory.create(env, std::move(sccMatrix)); solver->setLowerBound(storm::utility::zero()); - auto req = solver->getRequirements(env); + req = solver->getRequirements(env); req.clearLowerBounds(); if (req.upperBounds().isCritical()) { // Compute upper bounds on EVTs using techniques from Baier et al. [CAV'17] (https://doi.org/10.1007/978-3-319-63387-9_8) @@ -484,11 +490,6 @@ std::vector SparseDeterministicVisitingTimesHelper::comput req.clearUpperBounds(); } - if (req.acyclic().isCritical()) { - STORM_LOG_THROW(!hasCycles, storm::exceptions::UnmetRequirementException, "The solver requires an acyclic model, but the model is not acyclic."); - req.clearAcyclic(); - } - STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UnmetRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); std::vector eqSysValues(initialValues.size()); @@ -501,4 +502,4 @@ template class SparseDeterministicVisitingTimesHelper; template class SparseDeterministicVisitingTimesHelper; } // namespace helper } // namespace modelchecker -} // namespace storm \ No newline at end of file +} // namespace storm