Browse Source

fixed bug in sparse bisimulation quotient extraction related to rewards

tempestpy_adaptions
dehnert 7 years ago
parent
commit
d90c507431
  1. 18
      src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
  2. 2
      src/storm/solver/NativeLinearEquationSolver.cpp
  3. 18
      src/storm/storage/dd/bisimulation/QuotientExtractor.cpp

18
src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@ -124,23 +124,29 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
bool IterativeMinMaxLinearEquationSolver<ValueType>::internalSolveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const { bool IterativeMinMaxLinearEquationSolver<ValueType>::internalSolveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
bool result = false;
switch (this->getSettings().getSolutionMethod()) { switch (this->getSettings().getSolutionMethod()) {
case IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration: case IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration:
if (this->getSettings().getForceSoundness()) { if (this->getSettings().getForceSoundness()) {
return solveEquationsSoundValueIteration(dir, x, b);
result = solveEquationsSoundValueIteration(dir, x, b);
} else { } else {
return solveEquationsValueIteration(dir, x, b);
result = solveEquationsValueIteration(dir, x, b);
} }
break;
case IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration: case IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration:
return solveEquationsPolicyIteration(dir, x, b);
result = solveEquationsPolicyIteration(dir, x, b);
break;
case IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::Acyclic: case IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::Acyclic:
return solveEquationsAcyclic(dir, x, b);
result = solveEquationsAcyclic(dir, x, b);
break;
case IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::RationalSearch: case IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::RationalSearch:
return solveEquationsRationalSearch(dir, x, b);
result = solveEquationsRationalSearch(dir, x, b);
break;
default: default:
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "This solver does not implement the selected solution method"); STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "This solver does not implement the selected solution method");
} }
return false;
return result;
} }
template<typename ValueType> template<typename ValueType>

2
src/storm/solver/NativeLinearEquationSolver.cpp

@ -86,7 +86,7 @@ namespace storm {
void NativeLinearEquationSolverSettings<ValueType>::setForceSoundness(bool value) { void NativeLinearEquationSolverSettings<ValueType>::setForceSoundness(bool value) {
forceSoundness = value; forceSoundness = value;
if (forceSoundness && method != SolutionMethod::Power && method != SolutionMethod::RationalSearch) { if (forceSoundness && method != SolutionMethod::Power && method != SolutionMethod::RationalSearch) {
STORM_LOG_WARN("To guarantee soundness, the equation solving technique has been switched to '" << storm::settings::modules::NativeEquationSolverSettings::LinearEquationMethod::Power << "'.");
STORM_LOG_INFO("To guarantee soundness, the equation solving technique has been switched to '" << storm::settings::modules::NativeEquationSolverSettings::LinearEquationMethod::Power << "'.");
method = SolutionMethod::Power; method = SolutionMethod::Power;
} }
} }

18
src/storm/storage/dd/bisimulation/QuotientExtractor.cpp

@ -269,18 +269,13 @@ namespace storm {
} else { } else {
STORM_LOG_ASSERT(!this->rowPermutation.empty(), "Expected proper row permutation."); STORM_LOG_ASSERT(!this->rowPermutation.empty(), "Expected proper row permutation.");
std::vector<ValueType> valueVector = extractVectorInternal(vector, this->allSourceVariablesCube, this->nondeterminismOdd); std::vector<ValueType> valueVector = extractVectorInternal(vector, this->allSourceVariablesCube, this->nondeterminismOdd);
// Reorder the values according to the known row permutation. // Reorder the values according to the known row permutation.
for (uint64_t position = 0; position < valueVector.size(); ) {
if (rowPermutation[position] != position) {
std::swap(valueVector[position], valueVector[rowPermutation[position]]);
std::swap(rowPermutation[position], rowPermutation[rowPermutation[position]]);
} else {
++position;
}
std::vector<ValueType> reorderedValues(valueVector.size());
for (uint64_t pos = 0; pos < valueVector.size(); ++pos) {
reorderedValues[pos] = valueVector[rowPermutation[pos]];
} }
return valueVector;
return reorderedValues;
} }
} }
@ -857,7 +852,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> quotientTransitionMatrix = sparseExtractor.extractTransitionMatrix(model.getTransitionMatrix()); storm::storage::SparseMatrix<ValueType> quotientTransitionMatrix = sparseExtractor.extractTransitionMatrix(model.getTransitionMatrix());
auto end = std::chrono::high_resolution_clock::now(); auto end = std::chrono::high_resolution_clock::now();
STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms."); STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
start = std::chrono::high_resolution_clock::now(); start = std::chrono::high_resolution_clock::now();
storm::models::sparse::StateLabeling quotientStateLabeling(partition.getNumberOfBlocks()); storm::models::sparse::StateLabeling quotientStateLabeling(partition.getNumberOfBlocks());
quotientStateLabeling.addLabel("init", sparseExtractor.extractSetExists(model.getInitialStates())); quotientStateLabeling.addLabel("init", sparseExtractor.extractSetExists(model.getInitialStates()));
@ -892,7 +887,6 @@ namespace storm {
boost::optional<std::vector<ValueType>> quotientStateActionRewards; boost::optional<std::vector<ValueType>> quotientStateActionRewards;
if (rewardModel.hasStateActionRewards()) { if (rewardModel.hasStateActionRewards()) {
rewardModel.getStateActionRewardVector().exportToDot("vector.dot");
quotientStateActionRewards = sparseExtractor.extractStateActionVector(rewardModel.getStateActionRewardVector()); quotientStateActionRewards = sparseExtractor.extractStateActionVector(rewardModel.getStateActionRewardVector());
} }

Loading…
Cancel
Save