diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index 404ffe47e..3253a7d44 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -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* statesSorted) { nodes = std::vector(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* statesSorted) { nodes = std::vector(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) { diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h index bdd25a5f2..9de5ed07b 100644 --- a/src/storm-pars/analysis/Lattice.h +++ b/src/storm-pars/analysis/Lattice.h @@ -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* 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* 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* statesSorted; + private: std::vector nodes; diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp index f8cabe47a..b36230492 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -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 @@ -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(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 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 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,90 +368,19 @@ 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]; + 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 auto succ1 = successors->getNextSetIndex(0); auto succ2 = successors->getNextSetIndex(succ1 + 1); @@ -481,16 +390,16 @@ 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); stateNumber = statesToHandle->getNextSetIndex(0); } else if (successors->getNumberOfSetBits() == 2 - && ((lattice->contains(succ1) && !lattice->contains(succ2)) - || (!lattice->contains(succ1) && lattice->contains(succ2)))) { + && ((lattice->contains(succ1) && !lattice->contains(succ2)) + || (!lattice->contains(succ1) && lattice->contains(succ2)))) { if (!lattice->contains(succ1)) { std::swap(succ1, succ2); @@ -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,73 +439,70 @@ 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]; + } - // 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; - } - 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) { - auto result = extendAllSuccAdded(lattice, stateNumber, successors); - if (std::get<1>(result) != successors->size()) { - return result; - } - statesToHandle->set(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()); + + 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)); } } + } + if (!lattice->contains(stateNumber)) { + auto successors = stateMap[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); + auto result = extendAllSuccAdded(lattice, stateNumber, successors); + if (std::get<1>(result) != numberOfStates) { + // So we don't know the relation between all successor states + return result; } else { - stateNumber = *(statesSorted.begin());//lattice->getAddedStates()->getNextUnsetIndex(0); - statesSorted.erase(statesSorted.begin()); + assert (lattice->getNode(stateNumber) != nullptr); + if (!acyclic) { + lattice->statesToHandle->set(stateNumber); + } + statesSorted->erase(statesSorted->begin()); } - - lattice->add(stateNumber); - statesToHandle->set(stateNumber); } + assert (lattice->getNode(stateNumber) != nullptr); + assert (lattice->contains(stateNumber)); } + } assert (lattice->getAddedStates()->getNumberOfSetBits() == numberOfStates); - lattice->setDoneBuilding(true); + lattice->setDoneBuilding(true); return std::make_tuple(lattice, numberOfStates, numberOfStates); } + template + std::tuple LatticeExtender::allSuccAdded(storm::analysis::Lattice *lattice, uint_fast64_t stateNumber) { + auto successors = stateMap[stateNumber]; + auto numberOfStates = successors->size(); + + 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); + } + } + } + } + return std::make_tuple(true, numberOfStates, numberOfStates); + + } + template class LatticeExtender; } } diff --git a/src/storm-pars/analysis/LatticeExtender.h b/src/storm-pars/analysis/LatticeExtender.h index 42b743fa5..cc4e7370f 100644 --- a/src/storm-pars/analysis/LatticeExtender.h +++ b/src/storm-pars/analysis/LatticeExtender.h @@ -63,14 +63,10 @@ namespace storm { std::map stateMap; - std::vector statesSorted; - bool acyclic; bool assumptionSeen; - storm::storage::BitVector* statesToHandle; - storm::storage::StronglyConnectedComponentDecomposition sccs; storm::storage::SparseMatrix matrix; @@ -78,6 +74,8 @@ namespace storm { void handleAssumption(Lattice* lattice, std::shared_ptr assumption); std::tuple extendAllSuccAdded(Lattice* lattice, uint_fast64_t const & stateNumber, storm::storage::BitVector* successors); + + std::tuple allSuccAdded(Lattice* lattice, uint_fast64_t stateNumber); }; } } diff --git a/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp index bc331296d..987ef4ef7 100644 --- a/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp +++ b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp @@ -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 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 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( @@ -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 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 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(*expressionManager, expressionManager->getBooleanType(), diff --git a/src/test/storm-pars/analysis/AssumptionMakerTest.cpp b/src/test/storm-pars/analysis/AssumptionMakerTest.cpp index 71b7b1e7f..7268d0c5f 100644 --- a/src/test/storm-pars/analysis/AssumptionMakerTest.cpp +++ b/src/test/storm-pars/analysis/AssumptionMakerTest.cpp @@ -196,8 +196,9 @@ TEST(AssumptionMakerTest, Simple1) { storm::storage::BitVector below(5); below.set(4); storm::storage::BitVector initialMiddle(5); + std::vector 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(formulas[0], dtmc, region, 3); auto assumptionMaker = storm::analysis::AssumptionMaker(&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 statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); + + auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 5, &statesSorted); auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], dtmc, region, 3); auto assumptionMaker = storm::analysis::AssumptionMaker(&assumptionChecker, dtmc->getNumberOfStates(), true); diff --git a/src/test/storm-pars/analysis/LatticeTest.cpp b/src/test/storm-pars/analysis/LatticeTest.cpp index dbb590c41..3b9011b04 100644 --- a/src/test/storm-pars/analysis/LatticeTest.cpp +++ b/src/test/storm-pars/analysis/LatticeTest.cpp @@ -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));