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

Clean up lattice creation code

tempestpy_adaptions
Jip Spel 5 years ago
parent
8214c5758e
commit
1c5d6b7237
7 changed files with 119 additions and 189 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. 12
      src/storm-pars/analysis/Lattice.cpp
  2. 10
      src/storm-pars/analysis/Lattice.h
  3. 228
      src/storm-pars/analysis/LatticeExtender.cpp
  4. 6
      src/storm-pars/analysis/LatticeExtender.h
  5. 19
      src/test/storm-pars/analysis/AssumptionCheckerTest.cpp
  6. 7
      src/test/storm-pars/analysis/AssumptionMakerTest.cpp
  7. 6
      src/test/storm-pars/analysis/LatticeTest.cpp

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

@ -7,12 +7,15 @@ namespace storm {
Lattice::Lattice(storm::storage::BitVector* topStates,
storm::storage::BitVector* bottomStates,
storm::storage::BitVector* initialMiddleStates,
uint_fast64_t numberOfStates) {
uint_fast64_t numberOfStates,
std::vector<uint_fast64_t>* statesSorted) {
nodes = std::vector<Node *>(numberOfStates);
this->numberOfStates = numberOfStates;
this->addedStates = new storm::storage::BitVector(numberOfStates);
this->doneBuilding = false;
this->statesSorted = statesSorted;
this->statesToHandle = initialMiddleStates;
top = new Node();
bottom = new Node();
@ -38,12 +41,14 @@ namespace storm {
}
}
Lattice::Lattice(uint_fast64_t topState, uint_fast64_t bottomState, uint_fast64_t numberOfStates) {
Lattice::Lattice(uint_fast64_t topState, uint_fast64_t bottomState, uint_fast64_t numberOfStates, std::vector<uint_fast64_t>* statesSorted) {
nodes = std::vector<Node *>(numberOfStates);
this->numberOfStates = numberOfStates;
this->addedStates = new storm::storage::BitVector(numberOfStates);
this->doneBuilding = false;
this->statesSorted = statesSorted;
this->statesToHandle = new storm::storage::BitVector(numberOfStates);
top = new Node();
bottom = new Node();
@ -96,6 +101,9 @@ namespace storm {
newNode->statesAbove = storm::storage::BitVector((oldNode->statesAbove));
}
}
this->statesSorted = lattice->statesSorted;
this->statesToHandle = lattice->statesToHandle;
}
void Lattice::addBetween(uint_fast64_t state, Node *above, Node *below) {

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

@ -38,7 +38,8 @@ namespace storm {
Lattice(storm::storage::BitVector* topStates,
storm::storage::BitVector* bottomStates,
storm::storage::BitVector* initialMiddleStates,
uint_fast64_t numberOfStates);
uint_fast64_t numberOfStates,
std::vector<uint_fast64_t>* statesSorted);
/*!
* Constructs a lattice with the given top state and bottom state.
@ -49,7 +50,8 @@ namespace storm {
*/
Lattice(uint_fast64_t top,
uint_fast64_t bottom,
uint_fast64_t numberOfStates);
uint_fast64_t numberOfStates,
std::vector<uint_fast64_t>* statesSorted);
/*!
* Constructs a copy of the given lattice.
@ -208,6 +210,10 @@ namespace storm {
*/
void merge(uint_fast64_t var1, uint_fast64_t var2);
storm::storage::BitVector* statesToHandle;
std::vector<uint_fast64_t>* statesSorted;
private:
std::vector<Node*> nodes;

228
src/storm-pars/analysis/LatticeExtender.cpp
View File

@ -58,8 +58,6 @@ namespace storm {
for (auto i = 0; acyclic && i < sccs.size(); ++i) {
acyclic &= sccs.getBlock(i).size() <= 1;
}
statesSorted = storm::utility::graph::getTopologicalSort(matrix);
}
template <typename ValueType>
@ -98,32 +96,12 @@ namespace storm {
auto initialMiddleStates = storm::storage::BitVector(numberOfStates);
// Check if MC contains cycles
storm::storage::StronglyConnectedComponentDecompositionOptions const options;
auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<ValueType>(model->getTransitionMatrix(), options);
acyclic = true;
for (auto i = 0; acyclic && i < decomposition.size(); ++i) {
acyclic &= decomposition.getBlock(i).size() <= 1;
}
statesSorted = storm::utility::graph::getTopologicalSort(matrix);
// Create the Lattice
Lattice *lattice = new Lattice(&topStates, &bottomStates, &initialMiddleStates, numberOfStates);
if (acyclic) {
} else {
for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
stateMap[i] = new storm::storage::BitVector(numberOfStates, false);
auto row = matrix.getRow(i);
for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) {
// ignore self-loops when there are more transitions
if (i != rowItr->getColumn() || row.getNumberOfEntries() == 1) {
stateMap[i]->set(rowItr->getColumn(), true);
}
}
}
for (auto i = 0; i < decomposition.size(); ++i) {
// TODO: alleen als er nog geen van in de lattice zit
auto scc = decomposition.getBlock(i);
if (!acyclic) {
for (auto i = 0; i < sccs.size(); ++i) {
auto scc = sccs.getBlock(i);
if (scc.size() > 1) {
auto states = scc.getStates();
// check if the state has already one successor in bottom of top, in that case pick it
@ -135,7 +113,6 @@ namespace storm {
auto intersection = bottomStates | topStates;
if (intersection[succ1] || intersection[succ2]) {
initialMiddleStates.set(state);
// ipv daaraan toevoegen, hem toevoegen aan de lattice die we eerder al gecreerd hebben
break;
}
}
@ -143,7 +120,8 @@ namespace storm {
}
}
}
statesToHandle = &initialMiddleStates;
std::vector<uint_fast64_t> statesSorted = storm::utility::graph::getTopologicalSort(matrix);
Lattice *lattice = new Lattice(&topStates, &bottomStates, &initialMiddleStates, numberOfStates, &statesSorted);
return this->extendLattice(lattice);
}
@ -180,10 +158,11 @@ namespace storm {
uint_fast64_t bottom = bottomStates.getNextSetIndex(0);
uint_fast64_t top = topStates.getNextSetIndex(0);
Lattice* lattice = new Lattice(top, bottom, numberOfStates);
std::vector<uint_fast64_t> statesSorted = storm::utility::graph::getTopologicalSort(matrix);
Lattice *lattice = new Lattice(top, bottom, numberOfStates, &statesSorted);
for (auto state : statesSorted) {
for (auto state : *(lattice->statesSorted)) {
if (state != bottom && state != top) {
assert (lattice != nullptr);
auto successors = stateMap[state];
@ -258,6 +237,7 @@ namespace storm {
}
if (candidate != -1) {
lattice->add(candidate);
lattice->statesToHandle->set(candidate);
}
}
}
@ -388,88 +368,17 @@ namespace storm {
handleAssumption(lattice, assumption);
}
auto statesSorted = lattice->statesSorted;
auto oldNumberSet = numberOfStates;
while (oldNumberSet != lattice->getAddedStates()->getNumberOfSetBits()) {
oldNumberSet = lattice->getAddedStates()->getNumberOfSetBits();
if (!assumptionSeen && acyclic) {
if (statesSorted.size() > 0) {
auto nextState = *(statesSorted.begin());
while (lattice->contains(nextState) && statesSorted.size() > 1) {
// states.size()>1 such that there is at least one state left after erase
statesSorted.erase(statesSorted.begin());
nextState = *(statesSorted.begin());
}
if (!lattice->contains(nextState)) {
auto row = this->model->getTransitionMatrix().getRow(nextState);
auto successors = new storm::storage::BitVector(numberOfStates);
for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) {
// ignore self-loops when there are more transitions
if (nextState != rowItr->getColumn()) {
successors->set(rowItr->getColumn());
}
}
assert ((*(lattice->getAddedStates()) & *successors) == *successors);
auto result = extendAllSuccAdded(lattice, nextState, successors);
if (std::get<1>(result) != numberOfStates) {
return result;
} else {
assert (lattice->getNode(nextState) != nullptr);
statesSorted.erase(statesSorted.begin());
}
}
auto added = lattice->getAddedStates()->getNumberOfSetBits();
assert (lattice->getNode(nextState) != nullptr);
assert (lattice->contains(nextState));
}
} else if (assumptionSeen && acyclic) {
auto states = statesSorted;
if (states.size() > 0) {
auto nextState = *(states.begin());
while (lattice->contains(nextState) && states.size() > 1) {
// states.size()>1 such that there is at least one state left after erase
states.erase(states.begin());
nextState = *(states.begin());
}
if (!lattice->contains(nextState)) {
auto row = this->model->getTransitionMatrix().getRow(nextState);
auto successors = new storm::storage::BitVector(numberOfStates);
for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) {
// ignore self-loops when there are more transitions
if (nextState != rowItr->getColumn()) {
successors->set(rowItr->getColumn());
}
}
assert ((*(lattice->getAddedStates()) & *successors) == *successors);
auto result = extendAllSuccAdded(lattice, nextState, successors);
if (std::get<1>(result) != numberOfStates) {
return result;
} else {
assert (lattice->getNode(nextState) != nullptr);
states.erase(states.begin());
}
if (!assumptionSeen) {
statesSorted = states;
}
}
assert (lattice->getNode(nextState) != nullptr);
assert (lattice->contains(nextState));
}
} else if (!acyclic) {
if (assumptionSeen) {
statesToHandle = lattice->getAddedStates();
}
// Forward reasoning for cycles;
if (!acyclic) {
auto statesToHandle = lattice->statesToHandle;
auto stateNumber = statesToHandle->getNextSetIndex(0);
while (stateNumber != numberOfStates) {
storm::storage::BitVector *successors = stateMap[stateNumber];
// Checking for states which are already added to the lattice, and only have one successor left which haven't been added yet
@ -481,9 +390,9 @@ namespace storm {
if (!lattice->contains(succ1)) {
lattice->addToNode(succ1, lattice->getNode(stateNumber));
statesToHandle->set(succ1, true);
auto itr = std::find(statesSorted.begin(), statesSorted.end(), succ1);
if (itr != statesSorted.end()) {
statesSorted.erase(itr);
auto itr = std::find(statesSorted->begin(), statesSorted->end(), succ1);
if (itr != statesSorted->end()) {
statesSorted->erase(itr);
}
}
statesToHandle->set(stateNumber, false);
@ -498,18 +407,18 @@ namespace storm {
auto compare = lattice->compare(stateNumber, succ1);
if (compare == Lattice::ABOVE) {
auto itr = std::find(statesSorted.begin(), statesSorted.end(), succ2);
if (itr != statesSorted.end()) {
statesSorted.erase(itr);
auto itr = std::find(statesSorted->begin(), statesSorted->end(), succ2);
if (itr != statesSorted->end()) {
statesSorted->erase(itr);
}
lattice->addBetween(succ2, lattice->getTop(), lattice->getNode(stateNumber));
statesToHandle->set(succ2);
statesToHandle->set(stateNumber, false);
stateNumber = statesToHandle->getNextSetIndex(0);
} else if (compare == Lattice::BELOW) {
auto itr = std::find(statesSorted.begin(), statesSorted.end(), succ2);
if (itr != statesSorted.end()) {
statesSorted.erase(itr);
auto itr = std::find(statesSorted->begin(), statesSorted->end(), succ2);
if (itr != statesSorted->end()) {
statesSorted->erase(itr);
}
lattice->addBetween(succ2, lattice->getNode(stateNumber), lattice->getBottom());
statesToHandle->set(succ2);
@ -530,71 +439,68 @@ namespace storm {
}
}
if (!assumptionSeen) {
if (statesSorted.size() > 0) {
stateNumber = *(statesSorted.begin());
} else {
stateNumber = numberOfStates;
}
while (stateNumber != numberOfStates
&& lattice->contains(stateNumber)) {
statesSorted.erase(statesSorted.begin());
if (statesSorted.size() > 0) {
stateNumber = *(statesSorted.begin());
} else {
stateNumber = numberOfStates;
}
}
if (stateNumber != numberOfStates) {
storm::storage::BitVector *successors = stateMap[stateNumber];
// Normal backwardreasoning
if (statesSorted->size() > 0) {
auto stateNumber = *(statesSorted->begin());
while (lattice->contains(stateNumber) && statesSorted->size() > 1) {
// states.size()>1 such that there is at least one state left after erase
statesSorted->erase(statesSorted->begin());
stateNumber = *(statesSorted->begin());
// Check if current state has not been added yet, and all successors have, ignore selfloop in this
successors->set(stateNumber, false);
if ((*successors & *(lattice->getAddedStates())) == *successors) {
auto result = extendAllSuccAdded(lattice, stateNumber, successors);
if (std::get<1>(result) != successors->size()) {
return result;
if (lattice->contains(stateNumber)) {
auto resAllAdded = allSuccAdded(lattice, stateNumber);
if (!std::get<0>(resAllAdded)) {
return std::make_tuple(lattice, std::get<1>(resAllAdded), std::get<2>(resAllAdded));
}
statesToHandle->set(stateNumber);
}
}
} else {
auto notAddedStates = lattice->getAddedStates()->operator~();
for (auto stateNumber : notAddedStates) {
// Iterate over all not yet added states
storm::storage::BitVector* successors = stateMap[stateNumber];
// Check if current state has not been added yet, and all successors have, ignore selfloop in this
successors->set(stateNumber, false);
if ((*successors & *(lattice->getAddedStates())) == *successors) {
if (!lattice->contains(stateNumber)) {
auto successors = stateMap[stateNumber];
auto result = extendAllSuccAdded(lattice, stateNumber, successors);
if (std::get<1>(result) != successors->size()) {
if (std::get<1>(result) != numberOfStates) {
// So we don't know the relation between all successor states
return result;
} else {
assert (lattice->getNode(stateNumber) != nullptr);
if (!acyclic) {
lattice->statesToHandle->set(stateNumber);
}
statesToHandle->set(stateNumber);
statesSorted->erase(statesSorted->begin());
}
}
assert (lattice->getNode(stateNumber) != nullptr);
assert (lattice->contains(stateNumber));
}
// if nothing changed and there are states left, then add a state between top and bottom
if (oldNumberSet == lattice->getAddedStates()->getNumberOfSetBits() && oldNumberSet != numberOfStates) {
if (assumptionSeen || statesSorted.size() == 0) {
stateNumber = lattice->getAddedStates()->getNextUnsetIndex(0);
} else {
stateNumber = *(statesSorted.begin());//lattice->getAddedStates()->getNextUnsetIndex(0);
statesSorted.erase(statesSorted.begin());
}
assert (lattice->getAddedStates()->getNumberOfSetBits() == numberOfStates);
lattice->setDoneBuilding(true);
return std::make_tuple(lattice, numberOfStates, numberOfStates);
}
template <typename ValueType>
std::tuple<bool, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::allSuccAdded(storm::analysis::Lattice *lattice, uint_fast64_t stateNumber) {
auto successors = stateMap[stateNumber];
auto numberOfStates = successors->size();
lattice->add(stateNumber);
statesToHandle->set(stateNumber);
if (successors->getNumberOfSetBits() == 1) {
auto succ = successors->getNextSetIndex(0);
return std::make_tuple(lattice->contains(succ), succ, succ);
} else if (successors->getNumberOfSetBits() > 2) {
for (auto const& i : *successors) {
for (auto j = successors->getNextSetIndex(i+1); j < numberOfStates; j = successors->getNextSetIndex(j+1)) {
if (lattice->compare(i,j) == Lattice::UNKNOWN) {
return std::make_tuple(false, i, j);
}
}
}
assert (lattice->getAddedStates()->getNumberOfSetBits() == numberOfStates);
lattice->setDoneBuilding(true);
return std::make_tuple(lattice, numberOfStates, numberOfStates);
}
return std::make_tuple(true, numberOfStates, numberOfStates);
}
template class LatticeExtender<storm::RationalFunction>;

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

@ -63,14 +63,10 @@ namespace storm {
std::map<uint_fast64_t, storm::storage::BitVector*> stateMap;
std::vector<uint_fast64_t> statesSorted;
bool acyclic;
bool assumptionSeen;
storm::storage::BitVector* statesToHandle;
storm::storage::StronglyConnectedComponentDecomposition<ValueType> sccs;
storm::storage::SparseMatrix<ValueType> matrix;
@ -78,6 +74,8 @@ namespace storm {
void handleAssumption(Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption);
std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> extendAllSuccAdded(Lattice* lattice, uint_fast64_t const & stateNumber, storm::storage::BitVector* successors);
std::tuple<bool, uint_fast64_t, uint_fast64_t> allSuccAdded(Lattice* lattice, uint_fast64_t stateNumber);
};
}
}

19
src/test/storm-pars/analysis/AssumptionCheckerTest.cpp
View File

@ -88,7 +88,9 @@ TEST(AssumptionCheckerTest, Brp_no_bisimulation) {
below.set(1);
storm::storage::BitVector initialMiddle(8);
auto dummyLattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 8);
std::vector<uint_fast64_t> statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix());
auto dummyLattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 8, &statesSorted);
// Validate assumption
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyLattice));
// EXPECT_FALSE(checker.validated(assumption));
@ -105,7 +107,8 @@ TEST(AssumptionCheckerTest, Brp_no_bisimulation) {
below = storm::storage::BitVector(13);
below.set(9);
initialMiddle = storm::storage::BitVector(13);
dummyLattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 13);
dummyLattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 13, &statesSorted);
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption));
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyLattice));
// EXPECT_EQ(checker.validated(assumption));
@ -199,7 +202,9 @@ TEST(AssumptionCheckerTest, Simple2) {
below.set(4);
storm::storage::BitVector initialMiddle(5);
auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 5);
std::vector<uint_fast64_t> statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix());
auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 5, &statesSorted);
// Checking on samples and validate
auto assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(
@ -263,7 +268,9 @@ TEST(AssumptionCheckerTest, Simple3) {
below.set(5);
storm::storage::BitVector initialMiddle(6);
auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 6);
std::vector<uint_fast64_t> statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix());
auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 6, &statesSorted);
lattice->add(3);
// Checking on samples and validate
@ -330,7 +337,9 @@ TEST(AssumptionCheckerTest, Simple4) {
storm::storage::BitVector below(5);
below.set(4);
storm::storage::BitVector initialMiddle(5);
auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 5);
std::vector<uint_fast64_t> statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix());
auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 5, &statesSorted);
auto assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(
storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),

7
src/test/storm-pars/analysis/AssumptionMakerTest.cpp
View File

@ -196,8 +196,9 @@ TEST(AssumptionMakerTest, Simple1) {
storm::storage::BitVector below(5);
below.set(4);
storm::storage::BitVector initialMiddle(5);
std::vector<uint_fast64_t> statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix());
auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 5);
auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 5, &statesSorted);
auto assumptionChecker = storm::analysis::AssumptionChecker<storm::RationalFunction>(formulas[0], dtmc, region, 3);
auto assumptionMaker = storm::analysis::AssumptionMaker<storm::RationalFunction>(&assumptionChecker, dtmc->getNumberOfStates(), true);
@ -268,7 +269,9 @@ TEST(AssumptionMakerTest, Simple2) {
below.set(4);
storm::storage::BitVector initialMiddle(5);
auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 5);
std::vector<uint_fast64_t> statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix());
auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 5, &statesSorted);
auto assumptionChecker = storm::analysis::AssumptionChecker<storm::RationalFunction>(formulas[0], dtmc, region, 3);
auto assumptionMaker = storm::analysis::AssumptionMaker<storm::RationalFunction>(&assumptionChecker, dtmc->getNumberOfStates(), true);

