From 6c543df537a5aff38aecb39798c641b6180a74bf Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 15 Feb 2019 13:50:47 +0100 Subject: [PATCH] Fix in bisimulation of MDPs, which failed if all non-absorbing states in the quotient are initial --- CHANGELOG.md | 2 ++ .../NondeterministicModelBisimulationDecomposition.cpp | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 226abe92e..0c989225e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,8 @@ The releases of major and minor versions contain an overview of changes since th Version 1.3.x ------------- +### Version 1.3.1 (under development) +- Fixed sparse bisimulation of MDPs (which failed if all non-absorbing states in the quotient are initial) ### Version 1.3.0 (2018/12) - Slightly improved scheduler extraction diff --git a/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp b/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp index 019ec40c2..2abe49b1e 100644 --- a/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp +++ b/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp @@ -211,7 +211,7 @@ namespace storm { } // Finally construct the quotient model. - this->quotient = std::make_shared(builder.build(), std::move(newLabeling), std::move(rewardModels)); + this->quotient = std::make_shared(builder.build(0,this->size(), this->size()), std::move(newLabeling), std::move(rewardModels)); } template