diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index ba75757fa..053d1a4c3 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -157,31 +157,52 @@ namespace storm { // We then build the submatrix that only has the transitions of the maybe states. storm::storage::SparseMatrix submatrix = dtmc.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); + storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); // Before starting the model checking process, we assign priorities to states so we can use them to // impose ordering constraints later. std::vector statePriorities(submatrix.getRowCount()); + std::vector states(submatrix.getRowCount()); + for (std::size_t index = 0; index < states.size(); ++index) { + states[index] = index; + } if (storm::settings::parametricSettings().getEliminationOrder() == storm::settings::modules::ParametricSettings::EliminationOrder::Random) { - std::vector states(submatrix.getRowCount()); - for (std::size_t index = 0; index < states.size(); ++index) { - states[index] = index; - } - std::random_shuffle(states.begin(), states.end()); + } else { + std::vector distances; + if (storm::settings::parametricSettings().getEliminationOrder() == storm::settings::modules::ParametricSettings::EliminationOrder::Forward || storm::settings::parametricSettings().getEliminationOrder() == storm::settings::modules::ParametricSettings::EliminationOrder::ForwardReversed) { + distances = storm::utility::graph::getDistances(submatrix, newInitialStates); + } else if (storm::settings::parametricSettings().getEliminationOrder() == storm::settings::modules::ParametricSettings::EliminationOrder::Backward || storm::settings::parametricSettings().getEliminationOrder() == storm::settings::modules::ParametricSettings::EliminationOrder::BackwardReversed) { + // Since the target states were eliminated from the matrix already, we construct a replacement by + // treating all states that have some non-zero probability to go to a target state in one step. + storm::utility::ConstantsComparator comparator; + storm::storage::BitVector pseudoTargetStates(submatrix.getRowCount()); + for (std::size_t index = 0; index < oneStepProbabilities.size(); ++index) { + if (!comparator.isZero(oneStepProbabilities[index])) { + pseudoTargetStates.set(index); + } + } + + distances = storm::utility::graph::getDistances(submatrixTransposed, pseudoTargetStates); + } else { + STORM_LOG_ASSERT(false, "Illegal sorting order selected."); + } - for (std::size_t index = 0; index < states.size(); ++index) { - statePriorities[states[index]] = index; + // In case of the forward or backward ordering, we can sort the states according to the distances. + if (storm::settings::parametricSettings().getEliminationOrder() == storm::settings::modules::ParametricSettings::EliminationOrder::Forward || storm::settings::parametricSettings().getEliminationOrder() == storm::settings::modules::ParametricSettings::EliminationOrder::Backward) { + std::sort(states.begin(), states.end(), [&distances] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) { return distances[state1] < distances[state2]; } ); + } else { + // Otherwise, we sort them according to descending distances. + std::sort(states.begin(), states.end(), [&distances] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) { return distances[state1] > distances[state2]; } ); } - } else if (storm::settings::parametricSettings().getEliminationOrder() == storm::settings::modules::ParametricSettings::EliminationOrder::Forward) { - std::size_t distances = storm::utility::graph::getDistances(submatrix, initialStates); } + // Now convert the ordering of the states to priorities. + for (std::size_t index = 0; index < states.size(); ++index) { + statePriorities[states[index]] = index; + } - // To be able to apply heuristics later, we now determine the distance of each state to the initial state. - // We start by setting up the data structures. - - - return computeReachabilityProbability(submatrix, oneStepProbabilities, submatrix.transpose(), newInitialStates, phiStates, psiStates, distances); + return computeReachabilityProbability(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, statePriorities); } template diff --git a/src/settings/modules/BisimulationSettings.cpp b/src/settings/modules/BisimulationSettings.cpp index 4e2f3975e..291b9c9b5 100644 --- a/src/settings/modules/BisimulationSettings.cpp +++ b/src/settings/modules/BisimulationSettings.cpp @@ -29,10 +29,8 @@ namespace storm { } bool BisimulationSettings::check() const { - bool optionsSet = isStrongBisimulationSet() || isWeakBisimulationSet(); - + bool optionsSet = this->getOption(typeOptionName).getHasOptionBeenSet(); STORM_LOG_WARN_COND(storm::settings::generalSettings().isBisimulationSet() || !optionsSet, "Bisimulation minimization is not selected, so setting options for bisimulation has no effect."); - return true; } } // namespace modules