diff --git a/src/storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.cpp index 36231a419..910687adc 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.cpp @@ -18,17 +18,17 @@ namespace storm { template HybridInfiniteHorizonHelper::HybridInfiniteHorizonHelper(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix) : _model(model), _transitionMatrix(transitionMatrix), _markovianStates(nullptr), _exitRates(nullptr) { - // Intentionally left empty. + STORM_LOG_ASSERT(model.isNondeterministicModel() == Nondeterministic, "Template Parameter does not match model type."); } template HybridInfiniteHorizonHelper::HybridInfiniteHorizonHelper(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& exitRateVector) : _model(model), _transitionMatrix(transitionMatrix), _markovianStates(&markovianStates), _exitRates(&exitRateVector) { - // Intentionally left empty. + STORM_LOG_ASSERT(model.isNondeterministicModel() == Nondeterministic, "Template Parameter does not match model type."); } template HybridInfiniteHorizonHelper::HybridInfiniteHorizonHelper(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector) : _model(model), _transitionMatrix(transitionMatrix), _markovianStates(nullptr), _exitRates(&exitRateVector) { - // Intentionally left empty. + STORM_LOG_ASSERT(model.isNondeterministicModel() == Nondeterministic, "Template Parameter does not match model type."); } template @@ -38,7 +38,7 @@ namespace storm { storm::dd::Odd odd = _model.getReachableStates().createOdd(); // Translate all required components storm::storage::SparseMatrix explicitTransitionMatrix; - if (_model.isNondeterministicModel()) { + if (Nondeterministic) { explicitTransitionMatrix = _transitionMatrix.toMatrix(dynamic_cast const&>(_model).getNondeterminismVariables(), odd, odd); } else { explicitTransitionMatrix = _transitionMatrix.toMatrix(odd, odd); @@ -69,14 +69,18 @@ namespace storm { if (rewardModel.hasStateRewards()) { explicitStateRewards = rewardModel.getStateRewardVector().toVector(odd); } - if (_model.isNondeterministicModel() && rewardModel.hasStateActionRewards()) { + if (Nondeterministic && rewardModel.hasStateActionRewards()) { // Matrix and action-based vector have to be produced at the same time to guarantee the correct order auto matrixRewards = _transitionMatrix.toMatrixVector(rewardModel.getStateActionRewardVector(), dynamic_cast const&>(_model).getNondeterminismVariables(), odd, odd); explicitTransitionMatrix = std::move(matrixRewards.first); explicitActionRewards = std::move(matrixRewards.second); } else { // Translate matrix only - explicitTransitionMatrix = _transitionMatrix.toMatrix(dynamic_cast const&>(_model).getNondeterminismVariables(), odd, odd); + if (Nondeterministic) { + explicitTransitionMatrix = _transitionMatrix.toMatrix(dynamic_cast const&>(_model).getNondeterminismVariables(), odd, odd); + } else { + explicitTransitionMatrix = _transitionMatrix.toMatrix(odd, odd); + } if (rewardModel.hasStateActionRewards()) { // For deterministic models we can translate the action rewards easily explicitActionRewards = rewardModel.getStateActionRewardVector().toVector(odd);