diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index b71d15197..4d1df7a36 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -374,6 +374,7 @@ namespace storm { // Now compute reachability probabilities in the transformed model. storm::storage::SparseMatrix const& newTransitionMatrix = transformedModel.transitionMatrix.get(); std::vector conditionalProbabilities = computeUntilProbabilities(newTransitionMatrix, newTransitionMatrix.transpose(), storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), transformedModel.targetStates.get(), qualitative, linearEquationSolverFactory); + storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalProbabilities); } } diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index 8ec0cfc8a..c3a913a3c 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -47,6 +47,10 @@ namespace storm { static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> resultHint = boost::none); struct BaierTransformedModel { + BaierTransformedModel() : noTargetStates(false) { + // Intentionally left empty. + } + storm::storage::BitVector beforeStates; boost::optional> transitionMatrix; boost::optional targetStates; diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index aedd4a998..5c5b3e667 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/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 const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } ); Block* splitter = splitterQueue.front(); splitterQueue.pop_front(); splitter->data().setSplitter(false); diff --git a/test/functional/utility/ModelInstantiatorTest.cpp b/test/functional/utility/ModelInstantiatorTest.cpp index fe2ee4a7c..24512d886 100644 --- a/test/functional/utility/ModelInstantiatorTest.cpp +++ b/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(1))); - valuation.insert(std::make_pair(pK,carl::rationalize(1))); + valuation.insert(std::make_pair(pL,carl::rationalize(1.0))); + valuation.insert(std::make_pair(pK,carl::rationalize(1.0))); storm::models::sparse::Dtmc 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(1))); + valuation.insert(std::make_pair(pL,carl::rationalize(1.0))); valuation.insert(std::make_pair(pK,carl::rationalize(0.9))); storm::models::sparse::Dtmc const& instantiated(modelInstantiator.instantiate(valuation));