Browse Source

Corrected an assertion.

Former-commit-id: 54804b1599
tempestpy_adaptions
dehnert 10 years ago
parent
commit
adc1aa1442
  1. 2
      src/builder/ExplicitPrismModelBuilder.cpp

2
src/builder/ExplicitPrismModelBuilder.cpp

@ -220,7 +220,7 @@ namespace storm {
int_fast64_t assignedValue = evaluator.asInt(assignmentIt->getExpression());
STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
STORM_LOG_ASSERT(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) == assignedValue, "Writing to the bit vector bucket failed.");
STORM_LOG_ASSERT(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ").");
}
// Check that we processed all assignments.

Loading…
Cancel
Save