From 169293bfe58a243931db71948a140f175db9e4c9 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 26 Oct 2016 17:04:39 +0200
Subject: [PATCH] started on proper deadlock handling

Former-commit-id: a10c6b86abc5d3de957625099fa186e4f912806d [formerly c0b400e239b89dbe0e43a8c2915b790bdf96d887]
Former-commit-id: 549a0e9880030dcb6bfc62cae0e164c72ba869ef
---
 .../jit/ExplicitJitJaniModelBuilder.cpp       |  1 +
 src/builder/jit/ModelComponentsBuilder.cpp    | 29 ++++++++++++++-----
 src/builder/jit/ModelComponentsBuilder.h      |  1 +
 src/builder/jit/StateBehaviour.cpp            | 13 ++++++++-
 src/builder/jit/StateBehaviour.h              |  4 +++
 5 files changed, 39 insertions(+), 9 deletions(-)

diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp
index 41df6f10d..e0f601ea2 100644
--- a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp
+++ b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp
@@ -227,6 +227,7 @@ namespace storm {
                                         std::cout << "Exploring state " << currentState << ", id " << currentIndex << std::endl;
 #endif
                                         
+                                        behaviour.setExpanded();
                                         exploreNonSynchronizingEdges(currentState, currentIndex, behaviour, statesToExplore);
                                         
                                         this->addStateBehaviour(currentIndex, behaviour);
diff --git a/src/builder/jit/ModelComponentsBuilder.cpp b/src/builder/jit/ModelComponentsBuilder.cpp
index 2a02a6a7e..6935b1cab 100644
--- a/src/builder/jit/ModelComponentsBuilder.cpp
+++ b/src/builder/jit/ModelComponentsBuilder.cpp
@@ -4,6 +4,10 @@
 #include "src/models/sparse/Dtmc.h"
 #include "src/models/sparse/StandardRewardModel.h"
 
+#include "src/settings/SettingsManager.h"
+#include "src/settings/modules/CoreSettings.h"
+
+#include "src/exceptions/WrongFormatException.h"
 #include "src/utility/macros.h"
 
 namespace storm {
@@ -12,7 +16,8 @@ namespace storm {
             
             template <typename IndexType, typename ValueType>
             ModelComponentsBuilder<IndexType, ValueType>::ModelComponentsBuilder(storm::jani::ModelType const& modelType) : modelType(modelType), isDeterministicModel(storm::jani::isDeterministicModel(modelType)), isDiscreteTimeModel(storm::jani::isDiscreteTimeModel(modelType)), currentRowGroup(0), currentRow(0), transitionMatrixBuilder(std::make_unique<storm::storage::SparseMatrixBuilder<ValueType>>(0, 0, 0, true, !isDeterministicModel)) {
-                // Intentionally left empty.
+                
+                dontFixDeadlocks = storm::settings::getModule<storm::settings::modules::CoreSettings>().isDontFixDeadlocksSet();
             }
             
             template <typename IndexType, typename ValueType>
@@ -30,14 +35,22 @@ namespace storm {
                 if (!isDeterministicModel) {
                     transitionMatrixBuilder->newRowGroup(currentRow);
                 }
-                for (auto const& choice : behaviour.getChoices()) {
-                    // Add the elements to the transition matrix.
-                    for (auto const& element : choice.getDistribution()) {
-                        transitionMatrixBuilder->addNextValue(currentRow, element.getIndex(), element.getValue());
+                if (!behaviour.empty()) {
+                    for (auto const& choice : behaviour.getChoices()) {
+                        // Add the elements to the transition matrix.
+                        for (auto const& element : choice.getDistribution()) {
+                            transitionMatrixBuilder->addNextValue(currentRow, element.getIndex(), element.getValue());
+                        }
+                        
+                        // Proceed to next row.
+                        ++currentRow;
+                    }
+                } 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.");
+                    } else {
+                        // FIXME: fix deadlock
                     }
-                    
-                    // Proceed to next row.
-                    ++currentRow;
                 }
                 ++currentRowGroup;
             }
diff --git a/src/builder/jit/ModelComponentsBuilder.h b/src/builder/jit/ModelComponentsBuilder.h
index 6b399ff94..13080f2e9 100644
--- a/src/builder/jit/ModelComponentsBuilder.h
+++ b/src/builder/jit/ModelComponentsBuilder.h
@@ -46,6 +46,7 @@ namespace storm {
                 storm::jani::ModelType modelType;
                 bool isDeterministicModel;
                 bool isDiscreteTimeModel;
+                bool dontFixDeadlocks;
                 
                 IndexType currentRowGroup;
                 IndexType currentRow;
diff --git a/src/builder/jit/StateBehaviour.cpp b/src/builder/jit/StateBehaviour.cpp
index 7409abb1f..2a24d70ee 100644
--- a/src/builder/jit/StateBehaviour.cpp
+++ b/src/builder/jit/StateBehaviour.cpp
@@ -7,7 +7,7 @@ namespace storm {
         namespace jit {
             
             template <typename IndexType, typename ValueType>
-            StateBehaviour<IndexType, ValueType>::StateBehaviour() : compressed(true) {
+            StateBehaviour<IndexType, ValueType>::StateBehaviour() : compressed(true), expanded(false) {
                 // Intentionally left empty.
             }
             
@@ -56,6 +56,16 @@ namespace storm {
                 }
             }
             
+            template <typename IndexType, typename ValueType>
+            bool StateBehaviour<IndexType, ValueType>::isExpanded() const {
+                return expanded;
+            }
+            
+            template <typename IndexType, typename ValueType>
+            void StateBehaviour<IndexType, ValueType>::setExpaned() {
+                expanded = true;
+            }
+            
             template <typename IndexType, typename ValueType>
             bool StateBehaviour<IndexType, ValueType>::empty() const {
                 return choices.empty();
@@ -69,6 +79,7 @@ namespace storm {
             template <typename IndexType, typename ValueType>
             void StateBehaviour<IndexType, ValueType>::clear() {
                 choices.clear();
+                expanded = false;
                 compressed = true;
             }
             
diff --git a/src/builder/jit/StateBehaviour.h b/src/builder/jit/StateBehaviour.h
index 1a56eeda7..a5dd5d839 100644
--- a/src/builder/jit/StateBehaviour.h
+++ b/src/builder/jit/StateBehaviour.h
@@ -22,6 +22,9 @@ namespace storm {
                 void reduce(storm::jani::ModelType const& modelType);
                 void compress();
                 
+                bool isExpanded() const;
+                void setExpaned();
+                
                 bool empty() const;
                 std::size_t size() const;
                 void clear();
@@ -29,6 +32,7 @@ namespace storm {
             private:
                 ContainerType choices;
                 bool compressed;
+                bool expanded;
             };
             
         }