From 524efc616d71713a35c4fcf3edcb50d1b6bc4170 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Tue, 25 Apr 2017 19:45:26 +0200
Subject: [PATCH] Jit-builder now gives better diagnostics when nofixdl option
 is set.

---
 .../builder/jit/ExplicitJitJaniModelBuilder.cpp   | 15 +++++++++++++--
 src/storm/builder/jit/ModelComponentsBuilder.cpp  |  3 ++-
 2 files changed, 15 insertions(+), 3 deletions(-)

diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
index 6df0210e9..96c2738ed 100644
--- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
+++ b/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();
                                     }
diff --git a/src/storm/builder/jit/ModelComponentsBuilder.cpp b/src/storm/builder/jit/ModelComponentsBuilder.cpp
index 6f61feb19..752ab9b31 100644
--- a/src/storm/builder/jit/ModelComponentsBuilder.cpp
+++ b/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>());