From 4ab84bc42cdaf882f1611edd943a0a30e345c534 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@rwth-aachen.de>
Date: Sat, 25 Apr 2015 18:44:10 +0200
Subject: [PATCH] state elimination -- hybrid and standard method

Former-commit-id: bafea3658ccede034283ba01bf0a094b1a4d1c2a
---
 .../reachability/SparseDtmcEliminationModelChecker.h            | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
index 064a70499..b78944b13 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
@@ -107,7 +107,7 @@ namespace storm {
             std::vector<std::size_t> getStatePriorities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<ValueType> const& oneStepProbabilities);
             
             //eliminates some of the states according to different strategies.
-            void eliminateStates(storm::storage::BitVector& subsystem, FlexibleSparseMatrix& flexibleMatrix, std::vector<ValueType>& oneStepProbabilities, FlexibleSparseMatrix& flexibleBackwardTransitions, storm::storage::BitVector const& initialStates);
+            void eliminateStates(storm::storage::BitVector& subsystem, FlexibleSparseMatrix& flexibleMatrix, std::vector<ValueType>& oneStepProbabilities, FlexibleSparseMatrix& flexibleBackwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, boost::optional<std::vector<std::size_t>> const& statePriorities = {});
             
             void formulateModelWithSMT(storm::solver::Smt2SmtSolver& solver, std::vector<storm::RationalFunction::PolyType>& stateProbVars, storm::storage::BitVector const& subsystem, FlexibleSparseMatrix const& flexibleMatrix, std::vector<storm::RationalFunction> const& oneStepProbabilities);