From 9e8d8a2c27796638cc2ec696ca63b3445f8df4c8 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 27 Jan 2015 14:15:56 +0100 Subject: [PATCH] Fixed wrong calculation of reachability rewards in state-elimination-based model checker. Former-commit-id: bee99d61b04059854a5109f2c0a1de07fa7dff17 --- .../SparseDtmcEliminationModelChecker.cpp | 28 ++++++++----------- .../SparseDtmcEliminationModelCheckerTest.cpp | 2 +- 2 files changed, 13 insertions(+), 17 deletions(-) diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 8f3659eab..fcf1067c0 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -270,15 +270,15 @@ namespace storm { // Sort the states according to the priorities. std::sort(states.begin(), states.end(), [&statePriorities] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statePriorities[a] < statePriorities[b]; }); - STORM_PRINT_AND_LOG("Computing conditional probilities." << std::endl); - STORM_PRINT_AND_LOG("Eliminating " << states.size() << " states using the state elimination technique." << std::endl); + STORM_LOG_INFO("Computing conditional probilities." << std::endl); + STORM_LOG_INFO("Eliminating " << states.size() << " states using the state elimination technique." << std::endl); boost::optional> missingStateRewards; FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(submatrix); FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(submatrixTransposed, true); for (auto const& state : states) { eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, missingStateRewards); } - STORM_PRINT_AND_LOG("Eliminated " << states.size() << " states." << std::endl); + STORM_LOG_INFO("Eliminated " << states.size() << " states." << std::endl); eliminateState(flexibleMatrix, oneStepProbabilities, *newInitialStates.begin(), flexibleBackwardTransitions, missingStateRewards, false); @@ -363,8 +363,6 @@ namespace storm { FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(backwardTransitions, true); auto conversionEnd = std::chrono::high_resolution_clock::now(); - flexibleMatrix.print(); - std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now(); uint_fast64_t maximalDepth = 0; if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State) { @@ -379,16 +377,16 @@ namespace storm { std::sort(states.begin(), states.end(), [&statePriorities] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statePriorities.get()[a] < statePriorities.get()[b]; }); } - STORM_PRINT_AND_LOG("Eliminating " << states.size() << " states using the state elimination technique." << std::endl); + STORM_LOG_INFO("Eliminating " << states.size() << " states using the state elimination technique." << std::endl); for (auto const& state : states) { eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards); } - STORM_PRINT_AND_LOG("Eliminated " << states.size() << " states." << std::endl); + STORM_LOG_INFO("Eliminated " << states.size() << " states." << std::endl); } else if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) { // When using the hybrid technique, we recursively treat the SCCs up to some size. storm::utility::ConstantsComparator comparator; std::vector entryStateQueue; - STORM_PRINT_AND_LOG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique." << std::endl); + STORM_LOG_INFO("Eliminating " << subsystem.size() << " states using the hybrid elimination technique." << std::endl); maximalDepth = treatScc(flexibleMatrix, oneStepProbabilities, initialStates, subsystem, transitionMatrix, flexibleBackwardTransitions, false, 0, storm::settings::sparseDtmcEliminationModelCheckerSettings().getMaximalSccSize(), entryStateQueue, comparator, stateRewards, statePriorities); // If the entry states were to be eliminated last, we need to do so now. @@ -398,14 +396,14 @@ namespace storm { eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards); } } - STORM_PRINT_AND_LOG("Eliminated " << subsystem.size() << " states." << std::endl); + STORM_LOG_INFO("Eliminated " << subsystem.size() << " states." << std::endl); } // Finally eliminate initial state. if (!stateRewards) { // If we are computing probabilities, then we can simply call the state elimination procedure. It // will scale the transition row of the initial state with 1/(1-loopProbability). - STORM_PRINT_AND_LOG("Eliminating initial state " << *initialStates.begin() << "." << std::endl); + STORM_LOG_INFO("Eliminating initial state " << *initialStates.begin() << "." << std::endl); eliminateState(flexibleMatrix, oneStepProbabilities, *initialStates.begin(), flexibleBackwardTransitions, stateRewards); } else { // If we are computing rewards, we cannot call the state elimination procedure for technical reasons. @@ -415,20 +413,17 @@ namespace storm { // of the initial state, this amounts to checking whether the outgoing transitions of the initial // state are non-empty. if (!flexibleMatrix.getRow(*initialStates.begin()).empty()) { - flexibleMatrix.print(); STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).size() == 1, "At most one outgoing transition expected at this point, but found more."); STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).front().getColumn() == *initialStates.begin(), "Remaining entry should be a self-loop, but it is not."); ValueType loopProbability = flexibleMatrix.getRow(*initialStates.begin()).front().getValue(); loopProbability = storm::utility::one() / (storm::utility::one() - loopProbability); - loopProbability = storm::utility::pow(loopProbability, 2); - STORM_PRINT_AND_LOG("Scaling the transition reward of the initial state."); + STORM_LOG_INFO("Scaling the reward of the initial state " << stateRewards.get()[(*initialStates.begin())] << " with " << loopProbability); stateRewards.get()[(*initialStates.begin())] *= loopProbability; flexibleMatrix.getRow(*initialStates.begin()).clear(); } } // Make sure that we have eliminated all transitions from the initial state. - flexibleMatrix.print(); STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).empty(), "The transitions of the initial states are non-empty."); std::chrono::high_resolution_clock::time_point modelCheckingEnd = std::chrono::high_resolution_clock::now(); @@ -621,7 +616,7 @@ namespace storm { STORM_LOG_DEBUG("Eliminating state " << state << "."); if (counter > matrix.getNumberOfRows() / 10) { ++chunkCounter; - STORM_PRINT_AND_LOG("Eliminated " << (chunkCounter * 10) << "% of the states." << std::endl); + STORM_LOG_INFO("Eliminated " << (chunkCounter * 10) << "% of the states." << std::endl); counter = 0; } @@ -744,7 +739,8 @@ namespace storm { // If we are computing rewards, we basically scale the state reward of the state to eliminate and // add the result to the state reward of the predecessor. if (hasSelfLoop) { - stateRewards.get()[predecessor] += storm::utility::simplify(multiplyFactor * storm::utility::pow(loopProbability, 2) * stateRewards.get()[state]); +// stateRewards.get()[predecessor] += storm::utility::simplify(multiplyFactor * storm::utility::pow(loopProbability, 2) * stateRewards.get()[state]); + stateRewards.get()[predecessor] += storm::utility::simplify(multiplyFactor * loopProbability * stateRewards.get()[state]); } else { stateRewards.get()[predecessor] += storm::utility::simplify(multiplyFactor * stateRewards.get()[state]); } diff --git a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp index 04e944f8c..01a1a9c94 100644 --- a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp @@ -116,5 +116,5 @@ TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) { result = checker.check(*reachabilityRewardFormula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(1.044879046, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1.0448979, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); }