diff --git a/src/storm-pars/analysis/Transformer.cpp b/src/storm-pars/analysis/Transformer.cpp index 5cf39bb97..da16af00e 100644 --- a/src/storm-pars/analysis/Transformer.cpp +++ b/src/storm-pars/analysis/Transformer.cpp @@ -11,7 +11,30 @@ namespace storm { storm::storage::BitVector bottomStates, uint_fast64_t numberOfStates) { // TODO: take SparseModel as input // Transform the transition matrix into a vector containing the states with the state to which the transition goes. - std::vector stateVector = toStateVector(matrix, initialStates); + std::vector stateVector = std::vector({}); + + for (uint_fast64_t i = 0; i < numberOfStates; ++i) { + State* state = new State(); + state->stateNumber = i; + state->successor1 = numberOfStates; + state->successor2 = numberOfStates; + + auto row = matrix.getRow(i); + for (auto itr = row.begin(); itr < row.end() && state->successor2 == numberOfStates; ++itr) { + if ((*itr).getValue() != storm::RationalFunction(1)) { + if (state->successor1 == numberOfStates) { + state->successor1 = (*itr).getColumn(); + } else { + state->successor2 = (*itr).getColumn(); + } + } else { + state-> successor1 = (*itr).getColumn(); + state-> successor2 = (*itr).getColumn(); + } + } + stateVector.push_back(state); + } + // Start creating the Lattice Lattice *lattice = new Lattice(topStates, bottomStates, numberOfStates); @@ -48,7 +71,6 @@ namespace storm { Lattice::Node *below = lattice->getNode(successor2); std::vector states1 = above->below; std::vector states2 = below->above; - bool added = false; for (auto itr1 = states1.begin(); itr1 < states1.end(); ++itr1) { for (auto itr2 = states2.begin(); itr2 < states2.end(); ++itr2) { if ((*itr1)->states == (*itr2)->states) { @@ -60,14 +82,13 @@ namespace storm { && getProbability((*itr1)->states, below->states, matrix) == prob2) { lattice->addToNode(currentState->stateNumber, (*itr1)); seenStates.set(currentState->stateNumber); - added = true; } } } } - if (!added) { + if (!seenStates.get(currentState->stateNumber)) { // successor 1 is closer to top than successor 2 lattice->addBetween(currentState->stateNumber, lattice->getNode(successor1), lattice->getNode(successor2)); @@ -130,48 +151,6 @@ namespace storm { return lattice; } - std::vector - Transformer::toStateVector(storm::storage::SparseMatrix transitionMatrix, - storm::storage::BitVector const &initialStates) { - // TODO: Remove this, unnecessary - std::vector < State *> states = std::vector({}); - std::vector stack(initialStates.begin(), initialStates.end()); - std::vector seenStates(initialStates.begin(), initialStates.end()); - uint_fast64_t currentState; - - while (!stack.empty()) { - currentState = stack.back(); - stack.pop_back(); - std::vector successorStates(0, 2); - - // Assume there are at most 2 successors - for (auto const &successor : transitionMatrix.getRowGroup(currentState)) { - if (!storm::utility::isZero(successor.getValue())) { - // Only explore the state if the transition was actually there. - uint_fast64_t successorNumber = successor.getColumn(); - if (std::find(seenStates.begin(), seenStates.end(), successorNumber) == seenStates.end()) { - stack.push_back(successorNumber); - seenStates.push_back(successorNumber); - } - successorStates.push_back(successorNumber); - } - } - - State *state = new State(); - state->stateNumber = currentState; - state->successor1 = successorStates.back(); - successorStates.pop_back(); - if (!successorStates.empty()) { - state->successor2 = successorStates.back(); - successorStates.pop_back(); - } else { - state->successor2 = state->successor1; - } - states.push_back(state); - } - return states; - } - storm::RationalFunction Transformer::getProbability(storm::storage::BitVector state, storm::storage::BitVector successor, storm::storage::SparseMatrix matrix) { storm::RationalFunction result = storm::RationalFunction(1); uint_fast64_t index = successor.getNextSetIndex(0); diff --git a/src/storm-pars/analysis/Transformer.h b/src/storm-pars/analysis/Transformer.h index 65ecd859a..1d3bf64a1 100644 --- a/src/storm-pars/analysis/Transformer.h +++ b/src/storm-pars/analysis/Transformer.h @@ -5,6 +5,7 @@ #ifndef LATTICE_BUILDER_H #define LATTICE_BUILDER_H +#include #include "storm/storage/BitVector.h" #include "storm/storage/SparseMatrix.h" #include "Lattice.h" @@ -36,15 +37,12 @@ namespace storm { storm::storage::BitVector bottomStates, uint_fast64_t numberOfStates); private: - static std::vector - toStateVector(storm::storage::SparseMatrix transitionMatrix, - storm::storage::BitVector const &initialStates); - 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); static storm::RationalFunction getProbability(uint_fast64_t state, uint_fast64_t successor, storm::storage::SparseMatrix matrix); + }; } }