diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 836b020aa..2487dcd86 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -65,6 +65,7 @@ namespace storm { rpatl.setProbabilityOperatorsAllowed(true); rpatl.setReachabilityProbabilityFormulasAllowed(true); + rpatl.setUntilFormulasAllowed(true); return rpatl; } diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index c075ab6af..97dc26054 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -110,6 +110,8 @@ namespace storm { storm::logic::Formula const& formula = checkTask.getFormula(); if (formula.isReachabilityProbabilityFormula()) { return this->computeReachabilityProbabilities(env, checkTask.substituteFormula(formula.asReachabilityProbabilityFormula())); + } else if (formula.isUntilFormula()) { + return this->computeUntilProbabilities(env, checkTask.substituteFormula(formula.asUntilFormula())); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 9bf5a10e8..8d254b01f 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -23,34 +23,18 @@ namespace storm { // Initialize the solution vector. std::vector x = std::vector(transitionMatrix.getRowGroupCount() - psiStates.getNumberOfSetBits(), storm::utility::zero()); - std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(~psiStates, psiStates); - // Reduce matrix to ~Prob1 states- - //STORM_LOG_DEBUG("\n" << transitionMatrix); - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, ~psiStates, ~psiStates, false); - //STORM_LOG_DEBUG("\n" << submatrix); + // Relevant states are those states which are phiStates and not PsiStates. + storm::storage::BitVector relevantStates = phiStates & ~psiStates; + std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates); - //STORM_LOG_DEBUG("x = " << storm::utility::vector::toString(x)); - //STORM_LOG_DEBUG("b = " << storm::utility::vector::toString(b)); + // Reduce the matrix to relevant states + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); - storm::storage::BitVector clippedStatesOfCoalition(statesOfCoalition.size() - psiStates.getNumberOfSetBits()); - //STORM_LOG_DEBUG(psiStates); - //STORM_LOG_DEBUG(statesOfCoalition); - //STORM_LOG_DEBUG(clippedStatesOfCoalition); - - // TODO move this to BitVector-class - auto clippedStatesCounter = 0; - for(uint i = 0; i < psiStates.size(); i++) { - std::cout << i << " : " << psiStates.get(i) << " -> " << statesOfCoalition[i] << std::endl; - if(!psiStates.get(i)) { - clippedStatesOfCoalition.set(clippedStatesCounter, statesOfCoalition[i]); - clippedStatesCounter++; - } - } - //STORM_LOG_DEBUG(clippedStatesOfCoalition); + storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); + clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); clippedStatesOfCoalition.complement(); - //STORM_LOG_DEBUG(clippedStatesOfCoalition); storm::modelchecker::helper::internal::GameViHelper viHelper(submatrix, clippedStatesOfCoalition); std::unique_ptr> scheduler; @@ -59,27 +43,26 @@ namespace storm { } viHelper.performValueIteration(env, x, b, goal.direction()); + viHelper.fillResultVector(x, relevantStates, psiStates); - STORM_LOG_DEBUG(storm::utility::vector::toString(x)); if (produceScheduler) { - scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates)); - STORM_LOG_DEBUG("IsPartial?" << scheduler->isPartialScheduler()); + scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates)); } return MDPSparseModelCheckingHelperReturnType(std::move(x), std::move(scheduler)); } template - storm::storage::Scheduler SparseSmgRpatlHelper::expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates) { - //STORM_LOG_DEBUG(psiStates.size()); - for(uint i = 0; i < 2; i++) { - //STORM_LOG_DEBUG(scheduler.getChoice(i)); - } + storm::storage::Scheduler SparseSmgRpatlHelper::expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates) { storm::storage::Scheduler completeScheduler(psiStates.size()); uint_fast64_t maybeStatesCounter = 0; - for(uint stateCounter = 0; stateCounter < psiStates.size(); stateCounter++) { - //STORM_LOG_DEBUG(stateCounter << " : " << psiStates.get(stateCounter)); + uint schedulerSize = psiStates.size(); + for(uint stateCounter = 0; stateCounter < schedulerSize; stateCounter++) { + // psiStates already fulfill formulae so we can set an arbitrary action if(psiStates.get(stateCounter)) { completeScheduler.setChoice(0, stateCounter); + // ~phiStates do not fulfill formulae so we can set an arbitrary action + } else if(notPhiStates.get(stateCounter)) { + completeScheduler.setChoice(0, stateCounter); } else { completeScheduler.setChoice(scheduler.getChoice(maybeStatesCounter), stateCounter); maybeStatesCounter++; diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h index 9505bd51f..7152ab3db 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h @@ -39,7 +39,7 @@ namespace storm { static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(Environment const& env, 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, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); private: - static storm::storage::Scheduler expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates); + static storm::storage::Scheduler expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates); }; } diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index 5c9cab92e..8c354d945 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -82,11 +82,11 @@ namespace storm { //STORM_LOG_DEBUG("xOld = " << storm::utility::vector::toString(xOld())); //STORM_LOG_DEBUG("b = " << storm::utility::vector::toString(_b)); //STORM_LOG_DEBUG("xNew = " << storm::utility::vector::toString(xNew())); - _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew()); + _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), nullptr, &_statesOfCoalition); //std::cin.get(); } else { // Also keep track of the choices made. - _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices); + _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices, &_statesOfCoalition); } // compare applyPointwise @@ -133,6 +133,23 @@ namespace storm { return true; } + template + void GameViHelper::fillResultVector(std::vector& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates) + { + std::vector filledVector = std::vector(relevantStates.size(), storm::utility::zero()); + uint bitIndex = 0; + for(uint i = 0; i < filledVector.size(); i++) { + if (relevantStates.get(i)) { + filledVector.at(i) = result.at(bitIndex); + bitIndex++; + } + else if (psiStates.get(i)) { + filledVector.at(i) = 1; + } + } + result = filledVector; + } + template void GameViHelper::setProduceScheduler(bool value) { _produceScheduler = value; diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h index 92f963851..f3e353665 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h @@ -25,6 +25,11 @@ namespace storm { void performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir); + /*! + * Fills the result vector to the original size with ones for being psiStates, zeros for being not phiStates + */ + void fillResultVector(std::vector& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates); + /*h * Sets whether an optimal scheduler shall be constructed during the computation */ diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index f2a716038..194e37b81 100644 --- a/src/storm/storage/BitVector.cpp +++ b/src/storm/storage/BitVector.cpp @@ -1026,6 +1026,16 @@ namespace storm { } } + void BitVector::setClippedStatesOfCoalition(BitVector relevantStates, BitVector statesOfCoalition) + { + auto clippedStatesCounter = 0; + for(uint i = 0; i < relevantStates.size(); i++) { + if(relevantStates.get(i)) { + this->set(clippedStatesCounter, statesOfCoalition[i]); + clippedStatesCounter++; + } + } + } void BitVector::truncateLastBucket() { if ((bitCount & mod64mask) != 0) { diff --git a/src/storm/storage/BitVector.h b/src/storm/storage/BitVector.h index 323020b48..3dfdd8a55 100644 --- a/src/storm/storage/BitVector.h +++ b/src/storm/storage/BitVector.h @@ -536,6 +536,14 @@ namespace storm { */ bool compareAndSwap(uint_fast64_t start1, uint_fast64_t start2, uint_fast64_t length); + /*! + * Set clipped states of coalition for all states which are not in the winning region. + * + * @param psiStates Bitvector of states which are in the winning region. + * @param statesOfCoalition Bitvector of states which belong to the coalition. + */ + void setClippedStatesOfCoalition(BitVector relevantStates, BitVector statesOfCoalition); + friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector); void store(std::ostream&) const;