From bdd89d87b20bd33f83366339b0b5d5fc35508d62 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 19 Apr 2021 12:28:41 +0200 Subject: [PATCH] Prism next state generator now deals with unbounded integer variables. --- .../generator/PrismNextStateGenerator.cpp | 2 +- src/storm/generator/VariableInformation.cpp | 108 +++++++++++------- src/storm/generator/VariableInformation.h | 2 +- .../builder/ExplicitPrismModelBuilderTest.cpp | 12 ++ 4 files changed, 81 insertions(+), 43 deletions(-) diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index ead36e763..5bad7e1ba 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -33,7 +33,7 @@ namespace storm { // Only after checking validity of the program, we initialize the variable information. this->checkValid(); - this->variableInformation = VariableInformation(program, options.isAddOutOfBoundsStateSet()); + this->variableInformation = VariableInformation(program, options.getReservedBitsForUnboundedVariables(), options.isAddOutOfBoundsStateSet()); // Create a proper evalator. this->evaluator = std::make_unique>(program.getManager()); diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp index 91dcf30ee..7fc2c3403 100644 --- a/src/storm/generator/VariableInformation.cpp +++ b/src/storm/generator/VariableInformation.cpp @@ -34,7 +34,47 @@ namespace storm { // Intentionally left empty. } - VariableInformation::VariableInformation(storm::prism::Program const& program, bool outOfBoundsState) : totalBitOffset(0) { + /*! + * Small helper function that sets unspecified lower/upper bounds for an integer variable based on the provided reservedBitsForUnboundedVariables and returns the number of bits required to represent the final variable range + * @pre If has[Lower,Upper]Bound is true, [lower,upper]Bound must be set to the corresponding bound. + * @post lowerBound and upperBound are set to the considered bound for this variable + * @param hasLowerBound shall be true iff there is a lower bound given + * @param lowerBound a reference to the lower bound value + * @param hasUpperBound shall be true iff there is an upper bound given + * @param upperBound a reference to the upper bound + * @param reservedBitsForUnboundedVariables the number of bits that shall be used to represent unbounded variables + * @return the number of bits required to represent the final variable range + */ + uint64_t getBitWidthLowerUpperBound(bool const& hasLowerBound, int64_t& lowerBound, bool const& hasUpperBound, int64_t& upperBound, uint64_t const& reservedBitsForUnboundedVariables) { + if (hasLowerBound) { + if (hasUpperBound) { + STORM_LOG_THROW(lowerBound <= upperBound, storm::exceptions::WrongFormatException, "Lower bound must not be above upper bound"); + // We do not have to set any bounds in this case. + // Return the number of bits required to store all the values between lower and upper bound + return static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); + } else { + // We only have a lower bound. Find the largest upper bound we can store with the given number of bits. + upperBound = lowerBound + ((1ll << reservedBitsForUnboundedVariables) - 1); + } + } else { + if (hasUpperBound) { + // We only have an upper bound. Find the smallest lower bound we can store with the given number of bits + lowerBound = upperBound - ((1ll << reservedBitsForUnboundedVariables) - 1); + } else { + // We neither have a lower nor an upper bound. Take the usual n-bit integer values for lower/upper bounds + lowerBound = -(1ll << (reservedBitsForUnboundedVariables - 1)); // = -2^(reservedBits-1) + upperBound = (1ll << (reservedBitsForUnboundedVariables - 1)) - 1; // = 2^(reservedBits-1) - 1 + } + } + // If we reach this point, it means that the variable is unbounded. + // Lets check for potential overflows. + STORM_LOG_THROW(lowerBound <= upperBound, storm::exceptions::WrongFormatException, "Lower bound must not be above upper bound. Has there been an integer over-/underflow?"); + // By choice of the lower/upper bound, the number of reserved bits must coincide with the bitwidth + STORM_LOG_ASSERT(reservedBitsForUnboundedVariables == static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))), "Unexpected bitwidth for unbounded variable."); + return reservedBitsForUnboundedVariables; + } + + VariableInformation::VariableInformation(storm::prism::Program const& program, uint64_t reservedBitsForUnboundedVariables, bool outOfBoundsState) : totalBitOffset(0) { if (outOfBoundsState) { outOfBoundsBit = 0; ++totalBitOffset; @@ -47,11 +87,15 @@ namespace storm { ++totalBitOffset; } for (auto const& integerVariable : program.getGlobalIntegerVariables()) { - int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); - int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); - STORM_LOG_THROW(lowerBound <= upperBound, storm::exceptions::WrongFormatException, "Lower bound must not be above upper bound"); - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true, integerVariable.isObservable()); + int64_t lowerBound, upperBound; + if (integerVariable.hasLowerBoundExpression()) { + lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); + } + if (integerVariable.hasUpperBoundExpression()) { + upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); + } + uint64_t bitwidth = getBitWidthLowerUpperBound(integerVariable.hasLowerBoundExpression(), lowerBound, integerVariable.hasUpperBoundExpression(), upperBound, reservedBitsForUnboundedVariables); + integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true, integerVariable.isObservable(), !integerVariable.hasLowerBoundExpression() || !integerVariable.hasUpperBoundExpression()); totalBitOffset += bitwidth; } for (auto const& module : program.getModules()) { @@ -60,11 +104,15 @@ namespace storm { ++totalBitOffset; } for (auto const& integerVariable : module.getIntegerVariables()) { - int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); - int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); - STORM_LOG_THROW(lowerBound <= upperBound, storm::exceptions::WrongFormatException, "Lower bound must not be above upper bound"); - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, false, integerVariable.isObservable()); + int64_t lowerBound, upperBound; + if (integerVariable.hasLowerBoundExpression()) { + lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); + } + if (integerVariable.hasUpperBoundExpression()) { + upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); + } + uint64_t bitwidth = getBitWidthLowerUpperBound(integerVariable.hasLowerBoundExpression(), lowerBound, integerVariable.hasUpperBoundExpression(), upperBound, reservedBitsForUnboundedVariables); + integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, false, integerVariable.isObservable(), !integerVariable.hasLowerBoundExpression() || !integerVariable.hasUpperBoundExpression()); totalBitOffset += bitwidth; } } @@ -81,22 +129,6 @@ namespace storm { for (auto const& automaton : model.getAutomata()) { STORM_LOG_THROW(!automaton.getVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains non-transient real variables in automaton '" << automaton.getName() << "'."); } -// -// for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) { -// if (!variable.isTransient()) { -// booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true, true); -// ++totalBitOffset; -// } -// } -// for (auto const& variable : model.getGlobalVariables().getBoundedIntegerVariables()) { -// if (!variable.isTransient()) { -// int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); -// int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); -// uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); -// integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true, true); -// totalBitOffset += bitwidth; -// } -// } if (outOfBoundsState) { outOfBoundsBit = 0; @@ -181,30 +213,24 @@ namespace storm { } for (auto const& variable : variableSet.getBoundedIntegerVariables()) { if (!variable.isTransient()) { - int64_t lowerBound; - int64_t upperBound; + int64_t lowerBound, upperBound; + STORM_LOG_ASSERT(variable.hasLowerBound() || variable.hasUpperBound(), "Bounded integer variable has neither a lower nor an upper bound."); if (variable.hasLowerBound()) { lowerBound = variable.getLowerBound().evaluateAsInt(); - if (variable.hasUpperBound()) { - upperBound = variable.getUpperBound().evaluateAsInt(); - } else { - upperBound = lowerBound + ((1ll << reservedBitsForUnboundedVariables) - 1); - } - } else { - STORM_LOG_THROW(variable.hasUpperBound(), storm::exceptions::WrongFormatException, "Bounded integer variable has neither a lower nor an upper bound."); + } + if (variable.hasUpperBound()) { upperBound = variable.getUpperBound().evaluateAsInt(); - lowerBound = upperBound - ((1ll << reservedBitsForUnboundedVariables) - 1); } - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); + uint64_t bitwidth = getBitWidthLowerUpperBound(variable.hasLowerBound(), lowerBound, variable.hasUpperBound(), upperBound, reservedBitsForUnboundedVariables); integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, global, true, !variable.hasLowerBound() || !variable.hasUpperBound()); totalBitOffset += bitwidth; } } for (auto const& variable : variableSet.getUnboundedIntegerVariables()) { if (!variable.isTransient()) { - int64_t lowerBound = -(1ll << (reservedBitsForUnboundedVariables - 1)); - int64_t upperBound = (1ll << (reservedBitsForUnboundedVariables - 1)) - 1; - integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, reservedBitsForUnboundedVariables, global, true, true); + int64_t lowerBound, upperBound; + uint64_t bitwidth = getBitWidthLowerUpperBound(false, lowerBound, false, upperBound, reservedBitsForUnboundedVariables); + integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, global, true, true); totalBitOffset += reservedBitsForUnboundedVariables; } } diff --git a/src/storm/generator/VariableInformation.h b/src/storm/generator/VariableInformation.h index be97290f8..7c2586dbb 100644 --- a/src/storm/generator/VariableInformation.h +++ b/src/storm/generator/VariableInformation.h @@ -98,7 +98,7 @@ namespace storm { // A structure storing information about the used variables of the program. struct VariableInformation { - VariableInformation(storm::prism::Program const& program, bool outOfBoundsState = false); + VariableInformation(storm::prism::Program const& program, uint64_t reservedBitsForUnboundedVariables, bool outOfBoundsState = false); VariableInformation(storm::jani::Model const& model, std::vector> const& parallelAutomata, uint64_t reservedBitsForUnboundedVariables, bool outOfBoundsState); VariableInformation() = default; diff --git a/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp b/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp index f654d28f1..d7d324112 100644 --- a/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp +++ b/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp @@ -94,6 +94,12 @@ TEST(ExplicitPrismModelBuilderTest, Mdp) { model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(37ul, model->getNumberOfStates()); EXPECT_EQ(59ul, model->getNumberOfTransitions()); + + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm"); + program = modelDescription.preprocess("N=-7").asPrismProgram(); + model = storm::builder::ExplicitModelBuilder(program).build(); + EXPECT_EQ(9ul, model->getNumberOfStates()); + EXPECT_EQ(9ul, model->getNumberOfTransitions()); } TEST(ExplicitPrismModelBuilderTest, Ma) { @@ -125,3 +131,9 @@ TEST(ExplicitPrismModelBuilderTest, FailComposition) { STORM_SILENT_ASSERT_THROW(storm::builder::ExplicitModelBuilder(program).build(), storm::exceptions::WrongFormatException); } + +TEST(ExplicitPrismModelBuilderTest, FailUnbounded) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm"); + storm::prism::Program program = modelDescription.preprocess("N=7").asPrismProgram(); + STORM_SILENT_ASSERT_THROW(storm::builder::ExplicitModelBuilder(program).build(), storm::exceptions::WrongFormatException); +}