Browse Source

Prism next state generator now deals with unbounded integer variables.

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
commit
bdd89d87b2
No known key found for this signature in database GPG Key ID: 6EDE19592731EEC3
  1. 2
      src/storm/generator/PrismNextStateGenerator.cpp
  2. 108
      src/storm/generator/VariableInformation.cpp
  3. 2
      src/storm/generator/VariableInformation.h
  4. 12
      src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp

2
src/storm/generator/PrismNextStateGenerator.cpp

@ -33,7 +33,7 @@ namespace storm {
// Only after checking validity of the program, we initialize the variable information. // Only after checking validity of the program, we initialize the variable information.
this->checkValid(); this->checkValid();
this->variableInformation = VariableInformation(program, options.isAddOutOfBoundsStateSet());
this->variableInformation = VariableInformation(program, options.getReservedBitsForUnboundedVariables(), options.isAddOutOfBoundsStateSet());
// Create a proper evalator. // Create a proper evalator.
this->evaluator = std::make_unique<storm::expressions::ExpressionEvaluator<ValueType>>(program.getManager()); this->evaluator = std::make_unique<storm::expressions::ExpressionEvaluator<ValueType>>(program.getManager());

108
src/storm/generator/VariableInformation.cpp

@ -34,7 +34,47 @@ namespace storm {
// Intentionally left empty. // 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<uint64_t>(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<uint64_t>(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) { if (outOfBoundsState) {
outOfBoundsBit = 0; outOfBoundsBit = 0;
++totalBitOffset; ++totalBitOffset;
@ -47,11 +87,15 @@ namespace storm {
++totalBitOffset; ++totalBitOffset;
} }
for (auto const& integerVariable : program.getGlobalIntegerVariables()) { 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<uint_fast64_t>(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; totalBitOffset += bitwidth;
} }
for (auto const& module : program.getModules()) { for (auto const& module : program.getModules()) {
@ -60,11 +104,15 @@ namespace storm {
++totalBitOffset; ++totalBitOffset;
} }
for (auto const& integerVariable : module.getIntegerVariables()) { 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<uint_fast64_t>(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; totalBitOffset += bitwidth;
} }
} }
@ -81,22 +129,6 @@ namespace storm {
for (auto const& automaton : model.getAutomata()) { 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() << "'."); 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<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
// integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true, true);
// totalBitOffset += bitwidth;
// }
// }
if (outOfBoundsState) { if (outOfBoundsState) {
outOfBoundsBit = 0; outOfBoundsBit = 0;
@ -181,30 +213,24 @@ namespace storm {
} }
for (auto const& variable : variableSet.getBoundedIntegerVariables()) { for (auto const& variable : variableSet.getBoundedIntegerVariables()) {
if (!variable.isTransient()) { 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()) { if (variable.hasLowerBound()) {
lowerBound = variable.getLowerBound().evaluateAsInt(); 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(); upperBound = variable.getUpperBound().evaluateAsInt();
lowerBound = upperBound - ((1ll << reservedBitsForUnboundedVariables) - 1);
} }
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(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()); integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, global, true, !variable.hasLowerBound() || !variable.hasUpperBound());
totalBitOffset += bitwidth; totalBitOffset += bitwidth;
} }
} }
for (auto const& variable : variableSet.getUnboundedIntegerVariables()) { for (auto const& variable : variableSet.getUnboundedIntegerVariables()) {
if (!variable.isTransient()) { 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; totalBitOffset += reservedBitsForUnboundedVariables;
} }
} }

2
src/storm/generator/VariableInformation.h

@ -98,7 +98,7 @@ namespace storm {
// A structure storing information about the used variables of the program. // A structure storing information about the used variables of the program.
struct VariableInformation { 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<std::reference_wrapper<storm::jani::Automaton const>> const& parallelAutomata, uint64_t reservedBitsForUnboundedVariables, bool outOfBoundsState); VariableInformation(storm::jani::Model const& model, std::vector<std::reference_wrapper<storm::jani::Automaton const>> const& parallelAutomata, uint64_t reservedBitsForUnboundedVariables, bool outOfBoundsState);
VariableInformation() = default; VariableInformation() = default;

12
src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp

@ -94,6 +94,12 @@ TEST(ExplicitPrismModelBuilderTest, Mdp) {
model = storm::builder::ExplicitModelBuilder<double>(program).build(); model = storm::builder::ExplicitModelBuilder<double>(program).build();
EXPECT_EQ(37ul, model->getNumberOfStates()); EXPECT_EQ(37ul, model->getNumberOfStates());
EXPECT_EQ(59ul, model->getNumberOfTransitions()); 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<double>(program).build();
EXPECT_EQ(9ul, model->getNumberOfStates());
EXPECT_EQ(9ul, model->getNumberOfTransitions());
} }
TEST(ExplicitPrismModelBuilderTest, Ma) { TEST(ExplicitPrismModelBuilderTest, Ma) {
@ -125,3 +131,9 @@ TEST(ExplicitPrismModelBuilderTest, FailComposition) {
STORM_SILENT_ASSERT_THROW(storm::builder::ExplicitModelBuilder<double>(program).build(), storm::exceptions::WrongFormatException); STORM_SILENT_ASSERT_THROW(storm::builder::ExplicitModelBuilder<double>(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<double>(program).build(), storm::exceptions::WrongFormatException);
}
Loading…
Cancel
Save