6
src/test/storm-pars/analysis/LatticeTest.cpp
View File

@ -12,7 +12,7 @@ TEST(LatticeTest, Simple) {
below.set(1);
auto initialMiddle = storm::storage::BitVector(numberOfStates);
auto lattice = storm::analysis::Lattice(&above, &below, &initialMiddle, numberOfStates);
auto lattice = storm::analysis::Lattice(&above, &below, &initialMiddle, numberOfStates, nullptr);
EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(0,1));
EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(1,0));
EXPECT_EQ(nullptr, lattice.getNode(2));
@ -78,7 +78,7 @@ TEST(LatticeTest, copy_lattice) {
below.set(1);
auto initialMiddle = storm::storage::BitVector(numberOfStates);
auto lattice = storm::analysis::Lattice(&above, &below, &initialMiddle, numberOfStates);
auto lattice = storm::analysis::Lattice(&above, &below, &initialMiddle, numberOfStates, nullptr);
lattice.add(2);
lattice.add(3);
lattice.addToNode(4, lattice.getNode(2));
@ -143,7 +143,7 @@ TEST(LatticeTest, merge_nodes) {
below.set(1);
auto initialMiddle = storm::storage::BitVector(numberOfStates);
auto lattice = storm::analysis::Lattice(&above, &below, &initialMiddle, numberOfStates);
auto lattice = storm::analysis::Lattice(&above, &below, &initialMiddle, numberOfStates, nullptr);
lattice.add(2);
lattice.add(3);
lattice.addToNode(4, lattice.getNode(2));

Write Preview
Loading…
Cancel
Save