Jit-builder now gives better diagnostics when nofixdl option is set.

src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp

@@ -32,6 +32,9 @@
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/JitBuilderSettings.h"
 
+#include "storm/settings/modules/CoreSettings.h"
+
+
 #include "storm/utility/OsDetection.h"
 #include "storm-config.h"
 
@@ -535,6 +538,8 @@ namespace storm {
                 }
                 modelData["double"] = cpptempl::make_data(list);
 
+                modelData["dontFixDeadlocks"] = storm::settings::getModule<storm::settings::modules::CoreSettings>().isDontFixDeadlocksSet();
+
                 // If we are building a possibly parametric model, we need to create the parameters.
                 if (std::is_same<storm::RationalFunction, ValueType>::value) {
                     generateParameters(modelData);
@@ -1657,7 +1662,6 @@ namespace storm {
 #include "storm/builder/RewardModelInformation.h"
                 
 #include "storm/utility/constants.h"
-                
 #include "storm/exceptions/WrongFormatException.h"
                 
                 namespace storm {
@@ -2278,7 +2282,14 @@ namespace storm {
                                             // Explore all edges that participate in synchronization vectors.
                                             exploreSynchronizingEdges(currentState, behaviour, statesToExplore);
                                         }
-                                        
+
+                                        {% if dontFixDeadlocks %}
+                                        if (behaviour.empty() && behaviour.isExpanded() ) {
+                                            std::cout << currentState << std::endl;
+                                            throw storm::exceptions::WrongFormatException("Error while creating sparse matrix from JANI model: found deadlock state  and fixing deadlocks was explicitly disabled.");
+                                        }
+                                        {% endif %}
+
                                         this->addStateBehaviour(currentIndex, behaviour);
                                         behaviour.clear();
                                     }

src/storm/builder/jit/ModelComponentsBuilder.cpp

@@ -81,7 +81,8 @@ namespace storm {
                     }
                 } else {
                     if (behaviour.isExpanded() && dontFixDeadlocks) {
-                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating sparse matrix from JANI model: found deadlock state and fixing deadlocks was explicitly disabled.");
+                        // Skip on purpose; Error is produced in the generated code to provide better diagnostics.
+                        //STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating sparse matrix from JANI model: found deadlock state and fixing deadlocks was explicitly disabled.");
                     } else {
                         // Add the self-loop in the transition matrix.
                         transitionMatrixBuilder->addNextValue(currentRow, currentRowGroup, storm::utility::one<ValueType>());