Merge from future with compile errors

Former-commit-id: 36fd4385fc

src/models/sparse/MarkovAutomaton.cpp

@@ -85,6 +85,11 @@ namespace storm {
                 return this->exitRates;
             }
             
+            template <typename ValueType, typename RewardModelType>
+            std::vector<ValueType>& MarkovAutomaton<ValueType, RewardModelType>::getExitRates() {
+                return this->exitRates;
+            }
+            
             template <typename ValueType, typename RewardModelType>
             ValueType const& MarkovAutomaton<ValueType, RewardModelType>::getExitRate(storm::storage::sparse::state_type state) const {
                 return this->exitRates[state];

src/models/sparse/MarkovAutomaton.h

@@ -114,6 +114,13 @@ namespace storm {
                  */
                 std::vector<ValueType> const& getExitRates() const;
                 
+                /*!
+                 * Retrieves the vector representing the exit rates of the states.
+                 *
+                 * @return The exit rate vector of the model.
+                 */
+                std::vector<ValueType>& getExitRates();
+                
                 /*!
                  * Retrieves the exit rate of the given state.
                  *

src/models/sparse/Model.h

@@ -140,6 +140,21 @@ namespace storm {
                  */
                 storm::storage::SparseMatrix<ValueType>& getTransitionMatrix();
 
+                
+                /*!
+                 * Retrieves the reward models.
+                 *
+                 * @return A mapping from reward model names to the reward models.
+                 */
+                std::unordered_map<std::string, RewardModelType> const& getRewardModels() const;
+                
+                /*!
+                 * Retrieves the reward models.
+                 *
+                 * @return A mapping from reward model names to the reward models.
+                 */
+                std::unordered_map<std::string, RewardModelType>& getRewardModels();
+                
                 /*!
                  * Retrieves whether the model has a reward model with the given name.
                  *
@@ -318,20 +333,6 @@ namespace storm {
                  */
                 void printRewardModelsInformationToStream(std::ostream& out) const;
                 
-                /*!
-                 * Retrieves the reward models.
-                 *
-                 * @return A mapping from reward model names to the reward models.
-                 */
-                std::unordered_map<std::string, RewardModelType> const& getRewardModels() const;
-                
-                /*!
-                 * Retrieves the reward models.
-                 *
-                 * @return A mapping from reward model names to the reward models.
-                 */
-                std::unordered_map<std::string, RewardModelType>& getRewardModels();
-                
             private:
                 //  A matrix representing transition relation.
                 storm::storage::SparseMatrix<ValueType> transitionMatrix;

src/models/sparse/StochasticTwoPlayerGame.cpp

@@ -65,7 +65,7 @@ namespace storm {
 //            template class StochasticTwoPlayerGame<float>;
             
 #ifdef STORM_HAVE_CARL
-//            template class StochasticTwoPlayerGame<storm::RationalFunction>;
+            template class StochasticTwoPlayerGame<storm::RationalFunction>;
 #endif
             
         } // namespace sparse

src/solver/AbstractEquationSolver.h

@@ -1,6 +1,7 @@
 #ifndef STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_
 #define STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_
 
+#include <memory>
 #include "src/solver/TerminationCondition.h"
 #include <memory>
 

src/storage/BitVectorHashMap.cpp

@@ -1,5 +1,6 @@
 #include "src/storage/BitVectorHashMap.h"
 
+#include <algorithm>
 #include <iostream>
 #include <algorithm>
 

src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp

@@ -203,6 +203,7 @@ namespace storm {
         
         template<typename ModelType>
         void DeterministicModelBisimulationDecomposition<ModelType>::increaseProbabilityToSplitter(storm::storage::sparse::state_type predecessor, bisimulation::Block<BlockDataType> const& predecessorBlock, ValueType const& value) {
+            STORM_LOG_TRACE("Increasing probability of " << predecessor << " to splitter by " << value << ".");
             storm::storage::sparse::state_type predecessorPosition = this->partition.getPosition(predecessor);
             
             // If the position of the state is to the right of marker1, we have not seen it before.
@@ -269,6 +270,12 @@ namespace storm {
                         continue;
                     }
 
+                    // If we are computing a weak bisimulation on CTMCs and the predecessor block is the splitter, we
+                    // need to ignore it and proceed to the next predecessor.
+                    if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Ctmc && predecessorBlock == splitter) {
+                        continue;
+                    }
+                    
                     // We keep track of the probability of the predecessor moving to the splitter.
                     increaseProbabilityToSplitter(predecessor, predecessorBlock, predecessorEntry.getValue());
                     
@@ -278,7 +285,10 @@ namespace storm {
                         moveStateToMarker1(predecessor, predecessorBlock);
                     }
                     
-                    insertIntoPredecessorList(predecessorBlock, predecessorBlocks);
+                    // We must not insert the the splitter itself if we are not computing a weak bisimulation on CTMCs.
+                    if (this->options.getType() != BisimulationType::Weak || this->model.getType() != storm::models::ModelType::Ctmc || predecessorBlock != splitter) {
+                        insertIntoPredecessorList(predecessorBlock, predecessorBlocks);
+                    }
                 }
             }
             
@@ -431,7 +441,7 @@ namespace storm {
         template<typename