diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 6f67ca435..ab240471f 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -49,11 +49,7 @@ namespace storm { bool exact; }; - struct State { - uint_fast64_t stateNumber; - uint_fast64_t successor1; - uint_fast64_t successor2; - }; + template std::vector> parseRegions(std::shared_ptr const& model) { @@ -443,86 +439,7 @@ namespace storm { storm::pars::verifyWithSparseEngine(model->as>(), input, regions, samples); } - template - storm::analysis::Lattice* toLattice(std::shared_ptr> model, - storm::storage::BitVector topStates, - storm::storage::BitVector bottomStates) { - storm::storage::SparseMatrix matrix = model.get()->getTransitionMatrix(); - storm::storage::BitVector initialStates = model.get()->getInitialStates(); - uint_fast64_t numberOfStates = model.get()->getNumberOfStates(); - - // Transform the transition matrix into a vector containing the states with the state to which the transition goes. - 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); - //TODO assert that there are at most two successors - if ((*(row.begin())).getValue() != ValueType(1)) { - state->successor1 = (*(row.begin())).getColumn(); - state->successor2 = (*(++row.begin())).getColumn(); - } else { - state-> successor1 = (*(row.begin())).getColumn(); - state-> successor2 = (*(row.begin())).getColumn(); - } - stateVector.push_back(state); - } - // Start creating the Lattice - storm::analysis::Lattice *lattice = new storm::analysis::Lattice(topStates, bottomStates, numberOfStates); - storm::storage::BitVector oldStates(numberOfStates); - // Create a copy of the states already present in the lattice. - storm::storage::BitVector seenStates = topStates|= bottomStates; - - while (oldStates != seenStates) { - // As long as new states are added to the lattice, continue. - oldStates = storm::storage::BitVector(seenStates); - - for (auto itr = stateVector.begin(); itr != stateVector.end(); ++itr) { - // Iterate over all states - State *currentState = *itr; - - if (!seenStates[currentState->stateNumber] - && seenStates[currentState->successor1] - && seenStates[currentState->successor2]) { - - - // Otherwise, check how the two states compare, and add if the comparison is possible. - uint_fast64_t successor1 = currentState->successor1; - uint_fast64_t successor2 = currentState->successor2; - int compareResult = lattice->compare(successor1, successor2); - if (compareResult == 1 || compareResult == 2) { - // getNode will not return nullptr, as compare already checked this - if (compareResult == 2) { - // swap - auto temp = successor1; - successor1 = successor2; - successor2 = temp; - } - - // successor 1 is closer to top than successor 2 - lattice->addBetween(currentState->stateNumber, lattice->getNode(successor1), - lattice->getNode(successor2)); - // Add stateNumber to the set with seen states. - seenStates.set(currentState->stateNumber); - } else if (compareResult == 0) { - // the successors are at the same level - lattice->addToNode(currentState->stateNumber, lattice->getNode(successor1)); - // Add stateNumber to the set with seen states. - seenStates.set(currentState->stateNumber); - } else { - // TODO: what to do? - STORM_LOG_DEBUG("Failed to add" << currentState->stateNumber << "\n"); - } - - } - } - } - return lattice; - } template @@ -589,12 +506,12 @@ namespace storm { storm::storage::BitVector bottomStates = statesWithProbability01.first; // Transform to LatticeLattice - storm::analysis::Lattice* lattice = toLattice(sparseModel, topStates, bottomStates); + storm::storage::SparseMatrix matrix = sparseModel.get()->getTransitionMatrix(); + storm::analysis::Lattice* lattice = storm::analysis::Lattice::toLattice(matrix, topStates, bottomStates); lattice->toString(std::cout); // Monotonicity? bool monotoneInAll = true; - storm::storage::SparseMatrix matrix = sparseModel.get()->getTransitionMatrix(); for (uint_fast64_t i = 0; i < sparseModel.get()->getNumberOfStates(); ++i) { // go over all rows auto row = matrix.getRow(i); diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index f710f2fbb..3f0f8da3f 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -9,9 +9,9 @@ namespace storm { Lattice::Lattice(storm::storage::BitVector topStates, storm::storage::BitVector bottomStates, uint_fast64_t numberOfStates) { - Node *top = new Node(); + top = new Node(); top->states = topStates; - Node *bottom = new Node(); + bottom = new Node(); bottom->states = bottomStates; top->below.push_back(bottom); bottom->above.push_back(top); @@ -29,7 +29,6 @@ namespace storm { } void Lattice::addBetween(uint_fast64_t state, Node *above, Node *below) { - std::cout << "Adding: " << state << std::endl; Node *newNode = new Node(); newNode->states = storm::storage::BitVector(numberOfStates); newNode->states.set(state); @@ -47,6 +46,10 @@ namespace storm { nodes.at(state) = node; } + void Lattice::add(uint_fast64_t state) { + addBetween(state, top, bottom); + } + int Lattice::compare(uint_fast64_t state1, uint_fast64_t state2) { Node *node1 = getNode(state1); Node *node2 = getNode(state2); diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h index 14b7b341b..f6617871e 100644 --- a/src/storm-pars/analysis/Lattice.h +++ b/src/storm-pars/analysis/Lattice.h @@ -8,7 +8,10 @@ #include #include +#include "storm/models/sparse/Model.h" #include "storm/storage/BitVector.h" +#include "storm/storage/SparseMatrix.h" + namespace storm { namespace analysis { @@ -33,18 +36,24 @@ namespace storm { /*! * Adds a node with the given state below node1 and above node2. * @param state The given state. - * @param node1 The pointer to the node below which a new node is added. - * @param node2 The pointer to the node above which a new node is added. + * @param node1 The pointer to the node below which a new node (with state) is added + * @param node2 The pointer to the node above which a new node (with state) is added */ void addBetween(uint_fast64_t state, Node *node1, Node *node2); /*! * Adds state to the states of the given node. * @param state The state which is added. - * @param node The pointer to the node to which state is added. + * @param node The pointer to the node to which state is added, should not be nullptr. */ void addToNode(uint_fast64_t state, Node *node); + /*! + * Adds state between the top and bottom node of the lattice + * @param state The given state + */ + void add(uint_fast64_t state); + /*! * Compares the level of the nodes of the states. * Behaviour unknown when one or more of the states doesnot occur at any Node in the Lattice. @@ -74,11 +83,103 @@ namespace storm { */ void toString(std::ostream &out); -// std::vector addedStates; + /*! + * Creates a Lattice based on the transition matrix, topStates of the Lattice and bottomStates of the Lattice + * @tparam ValueType Type of the probabilities + * @param matrix The transition matrix. + * @param topStates Set of topStates of the Lattice. + * @param bottomStates Set of bottomStates of the Lattice. + * @return pointer to the created Lattice. + */ + template + static Lattice* toLattice(storm::storage::SparseMatrix matrix, + storm::storage::BitVector topStates, + storm::storage::BitVector bottomStates) { + uint_fast64_t numberOfStates = matrix.getColumnCount(); + + // Transform the transition matrix into a vector containing the states with the state to which the transition goes. + std::vector stateVector = std::vector({}); + for (uint_fast64_t i = 0; i < numberOfStates; ++i) { + State* state = new State(); + state->stateNumber = i; + + auto row = matrix.getRow(i); + //TODO assert that there are at most two successors + if ((*(row.begin())).getValue() != ValueType(1)) { + state->successor1 = (*(row.begin())).getColumn(); + state->successor2 = (*(++row.begin())).getColumn(); + } else { + state-> successor1 = (*(row.begin())).getColumn(); + state-> successor2 = (*(row.begin())).getColumn(); + } + + stateVector.push_back(state); + } + // Start creating the Lattice + storm::analysis::Lattice *lattice = new storm::analysis::Lattice(topStates, bottomStates, numberOfStates); + storm::storage::BitVector oldStates(numberOfStates); + // Create a copy of the states already present in the lattice. + storm::storage::BitVector seenStates = topStates|= bottomStates; + + while (oldStates != seenStates) { + // As long as new states are added to the lattice, continue. + oldStates = storm::storage::BitVector(seenStates); + + for (auto itr = stateVector.begin(); itr != stateVector.end(); ++itr) { + // Iterate over all states + State *currentState = *itr; + + if (!seenStates[currentState->stateNumber] + && seenStates[currentState->successor1] + && seenStates[currentState->successor2]) { + + + // Otherwise, check how the two states compare, and add if the comparison is possible. + uint_fast64_t successor1 = currentState->successor1; + uint_fast64_t successor2 = currentState->successor2; + int compareResult = lattice->compare(successor1, successor2); + if (compareResult == 1) { + // successor 1 is closer to top than successor 2 + lattice->addBetween(currentState->stateNumber, lattice->getNode(successor1), + lattice->getNode(successor2)); + // Add stateNumber to the set with seen states. + seenStates.set(currentState->stateNumber); + } else if (compareResult == 2) { + // successor 2 is closer to top than successor 1 + lattice->addBetween(currentState->stateNumber, lattice->getNode(successor2), + lattice->getNode(successor1)); + // Add stateNumber to the set with seen states. + seenStates.set(currentState->stateNumber); + } else if (compareResult == 0) { + // the successors are at the same level + lattice->addToNode(currentState->stateNumber, lattice->getNode(successor1)); + // Add stateNumber to the set with seen states. + seenStates.set(currentState->stateNumber); + } else { + // TODO: is this what we want? + lattice->add(currentState->stateNumber); + } + + } + } + } + + return lattice; + } private: + struct State { + uint_fast64_t stateNumber; + uint_fast64_t successor1; + uint_fast64_t successor2; + }; + std::vector nodes; + Node * top; + + Node * bottom; + uint_fast64_t numberOfStates; bool above(Node *, Node *);