diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index fd2b3d3a3..5bfb7ab7a 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -631,8 +631,6 @@ namespace storm { std::shared_ptr model = buildPreprocessExportModelWithValueTypeAndDdlib(input, engine); if (model) { - STORM_LOG_THROW(model->isSparseModel() || !storm::settings::getModule().isSoundSet(), storm::exceptions::NotSupportedException, "Forcing soundness is currently only supported for sparse models."); - if (coreSettings.isCounterexampleSet()) { auto ioSettings = storm::settings::getModule(); generateCounterexamples(model, input); diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 222ee8a00..171a7bf70 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -6,12 +6,14 @@ #include "storm/storage/dd/Add.h" #include "storm/storage/dd/Bdd.h" #include "storm/storage/dd/Odd.h" +#include "storm/storage/MaximalEndComponentDecomposition.h" #include "storm/utility/graph.h" #include "storm/utility/constants.h" #include "storm/models/symbolic/StandardRewardModel.h" +#include "storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" #include "storm/modelchecker/results/HybridQuantitativeCheckResult.h" @@ -25,6 +27,13 @@ namespace storm { namespace modelchecker { namespace helper { + template + struct SolverRequirementsData { + boost::optional> ecInformation; + boost::optional> initialScheduler; + storm::storage::BitVector properMaybeStates; + }; + template std::vector computeValidInitialSchedulerForUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& b) { uint64_t numberOfMaybeStates = transitionMatrix.getRowGroupCount(); @@ -60,11 +69,12 @@ namespace storm { std::unique_ptr HybridMdpPrctlHelper::computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 and 1 of satisfying the until-formula. + storm::dd::Bdd transitionMatrixBdd = transitionMatrix.notZero(); std::pair, storm::dd::Bdd> statesWithProbability01; if (dir == OptimizationDirection::Minimize) { - statesWithProbability01 = storm::utility::graph::performProb01Min(model, phiStates, psiStates); + statesWithProbability01 = storm::utility::graph::performProb01Min(model, transitionMatrixBdd, phiStates, psiStates); } else { - statesWithProbability01 = storm::utility::graph::performProb01Max(model, phiStates, psiStates); + statesWithProbability01 = storm::utility::graph::performProb01Max(model, transitionMatrixBdd, phiStates, psiStates); } storm::dd::Bdd maybeStates = !statesWithProbability01.first && !statesWithProbability01.second && model.getReachableStates(); @@ -77,15 +87,41 @@ namespace storm { } else { // If there are maybe states, we need to solve an equation system. if (!maybeStates.isZero()) { + // Check for requirements of the solver early so we can adjust the maybe state computation accordingly. + storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::UntilProbabilities, dir); + storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements; + SolverRequirementsData solverRequirementsData; + bool extendMaybeStates = true; + if (!clearedRequirements.empty()) { + if (clearedRequirements.requiresNoEndComponents()) { + STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it."); + extendMaybeStates = true; + clearedRequirements.clearNoEndComponents(); + } + if (clearedRequirements.requiresValidInitialScheduler()) { + STORM_LOG_DEBUG("Scheduling valid scheduler computation, because the solver requires it."); + clearedRequirements.clearValidInitialScheduler(); + } + clearedRequirements.clearBounds(); + STORM_LOG_THROW(clearedRequirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); + } + + storm::dd::Bdd extendedMaybeStates = maybeStates; + if (extendMaybeStates) { + // Extend the maybe states by all non-maybe states that can be reached from a maybe state within one step (they + // either are states with probability 0 or 1). + extendedMaybeStates |= maybeStates.relationalProduct(transitionMatrixBdd.existsAbstract(model.getNondeterminismVariables()), model.getRowVariables(), model.getColumnVariables()); + } + // Create the ODD for the translation between symbolic and explicit storage. - storm::dd::Odd odd = maybeStates.createOdd(); + storm::dd::Odd odd = extendedMaybeStates.createOdd(); // Create the matrix and the vector for the equation system. - storm::dd::Add maybeStatesAdd = maybeStates.template toAdd(); + storm::dd::Add extendedMaybeStatesAdd = extendedMaybeStates.template toAdd(); // Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting // non-maybe states in the matrix. - storm::dd::Add submatrix = transitionMatrix * maybeStatesAdd; + storm::dd::Add submatrix = transitionMatrix * extendedMaybeStatesAdd; // Then compute the vector that contains the one-step probabilities to a state with probability 1 for all // maybe states. @@ -103,26 +139,16 @@ namespace storm { // Translate the symbolic matrix/vector to their explicit representations and solve the equation system. std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); + if (requirements.requiresValidInitialScheduler()) { + solverRequirementsData.initialScheduler = computeValidInitialSchedulerForUntilProbabilities(explicitRepresentation.first, explicitRepresentation.second); + } + // Create the solution vector. std::vector x(explicitRepresentation.first.getRowGroupCount(), storm::utility::zero()); - - // Check for requirements of the solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::UntilProbabilities, dir); - boost::optional> initialScheduler; - if (!requirements.empty()) { - if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) { - STORM_LOG_DEBUG("Computing valid scheduler hint, because the solver requires it."); - initialScheduler = computeValidInitialSchedulerForUntilProbabilities(explicitRepresentation.first, explicitRepresentation.second); - - requirements.clearValidInitialScheduler(); - } - requirements.clearBounds(); - STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); - } std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first)); - if (initialScheduler) { - solver->setInitialScheduler(std::move(initialScheduler.get())); + if (solverRequirementsData.initialScheduler) { + solver->setInitialScheduler(std::move(solverRequirementsData.initialScheduler.get())); } solver->setBounds(storm::utility::zero(), storm::utility::one()); solver->setRequirementsChecked(); @@ -256,7 +282,7 @@ namespace storm { storm::storage::BitVector computeTargetStatesForReachabilityRewardsFromExplicitRepresentation(storm::storage::SparseMatrix const& transitionMatrix) { storm::storage::BitVector targetStates(transitionMatrix.getRowGroupCount()); - // A state is a target state if its row group is empty. + // A state is a target state iff its row group is empty. for (uint64_t rowGroup = 0; rowGroup < transitionMatrix.getRowGroupCount(); ++rowGroup) { if (transitionMatrix.getRowGroupIndices()[rowGroup] == transitionMatrix.getRowGroupIndices()[rowGroup + 1]) { targetStates.set(rowGroup); @@ -286,18 +312,8 @@ namespace storm { template void eliminateTargetStatesFromExplicitRepresentation(std::pair, std::vector>& explicitRepresentation, std::vector& scheduler, storm::storage::BitVector const& properMaybeStates) { - // Eliminate the superfluous entries from the rhs vector and the scheduler. + // Eliminate superfluous entries from the scheduler. uint64_t position = 0; - for (auto state : properMaybeStates) { - for (uint64_t row = explicitRepresentation.first.getRowGroupIndices()[state]; row < explicitRepresentation.first.getRowGroupIndices()[state + 1]; ++row) { - explicitRepresentation.second[position] = explicitRepresentation.second[row]; - position++; - } - } - explicitRepresentation.second.resize(position); - explicitRepresentation.second.shrink_to_fit(); - - position = 0; for (auto state : properMaybeStates) { scheduler[position] = scheduler[state]; position++; @@ -322,6 +338,60 @@ namespace storm { return expandedResult; } + template + void eliminateEndComponentsAndTargetStatesReachabilityRewards(std::pair, std::vector>& explicitRepresentation, SolverRequirementsData& solverRequirementsData) { + + // Get easier handles to the data. + auto& transitionMatrix = explicitRepresentation.first; + auto& rewardVector = explicitRepresentation.second; + + // Start by computing the choices with reward 0, as we only want ECs within this fragment. + storm::storage::BitVector zeroRewardChoices(transitionMatrix.getRowCount()); + + uint64_t index = 0; + for (auto const& e : rewardVector) { + if (storm::utility::isZero(e)) { + zeroRewardChoices.set(index); + } + ++index; + } + + // Compute the states that have some zero reward choice. + storm::storage::BitVector candidateStates(solverRequirementsData.properMaybeStates); + for (auto state : solverRequirementsData.properMaybeStates) { + bool keepState = false; + + for (auto row = transitionMatrix.getRowGroupIndices()[state], rowEnd = transitionMatrix.getRowGroupIndices()[state + 1]; row < rowEnd; ++row) { + if (zeroRewardChoices.get(row)) { + keepState = true; + break; + } + } + + if (!keepState) { + candidateStates.set(state, false); + } + } + + bool doDecomposition = !candidateStates.empty(); + + storm::storage::MaximalEndComponentDecomposition endComponentDecomposition; + if (doDecomposition) { + // Then compute the states that are in MECs with zero reward. + endComponentDecomposition = storm::storage::MaximalEndComponentDecomposition(transitionMatrix, transitionMatrix.transpose(), candidateStates, zeroRewardChoices); + } + + // Only do more work if there are actually end-components. + if (doDecomposition && !endComponentDecomposition.empty()) { + STORM_LOG_DEBUG("Eliminating " << endComponentDecomposition.size() << " EC(s)."); + std::vector subvector; + SparseMdpEndComponentInformation::eliminateEndComponents(endComponentDecomposition, transitionMatrix, rewardVector, solverRequirementsData.properMaybeStates, transitionMatrix, subvector); + rewardVector = std::move(subvector); + } else { + STORM_LOG_DEBUG("Not eliminating ECs as there are none."); + } + } + template std::unique_ptr HybridMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { @@ -352,19 +422,25 @@ namespace storm { if (!maybeStates.isZero()) { // Check for requirements of the solver this early so we can adapt the maybe states accordingly. storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::ReachabilityRewards, dir); - bool requireInitialScheduler = false; - if (!requirements.empty()) { - if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) { + storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements; + bool extendMaybeStates = false; + if (!clearedRequirements.empty()) { + if (clearedRequirements.requiresNoEndComponents()) { + STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it."); + extendMaybeStates = true; + clearedRequirements.clearNoEndComponents(); + } + if (clearedRequirements.requiresValidInitialScheduler()) { STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it."); - requireInitialScheduler = true; - requirements.clearValidInitialScheduler(); + extendMaybeStates = true; + clearedRequirements.clearValidInitialScheduler(); } - requirements.clearLowerBounds(); - STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); + clearedRequirements.clearLowerBounds(); + STORM_LOG_THROW(clearedRequirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); } // Compute the set of maybe states that we are required to keep in the translation to explicit. - storm::dd::Bdd requiredMaybeStates = requireInitialScheduler ? maybeStatesWithTargetStates : maybeStates; + storm::dd::Bdd requiredMaybeStates = extendMaybeStates ? maybeStatesWithTargetStates : maybeStates; // Create the ODD for the translation between symbolic and explicit storage. storm::dd::Odd odd = requiredMaybeStates.createOdd(); @@ -392,23 +468,27 @@ namespace storm { std::vector rowGroupSizes = stateActionAdd.sumAbstract(model.getNondeterminismVariables()).toVector(odd); // Finally cut away all columns targeting non-maybe states (or non-(maybe or target) states, respectively). - submatrix *= requireInitialScheduler ? maybeStatesWithTargetStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd() : maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); + submatrix *= extendMaybeStates ? maybeStatesWithTargetStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd() : maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); // Translate the symbolic matrix/vector to their explicit representations. std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); - // Compute a valid initial scheduler if necessary. - boost::optional> initialScheduler; - boost::optional properMaybeStates; - if (requireInitialScheduler) { - // Compute a valid initial scheduler. + // Fulfill the solver's requirements. + SolverRequirementsData solverRequirementsData; + if (requirements.requiresNoEndComponents() || requirements.requiresValidInitialScheduler()) { storm::storage::BitVector targetStates = computeTargetStatesForReachabilityRewardsFromExplicitRepresentation(explicitRepresentation.first); - properMaybeStates = ~targetStates; - initialScheduler = computeValidInitialSchedulerForReachabilityRewards(explicitRepresentation.first, properMaybeStates.get(), targetStates); - - // Since we needed the transitions to target states to be translated as well for the computation - // of the scheduler, we have to get rid of them now. - eliminateTargetStatesFromExplicitRepresentation(explicitRepresentation, initialScheduler.get(), properMaybeStates.get()); + solverRequirementsData.properMaybeStates = ~targetStates; + + if (requirements.requiresNoEndComponents()) { + eliminateEndComponentsAndTargetStatesReachabilityRewards(explicitRepresentation, solverRequirementsData); + } else { + // Compute a valid initial scheduler. + solverRequirementsData.initialScheduler = computeValidInitialSchedulerForReachabilityRewards(explicitRepresentation.first, solverRequirementsData.properMaybeStates, targetStates); + + // Since we needed the transitions to target states to be translated as well for the computation + // of the scheduler, we have to get rid of them now. + eliminateTargetStatesFromExplicitRepresentation(explicitRepresentation, solverRequirementsData.initialScheduler.get(), solverRequirementsData.properMaybeStates); + } } // Create the solution vector. @@ -418,8 +498,8 @@ namespace storm { std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first)); // Move the scheduler to the solver. - if (initialScheduler) { - solver->setInitialScheduler(std::move(initialScheduler.get())); + if (solverRequirementsData.initialScheduler) { + solver->setInitialScheduler(std::move(solverRequirementsData.initialScheduler.get())); } solver->setLowerBound(storm::utility::zero()); @@ -427,8 +507,16 @@ namespace storm { solver->solveEquations(dir, x, explicitRepresentation.second); // If we included the target states in the ODD, we need to expand the result from the solver. - if (requireInitialScheduler) { - x = insertTargetStateValuesIntoExplicitRepresentation(x, properMaybeStates.get()); + if (extendMaybeStates) { + if (requirements.requiresNoEndComponents()) { + if (solverRequirementsData.ecInformation) { + std::vector extendedVector(solverRequirementsData.properMaybeStates.size()); + solverRequirementsData.ecInformation.get().setValues(extendedVector, solverRequirementsData.properMaybeStates, x); + x = std::move(extendedVector); + } + } else { + x = insertTargetStateValuesIntoExplicitRepresentation(x, solverRequirementsData.properMaybeStates); + } } // Return a hybrid check result that stores the numerical values explicitly. diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp new file mode 100644 index 000000000..fb00c8243 --- /dev/null +++ b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp @@ -0,0 +1,325 @@ +#include "storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h" + +#include "storm/storage/BitVector.h" +#include "storm/storage/MaximalEndComponentDecomposition.h" + +#include "storm/adapters/RationalNumberAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" + +namespace storm { + namespace modelchecker { + namespace helper { + + template + SparseMdpEndComponentInformation::SparseMdpEndComponentInformation(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::BitVector const& maybeStates) : NOT_IN_EC(std::numeric_limits::max()), eliminatedEndComponents(false), numberOfMaybeStatesInEc(0), numberOfMaybeStatesNotInEc(0), numberOfEc(endComponentDecomposition.size()) { + + // (1) Compute how many maybe states there are before each other maybe state. + maybeStatesBefore = maybeStates.getNumberOfSetBitsBeforeIndices(); + + // (2) Create mapping from maybe states to their MEC. If they are not contained in an MEC, their value + // is set to a special constant. + maybeStateToEc.resize(maybeStates.getNumberOfSetBits(), NOT_IN_EC); + uint64_t mecIndex = 0; + for (auto const& mec : endComponentDecomposition) { + for (auto const& stateActions : mec) { + maybeStateToEc[maybeStatesBefore[stateActions.first]] = mecIndex; + ++numberOfMaybeStatesInEc; + } + ++mecIndex; + } + + // (3) Compute number of states not in MECs. + numberOfMaybeStatesNotInEc = maybeStateToEc.size() - numberOfMaybeStatesInEc; + } + + template + bool SparseMdpEndComponentInformation::isMaybeStateInEc(uint64_t maybeState) const { + return maybeStateToEc[maybeState] != NOT_IN_EC; + } + + template + bool SparseMdpEndComponentInformation::isStateInEc(uint64_t state) const { + return maybeStateToEc[maybeStatesBefore[state]] != NOT_IN_EC; + } + + template + std::vector SparseMdpEndComponentInformation::getNumberOfMaybeStatesNotInEcBeforeIndices() const { + std::vector result(maybeStateToEc.size()); + + uint64_t count = 0; + auto resultIt = result.begin(); + for (auto const& e : maybeStateToEc) { + *resultIt = count; + if (e != NOT_IN_EC) { + ++count; + } + ++resultIt; + } + + return result; + } + + template + uint64_t SparseMdpEndComponentInformation::getNumberOfMaybeStatesNotInEc() const { + return numberOfMaybeStatesNotInEc; + } + + template + uint64_t SparseMdpEndComponentInformation::getEc(uint64_t state) const { + return maybeStateToEc[maybeStatesBefore[state]]; + } + + template + uint64_t SparseMdpEndComponentInformation::getRowGroupAfterElimination(uint64_t state) const { + return numberOfMaybeStatesNotInEc + getEc(state); + } + + template + bool SparseMdpEndComponentInformation::getEliminatedEndComponents() const { + return eliminatedEndComponents; + } + + template + uint64_t SparseMdpEndComponentInformation::getNotInEcMarker() const { + return NOT_IN_EC; + } + + template + SparseMdpEndComponentInformation SparseMdpEndComponentInformation::eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const* sumColumns, storm::storage::BitVector const* selectedChoices, std::vector const* summand, storm::storage::SparseMatrix& submatrix, std::vector* columnSumVector, std::vector* summandResultVector) { + + SparseMdpEndComponentInformation result(endComponentDecomposition, maybeStates); + + // (1) Compute the number of maybe states not in ECs before any other maybe state. + std::vector maybeStatesNotInEcBefore = result.getNumberOfMaybeStatesNotInEcBeforeIndices(); + uint64_t numberOfStates = result.numberOfMaybeStatesNotInEc + result.numberOfEc; + + STORM_LOG_TRACE("Found " << numberOfStates << " states, " << result.numberOfMaybeStatesNotInEc << " not in ECs, " << result.numberOfMaybeStatesInEc << " in ECs and " << result.numberOfEc << " ECs."); + + // Prepare builder and vector storage. + storm::storage::SparseMatrixBuilder builder(0, numberOfStates, 0, true, true, numberOfStates); + STORM_LOG_ASSERT((sumColumns && columnSumVector) || (!sumColumns && !columnSumVector), "Expecting a bit vector for which columns to sum iff there is a column sum result vector."); + if (columnSumVector) { + columnSumVector->resize(numberOfStates); + } + STORM_LOG_ASSERT((summand && summandResultVector) || (!summand && !summandResultVector), "Expecting summand iff there is a summand result vector."); + if (summandResultVector) { + summandResultVector->resize(numberOfStates); + } + std::vector> ecValuePairs; + + // (2) Create the parts of the submatrix and vector b that belong to states not contained in ECs. + uint64_t currentRow = 0; + for (auto state : maybeStates) { + if (!result.isStateInEc(state)) { + builder.newRowGroup(currentRow); + for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row < endRow; ++row) { + // If the choices is not in the selected ones, drop it. + if (selectedChoices && !selectedChoices->get(row)) { + continue; + } + + ecValuePairs.clear(); + + if (summand) { + (*summandResultVector)[currentRow] += (*summand)[row]; + } + for (auto const& e : transitionMatrix.getRow(row)) { + if (sumColumns && sumColumns->get(e.getColumn())) { + (*columnSumVector)[currentRow] += e.getValue(); + } else if (maybeStates.get(e.getColumn())) { + // If the target state of the transition is not contained in an EC, we can just add the entry. + if (result.isStateInEc(e.getColumn())) { + builder.addNextValue(currentRow, maybeStatesNotInEcBefore[result.maybeStatesBefore[e.getColumn()]], e.getValue()); + } else { + // Otherwise, we store the information that the state can go to a certain EC. + ecValuePairs.emplace_back(result.getEc(e.getColumn()), e.getValue()); + } + } + } + + if (!ecValuePairs.empty()) { + std::sort(ecValuePairs.begin(), ecValuePairs.end()); + + for (auto const& e : ecValuePairs) { + builder.addNextValue(currentRow, result.numberOfMaybeStatesNotInEc + e.first, e.second); + } + } + + ++currentRow; + } + } + } + + // (3) Create the parts of the submatrix and vector b that belong to states contained in ECs. + for (auto const& mec : endComponentDecomposition) { + builder.newRowGroup(currentRow); + + for (auto const& stateActions : mec) { + uint64_t const& state = stateActions.first; + for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row < endRow; ++row) { + // If the choice is contained in the MEC, drop it. + if (stateActions.second.find(row) != stateActions.second.end()) { + continue; + } + // If the choices is not in the selected ones, drop it. + if (selectedChoices && !selectedChoices->get(row)) { + continue; + } + + ecValuePairs.clear(); + + if (summand) { + (*summandResultVector)[currentRow] += (*summand)[row]; + } + for (auto const& e : transitionMatrix.getRow(row)) { + if (sumColumns && sumColumns->get(e.getColumn())) { + (*columnSumVector)[currentRow] += e.getValue(); + } else if (maybeStates.get(e.getColumn())) { + // If the target state of the transition is not contained in an EC, we can just add the entry. + if (result.isStateInEc(e.getColumn())) { + builder.addNextValue(currentRow, maybeStatesNotInEcBefore[result.maybeStatesBefore[e.getColumn()]], e.getValue()); + } else { + // Otherwise, we store the information that the state can go to a certain EC. + ecValuePairs.emplace_back(result.getEc(e.getColumn()), e.getValue()); + } + } + } + + if (!ecValuePairs.empty()) { + std::sort(ecValuePairs.begin(), ecValuePairs.end()); + + for (auto const& e : ecValuePairs) { + builder.addNextValue(currentRow, result.getNumberOfMaybeStatesNotInEc() + e.first, e.second); + } + } + + ++currentRow; + } + } + } + + submatrix = builder.build(); + return result; + } + + template + SparseMdpEndComponentInformation SparseMdpEndComponentInformation::eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, std::vector& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix& submatrix, std::vector& subvector) { + + SparseMdpEndComponentInformation result(endComponentDecomposition, maybeStates); + + // (1) Compute the number of maybe states not in ECs before any other maybe state. + std::vector maybeStatesNotInEcBefore = result.getNumberOfMaybeStatesNotInEcBeforeIndices(); + uint64_t numberOfStates = result.numberOfMaybeStatesNotInEc + result.numberOfEc; + + STORM_LOG_TRACE("Found " << numberOfStates << " states, " << result.numberOfMaybeStatesNotInEc << " not in ECs, " << result.numberOfMaybeStatesInEc << " in ECs and " << result.numberOfEc << " ECs."); + + // Prepare builder and vector storage. + storm::storage::SparseMatrixBuilder builder(0, numberOfStates, 0, true, true, numberOfStates); + subvector.resize(numberOfStates); + + std::vector> ecValuePairs; + + // (2) Create the parts of the submatrix and vector b that belong to states not contained in ECs. + uint64_t currentRow = 0; + for (auto state : maybeStates) { + if (!result.isStateInEc(state)) { + builder.newRowGroup(currentRow); + for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row < endRow; ++row) { + // Copy over the entry of the vector. + subvector[currentRow] = rhsVector[row]; + + ecValuePairs.clear(); + for (auto const& e : transitionMatrix.getRow(row)) { + if (maybeStates.get(e.getColumn())) { + // If the target state of the transition is not contained in an EC, we can just add the entry. + if (result.isStateInEc(e.getColumn())) { + builder.addNextValue(currentRow, maybeStatesNotInEcBefore[result.maybeStatesBefore[e.getColumn()]], e.getValue()); + } else { + // Otherwise, we store the information that the state can go to a certain EC. + ecValuePairs.emplace_back(result.getEc(e.getColumn()), e.getValue()); + } + } + } + + if (!ecValuePairs.empty()) { + std::sort(ecValuePairs.begin(), ecValuePairs.end()); + + for (auto const& e : ecValuePairs) { + builder.addNextValue(currentRow, result.numberOfMaybeStatesNotInEc + e.first, e.second); + } + } + + ++currentRow; + } + } + } + + // (3) Create the parts of the submatrix and vector b that belong to states contained in ECs. + for (auto const& mec : endComponentDecomposition) { + builder.newRowGroup(currentRow); + + for (auto const& stateActions : mec) { + uint64_t const& state = stateActions.first; + for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row < endRow; ++row) { + // If the choice is contained in the MEC, drop it. + if (stateActions.second.find(row) != stateActions.second.end()) { + continue; + } + + // Copy over the entry of the vector. + subvector[currentRow] = rhsVector[row]; + + ecValuePairs.clear(); + for (auto const& e : transitionMatrix.getRow(row)) { + if (maybeStates.get(e.getColumn())) { + // If the target state of the transition is not contained in an EC, we can just add the entry. + if (result.isStateInEc(e.getColumn())) { + builder.addNextValue(currentRow, maybeStatesNotInEcBefore[result.maybeStatesBefore[e.getColumn()]], e.getValue()); + } else { + // Otherwise, we store the information that the state can go to a certain EC. + ecValuePairs.emplace_back(result.getEc(e.getColumn()), e.getValue()); + } + } + } + + if (!ecValuePairs.empty()) { + std::sort(ecValuePairs.begin(), ecValuePairs.end()); + + for (auto const& e : ecValuePairs) { + builder.addNextValue(currentRow, result.getNumberOfMaybeStatesNotInEc() + e.first, e.second); + } + } + + ++currentRow; + } + } + } + + submatrix = builder.build(); + return result; + } + + template + void SparseMdpEndComponentInformation::setValues(std::vector& result, storm::storage::BitVector const& maybeStates, std::vector const& fromResult) { + auto notInEcResultIt = result.begin(); + for (auto state : maybeStates) { + if (this->isStateInEc(state)) { + result[state] = result[this->getRowGroupAfterElimination(state)]; + } else { + result[state] = *notInEcResultIt; + ++notInEcResultIt; + } + } + STORM_LOG_ASSERT(notInEcResultIt == result.begin() + this->getNumberOfMaybeStatesNotInEc(), "Mismatching iterators."); + } + + template class SparseMdpEndComponentInformation; + +#ifdef STORM_HAVE_CARL + template class SparseMdpEndComponentInformation; + template class SparseMdpEndComponentInformation; +#endif + + } + } +} diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h new file mode 100644 index 000000000..a8a752305 --- /dev/null +++ b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h @@ -0,0 +1,76 @@ +#pragma once + +#include +#include + +namespace storm { + namespace storage { + class BitVector; + + template + class SparseMatrix; + + template + class MaximalEndComponentDecomposition; + } + + namespace modelchecker { + namespace helper { + + template + class SparseMdpEndComponentInformation { + public: + SparseMdpEndComponentInformation(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::BitVector const& maybeStates); + + bool isMaybeStateInEc(uint64_t maybeState) const; + bool isStateInEc(uint64_t state) const; + + /*! + * Retrieves for each maybe state the number of maybe states not contained in ECs with an index smaller + * than the requested one. + */ + std::vector getNumberOfMaybeStatesNotInEcBeforeIndices() const; + + /*! + * Retrieves the total number of maybe states on in ECs. + */ + uint64_t getNumberOfMaybeStatesNotInEc() const; + + /*! + * Retrieves the EC of the state (result may be NOT_IN_EC). + */ + uint64_t getEc(uint64_t state) const; + + /*! + * Retrieves the row group of the state after end component elimination. + */ + uint64_t getRowGroupAfterElimination(uint64_t state) const; + + bool getEliminatedEndComponents() const; + + uint64_t getNotInEcMarker() const; + + static SparseMdpEndComponentInformation eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const* sumColumns, storm::storage::BitVector const* selectedChoices, std::vector const* summand, storm::storage::SparseMatrix& submatrix, std::vector* columnSumVector, std::vector* summandResultVector); + + static SparseMdpEndComponentInformation eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, std::vector& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix& submatrix, std::vector& subvector); + + void setValues(std::vector& result, storm::storage::BitVector const& maybeStates, std::vector const& fromResult); + + private: + // A constant that marks that a state is not contained in any EC. + uint64_t NOT_IN_EC; + + // A flag storing whether end components have been eliminated. + bool eliminatedEndComponents; + + // Data about end components. + std::vector maybeStatesBefore; + uint64_t numberOfMaybeStatesInEc; + uint64_t numberOfMaybeStatesNotInEc; + uint64_t numberOfEc; + std::vector maybeStateToEc; + }; + + } + } +} diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 58b1e9601..37192633a 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -6,6 +6,7 @@ #include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" #include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h" #include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h" +#include "storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -458,191 +459,6 @@ namespace storm { b = transitionMatrix.getConstrainedRowGroupSumVector(qualitativeStateSets.maybeStates, qualitativeStateSets.statesWithProbability1); } - static const uint64_t NOT_IN_EC = std::numeric_limits::max(); - - template - struct SparseMdpEndComponentInformation { - SparseMdpEndComponentInformation(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::BitVector const& maybeStates) : eliminatedEndComponents(false), numberOfMaybeStatesInEc(0), numberOfMaybeStatesNotInEc(0), numberOfEc(endComponentDecomposition.size()) { - - // (1) Compute how many maybe states there are before each other maybe state. - maybeStatesBefore = maybeStates.getNumberOfSetBitsBeforeIndices(); - - // (2) Create mapping from maybe states to their MEC. If they are not contained in an MEC, their value - // is set to a special constant. - maybeStateToEc.resize(maybeStates.getNumberOfSetBits(), NOT_IN_EC); - uint64_t mecIndex = 0; - for (auto const& mec : endComponentDecomposition) { - for (auto const& stateActions : mec) { - maybeStateToEc[maybeStatesBefore[stateActions.first]] = mecIndex; - ++numberOfMaybeStatesInEc; - } - ++mecIndex; - } - - // (3) Compute number of states not in MECs. - numberOfMaybeStatesNotInEc = maybeStateToEc.size() - numberOfMaybeStatesInEc; - } - - bool isMaybeStateInEc(uint64_t maybeState) const { - return maybeStateToEc[maybeState] != NOT_IN_EC; - } - - bool isStateInEc(uint64_t state) const { - return maybeStateToEc[maybeStatesBefore[state]] != NOT_IN_EC; - } - - std::vector getNumberOfMaybeStatesNotInEcBeforeIndices() const { - std::vector result(maybeStateToEc.size()); - - uint64_t count = 0; - auto resultIt = result.begin(); - for (auto const& e : maybeStateToEc) { - *resultIt = count; - if (e != NOT_IN_EC) { - ++count; - } - ++resultIt; - } - - return result; - } - - uint64_t getEc(uint64_t state) const { - return maybeStateToEc[maybeStatesBefore[state]]; - } - - uint64_t getSubmatrixRowGroupOfStateInEc(uint64_t state) const { - return numberOfMaybeStatesNotInEc + getEc(state); - } - - bool eliminatedEndComponents; - - std::vector maybeStatesBefore; - uint64_t numberOfMaybeStatesInEc; - uint64_t numberOfMaybeStatesNotInEc; - uint64_t numberOfEc; - - std::vector maybeStateToEc; - }; - - template - SparseMdpEndComponentInformation eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const* sumColumns, storm::storage::BitVector const* selectedChoices, std::vector const* summand, storm::storage::SparseMatrix& submatrix, std::vector* columnSumVector, std::vector* summandResultVector) { - - SparseMdpEndComponentInformation result(endComponentDecomposition, maybeStates); - - // (1) Compute the number of maybe states not in ECs before any other maybe state. - std::vector maybeStatesNotInEcBefore = result.getNumberOfMaybeStatesNotInEcBeforeIndices(); - uint64_t numberOfStates = result.numberOfMaybeStatesNotInEc + result.numberOfEc; - - STORM_LOG_TRACE("Found " << numberOfStates << " states, " << result.numberOfMaybeStatesNotInEc << " not in ECs, " << result.numberOfMaybeStatesInEc << " in ECs and " << result.numberOfEc << " ECs."); - - // Prepare builder and vector storage. - storm::storage::SparseMatrixBuilder builder(0, numberOfStates, 0, true, true, numberOfStates); - STORM_LOG_ASSERT((sumColumns && columnSumVector) || (!sumColumns && !columnSumVector), "Expecting a bit vector for which columns to sum iff there is a column sum result vector."); - if (columnSumVector) { - columnSumVector->resize(numberOfStates); - } - STORM_LOG_ASSERT((summand && summandResultVector) || (!summand && !summandResultVector), "Expecting summand iff there is a summand result vector."); - if (summandResultVector) { - summandResultVector->resize(numberOfStates); - } - std::vector> ecValuePairs; - - // (2) Create the parts of the submatrix and vector b that belong to states not contained in ECs. - uint64_t currentRow = 0; - for (auto state : maybeStates) { - if (!result.isStateInEc(state)) { - builder.newRowGroup(currentRow); - for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row < endRow; ++row) { - // If the choices is not in the selected ones, drop it. - if (selectedChoices && !selectedChoices->get(row)) { - continue; - } - - ecValuePairs.clear(); - - if (summand) { - (*summandResultVector)[currentRow] += (*summand)[row]; - } - for (auto const& e : transitionMatrix.getRow(row)) { - if (sumColumns && sumColumns->get(e.getColumn())) { - (*columnSumVector)[currentRow] += e.getValue(); - } else if (maybeStates.get(e.getColumn())) { - // If the target state of the transition is not contained in an EC, we can just add the entry. - if (result.isStateInEc(e.getColumn())) { - builder.addNextValue(currentRow, maybeStatesNotInEcBefore[result.maybeStatesBefore[e.getColumn()]], e.getValue()); - } else { - // Otherwise, we store the information that the state can go to a certain EC. - ecValuePairs.emplace_back(result.getEc(e.getColumn()), e.getValue()); - } - } - } - - if (!ecValuePairs.empty()) { - std::sort(ecValuePairs.begin(), ecValuePairs.end()); - - for (auto const& e : ecValuePairs) { - builder.addNextValue(currentRow, result.numberOfMaybeStatesNotInEc + e.first, e.second); - } - } - - ++currentRow; - } - } - } - - // (3) Create the parts of the submatrix and vector b that belong to states contained in ECs. - for (auto const& mec : endComponentDecomposition) { - builder.newRowGroup(currentRow); - - for (auto const& stateActions : mec) { - uint64_t const& state = stateActions.first; - for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row < endRow; ++row) { - // If the choice is contained in the MEC, drop it. - if (stateActions.second.find(row) != stateActions.second.end()) { - continue; - } - // If the choices is not in the selected ones, drop it. - if (selectedChoices && !selectedChoices->get(row)) { - continue; - } - - ecValuePairs.clear(); - - if (summand) { - (*summandResultVector)[currentRow] += (*summand)[row]; - } - for (auto const& e : transitionMatrix.getRow(row)) { - if (sumColumns && sumColumns->get(e.getColumn())) { - (*columnSumVector)[currentRow] += e.getValue(); - } else if (maybeStates.get(e.getColumn())) { - // If the target state of the transition is not contained in an EC, we can just add the entry. - if (result.isStateInEc(e.getColumn())) { - builder.addNextValue(currentRow, maybeStatesNotInEcBefore[result.maybeStatesBefore[e.getColumn()]], e.getValue()); - } else { - // Otherwise, we store the information that the state can go to a certain EC. - ecValuePairs.emplace_back(result.getEc(e.getColumn()), e.getValue()); - } - } - } - - if (!ecValuePairs.empty()) { - std::sort(ecValuePairs.begin(), ecValuePairs.end()); - - for (auto const& e : ecValuePairs) { - builder.addNextValue(currentRow, result.numberOfMaybeStatesNotInEc + e.first, e.second); - } - } - - ++currentRow; - } - } - } - - submatrix = builder.build(); - return result; - } - template boost::optional> computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, QualitativeStateSetsUntilProbabilities const& qualitativeStateSets, storm::storage::SparseMatrix& submatrix, std::vector& b) { @@ -651,29 +467,15 @@ namespace storm { // Only do more work if there are actually end-components. if (!endComponentDecomposition.empty()) { - STORM_LOG_DEBUG("Eliminating " << endComponentDecomposition.size() << " ECs."); - return eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, &qualitativeStateSets.statesWithProbability1, nullptr, nullptr, submatrix, &b, nullptr); + STORM_LOG_DEBUG("Eliminating " << endComponentDecomposition.size() << " EC(s)."); + return SparseMdpEndComponentInformation::eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, &qualitativeStateSets.statesWithProbability1, nullptr, nullptr, submatrix, &b, nullptr); } else { STORM_LOG_DEBUG("Not eliminating ECs as there are none."); computeFixedPointSystemUntilProbabilities(transitionMatrix, qualitativeStateSets, submatrix, b); return boost::none; } } - - template - void setResultValuesWrtEndComponents(SparseMdpEndComponentInformation const& ecInformation, std::vector& result, storm::storage::BitVector const& maybeStates, std::vector const& fromResult) { - auto notInEcResultIt = result.begin(); - for (auto state : maybeStates) { - if (ecInformation.isStateInEc(state)) { - result[state] = result[ecInformation.getSubmatrixRowGroupOfStateInEc(state)]; - } else { - result[state] = *notInEcResultIt; - ++notInEcResultIt; - } - } - STORM_LOG_ASSERT(notInEcResultIt == result.begin() + ecInformation.numberOfMaybeStatesNotInEc, "Mismatching iterators."); - } - + template MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { STORM_LOG_THROW(!qualitative || !produceScheduler, storm::exceptions::InvalidSettingsException, "Cannot produce scheduler when performing qualitative model checking only."); @@ -717,7 +519,7 @@ namespace storm { ecInformation = computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(transitionMatrix, backwardTransitions, qualitativeStateSets, submatrix, b); // Make sure we are not supposed to produce a scheduler if we actually eliminate end components. - STORM_LOG_THROW(!ecInformation || !ecInformation.get().eliminatedEndComponents || !produceScheduler, storm::exceptions::NotSupportedException, "Producing schedulers is not supported if end-components need to be eliminated for the solver."); + STORM_LOG_THROW(!ecInformation || !ecInformation.get().getEliminatedEndComponents() || !produceScheduler, storm::exceptions::NotSupportedException, "Producing schedulers is not supported if end-components need to be eliminated for the solver."); } else { // Otherwise, we compute the standard equations. computeFixedPointSystemUntilProbabilities(transitionMatrix, qualitativeStateSets, submatrix, b); @@ -728,8 +530,8 @@ namespace storm { MaybeStateResult resultForMaybeStates = computeValuesForMaybeStates(std::move(goal), std::move(submatrix), b, produceScheduler, minMaxLinearEquationSolverFactory, hintInformation); // If we eliminated end components, we need to extract the result differently. - if (ecInformation && ecInformation.get().eliminatedEndComponents) { - setResultValuesWrtEndComponents(ecInformation.get(), result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); + if (ecInformation && ecInformation.get().getEliminatedEndComponents()) { + ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); } else { // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); @@ -987,7 +789,7 @@ namespace storm { // Only do more work if there are actually end-components. if (doDecomposition && !endComponentDecomposition.empty()) { STORM_LOG_DEBUG("Eliminating " << endComponentDecomposition.size() << " ECs."); - return eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, oneStepTargetProbabilities ? &targetStates : nullptr, selectedChoices ? &selectedChoices.get() : nullptr, &rewardVector, submatrix, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr, &b); + return SparseMdpEndComponentInformation::eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, oneStepTargetProbabilities ? &targetStates : nullptr, selectedChoices ? &selectedChoices.get() : nullptr, &rewardVector, submatrix, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr, &b); } else { STORM_LOG_DEBUG("Not eliminating ECs as there are none."); computeFixedPointSystemReachabilityRewards(transitionMatrix, qualitativeStateSets, targetStates, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr); @@ -1063,7 +865,7 @@ namespace storm { ecInformation = computeFixedPointSystemReachabilityRewardsEliminateEndComponents(transitionMatrix, backwardTransitions, qualitativeStateSets, targetStates, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities); // Make sure we are not supposed to produce a scheduler if we actually eliminate end components. - STORM_LOG_THROW(!ecInformation || !ecInformation.get().eliminatedEndComponents || !produceScheduler, storm::exceptions::NotSupportedException, "Producing schedulers is not supported if end-components need to be eliminated for the solver."); + STORM_LOG_THROW(!ecInformation || !ecInformation.get().getEliminatedEndComponents() || !produceScheduler, storm::exceptions::NotSupportedException, "Producing schedulers is not supported if end-components need to be eliminated for the solver."); } else { // Otherwise, we compute the standard equations. computeFixedPointSystemReachabilityRewards(transitionMatrix, qualitativeStateSets, targetStates, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr); @@ -1080,8 +882,8 @@ namespace storm { MaybeStateResult resultForMaybeStates = computeValuesForMaybeStates(std::move(goal), std::move(submatrix), b, produceScheduler, minMaxLinearEquationSolverFactory, hintInformation); // If we eliminated end components, we need to extract the result differently. - if (ecInformation && ecInformation.get().eliminatedEndComponents) { - setResultValuesWrtEndComponents(ecInformation.get(), result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); + if (ecInformation && ecInformation.get().getEliminatedEndComponents()) { + ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); } else { // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); diff --git a/src/storm/settings/modules/NativeEquationSolverSettings.cpp b/src/storm/settings/modules/NativeEquationSolverSettings.cpp index 1715fc78c..aa3a948ee 100644 --- a/src/storm/settings/modules/NativeEquationSolverSettings.cpp +++ b/src/storm/settings/modules/NativeEquationSolverSettings.cpp @@ -121,7 +121,9 @@ namespace storm { case NativeEquationSolverSettings::LinearEquationMethod::SOR: out << "sor"; break; case NativeEquationSolverSettings::LinearEquationMethod::WalkerChae: out << "walkerchae"; break; case NativeEquationSolverSettings::LinearEquationMethod::Power: out << "power"; break; + case NativeEquationSolverSettings::LinearEquationMethod::RationalSearch: out << "ratsearch"; break; } + return out; } } // namespace modules diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index 3cf349c69..c41455e16 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -189,7 +189,7 @@ namespace storm { template void MinMaxLinearEquationSolverFactory::setMinMaxMethod(MinMaxMethod const& newMethod) { - STORM_LOG_WARN_COND(!(std::is_same::value) || newMethod == MinMaxMethod::PolicyIteration, "The selected solution method does not guarantee exact results. Consider using policy iteration."); + STORM_LOG_WARN_COND(!(std::is_same::value) || (newMethod == MinMaxMethod::PolicyIteration || newMethod == MinMaxMethod::RationalSearch), "The selected solution method does not guarantee exact results. Consider using policy iteration."); method = newMethod; } diff --git a/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp b/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp index 4c216181f..005d57977 100644 --- a/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp @@ -37,7 +37,7 @@ namespace storm { return noEndComponents; } - bool MinMaxLinearEquationSolverRequirements::requiresValidIntialScheduler() const { + bool MinMaxLinearEquationSolverRequirements::requiresValidInitialScheduler() const { return validInitialScheduler; } diff --git a/src/storm/solver/MinMaxLinearEquationSolverRequirements.h b/src/storm/solver/MinMaxLinearEquationSolverRequirements.h index 123b5e440..33e3511ad 100644 --- a/src/storm/solver/MinMaxLinearEquationSolverRequirements.h +++ b/src/storm/solver/MinMaxLinearEquationSolverRequirements.h @@ -29,7 +29,7 @@ namespace storm { MinMaxLinearEquationSolverRequirements& requireBounds(); bool requiresNoEndComponents() const; - bool requiresValidIntialScheduler() const; + bool requiresValidInitialScheduler() const; bool requiresLowerBounds() const; bool requiresUpperBounds() const; bool requires(Element const& element) const; diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 1cd70c0fd..889734d45 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -1056,22 +1056,30 @@ namespace storm { template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + return performProb01Max(model, model.getTransitionMatrix().notZero(), phiStates, psiStates); + } + + template + std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { std::pair, storm::dd::Bdd> result; - storm::dd::Bdd transitionMatrix = model.getTransitionMatrix().notZero(); result.first = performProb0A(model, transitionMatrix, phiStates, psiStates); result.second = performProb1E(model, transitionMatrix, phiStates, psiStates, !result.first && model.getReachableStates()); return result; } - + template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + return performProb01Min(model, model.getTransitionMatrix().notZero(), phiStates, psiStates); + } + + template + std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { std::pair, storm::dd::Bdd> result; - storm::dd::Bdd transitionMatrix = model.getTransitionMatrix().notZero(); result.first = performProb0E(model, transitionMatrix, phiStates, psiStates); result.second = performProb1A(model, transitionMatrix, psiStates, !result.first && model.getReachableStates()); return result; } - + template GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) { @@ -1550,9 +1558,13 @@ namespace storm { template storm::dd::Bdd computeSchedulerProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbability1E); template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - + + template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - + + template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); template GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional> const& player1Candidates); @@ -1586,9 +1598,13 @@ namespace storm { template storm::dd::Bdd computeSchedulerProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbability1E); template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - + + template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); template GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional> const& player1Candidates); @@ -1622,9 +1638,13 @@ namespace storm { template storm::dd::Bdd computeSchedulerProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbability1E); template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - + + template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - + + template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + // Instantiations for Sylvan (rational function). template storm::dd::Bdd performProbGreater0(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, boost::optional const& stepBound = boost::optional()); @@ -1654,9 +1674,13 @@ namespace storm { template storm::dd::Bdd computeSchedulerProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbability1E); template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - + + template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - + + template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + } // namespace graph } // namespace utility } // namespace storm diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index d0f3dde15..79cefffc2 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -529,10 +529,16 @@ namespace storm { template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - + + template + std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template + std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template struct GameProb01Result { GameProb01Result() = default;