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

basic implementation done

main
Fabian Russold 7 months ago
committed by sp
parent
9a41444217
commit
2de38edbff
3 changed files with 39 additions and 30 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. 63
      src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
  3. 4
      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, backwardTransitions, statesOfCoalition, goal.direction());
storm::modelchecker::helper::internal::SoundGameViHelper<ValueType> viHelper(transitionMatrix, backwardTransitions, statesOfCoalition, psiStates, goal.direction());
// Initialize the x vector and solution vector result.
// TODO Fabian: maybe relevant states (later)

63
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::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _backwardTransitions(backwardTransitions), _statesOfCoalition(statesOfCoalition), _optimizationDirection(optimizationDirection) {
SoundGameViHelper<ValueType>::SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector statesOfCoalition, storm::storage::BitVector psiStates, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _backwardTransitions(backwardTransitions), _statesOfCoalition(statesOfCoalition), _psiStates(psiStates), _optimizationDirection(optimizationDirection) {
// Intentionally left empty.
}
@ -98,40 +98,47 @@ namespace storm {
// restricting the none optimal minimizer choices
storage::SparseMatrix<ValueType> restrictedTransMatrix = this->_transitionMatrix.restrictRows(reducedMinimizerActions);
_multiplierRestricted = storm::solver::MultiplierFactory<ValueType>().create(env, restrictedTransMatrix);
// storage::SparseMatrix<ValueType> restrictedBackMatrix = this->_backwardTransitions.restrictRows(reducedMinimizerActions);
STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix);
// storage::SparseMatrix<ValueType> restrictedBackMatrix = this->_backwardTransitions.restrictRows(reducedMinimizerActions);
// STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix);
// TODO Fabian: find_MSECs() & deflate()
// find_MSECs() & deflate()
storm::storage::MaximalEndComponentDecomposition<ValueType> MECD = storm::storage::MaximalEndComponentDecomposition<ValueType>(restrictedTransMatrix, _backwardTransitions);
STORM_LOG_DEBUG("MECD: \n" << MECD);
// deflate(MECD,restrictedTransMatrix, xNewU());
// 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);
void SoundGameViHelper<ValueType>::deflate(storm::storage::MaximalEndComponentDecomposition<ValueType> const MECD, storage::SparseMatrix<ValueType> const restrictedMatrix, std::vector<ValueType>& xU) {
auto rowGroupIndices = restrictedMatrix.getRowGroupIndices();
// iterating over all MSECs
for (auto smec_it : MECD) {
ValueType bestExit = 0;
for (uint state = 0; state < rowGroupIndices.size() - 1; state++) {
uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state];
if (!_minimizerStates[state] && smec_it.containsState(state)) { // check if current state is maximizer state
// getting the optimal minimizer choice for the given state
for (uint choice = 0; choice < rowGroupSize; choice++) {
if (!smec_it.containsChoice(state, choice + rowGroupIndices[state])) {
ValueType choiceValue = 0;
_multiplierRestricted->multiplyRow(choice + rowGroupIndices[state], xU, choiceValue);
if (choiceValue > bestExit)
bestExit = choiceValue;
}
}
}
// reducing the xNew() (choiceValues) vector for minimizer states
choiceValues[state] = optChoice;
}
} */
auto stateSet = smec_it.getStateSet();
for (auto smec_state : stateSet)
{
if (!_psiStates[smec_state])
xU[smec_state] = std::min(xU[smec_state], bestExit);
}
}
}
template <typename ValueType>
@ -178,9 +185,9 @@ namespace storm {
STORM_LOG_ASSERT(_multiplier, "tried to check for convergence without doing an iteration first.");
// Now check whether the currently produced results are precise enough
STORM_LOG_ASSERT(threshold > storm::utility::zero<ValueType>(), "Did not expect a non-positive threshold.");
auto x1It = xOldL().begin();
auto x1Ite = xOldL().end();
auto x2It = xNewL().begin();
auto x1It = xNewL().begin();
auto x1Ite = xNewL().end();
auto x2It = xNewU().begin();
ValueType maxDiff = (*x2It - *x1It);
ValueType minDiff = maxDiff;
// The difference between maxDiff and minDiff is zero at this point. Thus, it doesn't make sense to check the threshold now.

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

@ -20,7 +20,7 @@ namespace storm {
template <typename ValueType>
class SoundGameViHelper {
public:
SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection);
SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector statesOfCoalition, storm::storage::BitVector psiStates, OptimizationDirection const& optimizationDirection);
void prepareSolversAndMultipliers(const Environment& env);
@ -114,8 +114,10 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> _transitionMatrix;
storm::storage::SparseMatrix<ValueType> _backwardTransitions;
storm::storage::BitVector _statesOfCoalition;
storm::storage::BitVector _psiStates;
std::vector<ValueType> _x, _x1L, _x2L, _x1U, _x2U;
std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier;
std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplierRestricted;
OptimizationDirection _optimizationDirection;
bool _produceScheduler = false;

Write Preview
Loading…
Cancel
Save