started on proper deadlock handling

Former-commit-id: a10c6b86ab [formerly c0b400e239]
Former-commit-id: 549a0e9880

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);

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;
             }

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;

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;
             }
             

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;
             };
             
         }