Browse Source

Refactor constructor Lattice

tempestpy_adaptions
Jip Spel 6 years ago
parent
commit
116dbc8bba
  1. 7
      src/storm-pars/analysis/Lattice.cpp
  2. 3
      src/storm-pars/analysis/Lattice.h
  3. 5
      src/storm-pars/analysis/Transformer.cpp

7
src/storm-pars/analysis/Lattice.cpp

@ -6,11 +6,12 @@
#include "Lattice.h"
namespace storm {
namespace analysis {
Lattice::Lattice(Node *topNode, Node *bottomNode, uint_fast64_t numberOfStates) {
Lattice::Lattice(storm::storage::BitVector topStates,
storm::storage::BitVector bottomStates, uint_fast64_t numberOfStates) {
Node *top = new Node();
top->states = topNode->states;
top->states = topStates;
Node *bottom = new Node();
bottom->states = bottomNode->states;
bottom->states = bottomStates;
top->below.push_back(bottom);
bottom->above.push_back(top);
nodes = std::vector<Node *>({top, bottom});

3
src/storm-pars/analysis/Lattice.h

@ -27,7 +27,8 @@ namespace storm {
* @param topNode The top node of the resulting lattice.
* @param bottomNode The bottom node of the resulting lattice.
*/
Lattice(Node *topNode, Node *bottomNode, uint_fast64_t numberOfStates);
Lattice(storm::storage::BitVector topStates,
storm::storage::BitVector bottomStates, uint_fast64_t numberOfStates);
/*!
* Adds a node with the given state below node1 and above node2.

5
src/storm-pars/analysis/Transformer.cpp

@ -13,11 +13,8 @@ namespace storm {
// Transform the transition matrix into a vector containing the states with the state to which the transition goes.
std::vector<State*> stateVector = toStateVector(matrix, initialStates);
// TODO: not initializing all fields of Lattice::Node yet, what to do?
// Start creating the Lattice
Lattice::Node top = {topStates};
Lattice::Node bottom = {bottomStates};
Lattice *lattice = new Lattice(&top, &bottom, numberOfStates);
Lattice *lattice = new 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;

Loading…
Cancel
Save