From 41b494edd39f0293595b555795dc4e73f109e00d Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 1 Jun 2018 08:57:11 +0200 Subject: [PATCH] fixing bug due to too few variables being reserved --- src/storm/abstraction/jani/EdgeAbstractor.cpp | 4 ++-- src/storm/abstraction/prism/CommandAbstractor.cpp | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm/abstraction/jani/EdgeAbstractor.cpp index f60d99ece..e37676c64 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.cpp +++ b/src/storm/abstraction/jani/EdgeAbstractor.cpp @@ -344,8 +344,8 @@ namespace storm { // We now compute how many variables we need to encode the choices. We add one to the maximal number of // choices to account for a possible transition to a bottom state. - uint_fast64_t numberOfVariablesNeeded = static_cast(std::ceil(std::log2(maximalNumberOfChoices + (blockCounter == 0 ? 1 : 0)))); - + uint_fast64_t numberOfVariablesNeeded = (maximalNumberOfChoices > 1) ? (static_cast(std::ceil(std::log2(maximalNumberOfChoices + (blockCounter == 0 ? 1 : 0))))) : (blockCounter == 0 ? 1 : 0); + // Finally, build overall result. storm::dd::Bdd resultBdd = this->getAbstractionInformation().getDdManager().getBddZero(); diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp index 26a3d2c69..bc65bc453 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.cpp +++ b/src/storm/abstraction/prism/CommandAbstractor.cpp @@ -344,7 +344,7 @@ namespace storm { // We now compute how many variables we need to encode the choices. We add one to the maximal number of // choices to account for a possible transition to a bottom state. - uint_fast64_t numberOfVariablesNeeded = maximalNumberOfChoices > 1 ? static_cast(std::ceil(std::log2(maximalNumberOfChoices + (blockCounter == 0 ? 1 : 0)))) : 0; + uint_fast64_t numberOfVariablesNeeded = (maximalNumberOfChoices > 1) ? (static_cast(std::ceil(std::log2(maximalNumberOfChoices + (blockCounter == 0 ? 1 : 0))))) : (blockCounter == 0 ? 1 : 0); // Finally, build overall result. storm::dd::Bdd resultBdd = this->getAbstractionInformation().getDdManager().getBddZero();