Browse Source

DdJaniModelBuilder: Added proper error message in case a bounded integer variable only has an upper or a lower bound.

tempestpy_adaptions
Tim Quatmann 3 years ago
parent
commit
3d05cc5791
No known key found for this signature in database GPG Key ID: 6EDE19592731EEC3
  1. 2
      src/storm/builder/DdJaniModelBuilder.cpp

2
src/storm/builder/DdJaniModelBuilder.cpp

@ -434,6 +434,8 @@ namespace storm {
} }
void createVariable(storm::jani::BoundedIntegerVariable const& variable, CompositionVariables<Type, ValueType>& result) { void createVariable(storm::jani::BoundedIntegerVariable const& variable, CompositionVariables<Type, ValueType>& result) {
STORM_LOG_THROW(variable.hasLowerBound(), storm::exceptions::NotSupportedException, "DdJaniModelBuilder only supports bounded variables. Variable " << variable.getName() << " has no lower bound.");
STORM_LOG_THROW(variable.hasUpperBound(), storm::exceptions::NotSupportedException, "DdJaniModelBuilder only supports bounded variables. Variable " << variable.getName() <<" has no upper bound.");
int_fast64_t low = variable.getLowerBound().evaluateAsInt(); int_fast64_t low = variable.getLowerBound().evaluateAsInt();
int_fast64_t high = variable.getUpperBound().evaluateAsInt(); int_fast64_t high = variable.getUpperBound().evaluateAsInt();
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(variable.getExpressionVariable().getName(), low, high); std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(variable.getExpressionVariable().getName(), low, high);

Loading…
Cancel
Save