diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index 77f4e83f8..393079afb 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -14,8 +14,6 @@ namespace storm { top->below.push_back(bottom); bottom->above.push_back(top); nodes = std::vector({top, bottom}); -// addedStates.insert(addedStates.end(), top->states.begin(), top->states.end()); -// addedStates.insert(addedStates.end(), bottom->states.begin(), bottom->states.end()); this->numberOfStates = numberOfStates; } @@ -30,12 +28,10 @@ namespace storm { (below->above).push_back(newNode); above->below.push_back(newNode); nodes.push_back(newNode); -// addedStates.push_back(state); } void Lattice::addToNode(uint_fast64_t state, Node *node) { node->states.set(state); -// addedStates.push_back(state); } int Lattice::compare(uint_fast64_t state1, uint_fast64_t state2) { diff --git a/src/storm-pars/analysis/Transformer.cpp b/src/storm-pars/analysis/Transformer.cpp index 9a2baba53..183a0412c 100644 --- a/src/storm-pars/analysis/Transformer.cpp +++ b/src/storm-pars/analysis/Transformer.cpp @@ -175,47 +175,22 @@ namespace storm { return states; } - void Transformer::print(storm::storage::BitVector vector, std::string message) { - // TODO: Remove this, unnecessary - - uint_fast64_t index = vector.getNextSetIndex(0); - std::cout << message <<": {"; - while (index < vector.size()) { - std::cout << index; - index = vector.getNextSetIndex(index+1); - if (index < vector.size()) { - std::cout << ", "; - } - } - std::cout << "}" << std::endl; - } - - std::vector Transformer::getNumbers(storm::storage::BitVector vector) { - // TODO: Remove this, unnecessary - std::vector result = std::vector({}); - uint_fast64_t index = vector.getNextSetIndex(0); - while (index < vector.size()) { - result.push_back(index); - index = vector.getNextSetIndex(index+1); - - } - return result; - } - storm::RationalFunction Transformer::getProbability(storm::storage::BitVector state, storm::storage::BitVector successor, storm::storage::SparseMatrix matrix) { - std::vector successorNumbers = getNumbers(successor); storm::RationalFunction result = storm::RationalFunction(1); - for (auto itr = successorNumbers.begin(); itr < successorNumbers.end() && result == storm::RationalFunction(1); ++itr) { - result = getProbability(state, (*itr), matrix); + uint_fast64_t index = successor.getNextSetIndex(0); + while (index < successor.size() && result == storm::RationalFunction(1)) { + result = getProbability(state, index, matrix); + index = successor.getNextSetIndex(index+1); } return result; } storm::RationalFunction Transformer::getProbability(storm::storage::BitVector state, uint_fast64_t successor, storm::storage::SparseMatrix matrix) { - std::vector stateNumbers = getNumbers(state); storm::RationalFunction result = storm::RationalFunction(1); - for (auto itr = stateNumbers.begin(); itr < stateNumbers.end() && result == storm::RationalFunction(1); ++itr) { - result = getProbability((*itr), successor, matrix); + uint_fast64_t index = state.getNextSetIndex(0); + while (index < state.size() && result == storm::RationalFunction(1)) { + result = getProbability(index, successor, matrix); + index = state.getNextSetIndex(index+1); } return result; } diff --git a/src/storm-pars/analysis/Transformer.h b/src/storm-pars/analysis/Transformer.h index d584227f2..65ecd859a 100644 --- a/src/storm-pars/analysis/Transformer.h +++ b/src/storm-pars/analysis/Transformer.h @@ -40,10 +40,6 @@ namespace storm { toStateVector(storm::storage::SparseMatrix transitionMatrix, storm::storage::BitVector const &initialStates); - static void print(storm::storage::BitVector vector, std::string message); - - static std::vector getNumbers(storm::storage::BitVector vector); - static storm::RationalFunction getProbability(storm::storage::BitVector state, storm::storage::BitVector successor, storm::storage::SparseMatrix matrix); static storm::RationalFunction getProbability(storm::storage::BitVector state, uint_fast64_t successor, storm::storage::SparseMatrix matrix);