Merge branch 'future' into TimParamSysAndSMT

Former-commit-id: f38789ae1f

src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp

@@ -374,6 +374,7 @@ namespace storm {
                         // Now compute reachability probabilities in the transformed model.
                         storm::storage::SparseMatrix<ValueType> const& newTransitionMatrix = transformedModel.transitionMatrix.get();
                         std::vector<ValueType> conditionalProbabilities = computeUntilProbabilities(newTransitionMatrix, newTransitionMatrix.transpose(), storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), transformedModel.targetStates.get(), qualitative, linearEquationSolverFactory);
+                        
                         storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalProbabilities);
                     }
                 }

src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h

@@ -47,6 +47,10 @@ namespace storm {
                 static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, boost::optional<std::vector<ValueType>> resultHint = boost::none);
                 
                 struct BaierTransformedModel {
+                    BaierTransformedModel() : noTargetStates(false) {
+                        // Intentionally left empty.
+                    }
+                    
                     storm::storage::BitVector beforeStates;
                     boost::optional<storm::storage::SparseMatrix<ValueType>> transitionMatrix;
                     boost::optional<storm::storage::BitVector> targetStates;

src/storage/bisimulation/BisimulationDecomposition.cpp

@@ -240,6 +240,9 @@ namespace storm {
                 ++iterations;
 
                 // Get and prepare the next splitter.
+                // Sort the splitters according to their sizes to prefer small splitters. That is just a heuristic, but
+                // tends to work well.
+                std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block<BlockDataType> const* b1, Block<BlockDataType> const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } );
                 Block<BlockDataType>* splitter = splitterQueue.front();
                 splitterQueue.pop_front();
                 splitter->data().setSplitter(false);

test/functional/utility/ModelInstantiatorTest.cpp

@@ -77,8 +77,8 @@ TEST(ModelInstantiatorTest, BrpProb) {
         ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
         storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
         ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
-        valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1)));
-        valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(1)));
+        valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1.0)));
+        valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(1.0)));
 
         storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));
 
@@ -110,7 +110,7 @@ TEST(ModelInstantiatorTest, BrpProb) {
         ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
         storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
         ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
-        valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1)));
+        valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1.0)));
         valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.9)));
 
         storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));