From 3d05cc5791289ea0aa14d6b46f2e379effd495cb Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 15 Jul 2021 11:58:33 +0200
Subject: [PATCH] DdJaniModelBuilder: Added proper error message in case a
 bounded integer variable only has an upper or a lower bound.

---
 src/storm/builder/DdJaniModelBuilder.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp
index ff5b3609a..9fbe1d25d 100644
--- a/src/storm/builder/DdJaniModelBuilder.cpp
+++ b/src/storm/builder/DdJaniModelBuilder.cpp
@@ -434,6 +434,8 @@ namespace storm {
             }
             
             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 high = variable.getUpperBound().evaluateAsInt();
                 std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(variable.getExpressionVariable().getName(), low, high);