work on MA in JIT-builder

Former-commit-id: 8e91fdc6e7 [formerly e8614cdf45]
Former-commit-id: 9919640630

src/builder/ExplicitModelBuilder.h

@@ -153,16 +153,6 @@ namespace storm {
              */
             ModelComponents buildModelComponents();
             
-            /*!
-             * Set the markovian states of the given modelComponents,
-             * makes sure that each state has at most one markovian choice,
-             * and makes this choice the first one of the corresponding state
-             *
-             * @param modelComponents The components of the model build so far
-             * @markovianChoices bit vector storing whether a choice is markovian
-             */
-            void buildMarkovianStates(ModelComponents& modelComponents, storm::storage::BitVector const& markovianChoices) const;
-            
             /*!
              * Builds the state labeling for the given program.
              *

src/builder/jit/Choice.cpp

@@ -7,7 +7,7 @@ namespace storm {
         namespace jit {
             
             template <typename IndexType, typename ValueType>
-            Choice<IndexType, ValueType>::Choice() : markovian(false) {
+            Choice<IndexType, ValueType>::Choice(bool markovian) : markovian(markovian) {
                 // Intentionally left empty.
             }
             

src/builder/jit/Choice.h

@@ -11,9 +11,19 @@ namespace storm {
             template <typename IndexType, typename ValueType>
             class Choice {
             public:
-                Choice();
+                /*!
+                 * Creates a new probabilistic/Markovian choice.
+                 */
+                Choice(bool markovian = false);
                 
+                /*!
+                 * Marks the choice as being Markovian (rather than probabilistic).
+                 */
                 void setMarkovian(bool value);
+                
+                /*!
+                 * Retrieves whether the choice is Markovian.
+                 */
                 bool isMarkovian() const;
                 
                 void add(DistributionEntry<IndexType, ValueType> const& entry);

src/builder/jit/ModelComponentsBuilder.cpp

@@ -21,7 +21,11 @@ namespace storm {
         namespace jit {
             
             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)) {
+            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), markovianStates(nullptr), transitionMatrixBuilder(std::make_unique<storm::storage::SparseMatrixBuilder<ValueType>>(0, 0, 0, true, !isDeterministicModel)) {
+                
+                if (modelType == storm::jani::ModelType::MA) {
+                    markovianStates = std::make_unique<storm::storage::BitVector>(10);
+                }
                 
                 dontFixDeadlocks = storm::settings::getModule<storm::settings::modules::CoreSettings>().isDontFixDeadlocksSet();
             }
@@ -69,6 +73,12 @@ namespace storm {
                         // Proceed to next row.
                         ++currentRow;
                     }
+                    
+                    // Mark the state as Markovian, if there is at least one Markovian choice.
+                    if (markovianStates) {
+                        markovianStates->grow(currentRowGroup + 1, false);
+                        markovianStates->set(currentRowGroup, behaviour.isMarkovianOrHybrid());
+                    }
                 } 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.");
@@ -88,6 +98,12 @@ namespace storm {
                                 rewardModelBuilder.addStateActionReward(storm::utility::zero<ValueType>());
                             }
                         }
+                        
+                        // Mark the state as Markovian.
+                        if (markovianStates) {
+                            markovianStates->grow(currentRowGroup + 1, false);
+                            markovianStates->set(currentRowGroup);
+                        }
                     }
                 }
                 ++currentRowGroup;

src/builder/jit/ModelComponentsBuilder.h

@@ -57,6 +57,7 @@ namespace storm {
                 
                 IndexType currentRowGroup;
                 IndexType currentRow;
+                std::unique_ptr<storm::storage::BitVector> markovianStates;
                 std::unique_ptr<storm::storage::SparseMatrixBuilder<ValueType>> transitionMatrixBuilder;
                 std::vector<storm::builder::RewardModelBuilder<ValueType>> rewardModelBuilders;
                 std::vector<std::pair<std::string, storm::storage::BitVector>> labels;

src/builder/jit/StateBehaviour.cpp

@@ -148,6 +148,21 @@ namespace storm {
                 }
             }
             
+            template <typename IndexType, typename ValueType>
+            bool StateBehaviour<IndexType, ValueType>::isHybrid() const {
+                return choices.size() > 1 && choices.front().isMarkovian() && !choices.back().isMarkovian();
+            }
+            
+            template <typename IndexType, typename ValueType>
+            bool StateBehaviour<IndexType, ValueType>::isMarkovian() const {
+                return choices.size() == 1 && choices.front().isMarkovian();
+            }
+            
+            template <typename IndexType, typename ValueType>
+            bool StateBehaviour<IndexType, ValueType>::isMarkovianOrHybrid() const {
+                return choices.front().isMarkovian();
+            }
+            
             template <typename IndexType, typename ValueType>
             bool StateBehaviour<IndexType, ValueType>::isExpanded() const {
                 return expanded;

src/builder/jit/StateBehaviour.h

@@ -32,9 +32,29 @@ namespace storm {
                  * Retrieves the rewards for this state.
                  */
                 std::vector<ValueType> const& getStateRewards() const;
-                
+
+                /*!
+                 * Reduces this behaviour to one that is suitable for the provided model type.
+                 */
                 void reduce(storm::jani::ModelType const& modelType);
                 
+                /*!
+                 * Determines whether the state behaviour has Markovian as well as probabilistic choices. Note that this
+                 * only yields the desired result after the state behaviour has been reduced.
+                 */
+                bool isHybrid() const;
+                
+                /*!
+                 * Determines whether the behaviour has Markovian choices only. Note that this only yields the desired
+                 * result after the state behaviour has been reduced.
+                 */
+                bool isMarkovian() const;
+                
+                /*!
+                 * Retrieves whether the state behaviour has any Markovian choices.
+                 */
+                bool isMarkovianOrHybrid() const;
+                
                 bool isExpanded() const;
                 void setExpanded();