From ee8971c608599a8de14c3278365df7e4dee54d6e Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Mon, 27 Aug 2018 10:22:22 +0200
Subject: [PATCH] Clean up
---
src/storm-pars/analysis/Lattice.cpp | 9 +--------
src/storm-pars/analysis/Lattice.h | 9 +++------
2 files changed, 4 insertions(+), 14 deletions(-)
diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp
index 66c3af007..b2fa043e7 100644
--- a/src/storm-pars/analysis/Lattice.cpp
+++ b/src/storm-pars/analysis/Lattice.cpp
@@ -180,9 +180,8 @@ namespace storm {
}
out << "}" << std::endl;
-
-
}
+
bool Lattice::above(Node *node1, Node *node2) {
bool result = !node1->below.empty() && std::find(node1->below.begin(), node1->below.end(), node2) != node1->below.end();
@@ -191,11 +190,5 @@ namespace storm {
}
return result;
}
-
- void Lattice::setStates(std::vector<uint_fast64_t> states, Node *node) {
- for (auto itr = states.begin(); itr < states.end(); ++itr) {
- node->states.set(*itr);
- }
- }
}
}
diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h
index 698b2d058..03147431e 100644
--- a/src/storm-pars/analysis/Lattice.h
+++ b/src/storm-pars/analysis/Lattice.h
@@ -150,17 +150,17 @@ namespace storm {
for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) {
stateMap[i].set(rowItr->getColumn(), true);
}
- // TODO: allow more than 2 transitions
+ // TODO: allow more than 2 transitions? or fix this in preprocessing?
STORM_LOG_THROW(stateMap[i].getNumberOfSetBits() <= 2, storm::exceptions::NotSupportedException, "Only two outgoing transitions per state allowed");
}
// 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;
- matrix.printAsMatlabMatrix(std::cout);
while (oldStates != seenStates) {
// As long as new states are added to the lattice, continue.
oldStates = storm::storage::BitVector(seenStates);
@@ -181,7 +181,7 @@ namespace storm {
lattice->addToNode(stateNumber, lattice->getNode(successors.getNextSetIndex(0)));
seenStates.set(stateNumber);
} else if (check && successors.getNumberOfSetBits() > 1) {
- // TODO: allow more than 2 transitions
+ // TODO: allow more than 2 transitions?
// Otherwise, check how the two states compare, and add if the comparison is possible.
uint_fast64_t successor1 = successors.getNextSetIndex(0);
@@ -220,9 +220,6 @@ namespace storm {
uint_fast64_t numberOfStates;
bool above(Node *, Node *);
-
- void setStates(std::vector<uint_fast64_t> states, Node *node);
-
};
}
}