From 0a68d8afa290e41472b9697b403c3f68b7a1b5f0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 29 Mar 2018 09:44:58 +0200 Subject: [PATCH] fixed out-of-bounds access in symbolic to explicit conversion of game-based abstraction --- src/storm/abstraction/MenuGameRefiner.cpp | 2 ++ .../modelchecker/abstraction/GameBasedMdpModelChecker.cpp | 4 ++-- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 76e528ee7..f8209ee99 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -672,6 +672,8 @@ namespace storm { if (!interpolant.isTrue() && !interpolant.isFalse()) { STORM_LOG_DEBUG("Derived new predicate (based on interpolation): " << interpolant); interpolants.push_back(interpolant); + } else { + STORM_LOG_TRACE("Found interpolant is '" << interpolant << "'."); } } return boost::make_optional(RefinementPredicates(RefinementPredicates::Source::Interpolation, interpolants)); diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 7dd306a81..35d838d55 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -680,12 +680,12 @@ namespace storm { std::vector player2BackwardTransitions(transitionMatrix.getRowGroupCount()); uint64_t player2State = 0; - for (uint64_t player1State = 0; player1State < player2RowGrouping.size() - 1; ++player1State) { + for (uint64_t player1State = 0; player1State < player1RowGrouping.size() - 1; ++player1State) { while (player1RowGrouping[player1State + 1] > player2RowGrouping[player2State]) { player2BackwardTransitions[player2State] = player1State; ++player2State; } - + player1Groups[player1State + 1] = player2State; }