Merge branch 'future' into menu_games

Former-commit-id: 064786db6d

src/adapters/MathsatExpressionAdapter.h

@@ -22,9 +22,9 @@
 namespace std {
     // Define hashing operator for MathSAT's declarations.
     template <>
-    struct std::hash<msat_decl> {
-        std::size_t operator()(msat_decl const& declaration) const {
-            return std::hash<void*>()(declaration.repr);
+    struct hash<msat_decl> {
+        size_t operator()(msat_decl const& declaration) const {
+            return hash<void*>()(declaration.repr);
         }
     };
 }

src/builder/ExplicitPrismModelBuilder.cpp

@@ -249,7 +249,7 @@ namespace storm {
             // not only appear in the probabilities, we re
             if (!std::is_same<ValueType, storm::RationalFunction>::value && preparedProgram->hasUndefinedConstants()) {
 #else
-            if (preparedProgram.hasUndefinedConstants()) {
+            if (preparedProgram->hasUndefinedConstants()) {
 #endif
                 std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = preparedProgram->getUndefinedConstants();
                 std::stringstream stream;

src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp

@@ -262,10 +262,6 @@ namespace storm {
                 if (startingIteration == 0) {
                     result = values;
                     storm::utility::vector::scaleVectorInPlace(result, std::get<3>(foxGlynnResult)[0]);
-                    std::function<ValueType(ValueType const&, ValueType const&)> addAndScale = [&foxGlynnResult] (ValueType const& a, ValueType const& b) { return a + std::get<3>(foxGlynnResult)[0] * b; };
-                    if (addVector != nullptr) {
-                        storm::utility::vector::applyPointwise(result, *addVector, result, addAndScale);
-                    }
                     ++startingIteration;
                 } else {
                     if (computeCumulativeReward) {

src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp

@@ -503,7 +503,7 @@ namespace storm {
             }
             
             template class SparseMarkovAutomatonCslHelper<double>;
-            //template std::vector<double> SparseMarkovAutomatonCslHelper<double>::computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, std::vector<double> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel<double> const& rewardModel, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory);
+            template std::vector<double> SparseMarkovAutomatonCslHelper<double>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, std::vector<double> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel<double> const& rewardModel, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory);
             
         }
     }

src/models/sparse/Model.cpp

@@ -320,6 +320,9 @@ namespace storm {
                 return this->rewardModels;
             }
 
+            std::set<storm::Variable> getProbabilityParameters(Model<storm::RationalFunction> const& model) {
+                return storm::storage::getVariables(model.getTransitionMatrix());
+            }
             
             template class Model<double>;
             template class Model<float>;

src/models/sparse/Model.h

@@ -345,6 +345,7 @@ namespace storm {
                 boost::optional<std::vector<LabelSet>> choiceLabeling;
             };
             
+            std::set<storm::Variable> getProbabilityParameters(Model<storm::RationalFunction> const& model);
         } // namespace sparse
     } // namespace models
 } // namespace storm

src/storage/SparseMatrix.cpp

@@ -1208,6 +1208,19 @@ namespace storm {
             return result;
         }
         
+        
+#ifdef STORM_HAVE_CARL
+        std::set<storm::Variable> getVariables(SparseMatrix<storm::RationalFunction> const& matrix)
+        {
+            std::set<storm::Variable> result;
+            for(auto const& entry : matrix) {
+                entry.getValue().gatherVariables(result);
+            }
+            return result;
+        }
+        
+#endif
+        
         // Explicitly instantiate the entry, builder and the matrix.
         // double
         template class MatrixEntry<typename SparseMatrix<double>::index_type, double>;

src/storage/SparseMatrix.h

@@ -8,7 +8,7 @@
 #include <iterator>
 
 #include "src/utility/OsDetection.h"
-
+#include "src/adapters/CarlAdapter.h"
 #include <boost/functional/hash.hpp>
 
 // Forward declaration for adapter classes.
@@ -969,7 +969,11 @@ namespace storm {
             std::vector<index_type> rowGroupIndices;
             
         };
-
+        
+#ifdef STORM_HAVE_CARL
+        std::set<storm::Variable> getVariables(SparseMatrix<storm::RationalFunction> const& matrix);
+#endif
+        
     } // namespace storage
 } // namespace storm
 

src/storage/bisimulation/BisimulationDecomposition.cpp

@@ -44,7 +44,7 @@ namespace storm {
         }
         
         template<typename ModelType, typename BlockDataType>
-        BisimulationDecomposition<ModelType, BlockDataType>::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), keepRewards(false), type(BisimulationType::Strong), bounded(false), buildQuotient(true) {
+        BisimulationDecomposition<ModelType, BlockDataType>::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), buildQuotient(true), keepRewards(false), type(BisimulationType::Strong), bounded(false) {
             // Intentionally left empty.
         }
         
