From 89f3aac33fba08401e86eac4d4a8bb9e9b805471 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Sun, 6 May 2018 22:18:15 +0200
Subject: [PATCH] add error messages for sparse model building when lower
 bounds for variables are above upper bounds

---
 src/storm/generator/VariableInformation.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp
index 5da944839..7f7ce0708 100644
--- a/src/storm/generator/VariableInformation.cpp
+++ b/src/storm/generator/VariableInformation.cpp
@@ -13,7 +13,6 @@
 #include "storm/exceptions/WrongFormatException.h"
 
 #include <cmath>
-#include <storm/exceptions/InvalidJaniException.h>
 
 namespace storm {
     namespace generator {
@@ -44,6 +43,7 @@ namespace storm {
             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);
                 totalBitOffset += bitwidth;
@@ -56,6 +56,7 @@ namespace storm {
                 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);
                     totalBitOffset += bitwidth;