From 2bf640272542f66dbd12502b7888bb185e548324 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Tue, 9 Feb 2021 22:14:47 +0100 Subject: [PATCH 01/14] implemented until formulae --- src/storm/logic/FragmentSpecification.cpp | 1 + .../rpatl/SparseSmgRpatlModelChecker.cpp | 2 + .../rpatl/helper/SparseSmgRpatlHelper.cpp | 41 +++++++++++++++++-- 3 files changed, 41 insertions(+), 3 deletions(-) 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..cbbcbed3e 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -23,13 +23,46 @@ 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); + + STORM_LOG_DEBUG("phiStates are " << phiStates); + STORM_LOG_DEBUG("psiStates are " << psiStates); + STORM_LOG_DEBUG("~psiStates are " <<~psiStates); + + // states are those states which are phiStates and not PsiStates + // so that we can not only leave out the PsiStates in the matrix, but also leave out those which are not in the phiStates + storm::storage::BitVector states(phiStates.size()); + for(int counter = 0; counter < states.size(); counter++) + { + if(phiStates.get(counter) && !psiStates.get(counter)) + { + states.set(counter); + } + } + + STORM_LOG_DEBUG("states are " << states); + + // TRY to change b to the new states + // TODO: only states in the phiStates can be chosen as initial states, e.g. the output is for initial states = 0, 1, 4 + std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(states, psiStates); +/* std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(~psiStates, psiStates); + for(int counter = 0; counter < states.size(); counter++) + { + if(!phiStates.get(counter)) + { + b.at(counter) = 0; + } + }*/ + //std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(~psiStates, psiStates); + + //STORM_LOG_DEBUG("\n" << b); // 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); + //storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, ~psiStates, ~psiStates, false); + // Reduce TRY to use only the states from phi which satisfy the left side and psi which satisfy the right side + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, states, states, false); + //STORM_LOG_DEBUG("\n" << submatrix); //STORM_LOG_DEBUG("x = " << storm::utility::vector::toString(x)); //STORM_LOG_DEBUG("b = " << storm::utility::vector::toString(b)); @@ -60,6 +93,8 @@ namespace storm { viHelper.performValueIteration(env, x, b, goal.direction()); + // TODO: here is the debug output for all states, should I fill up the vector again with 0 for the states i left out? + STORM_LOG_DEBUG(storm::utility::vector::toString(x)); if (produceScheduler) { scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates)); From 781f105ca13983189b5531b3254c5aa7301b3b7d Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Thu, 11 Feb 2021 17:42:39 +0100 Subject: [PATCH 02/14] introduced name relevantStates, moved methods to Bitvector class --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 27 ++++++++++--------- src/storm/storage/BitVector.cpp | 25 +++++++++++++++++ src/storm/storage/BitVector.h | 16 +++++++++++ 3 files changed, 56 insertions(+), 12 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index cbbcbed3e..57ea8ba29 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -30,20 +30,20 @@ namespace storm { // states are those states which are phiStates and not PsiStates // so that we can not only leave out the PsiStates in the matrix, but also leave out those which are not in the phiStates - storm::storage::BitVector states(phiStates.size()); - for(int counter = 0; counter < states.size(); counter++) + storm::storage::BitVector relevantStates(phiStates.size()); + relevantStates.setRelevantStates(phiStates, ~psiStates); + +/* for(int counter = 0; counter < states.size(); counter++) { if(phiStates.get(counter) && !psiStates.get(counter)) { states.set(counter); } - } + }*/ - STORM_LOG_DEBUG("states are " << states); + STORM_LOG_DEBUG("relevant states are " << relevantStates); - // TRY to change b to the new states - // TODO: only states in the phiStates can be chosen as initial states, e.g. the output is for initial states = 0, 1, 4 - std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(states, psiStates); + std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates); /* std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(~psiStates, psiStates); for(int counter = 0; counter < states.size(); counter++) { @@ -61,7 +61,7 @@ namespace storm { //storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, ~psiStates, ~psiStates, false); // Reduce TRY to use only the states from phi which satisfy the left side and psi which satisfy the right side - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, states, states, false); + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); //STORM_LOG_DEBUG("\n" << submatrix); //STORM_LOG_DEBUG("x = " << storm::utility::vector::toString(x)); @@ -72,15 +72,17 @@ namespace storm { //STORM_LOG_DEBUG(statesOfCoalition); //STORM_LOG_DEBUG(clippedStatesOfCoalition); - // TODO move this to BitVector-class - auto clippedStatesCounter = 0; +/* 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++; } - } + }*/ + + clippedStatesOfCoalition.setClippedStatesOfCoalition(psiStates, statesOfCoalition); + //STORM_LOG_DEBUG(clippedStatesOfCoalition); clippedStatesOfCoalition.complement(); //STORM_LOG_DEBUG(clippedStatesOfCoalition); @@ -93,7 +95,8 @@ namespace storm { viHelper.performValueIteration(env, x, b, goal.direction()); - // TODO: here is the debug output for all states, should I fill up the vector again with 0 for the states i left out? + // TODO: here is the debug output for all states, should I fill up the vector again with 0 for the states i left out + // e.g. phi states are [ 2 3 ], the probability output is for the first state (state 2) but the initial sate is 0 STORM_LOG_DEBUG(storm::utility::vector::toString(x)); if (produceScheduler) { diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index f2a716038..9b5db6834 100644 --- a/src/storm/storage/BitVector.cpp +++ b/src/storm/storage/BitVector.cpp @@ -1026,6 +1026,31 @@ namespace storm { } } + void BitVector::setRelevantStates(BitVector bitVector1, BitVector bitVector2) + { + for(int counter = 0; counter < this->size(); counter++) + { + if(bitVector1.get(counter) && bitVector2.get(counter)) + { + this->set(counter); + } + } + } + + void BitVector::setClippedStatesOfCoalition(BitVector psiStates, BitVector statesOfCoalition) + { + 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)) { + 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..fc49999b8 100644 --- a/src/storm/storage/BitVector.h +++ b/src/storm/storage/BitVector.h @@ -536,6 +536,22 @@ namespace storm { */ bool compareAndSwap(uint_fast64_t start1, uint_fast64_t start2, uint_fast64_t length); + /*! + * Compare two bitvectors and set the bits which are set in both of them. + * + * @param bitVector1 First Source for comparison. + * @param bitVector2 Second Source for comparison. + */ + void setRelevantStates(BitVector bitVector1, BitVector bitVector2); + + /*! + * 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 psiStates, BitVector statesOfCoalition); + friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector); void store(std::ostream&) const; From 58ec5b89e9de21f0ec3f9e24759f5e0e61aac661 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 15 Feb 2021 14:55:04 +0100 Subject: [PATCH 03/14] set direction overrides --- src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index 5c9cab92e..fb8882a5d 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 From 37d36c52b3d1e2c573415db89b065d21f4d6805c Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 15 Feb 2021 15:46:07 +0100 Subject: [PATCH 04/14] fill up the result vector for ~relevantStates --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 7 +++---- .../rpatl/helper/internal/GameViHelper.cpp | 17 +++++++++++++++++ .../rpatl/helper/internal/GameViHelper.h | 5 +++++ 3 files changed, 25 insertions(+), 4 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 57ea8ba29..b30cea558 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -94,11 +94,10 @@ namespace storm { } viHelper.performValueIteration(env, x, b, goal.direction()); - - // TODO: here is the debug output for all states, should I fill up the vector again with 0 for the states i left out - // e.g. phi states are [ 2 3 ], the probability output is for the first state (state 2) but the initial sate is 0 - + //STORM_LOG_DEBUG(storm::utility::vector::toString(x)); + 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()); diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index fb8882a5d..bff9bc052 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -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 filled_vector = std::vector(relevantStates.size(), storm::utility::zero()); + uint bit_index = 0; + for(uint i = 0; i < filled_vector.size(); i++) { + if (relevantStates.get(i)) { + filled_vector.at(i) = result.at(bit_index); + bit_index++; + } + else if (psiStates.get(i)) { + filled_vector.at(i) = 1; + } + } + result = filled_vector; + } + 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 */ From 7a25fb78818c9a5dde2cff8ca9abfe50b17578d3 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 15 Feb 2021 16:03:34 +0100 Subject: [PATCH 05/14] small code clean up, added todo for refactoring bitvector method --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 38 +++++-------------- 1 file changed, 9 insertions(+), 29 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index b30cea558..c90a53e20 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -24,43 +24,23 @@ namespace storm { // Initialize the solution vector. std::vector x = std::vector(transitionMatrix.getRowGroupCount() - psiStates.getNumberOfSetBits(), storm::utility::zero()); - STORM_LOG_DEBUG("phiStates are " << phiStates); - STORM_LOG_DEBUG("psiStates are " << psiStates); - STORM_LOG_DEBUG("~psiStates are " <<~psiStates); + //STORM_LOG_DEBUG("phiStates: " << phiStates); + //STORM_LOG_DEBUG("psiStates: " << psiStates); + //STORM_LOG_DEBUG("~psiStates: " <<~psiStates); // states are those states which are phiStates and not PsiStates // so that we can not only leave out the PsiStates in the matrix, but also leave out those which are not in the phiStates storm::storage::BitVector relevantStates(phiStates.size()); - relevantStates.setRelevantStates(phiStates, ~psiStates); -/* for(int counter = 0; counter < states.size(); counter++) - { - if(phiStates.get(counter) && !psiStates.get(counter)) - { - states.set(counter); - } - }*/ + // TODO: AND for Bitvectors already exists, try to use this instead: + // first: copy one Bitvector to relevantStates, second: logical AND with the other one. + relevantStates.setRelevantStates(phiStates, ~psiStates); - STORM_LOG_DEBUG("relevant states are " << relevantStates); + STORM_LOG_DEBUG("relevant states: " << relevantStates); std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates); -/* std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(~psiStates, psiStates); - for(int counter = 0; counter < states.size(); counter++) - { - if(!phiStates.get(counter)) - { - b.at(counter) = 0; - } - }*/ - //std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(~psiStates, psiStates); - - //STORM_LOG_DEBUG("\n" << b); - // Reduce matrix to ~Prob1 states- - //STORM_LOG_DEBUG("\n" << transitionMatrix); - //storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, ~psiStates, ~psiStates, false); - - // Reduce TRY to use only the states from phi which satisfy the left side and psi which satisfy the right side + // use only the states from phi which satisfy the left side and psi which satisfy the right side storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); //STORM_LOG_DEBUG("\n" << submatrix); @@ -83,7 +63,7 @@ namespace storm { clippedStatesOfCoalition.setClippedStatesOfCoalition(psiStates, statesOfCoalition); - //STORM_LOG_DEBUG(clippedStatesOfCoalition); + STORM_LOG_DEBUG(clippedStatesOfCoalition); clippedStatesOfCoalition.complement(); //STORM_LOG_DEBUG(clippedStatesOfCoalition); From 318544a94078ef4776374f000fc191c2736e5fab Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 15 Feb 2021 16:45:14 +0100 Subject: [PATCH 06/14] refactor computation of relevantStates from BitVector method to logical AND --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 9 ++------- src/storm/storage/BitVector.cpp | 14 -------------- src/storm/storage/BitVector.h | 8 -------- 3 files changed, 2 insertions(+), 29 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index c90a53e20..0e8171272 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -28,13 +28,8 @@ namespace storm { //STORM_LOG_DEBUG("psiStates: " << psiStates); //STORM_LOG_DEBUG("~psiStates: " <<~psiStates); - // states are those states which are phiStates and not PsiStates - // so that we can not only leave out the PsiStates in the matrix, but also leave out those which are not in the phiStates - storm::storage::BitVector relevantStates(phiStates.size()); - - // TODO: AND for Bitvectors already exists, try to use this instead: - // first: copy one Bitvector to relevantStates, second: logical AND with the other one. - relevantStates.setRelevantStates(phiStates, ~psiStates); + // relevant states are those states which are phiStates and not PsiStates + storm::storage::BitVector relevantStates = phiStates & ~psiStates; STORM_LOG_DEBUG("relevant states: " << relevantStates); diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index 9b5db6834..506613965 100644 --- a/src/storm/storage/BitVector.cpp +++ b/src/storm/storage/BitVector.cpp @@ -1026,17 +1026,6 @@ namespace storm { } } - void BitVector::setRelevantStates(BitVector bitVector1, BitVector bitVector2) - { - for(int counter = 0; counter < this->size(); counter++) - { - if(bitVector1.get(counter) && bitVector2.get(counter)) - { - this->set(counter); - } - } - } - void BitVector::setClippedStatesOfCoalition(BitVector psiStates, BitVector statesOfCoalition) { auto clippedStatesCounter = 0; @@ -1049,9 +1038,6 @@ namespace storm { } } - - - void BitVector::truncateLastBucket() { if ((bitCount & mod64mask) != 0) { buckets[bucketCount() - 1] &= ~((1ll << (64 - (bitCount & mod64mask))) - 1ll); diff --git a/src/storm/storage/BitVector.h b/src/storm/storage/BitVector.h index fc49999b8..83f656a4b 100644 --- a/src/storm/storage/BitVector.h +++ b/src/storm/storage/BitVector.h @@ -536,14 +536,6 @@ namespace storm { */ bool compareAndSwap(uint_fast64_t start1, uint_fast64_t start2, uint_fast64_t length); - /*! - * Compare two bitvectors and set the bits which are set in both of them. - * - * @param bitVector1 First Source for comparison. - * @param bitVector2 Second Source for comparison. - */ - void setRelevantStates(BitVector bitVector1, BitVector bitVector2); - /*! * Set clipped states of coalition for all states which are not in the winning region. * From 86bf1a0d8911d6f1d3e8f27004fea8f20d928977 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 15 Feb 2021 16:51:08 +0100 Subject: [PATCH 07/14] small clean up --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 0e8171272..60a7440e9 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -43,22 +43,14 @@ namespace storm { //STORM_LOG_DEBUG("b = " << storm::utility::vector::toString(b)); storm::storage::BitVector clippedStatesOfCoalition(statesOfCoalition.size() - psiStates.getNumberOfSetBits()); + //STORM_LOG_DEBUG(psiStates); //STORM_LOG_DEBUG(statesOfCoalition); //STORM_LOG_DEBUG(clippedStatesOfCoalition); -/* 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++; - } - }*/ - clippedStatesOfCoalition.setClippedStatesOfCoalition(psiStates, statesOfCoalition); - STORM_LOG_DEBUG(clippedStatesOfCoalition); + //STORM_LOG_DEBUG(clippedStatesOfCoalition); clippedStatesOfCoalition.complement(); //STORM_LOG_DEBUG(clippedStatesOfCoalition); From e1cbf087497cf860b660f593b4db8de0c9491810 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 15 Feb 2021 19:06:35 +0100 Subject: [PATCH 08/14] Removed DEBUG messages, changed description of submatrix --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 28 ++----------------- 1 file changed, 2 insertions(+), 26 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 60a7440e9..cb1b399dd 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -24,35 +24,17 @@ namespace storm { // Initialize the solution vector. std::vector x = std::vector(transitionMatrix.getRowGroupCount() - psiStates.getNumberOfSetBits(), storm::utility::zero()); - //STORM_LOG_DEBUG("phiStates: " << phiStates); - //STORM_LOG_DEBUG("psiStates: " << psiStates); - //STORM_LOG_DEBUG("~psiStates: " <<~psiStates); - - // relevant states are those states which are phiStates and not PsiStates + // Relevant states are those states which are phiStates and not PsiStates. storm::storage::BitVector relevantStates = phiStates & ~psiStates; - STORM_LOG_DEBUG("relevant states: " << relevantStates); - std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates); - // use only the states from phi which satisfy the left side and psi which satisfy the right side + // Reduce matrix to only relevant States storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); - //STORM_LOG_DEBUG("\n" << submatrix); - - //STORM_LOG_DEBUG("x = " << storm::utility::vector::toString(x)); - //STORM_LOG_DEBUG("b = " << storm::utility::vector::toString(b)); storm::storage::BitVector clippedStatesOfCoalition(statesOfCoalition.size() - psiStates.getNumberOfSetBits()); - - //STORM_LOG_DEBUG(psiStates); - //STORM_LOG_DEBUG(statesOfCoalition); - //STORM_LOG_DEBUG(clippedStatesOfCoalition); - clippedStatesOfCoalition.setClippedStatesOfCoalition(psiStates, statesOfCoalition); - - //STORM_LOG_DEBUG(clippedStatesOfCoalition); clippedStatesOfCoalition.complement(); - //STORM_LOG_DEBUG(clippedStatesOfCoalition); storm::modelchecker::helper::internal::GameViHelper viHelper(submatrix, clippedStatesOfCoalition); std::unique_ptr> scheduler; @@ -61,27 +43,21 @@ namespace storm { } viHelper.performValueIteration(env, x, b, goal.direction()); - //STORM_LOG_DEBUG(storm::utility::vector::toString(x)); 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()); } 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 completeScheduler(psiStates.size()); uint_fast64_t maybeStatesCounter = 0; for(uint stateCounter = 0; stateCounter < psiStates.size(); stateCounter++) { - //STORM_LOG_DEBUG(stateCounter << " : " << psiStates.get(stateCounter)); if(psiStates.get(stateCounter)) { completeScheduler.setChoice(0, stateCounter); } else { From 5dfe48e51e8e2510ecd07676d1877498e6db5d99 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 15 Feb 2021 19:18:52 +0100 Subject: [PATCH 09/14] changed description of submatrix --- src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index cb1b399dd..3edff110e 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -29,7 +29,7 @@ namespace storm { std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates); - // Reduce matrix to only relevant States + // Reduce the matrix to relevant states storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); storm::storage::BitVector clippedStatesOfCoalition(statesOfCoalition.size() - psiStates.getNumberOfSetBits()); From 5473966cd1048c15c9bd862a7cecb201b7d131d2 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 15 Feb 2021 20:04:14 +0100 Subject: [PATCH 10/14] changed clippedStatesOfCoalition with size and values from relevantStates --- .../modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 4 ++-- src/storm/storage/BitVector.cpp | 7 +++---- src/storm/storage/BitVector.h | 2 +- 3 files changed, 6 insertions(+), 7 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 3edff110e..ed535f8d4 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -32,8 +32,8 @@ namespace storm { // Reduce the matrix to relevant states storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); - storm::storage::BitVector clippedStatesOfCoalition(statesOfCoalition.size() - psiStates.getNumberOfSetBits()); - clippedStatesOfCoalition.setClippedStatesOfCoalition(psiStates, statesOfCoalition); + storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); + clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); clippedStatesOfCoalition.complement(); storm::modelchecker::helper::internal::GameViHelper viHelper(submatrix, clippedStatesOfCoalition); diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index 506613965..194e37b81 100644 --- a/src/storm/storage/BitVector.cpp +++ b/src/storm/storage/BitVector.cpp @@ -1026,12 +1026,11 @@ namespace storm { } } - void BitVector::setClippedStatesOfCoalition(BitVector psiStates, BitVector statesOfCoalition) + void BitVector::setClippedStatesOfCoalition(BitVector relevantStates, BitVector statesOfCoalition) { 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)) { + for(uint i = 0; i < relevantStates.size(); i++) { + if(relevantStates.get(i)) { this->set(clippedStatesCounter, statesOfCoalition[i]); clippedStatesCounter++; } diff --git a/src/storm/storage/BitVector.h b/src/storm/storage/BitVector.h index 83f656a4b..3dfdd8a55 100644 --- a/src/storm/storage/BitVector.h +++ b/src/storm/storage/BitVector.h @@ -542,7 +542,7 @@ namespace storm { * @param psiStates Bitvector of states which are in the winning region. * @param statesOfCoalition Bitvector of states which belong to the coalition. */ - void setClippedStatesOfCoalition(BitVector psiStates, BitVector statesOfCoalition); + void setClippedStatesOfCoalition(BitVector relevantStates, BitVector statesOfCoalition); friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector); From 7807c8a143be1653824c6ca7c43f7e26b4192cae Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 15 Feb 2021 20:16:06 +0100 Subject: [PATCH 11/14] changed variable names to camelCase --- .../rpatl/helper/internal/GameViHelper.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index bff9bc052..8c354d945 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -136,18 +136,18 @@ namespace storm { template void GameViHelper::fillResultVector(std::vector& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates) { - std::vector filled_vector = std::vector(relevantStates.size(), storm::utility::zero()); - uint bit_index = 0; - for(uint i = 0; i < filled_vector.size(); i++) { + 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)) { - filled_vector.at(i) = result.at(bit_index); - bit_index++; + filledVector.at(i) = result.at(bitIndex); + bitIndex++; } else if (psiStates.get(i)) { - filled_vector.at(i) = 1; + filledVector.at(i) = 1; } } - result = filled_vector; + result = filledVector; } template From e48f3d070583cf159dcdc28b617c26d482f7a792 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Tue, 16 Feb 2021 16:09:46 +0100 Subject: [PATCH 12/14] added notPhiStates to expandScheduler --- .../modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 6 ++++-- src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h | 2 +- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index ed535f8d4..5a303017c 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -46,13 +46,13 @@ namespace storm { viHelper.fillResultVector(x, relevantStates, psiStates); if (produceScheduler) { - scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates)); + 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::storage::Scheduler SparseSmgRpatlHelper::expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates) { for(uint i = 0; i < 2; i++) { } storm::storage::Scheduler completeScheduler(psiStates.size()); @@ -60,6 +60,8 @@ namespace storm { for(uint stateCounter = 0; stateCounter < psiStates.size(); stateCounter++) { if(psiStates.get(stateCounter)) { completeScheduler.setChoice(0, stateCounter); + } 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); }; } From aa2489cb36aa12e78b2be61d45924e00da314636 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Tue, 16 Feb 2021 17:29:20 +0100 Subject: [PATCH 13/14] added some comments to expansion of scheduler --- src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 5a303017c..89b93aa1d 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -58,8 +58,10 @@ namespace storm { storm::storage::Scheduler completeScheduler(psiStates.size()); uint_fast64_t maybeStatesCounter = 0; for(uint stateCounter = 0; stateCounter < psiStates.size(); 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 { From afa0c079470c59d01ce5022aa973c34a4d85cde7 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Wed, 17 Feb 2021 11:24:48 +0100 Subject: [PATCH 14/14] introduced schedulerSize, removed empty for-loop --- src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 89b93aa1d..8d254b01f 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -53,11 +53,10 @@ namespace storm { template storm::storage::Scheduler SparseSmgRpatlHelper::expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates) { - for(uint i = 0; i < 2; i++) { - } storm::storage::Scheduler completeScheduler(psiStates.size()); uint_fast64_t maybeStatesCounter = 0; - for(uint stateCounter = 0; stateCounter < psiStates.size(); 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);