sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Change deepCopy into constructor

main
Jip Spel 7 years ago
parent
19475b30b9
commit
bb1f1a3701
3 changed files with 66 additions and 40 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 8
      src/storm-pars/analysis/AssumptionMaker.cpp
  2. 80
      src/storm-pars/analysis/Lattice.cpp
  3. 6
      src/storm-pars/analysis/Lattice.h

8
src/storm-pars/analysis/AssumptionMaker.cpp
View File

@ -38,7 +38,7 @@ namespace storm {
var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
storm::expressions::BinaryRelationExpression::RelationType::Greater));
assumptions1.insert(assumption1);
auto lattice1 = lattice->deepCopy();
auto lattice1 = new Lattice(lattice);
auto myMap = (runRecursive(lattice1, assumptions1));
result.insert(myMap.begin(), myMap.end());
@ -49,7 +49,7 @@ namespace storm {
storm::expressions::BinaryRelationExpression::RelationType::Greater));
assumptions2.insert(assumption2);
auto lattice2 = lattice->deepCopy();
auto lattice2 = new Lattice(lattice);
auto myMap2 = (runRecursive(lattice2, assumptions2));
result.insert(myMap2.begin(), myMap2.end());
}
@ -72,7 +72,7 @@ namespace storm {
var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
storm::expressions::BinaryRelationExpression::RelationType::Greater));
assumptions1.insert(assumption1);
auto lattice1 = lattice->deepCopy();
auto lattice1 = new Lattice(lattice);
auto myMap = (runRecursive(lattice1, assumptions1));
result.insert(myMap.begin(), myMap.end());
@ -82,7 +82,7 @@ namespace storm {
var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(),
storm::expressions::BinaryRelationExpression::RelationType::Greater)) ;
assumptions2.insert(assumption2);
auto lattice2 = lattice->deepCopy();
auto lattice2 = new Lattice(lattice);
myMap = (runRecursive(lattice2, assumptions2));
result.insert(myMap.begin(), myMap.end());
}

80
src/storm-pars/analysis/Lattice.cpp
View File

@ -29,6 +29,53 @@ namespace storm {
this->addedStates.operator|=(bottomStates);
}
Lattice::Lattice(Lattice* lattice) {
top = new Node();
top->states = storm::storage::BitVector(lattice->getTop()->states);
bottom = new Node();
bottom->states = storm::storage::BitVector(lattice->getBottom()->states);
numberOfStates = top->states.size();
nodes = std::vector<Node *>(numberOfStates);
addedStates = storm::storage::BitVector(numberOfStates);
addedStates.operator|=(top->states);
addedStates.operator|=(bottom->states);
for (auto i = top->states.getNextSetIndex(0); i < numberOfStates; i = top->states.getNextSetIndex(i+1)) {
nodes.at(i) = top;
}
for (auto i = bottom->states.getNextSetIndex(0); i < numberOfStates; i = bottom->states.getNextSetIndex(i+1)) {
nodes.at(i) = bottom;
}
// Create all nodes
for (auto itr = lattice->getNodes().begin(); itr != lattice->getNodes().end(); ++itr) {
Node* oldNode = (*itr);
if (oldNode != nullptr) {
Node *newNode = new Node();
newNode->states = storm::storage::BitVector(oldNode->states);
for (auto i = newNode->states.getNextSetIndex(0);
i < numberOfStates; i = newNode->states.getNextSetIndex(i + 1)) {
addedStates.set(i);
nodes.at(i) = newNode;
}
}
}
// Create transitions
for (auto itr = lattice->getNodes().begin(); itr != lattice->getNodes().end(); ++itr) {
Node* oldNode = (*itr);
if (oldNode != nullptr) {
auto state = (*itr)->states.getNextSetIndex(0);
for (auto itr2 = (*itr)->below.begin(); itr2 != (*itr)->below.end(); ++itr2) {
auto stateBelow = (*itr2)->states.getNextSetIndex(0);
addRelationNodes(getNode((state)), getNode((stateBelow)));
}
}
}
}
void Lattice::addBetween(uint_fast64_t state, Node *above, Node *below) {
Node *newNode = new Node();
newNode->states = storm::storage::BitVector(numberOfStates);
@ -102,6 +149,11 @@ namespace storm {
return bottom;
}
std::vector<Lattice::Node*> Lattice::getNodes() {
return nodes;
}
storm::storage::BitVector Lattice::getAddedStates() {
return addedStates;
}
@ -203,34 +255,6 @@ namespace storm {
out << "}" << std::endl;
}
Lattice* Lattice::deepCopy() {
Lattice* result = new Lattice(top->states, bottom->states, numberOfStates);
// Create all nodes
for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) {
Node* oldNode = (*itr);
if (oldNode != nullptr) {
Node *newNode = new Node();
newNode->states = storm::storage::BitVector(oldNode->states);
for (auto i = newNode->states.getNextSetIndex(0);
i < numberOfStates; i = newNode->states.getNextSetIndex(i + 1)) {
result->addedStates.set(i);
result->nodes.at(i) = newNode;
}
}
}
// Create transitions
for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) {
if (*itr != nullptr) {
auto state = (*itr)->states.getNextSetIndex(0);
for (auto itr2 = (*itr)->below.begin(); itr2 != (*itr)->below.end(); ++itr2) {
auto stateBelow = (*itr2)->states.getNextSetIndex(0);
result->addRelationNodes(result->getNode((state)), result->getNode((stateBelow)));
}
}
}
return result;
}
bool Lattice::above(Node *node1, Node *node2, std::set<Node *>* seenNodes) {
bool result = !node1->below.empty() && std::find(node1->below.begin(), node1->below.end(), node2) != node1->below.end();

6
src/storm-pars/analysis/Lattice.h
View File

@ -31,6 +31,8 @@ namespace storm {
Lattice(storm::storage::BitVector topStates,
storm::storage::BitVector bottomStates, uint_fast64_t numberOfStates);
Lattice(Lattice* lattice);
/*!
* Adds a node with the given state below node1 and above node2.
* @param state The given state.
@ -88,6 +90,8 @@ namespace storm {
Node* getBottom();
std::vector<Node*> getNodes();
storm::storage::BitVector getAddedStates();
/*!
@ -104,8 +108,6 @@ namespace storm {
*/
void toDotFile(std::ostream &out);
Lattice* deepCopy();
static const int UNKNOWN = -1;
static const int BELOW = 2;
static const int ABOVE = 1;

Write Preview
Loading…
Cancel
Save