sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

finding MSECs done, in progress: deflating the MSECs

main
Fabian Russold 7 months ago
committed by sp
parent
61b59e64fc
commit
9a41444217
3 changed files with 44 additions and 10 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
  2. 44
      src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
  3. 8
      src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h

2
src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
View File

@ -63,7 +63,7 @@ namespace storm {
template<typename ValueType>
SMGSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeUntilProbabilitiesSound(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) {
storm::modelchecker::helper::internal::SoundGameViHelper<ValueType> viHelper(transitionMatrix, statesOfCoalition, goal.direction());
storm::modelchecker::helper::internal::SoundGameViHelper<ValueType> viHelper(transitionMatrix, backwardTransitions, statesOfCoalition, goal.direction());
// Initialize the x vector and solution vector result.
// TODO Fabian: maybe relevant states (later)

44
src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
View File

@ -14,7 +14,7 @@ namespace storm {
namespace internal {
template <typename ValueType>
SoundGameViHelper<ValueType>::SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition), _optimizationDirection(optimizationDirection) {
SoundGameViHelper<ValueType>::SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _backwardTransitions(backwardTransitions), _statesOfCoalition(statesOfCoalition), _optimizationDirection(optimizationDirection) {
// Intentionally left empty.
}
@ -34,7 +34,6 @@ namespace storm {
// Get precision for convergence check.
ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().game().getPrecision());
STORM_LOG_DEBUG("hello" << "world");
uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations();
//_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
_x1L = xL;
@ -97,14 +96,48 @@ namespace storm {
_multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), nullptr, &_statesOfCoalition);
// restricting the none optimal minimizer choices
storage::SparseMatrix<ValueType> restrictedTransMatrix = this->_transitionMatrix.restrictRows(reducedMinimizerActions);
// storage::SparseMatrix<ValueType> restrictedBackMatrix = this->_backwardTransitions.restrictRows(reducedMinimizerActions);
STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix);
// TODO Fabian: find_MSECs() & deflate()
storm::storage::MaximalEndComponentDecomposition<ValueType> MECD = storm::storage::MaximalEndComponentDecomposition<ValueType>(restrictedTransMatrix, _backwardTransitions);
STORM_LOG_DEBUG("MECD: \n" << MECD);
// deflate(MECD,restrictedTransMatrix, xNewU());
}
template <typename ValueType>
void SoundGameViHelper<ValueType>::deflate(storm::storage::MaximalEndComponentDecomposition<ValueType> const MECD, storage::SparseMatrix<ValueType> const restrictedMatrix, std::vector<ValueType>& xU)
{
/* auto rowGroupIndices = restrictedMatrix.getRowGroupIndices();
auto mec_it = MECD.begin();
for(uint state = 0; state < rowGroupIndices.size() - 1; state++) {
uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state];
ValueType optChoice;
if (!_minimizerStates[state]) { // check if current state is maximizer state
// getting the optimal minimizer choice for the given state
optChoice = *std::min_element(choice_it, choice_it + rowGroupSize);
for (uint choice = 0; choice < rowGroupSize; choice++, choice_it++) {
if (*choice_it > optChoice) {
result->set(rowGroupIndices[state] + choice, 0);
}
}
// reducing the xNew() (choiceValues) vector for minimizer states
choiceValues[state] = optChoice;
}
} */
}
template <typename ValueType>
void SoundGameViHelper<ValueType>::reduceChoiceValues(std::vector<ValueType>& choiceValues, storm::storage::BitVector* result)
{
// result BitVec should be initialized with 1s outside the function
// restrict rows
// result BitVec should be initialized with 1s outside the method
auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices();
auto choice_it = choiceValues.begin();
@ -137,8 +170,6 @@ namespace storm {
}
}
choiceValues.resize(this->_transitionMatrix.getRowGroupCount());
STORM_LOG_DEBUG("reduced BitVec: " << *result);
STORM_LOG_DEBUG("reduced x Vector: " << choiceValues);
}
@ -177,6 +208,7 @@ namespace storm {
_produceScheduler = value;
}
template <typename ValueType>
bool SoundGameViHelper<ValueType>::isProduceSchedulerSet() const {
return _produceScheduler;

8
src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h
View File

@ -4,6 +4,7 @@
#include "storm/solver/LinearEquationSolver.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/solver/Multiplier.h"
#include "storm/storage/MaximalEndComponentDecomposition.h"
namespace storm {
class Environment;
@ -19,7 +20,7 @@ namespace storm {
template <typename ValueType>
class SoundGameViHelper {
public:
SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection);
SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection);
void prepareSolversAndMultipliers(const Environment& env);
@ -73,9 +74,9 @@ namespace storm {
*/
void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);
void deflate(storm::storage::MaximalEndComponentDecomposition<ValueType> const MECD, storage::SparseMatrix<ValueType> const restrictedMatrix, std::vector<ValueType>& xU);
void reduceChoiceValues(std::vector<ValueType>& choiceValues, storm::storage::BitVector* result);
//
// für alle minimizer states -> reduce zu optimal actions
/*!
* Checks whether the curently computed value achieves the desired precision
@ -111,6 +112,7 @@ namespace storm {
std::vector<uint64_t>& getProducedOptimalChoices();
storm::storage::SparseMatrix<ValueType> _transitionMatrix;
storm::storage::SparseMatrix<ValueType> _backwardTransitions;
storm::storage::BitVector _statesOfCoalition;
std::vector<ValueType> _x, _x1L, _x2L, _x1U, _x2U;
std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier;

Write Preview
Loading…
Cancel
Save