diff --git a/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp b/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp index f6ecc1055..ed51aa0fa 100644 --- a/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp +++ b/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp @@ -12,6 +12,8 @@ #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/models/sparse/StandardRewardModel.h" + #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" @@ -157,13 +159,14 @@ namespace storm { } template - void SparseMdpLearningModelChecker::detectEndComponents(std::vector> const& stateActionStack, boost::container::flat_set const& targetStates, std::vector>> const& transitionMatrix, std::vector const& rowGroupIndices, std::vector const& stateToRowGroupMapping, std::vector& lowerBoundsPerAction, std::vector& upperBoundsPerAction, std::vector& lowerBoundsPerState, std::vector& upperBoundsPerState, std::unordered_map& unexploredStates, StateType const& unexploredMarker) const { + void SparseMdpLearningModelChecker::detectEndComponents(std::vector> const& stateActionStack, boost::container::flat_set const& targetStates, std::vector>>& transitionMatrix, std::vector const& rowGroupIndices, std::vector const& stateToRowGroupMapping, std::vector& lowerBoundsPerAction, std::vector& upperBoundsPerAction, std::vector& lowerBoundsPerState, std::vector& upperBoundsPerState, std::unordered_map& unexploredStates, StateType const& unexploredMarker) const { + + STORM_LOG_TRACE("Starting EC detection."); // Outline: // 1. construct a sparse transition matrix of the relevant part of the state space. // 2. use this matrix to compute an MEC decomposition. // 3. if non-empty analyze the decomposition for accepting/rejecting MECs. - // 4. modify matrix to account for the findings of 3. // Start with 1. storm::storage::SparseMatrixBuilder builder(0, 0, 0, false, true, 0); @@ -196,19 +199,52 @@ namespace storm { unexpandedProbability += entry.getValue(); } } - builder.addNextValue(currentRow, unexploredState, unexpandedProbability); + if (unexpandedProbability != storm::utility::zero()) { + builder.addNextValue(currentRow, unexploredState, unexpandedProbability); + } ++currentRow; } } + // Finally, make the unexpanded state absorbing. builder.newRowGroup(currentRow); - + builder.addNextValue(currentRow, unexploredState, storm::utility::one()); + STORM_LOG_TRACE("Successfully built matrix for MEC decomposition."); // Go on to step 2. - storm::storage::MaximalEndComponentDecomposition mecDecomposition; + storm::storage::SparseMatrix relevantStatesMatrix = builder.build(); + storm::storage::MaximalEndComponentDecomposition mecDecomposition(relevantStatesMatrix, relevantStatesMatrix.transpose(true)); + STORM_LOG_TRACE("Successfully computed MEC decomposition. Found " << (mecDecomposition.size() > 1 ? (mecDecomposition.size() - 1) : 0) << " MEC(s)."); // 3. Analyze the MEC decomposition. + std::unordered_map> stateToOutgoingChoices; + for (auto const& mec : mecDecomposition) { + // Ignore the (expected) MEC of the unexplored state. + if (mec.containsState(unexploredState)) { + continue; + } + + // Now we delete all choices that belong to the MEC. + for (auto const& stateAndChoices : mec) { + // Compute the state of the original model that corresponds to the current state. + StateType originalState = stateToRowGroupMapping[relevantStates[relevantStateToNewRowGroupMapping.at(stateAndChoices.first)]]; + + auto includedChoicesIt = stateAndChoices.second.begin(); + auto includedChoicesIte = stateAndChoices.second.end(); + + // Now iterate through all the choices and delete the ones included in the MEC and record outgoing + // choices (to make them available in the other states of the EC). + for (auto choice = rowGroupIndices[originalState]; choice < rowGroupIndices[originalState + 1]; ++choice) { + if (includedChoicesIt != includedChoicesIte && choice - rowGroupIndices[originalState] == *includedChoicesIt - relevantStatesMatrix.getRowGroupIndices()[stateAndChoices.first]) { + transitionMatrix[choice].clear(); + transitionMatrix[choice].shrink_to_fit(); + } else { + + } + } + } + } - // 4. Finally modify the system + exit(-1); } template diff --git a/src/modelchecker/reachability/SparseMdpLearningModelChecker.h b/src/modelchecker/reachability/SparseMdpLearningModelChecker.h index 60dc25bc2..9d4820b51 100644 --- a/src/modelchecker/reachability/SparseMdpLearningModelChecker.h +++ b/src/modelchecker/reachability/SparseMdpLearningModelChecker.h @@ -50,7 +50,7 @@ namespace storm { StateType sampleSuccessorFromAction(StateType currentStateId, std::vector>> const& transitionMatrix, std::vector const& rowGroupIndices, std::vector const& stateToRowGroupMapping); - void detectEndComponents(std::vector> const& stateActionStack, boost::container::flat_set const& targetStates, std::vector>> const& transitionMatrix, std::vector const& rowGroupIndices, std::vector const& stateToRowGroupMapping, std::vector& lowerBoundsPerAction, std::vector& upperBoundsPerAction, std::vector& lowerBoundsPerState, std::vector& upperBoundsPerState, std::unordered_map& unexploredStates, StateType const& unexploredMarker) const; + void detectEndComponents(std::vector> const& stateActionStack, boost::container::flat_set const& targetStates, std::vector>>& transitionMatrix, std::vector const& rowGroupIndices, std::vector const& stateToRowGroupMapping, std::vector& lowerBoundsPerAction, std::vector& upperBoundsPerAction, std::vector& lowerBoundsPerState, std::vector& upperBoundsPerState, std::unordered_map& unexploredStates, StateType const& unexploredMarker) const; storm::expressions::Expression getTargetStateExpression(storm::logic::Formula const& subformula); diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index 31c421224..87c4bc509 100644 --- a/src/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -74,7 +74,7 @@ namespace storm { // from iterator to const_iterator only for "set, multiset, map [and] multimap". for (std::list::const_iterator mecIterator = endComponentStateSets.begin(); mecIterator != endComponentStateSets.end();) { StateBlock const& mec = *mecIterator; - + // Keep track of whether the MEC changed during this iteration. bool mecChanged = false; @@ -98,6 +98,10 @@ namespace storm { for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { bool choiceContainedInMEC = true; for (auto const& entry : transitionMatrix.getRow(choice)) { + if (entry.getValue() != storm::utility::zero()) { + continue; + } + if (!scc.containsState(entry.getColumn())) { choiceContainedInMEC = false; break;