From 8cee934a2b32bed1231b462d5b44f1f29d0b8265 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 6 Aug 2026 18:43:41 +0000 Subject: [PATCH 1/4] Initial plan From d017de37d40f5c3aca48961a6cb78dc4848cae1a Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 6 Aug 2026 20:31:32 +0000 Subject: [PATCH 2/4] Fix: use phiStates in computeAllTransientProbabilities to correctly absorb non-phi states Co-authored-by: sjunges <13627276+sjunges@users.noreply.github.com> --- .../modelchecker/csl/helper/SparseCtmcCslHelper.cpp | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 04a56a0dff..4c7d7f2bf5 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -522,18 +522,16 @@ std::vector SparseCtmcCslHelper::computeAllTransientProbabilities(Env // Create the result vector. std::vector result = std::vector(numberOfStates, storm::utility::zero()); + // States that are psi are absorbing; states that are neither phi nor psi are also absorbing + // (paths must stay within phiStates until psiStates is reached) + storm::storage::BitVector absorbingStates = ~phiStates | psiStates; storm::storage::SparseMatrix transposedMatrix(rateMatrix); - transposedMatrix.makeRowsAbsorbing(psiStates); + transposedMatrix.makeRowsAbsorbing(absorbingStates); std::vector newRates = exitRates; - for (auto state : psiStates) { + for (auto state : absorbingStates) { newRates[state] = storm::utility::one(); } - // Identify all maybe states which have a probability greater than 0 to be reached from the initial state. - // storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(transposedMatrix, phiStates, initialStates); - // STORM_LOG_INFO("Found " << statesWithProbabilityGreater0.getNumberOfSetBits() << " states with probability greater 0."); - - // storm::storage::BitVector relevantStates = statesWithProbabilityGreater0 & ~initialStates;//phiStates | psiStates; storm::storage::BitVector relevantStates(numberOfStates, true); STORM_LOG_DEBUG(relevantStates.getNumberOfSetBits() << " relevant states."); From a7637d8d904b81ccac3e939db27eed6773c9c2ed Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 7 Aug 2026 12:00:27 +0000 Subject: [PATCH 3/4] Add test: TransientProbabilitiesWithPhiStates verifying phiStates fix; fix existing test to use phiStates=all Co-authored-by: sjunges <13627276+sjunges@users.noreply.github.com> --- .../csl/CtmcCslModelCheckerTest.cpp | 37 ++++++++++++++++++- 1 file changed, 36 insertions(+), 1 deletion(-) diff --git a/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp index 8a50c0e6a5..328cf77b35 100644 --- a/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp @@ -520,7 +520,8 @@ TEST(CtmcCslModelCheckerTest, TransientProbabilities) { std::vector exitRates = {3, 2}; storm::storage::BitVector initialStates(2); initialStates.set(0); - storm::storage::BitVector phiStates(2); + // phiStates = all states (true U ...), psiStates = empty (computing transient distribution) + storm::storage::BitVector phiStates(2, true); storm::storage::BitVector psiStates(2); storm::Environment env; std::vector result = @@ -530,6 +531,40 @@ TEST(CtmcCslModelCheckerTest, TransientProbabilities) { EXPECT_NEAR(0.595957, result[1], 1e-6); } +TEST(CtmcCslModelCheckerTest, TransientProbabilitiesWithPhiStates) { + // 3-state CTMC: state 0 -> state 1 (rate 3), state 1 -> state 2 (rate 2), state 2 -> state 0 (rate 1) + // We test that phiStates is correctly applied: if state 1 is not in phiStates, + // probability mass starting in state 0 should not propagate to state 2 via state 1. + storm::storage::SparseMatrixBuilder matrixBuilder; + matrixBuilder.addNextValue(0, 1, 3.0); + matrixBuilder.addNextValue(1, 2, 2.0); + matrixBuilder.addNextValue(2, 0, 1.0); + storm::storage::SparseMatrix matrix = matrixBuilder.build(); + + std::vector exitRates = {3, 2, 1}; + storm::storage::BitVector initialStates(3); + initialStates.set(0); + storm::Environment env; + + // phiStates excludes state 1: state 1 is absorbing, so probability cannot reach state 2 + storm::storage::BitVector phiStatesRestricted(3, true); + phiStatesRestricted.set(1, false); + storm::storage::BitVector psiStates(3); + std::vector resultRestricted = storm::modelchecker::helper::SparseCtmcCslHelper::computeAllTransientProbabilities( + env, matrix, initialStates, phiStatesRestricted, psiStates, exitRates, 1.0); + + // With state 1 absorbing, probability can only flow from 0 to 1 but not further to 2 + EXPECT_NEAR(0.0, resultRestricted[2], 1e-6); + + // phiStates = all states: probability can flow freely through all states + storm::storage::BitVector phiStatesAll(3, true); + std::vector resultAll = storm::modelchecker::helper::SparseCtmcCslHelper::computeAllTransientProbabilities( + env, matrix, initialStates, phiStatesAll, psiStates, exitRates, 1.0); + + // With no restriction, some probability reaches state 2 + EXPECT_GT(resultAll[2], 1e-6); +} + TYPED_TEST(CtmcCslModelCheckerTest, LtlProbabilitiesEmbedded) { #ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT std::string formulasString = "P=? [ X F (!\"down\" U \"fail_sensors\") ]"; From c3eeb0eb7dea5551390a4ecaa1946b6166448c9a Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 8 Aug 2026 22:23:59 +0200 Subject: [PATCH 4/4] fix format --- src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp index 328cf77b35..cebee1aa1d 100644 --- a/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp @@ -558,8 +558,8 @@ TEST(CtmcCslModelCheckerTest, TransientProbabilitiesWithPhiStates) { // phiStates = all states: probability can flow freely through all states storm::storage::BitVector phiStatesAll(3, true); - std::vector resultAll = storm::modelchecker::helper::SparseCtmcCslHelper::computeAllTransientProbabilities( - env, matrix, initialStates, phiStatesAll, psiStates, exitRates, 1.0); + std::vector resultAll = + storm::modelchecker::helper::SparseCtmcCslHelper::computeAllTransientProbabilities(env, matrix, initialStates, phiStatesAll, psiStates, exitRates, 1.0); // With no restriction, some probability reaches state 2 EXPECT_GT(resultAll[2], 1e-6);