@@ -163,9 +163,9 @@ namespace storm {
 
         template<typename ModelType, typename BlockDataType>
         BisimulationDecomposition<ModelType, BlockDataType>::BisimulationDecomposition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Options const& options) : model(model), backwardTransitions(backwardTransitions), options(options), partition(), comparator(), quotient(nullptr) {
-            STORM_LOG_THROW(!options.keepRewards || !model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model.");
-            STORM_LOG_THROW(!options.keepRewards || !model.hasRewardModel() || model.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently supported for models with state rewards only. Consider converting the transition rewards to state rewards (via suitable function calls).");
-            STORM_LOG_THROW(options.type != BisimulationType::Weak || !options.bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties.");
+            STORM_LOG_THROW(!options.getKeepRewards() || !model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model.");
+            STORM_LOG_THROW(!options.getKeepRewards() || !model.hasRewardModel() || model.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently supported for models with state rewards only. Consider converting the transition rewards to state rewards (via suitable function calls).");
+            STORM_LOG_THROW(options.getType() != BisimulationType::Weak || !options.getBounded(), storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties.");
             
             // Fix the respected atomic propositions if they were not explicitly given.
             if (!this->options.respectedAtomicPropositions) {
@@ -270,7 +270,7 @@ namespace storm {
             
             // If the model has state rewards, we need to consider them, because otherwise reward properties are not
             // preserved.
-            if (options.keepRewards && model.hasRewardModel()) {
+            if (options.getKeepRewards() && model.hasRewardModel()) {
                 this->splitInitialPartitionBasedOnStateRewards();
             }
         }
@@ -284,11 +284,11 @@ namespace storm {
                 representativePsiState = *options.psiStates.get().begin();
             }
             
-            partition = storm::storage::bisimulation::Partition<BlockDataType>(model.getNumberOfStates(), statesWithProbability01.first, options.bounded || options.keepRewards ? options.psiStates.get() : statesWithProbability01.second, representativePsiState);
+            partition = storm::storage::bisimulation::Partition<BlockDataType>(model.getNumberOfStates(), statesWithProbability01.first, options.getBounded() || options.getKeepRewards() ? options.psiStates.get() : statesWithProbability01.second, representativePsiState);
             
             // If the model has state rewards, we need to consider them, because otherwise reward properties are not
             // preserved.
-            if (options.keepRewards && model.hasRewardModel()) {
+            if (options.getKeepRewards() && model.hasRewardModel()) {
                 this->splitInitialPartitionBasedOnStateRewards();
             }
         }

src/storage/bisimulation/BisimulationDecomposition.h

@@ -3,6 +3,8 @@
 
 #include <deque>
 
+#include "src/settings/SettingsManager.h"
+#include "src/settings/modules/BisimulationSettings.h"
 #include "src/storage/sparse/StateType.h"
 #include "src/storage/Decomposition.h"
 #include "src/storage/StateBlock.h"
@@ -25,6 +27,23 @@ namespace storm {
     namespace storage {
 
         enum class BisimulationType { Strong, Weak };
+        enum class BisimulationTypeChoice { Strong, Weak, FromSettings };
+        
+        inline BisimulationType resolveBisimulationTypeChoice(BisimulationTypeChoice c) {
+            switch(c) {
+                case BisimulationTypeChoice::Strong:
+                    return BisimulationType::Strong;
+                case BisimulationTypeChoice::Weak:
+                    return BisimulationType::Weak;
+                case BisimulationTypeChoice::FromSettings:
+                    if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
+                        return BisimulationType::Weak;
+                    } else {
+                        return BisimulationType::Strong;
+                    }
+                    
+            }
+        }
         
         /*!
          * This class is the superclass of all decompositions of a sparse model into its bisimulation quotient.
@@ -37,6 +56,8 @@ namespace storm {
             
             // A class that offers the possibility to customize the bisimulation.
             struct Options {
+                
+                
                 // Creates an object representing the default values for all options.
                 Options();
                 
@@ -68,33 +89,74 @@ namespace storm {
                  */
                 void preserveFormula(ModelType const& model, storm::logic::Formula const& formula);
                 
+                
+                /**
+                 * Sets the bisimulation type. If the bisimulation type is set to weak,
+                 * we also change the bounded flag (as bounded properties are not preserved under 
+                 * weak bisimulation).
+                 */
+                void setType(BisimulationType t) {
+                    if(t == BisimulationType::Weak) {
+                        bounded = false;
+                    }
+                    type = t;
+                }
+                
+                BisimulationType getType() const {
+                    return this->type;
+                }
+                
+                bool getBounded() const {
+                    return this->bounded;
+                }
+                
+                bool getKeepRewards() const {
+                    return this->keepRewards;
+                }
+                
+                bool isOptimizationDirectionSet() const {
+                    return static_cast<bool>(optimalityType);
+                }
+                
+                OptimizationDirection getOptimizationDirection() const {
+                    assert(optimalityType);
+                    return optimalityType.get();
+                }
                 // A flag that indicates whether a measure driven initial partition is to be used. If this flag is set
                 // to true, the two optional pairs phiStatesAndLabel and psiStatesAndLabel must be set. Then, the
                 // measure driven initial partition wrt. to the states phi and psi is taken.
                 bool measureDrivenInitialPartition;
                 boost::optional<storm::storage::BitVector> phiStates;
                 boost::optional<storm::storage::BitVector> psiStates;
-                boost::optional<OptimizationDirection> optimalityType;
                 
-                // An optional set of strings that indicate which of the atomic propositions of the model are to be
-                // respected and which may be ignored. If not given, all atomic propositions of the model are respected.
+                /// An optional set of strings that indicate which of the atomic propositions of the model are to be
+                /// respected and which may be ignored. If not given, all atomic propositions of the model are respected.
                 boost::optional<std::set<std::string>> respectedAtomicPropositions;
                 
-                // A flag that indicates whether or not the state-rewards of the model are to be respected (and should
-                // be kept in the quotient model, if one is built).
+                /// A flag that governs whether the quotient model is actually built or only the decomposition is computed.
+                bool buildQuotient;
+                
+            private:
+                
+                boost::optional<OptimizationDirection> optimalityType;
+                
+                
+                
+                
+                /// A flag that indicates whether or not the state-rewards of the model are to be respected (and should
+                /// be kept in the quotient model, if one is built).
                 bool keepRewards;
                 
-                // A flag that indicates whether a strong or a weak bisimulation is to be computed.
+                /// A flag that indicates whether a strong or a weak bisimulation is to be computed.
                 BisimulationType type;
                 
-                // A flag that indicates whether step-bounded properties are to be preserved. This may only be set to tru
-                // when computing strong bisimulation equivalence.
+                /// A flag that indicates whether step-bounded properties are to be preserved. This may only be set to tru
+                /// when computing strong bisimulation equivalence.
                 bool bounded;
                 
-                // A flag that governs whether the quotient model is actually built or only the decomposition is computed.
-                bool buildQuotient;
                 
-            private:
+                
+                
                 /*!
                  * Sets the options under the assumption that the given formula is the only one that is to be checked.
                  *

src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp

@@ -122,7 +122,7 @@ namespace storm {
         void DeterministicModelBisimulationDecomposition<ModelType>::initializeMeasureDrivenPartition() {
             BisimulationDecomposition<ModelType, BlockDataType>::initializeMeasureDrivenPartition();
             
-            if (this->options.type == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
+            if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
                 this->initializeWeakDtmcBisimulation();
             }
         }
@@ -131,7 +131,7 @@ namespace storm {
         void DeterministicModelBisimulationDecomposition<ModelType>::initializeLabelBasedPartition() {
             BisimulationDecomposition<ModelType, BlockDataType>::initializeLabelBasedPartition();
             
-            if (this->options.type == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
+            if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
                 this->initializeWeakDtmcBisimulation();
             }
         }
@@ -494,7 +494,7 @@ namespace storm {
             }
             
             // Finally, we split the block based on the precomputed probabilities and the chosen bisimulation type.
-            if (this->options.type == BisimulationType::Strong || this->model.getType() == storm::models::ModelType::Ctmc) {
+            if (this->options.getType() == BisimulationType::Strong || this->model.getType() == storm::models::ModelType::Ctmc) {
                 refinePredecessorBlocksOfSplitterStrong(predecessorBlocks, splitterQueue);
             } else {
                 // If the splitter is a predecessor of we can use the computed probabilities to update the silent
@@ -528,7 +528,7 @@ namespace storm {
             
             // If the model had state rewards, we need to build the state rewards for the quotient as well.
             boost::optional<std::vector<ValueType>> stateRewards;
-            if (this->options.keepRewards && this->model.hasRewardModel()) {
+            if (this->options.getKeepRewards() && this->model.hasRewardModel()) {
                 stateRewards = std::vector<ValueType>(this->blocks.size());
             }
             
@@ -542,7 +542,7 @@ namespace storm {
                 
                 // However, for weak bisimulation, we need to make sure the representative state is a non-silent one (if
                 // there is any such state).
-                if (this->options.type == BisimulationType::Weak) {
+                if (this->options.getType() == BisimulationType::Weak) {
                     for (auto const& state : block) {
                         if (!isSilent(state)) {
                             representativeState = state;
@@ -576,7 +576,7 @@ namespace storm {
                         storm::storage::sparse::state_type targetBlock = this->partition.getBlock(entry.getColumn()).getId();
                         
                         // If we are computing a weak bisimulation quotient, there is no need to add self-loops.
-                        if ((this->options.type == BisimulationType::Weak) && targetBlock == blockIndex) {
+                        if ((this->options.getType() == BisimulationType::Weak) && targetBlock == blockIndex) {
                             continue;
                         }
                         
@@ -590,7 +590,7 @@ namespace storm {
                     
                     // Now add them to the actual matrix.
                     for (auto const& probabilityEntry : blockProbability) {
-                        if (this->options.type == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
+                        if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
                             builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second / (storm::utility::one<ValueType>() - getSilentProbability(representativeState)));
                         } else {
                             builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second);
@@ -608,7 +608,7 @@ namespace storm {
                 
                 // If the model has state rewards, we simply copy the state reward of the representative state, because
                 // all states in a block are guaranteed to have the same state reward.
-                if (this->options.keepRewards && this->model.hasRewardModel()) {
+                if (this->options.getKeepRewards() && this->model.hasRewardModel()) {
                     typename std::unordered_map<std::string, typename ModelType::RewardModelType>::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel();
                     stateRewards.get()[blockIndex] = nameRewardModelPair->second.getStateRewardVector()[representativeState];
                 }
@@ -622,7 +622,7 @@ namespace storm {
             
             // Construct the reward model mapping.
             std::unordered_map<std::string, typename ModelType::RewardModelType> rewardModels;
-            if (this->options.keepRewards && this->model.hasRewardModel()) {
+            if (this->options.getKeepRewards() && this->model.hasRewardModel()) {
                 typename std::unordered_map<std::string, typename ModelType::RewardModelType>::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel();
                 rewardModels.insert(std::make_pair(nameRewardModelPair->first, typename ModelType::RewardModelType(stateRewards)));
             }

src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp

@@ -17,13 +17,13 @@ namespace storm {
         
         template<typename ModelType>
         NondeterministicModelBisimulationDecomposition<ModelType>::NondeterministicModelBisimulationDecomposition(ModelType const& model, typename BisimulationDecomposition<ModelType, NondeterministicModelBisimulationDecomposition::BlockDataType>::Options const& options) : BisimulationDecomposition<ModelType, NondeterministicModelBisimulationDecomposition::BlockDataType>(model, model.getTransitionMatrix().transpose(false), options), choiceToStateMapping(model.getNumberOfChoices()), quotientDistributions(model.getNumberOfChoices()), orderedQuotientDistributions(model.getNumberOfChoices()) {
-            STORM_LOG_THROW(options.type == BisimulationType::Strong, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation is currently not supported for nondeterministic models.");
+            STORM_LOG_THROW(options.getType() == BisimulationType::Strong, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation is currently not supported for nondeterministic models.");
         }
         
         template<typename ModelType>
         std::pair<storm::storage::BitVector, storm::storage::BitVector> NondeterministicModelBisimulationDecomposition<ModelType>::getStatesWithProbability01() {
-            STORM_LOG_THROW(static_cast<bool>(this->options.optimalityType), storm::exceptions::IllegalFunctionCallException, "Can only compute states with probability 0/1 with an optimization direction (min/max).");
-            if (this->options.optimalityType.get() == OptimizationDirection::Minimize) {
+            STORM_LOG_THROW(this->options.isOptimizationDirectionSet(), storm::exceptions::IllegalFunctionCallException, "Can only compute states with probability 0/1 with an optimization direction (min/max).");
+            if (this->options.getOptimizationDirection() == OptimizationDirection::Minimize) {
                 return storm::utility::graph::performProb01Min(this->model.getTransitionMatrix(), this->model.getTransitionMatrix().getRowGroupIndices(), this->model.getBackwardTransitions(), this->options.phiStates.get(), this->options.psiStates.get());
             } else {
                 return storm::utility::graph::performProb01Max(this->model.getTransitionMatrix(), this->model.getTransitionMatrix().getRowGroupIndices(), this->model.getBackwardTransitions(), this->options.phiStates.get(), this->options.psiStates.get());
@@ -109,7 +109,7 @@ namespace storm {
             
             // If the model had state rewards, we need to build the state rewards for the quotient as well.
             boost::optional<std::vector<ValueType>> stateRewards;
-            if (this->options.keepRewards && this->model.hasRewardModel()) {
+            if (this->options.getKeepRewards() && this->model.hasRewardModel()) {
                 stateRewards = std::vector<ValueType>(this->blocks.size());
             }
             
@@ -169,7 +169,7 @@ namespace storm {
                 
                 // If the model has state rewards, we simply copy the state reward of the representative state, because
                 // all states in a block are guaranteed to have the same state reward.
-                if (this->options.keepRewards && this->model.hasRewardModel()) {
+                if (this->options.getKeepRewards() && this->model.hasRewardModel()) {
                     typename std::unordered_map<std::string, typename ModelType::RewardModelType>::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel();
                     stateRewards.get()[blockIndex] = nameRewardModelPair->second.getStateRewardVector()[representativeState];
                 }
@@ -183,7 +183,7 @@ namespace storm {
             
             // Construct the reward model mapping.
             std::unordered_map<std::string, typename ModelType::RewardModelType> rewardModels;
-            if (this->options.keepRewards && this->model.hasRewardModel()) {
+            if (this->options.getKeepRewards() && this->model.hasRewardModel()) {
                 typename std::unordered_map<std::string, typename ModelType::RewardModelType>::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel();
                 rewardModels.insert(std::make_pair(nameRewardModelPair->first, typename ModelType::RewardModelType(stateRewards)));
             }

src/utility/graph.cpp

@@ -1155,9 +1155,10 @@ namespace storm {
             
             template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
             
-            template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<double>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
-            template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
-            
+            template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<double>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+#ifdef STORM_HAVE_CARL
+            template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+#endif
             
             template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
             
@@ -1173,19 +1174,24 @@ namespace storm {
             
             
             template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<double>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+#ifdef STORM_HAVE_CARL
             template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+#endif
             template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,  storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
             
             template storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<double>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+#ifdef STORM_HAVE_CARL
             template storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+#endif
             template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
             
             template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
             
             
             template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<double>> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
-            template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
-            
+#ifdef STORM_HAVE_CARL
+			template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+#endif
             
             template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<double> const& matrix) ;
             

src/utility/storm.h

@@ -138,16 +138,13 @@ namespace storm {
     }
     
     template<typename ModelType>
-    std::shared_ptr<ModelType> performDeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+    std::shared_ptr<ModelType> performDeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas, storm::storage::BisimulationType type) {
         std::cout << "Performing bisimulation minimization... ";
         typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options options;
         if (!formulas.empty()) {
             options = typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options(*model, formulas);
         }
-        if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
-            options.type = storm::storage::BisimulationType::Weak;
-            options.bounded = false;
-        }
+        options.setType(type);
         
         storm::storage::DeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options);
         bisimulationDecomposition.computeBisimulationDecomposition();
@@ -157,16 +154,14 @@ namespace storm {
     }
     
     template<typename ModelType>
-    std::shared_ptr<ModelType> performNondeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+    std::shared_ptr<ModelType> performNondeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas, storm::storage::BisimulationType type) {
         std::cout << "Performing bisimulation minimization... ";
         typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options options;
         if (!formulas.empty()) {
             options = typename storm::storage::NondeterministicModelBisimulationDecomposition<ModelType>::Options(*model, formulas);
         }
-        if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
-            options.type = storm::storage::BisimulationType::Weak;
-            options.bounded = false;
-        }
+        options.setType(type);
+        
         
         storm::storage::NondeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options);
         bisimulationDecomposition.computeBisimulationDecomposition();
@@ -175,23 +170,30 @@ namespace storm {
         return model;
     }
     
+    template<typename ModelType, typename ValueType = typename ModelType::ValueType, typename std::enable_if<std::is_base_of<storm::models::sparse::Model<ValueType>, ModelType>::value, bool>::type = 0>
+    std::shared_ptr<storm::models::ModelBase> performBisimulationMinimization(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas, storm::storage::BisimulationType type) {
+        STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs, CTMCs and MDPs.");
+        model->reduceToStateBasedRewards();
+
+        if (model->isOfType(storm::models::ModelType::Dtmc)) {
+            return performDeterministicSparseBisimulationMinimization<storm::models::sparse::Dtmc<ValueType>>(model->template as<storm::models::sparse::Dtmc<ValueType>>(), formulas, type);
+        } else if (model->isOfType(storm::models::ModelType::Ctmc)) {
+            return performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(model->template as<storm::models::sparse::Ctmc<ValueType>>(), formulas, type);
+        } else {
+            return performNondeterministicSparseBisimulationMinimization<storm::models::sparse::Mdp<ValueType>>(model->template as<storm::models::sparse::Mdp<ValueType>>(), formulas, type);
+        }       
+    }
+    
     template<typename ModelType, typename ValueType = typename ModelType::ValueType, typename std::enable_if<std::is_base_of<storm::models::sparse::Model<ValueType>, ModelType>::value, bool>::type = 0>
     std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
         if (storm::settings::generalSettings().isBisimulationSet()) {
-            
-            STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models.");
-            STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs, CTMCs and MDPs.");
-
-            model->reduceToStateBasedRewards();
-
-            if (model->isOfType(storm::models::ModelType::Dtmc)) {
-                return performDeterministicSparseBisimulationMinimization<storm::models::sparse::Dtmc<ValueType>>(model->template as<storm::models::sparse::Dtmc<ValueType>>(), formulas);
-            } else if (model->isOfType(storm::models::ModelType::Ctmc)) {
-                return performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(model->template as<storm::models::sparse::Ctmc<ValueType>>(), formulas);
-            } else {
-                return performNondeterministicSparseBisimulationMinimization<storm::models::sparse::Mdp<ValueType>>(model->template as<storm::models::sparse::Mdp<ValueType>>(), formulas);
+            storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
+            if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
+                bisimType = storm::storage::BisimulationType::Weak;
             }
             
+            STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models.");
+            return performBisimulationMinimization(model, formulas, bisimType);
         }
         return model;
     }

test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp

@@ -10,6 +10,9 @@
 #include "src/models/sparse/StandardRewardModel.h"
 #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
 
+
+#ifdef STORM_HAVE_MSAT
+
 TEST(SmtPermissiveSchedulerTest, DieSelection) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die_c1.nm");
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
@@ -58,3 +61,5 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) {
     //
     
 }
+
+#endif // STORM_HAVE_MSAT

test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp

@@ -35,8 +35,7 @@ TEST(DeterministicModelBisimulationDecomposition, Die) {
     EXPECT_EQ(5ul, result->getNumberOfStates());
     EXPECT_EQ(8ul, result->getNumberOfTransitions());
 
-    options.bounded = false;
-    options.type = storm::storage::BisimulationType::Weak;
+    options.setType(storm::storage::BisimulationType::Weak);
 
     storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim3(*dtmc, options);
     ASSERT_NO_THROW(bisim3.computeBisimulationDecomposition());
@@ -93,8 +92,7 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) {
     EXPECT_EQ(65ul, result->getNumberOfStates());
     EXPECT_EQ(105ul, result->getNumberOfTransitions());
 
-    options.bounded = false;
-    options.type = storm::storage::BisimulationType::Weak;
+    options.setType(storm::storage::BisimulationType::Weak);
 
     storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim3(*dtmc, options);
     ASSERT_NO_THROW(bisim3.computeBisimulationDecomposition());