From af23545a7b9ed90f324307d03093151623536a12 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Mon, 29 Oct 2018 10:27:22 +0100 Subject: [PATCH] Clean up Lattice Extender --- src/storm-pars/analysis/Lattice.cpp | 8 +- src/storm-pars/analysis/Lattice.h | 4 +- src/storm-pars/analysis/LatticeExtender.cpp | 279 +++++++++--------- src/storm-pars/analysis/LatticeExtender.h | 4 +- .../analysis/AssumptionCheckerTest.cpp | 7 +- src/test/storm-pars/analysis/LatticeTest.cpp | 6 +- .../analysis/MonotonicityCheckerTest.cpp | 6 +- 7 files changed, 164 insertions(+), 150 deletions(-) diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index 461962f3d..9a1bacbc4 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -9,7 +9,9 @@ namespace storm { namespace analysis { Lattice::Lattice(storm::storage::BitVector topStates, - storm::storage::BitVector bottomStates, uint_fast64_t numberOfStates) { + storm::storage::BitVector bottomStates, + storm::storage::BitVector initialMiddleStates, + uint_fast64_t numberOfStates) { assert(topStates.getNumberOfSetBits() != 0); assert(bottomStates.getNumberOfSetBits() != 0); assert((topStates & bottomStates).getNumberOfSetBits() == 0); @@ -37,6 +39,10 @@ namespace storm { this->addedStates = storm::storage::BitVector(numberOfStates); this->addedStates |= (topStates); this->addedStates |= (bottomStates); + + for (auto state = initialMiddleStates.getNextSetIndex(0); state < numberOfStates; state = initialMiddleStates.getNextSetIndex(state + 1)) { + add(state); + } } Lattice::Lattice(Lattice* lattice) { diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h index e2938cd79..4bf9a68ee 100644 --- a/src/storm-pars/analysis/Lattice.h +++ b/src/storm-pars/analysis/Lattice.h @@ -29,7 +29,9 @@ namespace storm { * @param bottomNode The bottom node of the resulting lattice. */ Lattice(storm::storage::BitVector topStates, - storm::storage::BitVector bottomStates, uint_fast64_t numberOfStates); + storm::storage::BitVector bottomStates, + storm::storage::BitVector initialMiddleStates, + uint_fast64_t numberOfStates); /*! * Constructs a copy of the given lattice. diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp index 4cc596571..d378f7e0a 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -78,8 +78,8 @@ namespace storm { } } - auto initialMiddleStates = storm::storage::BitVector(model->getNumberOfStates()); - // Check if MC is acyclic + auto initialMiddleStates = storm::storage::BitVector(numberOfStates); + // Check if MC contains cycles auto decomposition = storm::storage::StronglyConnectedComponentDecomposition(model->getTransitionMatrix(), false, false); for (auto i = 0; i < decomposition.size(); ++i) { auto scc = decomposition.getBlock(i); @@ -93,25 +93,17 @@ namespace storm { auto succ1 = successors.getNextSetIndex(0); auto succ2 = successors.getNextSetIndex(succ1 + 1); auto intersection = bottomStates | topStates; - if ((intersection[succ1] && ! intersection[succ2]) - || (intersection[succ2] && !intersection[succ1])) { + if (intersection[succ1] || intersection[succ2]) { initialMiddleStates.set(*stateItr); found = true; - } else if (intersection[succ1] && intersection[succ2]) { - found = true; } } - } } } // Create the Lattice - Lattice *lattice = new Lattice(topStates, bottomStates, numberOfStates); - for (auto state = initialMiddleStates.getNextSetIndex(0); state != numberOfStates; state = initialMiddleStates.getNextSetIndex(state + 1)) { - lattice->add(state); - } - + Lattice *lattice = new Lattice(topStates, bottomStates, initialMiddleStates, numberOfStates); latticeWatch.stop(); STORM_PRINT(std::endl << "Time for initialization of lattice: " << latticeWatch << "." << std::endl << std::endl); @@ -119,164 +111,169 @@ namespace storm { } template - std::tuple LatticeExtender::extendLattice(Lattice* lattice, std::shared_ptr assumption) { - // TODO: split up - auto numberOfStates = this->model->getNumberOfStates(); - // First handle assumption - if (assumption != nullptr) { - storm::expressions::BinaryRelationExpression expr = *assumption; - STORM_LOG_THROW(expr.getRelationType() == - storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual - || expr.getRelationType() == - storm::expressions::BinaryRelationExpression::RelationType::Equal, - storm::exceptions::NotImplementedException, "Only GreaterOrEqual or Equal assumptions allowed"); - if (expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) { - assert (expr.getFirstOperand()->isVariable() && expr.getSecondOperand()->isVariable()); - storm::expressions::Variable var1 = expr.getFirstOperand()->asVariableExpression().getVariable(); - storm::expressions::Variable var2 = expr.getSecondOperand()->asVariableExpression().getVariable(); - auto val1 = std::stoul(var1.getName(), nullptr, 0); - auto val2 = std::stoul(var2.getName(), nullptr, 0); - auto comp = lattice->compare(val1, val2); - assert (comp == Lattice::UNKNOWN || comp == Lattice::SAME); - Lattice::Node *n1 = lattice->getNode(val1); - Lattice::Node *n2 = lattice->getNode(val2); - - if (n1 != nullptr && n2 != nullptr) { - assert(false); -// lattice->mergeNodes(n1, n2); - } else if (n1 != nullptr) { - lattice->addToNode(val2, n1); - } else if (n2 != nullptr) { - lattice->addToNode(val1, n2); - } else { - lattice->add(val1); - lattice->addToNode(val2, lattice->getNode(val1)); + void LatticeExtender::handleAssumption(Lattice* lattice, std::shared_ptr assumption) { + assert (assumption != nullptr); + + storm::expressions::BinaryRelationExpression expr = *assumption; + assert (expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual + || expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal); + + if (expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) { + assert (expr.getFirstOperand()->isVariable() && expr.getSecondOperand()->isVariable()); + storm::expressions::Variable var1 = expr.getFirstOperand()->asVariableExpression().getVariable(); + storm::expressions::Variable var2 = expr.getSecondOperand()->asVariableExpression().getVariable(); + auto val1 = std::stoul(var1.getName(), nullptr, 0); + auto val2 = std::stoul(var2.getName(), nullptr, 0); + auto comp = lattice->compare(val1, val2); + + assert (comp == Lattice::UNKNOWN); + Lattice::Node *n1 = lattice->getNode(val1); + Lattice::Node *n2 = lattice->getNode(val2); + + if (n1 != nullptr && n2 != nullptr) { + // TODO: mergeNode method + assert(false); + } else if (n1 != nullptr) { + lattice->addToNode(val2, n1); + } else if (n2 != nullptr) { + lattice->addToNode(val1, n2); + } else { + lattice->add(val1); + lattice->addToNode(val2, lattice->getNode(val1)); + } + } else { + assert (expr.getFirstOperand()->isVariable() && expr.getSecondOperand()->isVariable()); + storm::expressions::Variable largest = expr.getFirstOperand()->asVariableExpression().getVariable(); + storm::expressions::Variable smallest = expr.getSecondOperand()->asVariableExpression().getVariable(); + auto val1 = std::stoul(largest.getName(), nullptr, 0); + auto val2 = std::stoul(smallest.getName(), nullptr, 0); + auto compareRes = lattice->compare(val1, val2); + + assert(compareRes == Lattice::UNKNOWN); + Lattice::Node *n1 = lattice->getNode(val1); + Lattice::Node *n2 = lattice->getNode(val2); + + if (n1 != nullptr && n2 != nullptr) { + lattice->addRelationNodes(n1, n2); + } else if (n1 != nullptr) { + lattice->addBetween(val2, n1, lattice->getBottom()); + } else if (n2 != nullptr) { + lattice->addBetween(val1, lattice->getTop(), n2); + } else { + lattice->add(val1); + lattice->addBetween(val2, lattice->getNode(val1), lattice->getBottom()); + } + } + } - } + template + std::tuple LatticeExtender::extendAllSuccAdded(Lattice* lattice, uint_fast64_t stateNumber, storm::storage::BitVector successors) { + auto numberOfStates = successors.size(); + assert (lattice->getAddedStates().size() == numberOfStates); + + if (successors.getNumberOfSetBits() == 1) { + // As there is only one successor the current state and its successor must be at the same nodes. + lattice->addToNode(stateNumber, lattice->getNode(successors.getNextSetIndex(0))); + } else if (successors.getNumberOfSetBits() == 2) { + // Otherwise, check how the two states compare, and add if the comparison is possible. + uint_fast64_t successor1 = successors.getNextSetIndex(0); + uint_fast64_t successor2 = successors.getNextSetIndex(successor1 + 1); + + int compareResult = lattice->compare(successor1, successor2); + if (compareResult == Lattice::ABOVE) { + // successor 1 is closer to top than successor 2 + lattice->addBetween(stateNumber, lattice->getNode(successor1), + lattice->getNode(successor2)); + } else if (compareResult == Lattice::BELOW) { + // successor 2 is closer to top than successor 1 + lattice->addBetween(stateNumber, lattice->getNode(successor2), + lattice->getNode(successor1)); + } else if (compareResult == Lattice::SAME) { + // the successors are at the same level + lattice->addToNode(stateNumber, lattice->getNode(successor1)); } else { - assert (expr.getFirstOperand()->isVariable() && expr.getSecondOperand()->isVariable()); - storm::expressions::Variable largest = expr.getFirstOperand()->asVariableExpression().getVariable(); - storm::expressions::Variable smallest = expr.getSecondOperand()->asVariableExpression().getVariable(); - auto compareRes = lattice->compare(std::stoul(largest.getName(), nullptr, 0), - std::stoul(smallest.getName(), nullptr, 0)); - assert(compareRes == Lattice::UNKNOWN); - if (compareRes != Lattice::ABOVE) { - Lattice::Node *n1 = lattice->getNode( - std::stoul(largest.getName(), nullptr, 0)); - Lattice::Node *n2 = lattice->getNode( - std::stoul(smallest.getName(), nullptr, 0)); - - if (n1 != nullptr && n2 != nullptr) { - lattice->addRelationNodes(n1, n2); - } else if (n1 != nullptr) { - lattice->addBetween(std::stoul(smallest.getName(), nullptr, 0), n1, - lattice->getBottom()); - } else if (n2 != nullptr) { - lattice->addBetween(std::stoul(largest.getName(), nullptr, 0), lattice->getTop(), n2); - } else { - lattice->add(std::stoul(largest.getName(), nullptr, 0)); - lattice->addBetween(std::stoul(smallest.getName(), nullptr, 0), - lattice->getNode(std::stoul(largest.getName(), nullptr, 0)), - lattice->getBottom()); + assert(lattice->compare(successor1, successor2) == Lattice::UNKNOWN); + return std::make_tuple(lattice, successor1, successor2); + } + } else if (successors.getNumberOfSetBits() > 2) { + for (auto i = successors.getNextSetIndex(0); i < numberOfStates; i = successors.getNextSetIndex(i+1)) { + 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(lattice, i, j); } } } + + auto highest = successors.getNextSetIndex(0); + auto lowest = highest; + for (auto i = successors.getNextSetIndex(highest+1); i < numberOfStates; i = successors.getNextSetIndex(i+1)) { + if (lattice->compare(i, highest) == Lattice::ABOVE) { + highest = i; + } + if (lattice->compare(lowest, i) == Lattice::ABOVE) { + lowest = i; + } + } + lattice->addBetween(stateNumber, lattice->getNode(highest), lattice->getNode(lowest)); + } + return std::make_tuple(lattice, numberOfStates, numberOfStates); + } + + template + std::tuple LatticeExtender::extendLattice(Lattice* lattice, std::shared_ptr assumption) { + auto numberOfStates = this->model->getNumberOfStates(); + + if (assumption != nullptr) { + handleAssumption(lattice, assumption); } auto oldNumberSet = numberOfStates; while (oldNumberSet != lattice->getAddedStates().getNumberOfSetBits()) { oldNumberSet = lattice->getAddedStates().getNumberOfSetBits(); + // TODO: kan dit niet efficienter for (auto stateItr = stateMap.begin(); stateItr != stateMap.end(); ++stateItr) { - storm::storage::BitVector seenStates = (lattice->getAddedStates()); // Iterate over all states auto stateNumber = stateItr->first; storm::storage::BitVector successors = stateItr->second; + auto seenStates = (lattice->getAddedStates()); + // Check if current state has not been added yet, and all successors have bool check = !seenStates[stateNumber]; - for (auto succIndex = successors.getNextSetIndex(0); check && succIndex != numberOfStates; succIndex = successors.getNextSetIndex(++succIndex)) { + for (auto succIndex = successors.getNextSetIndex(0); check && succIndex != successors.size(); succIndex = successors.getNextSetIndex(++succIndex)) { + // if the stateNumber equals succIndex we have a self-loop, ignoring selfloop as seenStates[stateNumber] = false if (succIndex != stateNumber) { check &= seenStates[succIndex]; } - // if the stateNumber equals succIndex we have a self-loop } - if (check && successors.getNumberOfSetBits() == 1) { - // As there is only one successor the current state and its successor must be at the same nodes. - lattice->addToNode(stateNumber, lattice->getNode(successors.getNextSetIndex(0))); - } else if (check && successors.getNumberOfSetBits() == 2) { - // Otherwise, check how the two states compare, and add if the comparison is possible. - uint_fast64_t successor1 = successors.getNextSetIndex(0); - uint_fast64_t successor2 = successors.getNextSetIndex(successor1 + 1); - - int compareResult = lattice->compare(successor1, successor2); - if (compareResult == Lattice::ABOVE) { - // successor 1 is closer to top than successor 2 - lattice->addBetween(stateNumber, lattice->getNode(successor1), - lattice->getNode(successor2)); - } else if (compareResult == Lattice::BELOW) { - // successor 2 is closer to top than successor 1 - lattice->addBetween(stateNumber, lattice->getNode(successor2), - lattice->getNode(successor1)); - } else if (compareResult == Lattice::SAME) { - // the successors are at the same level - lattice->addToNode(stateNumber, lattice->getNode(successor1)); - } else { - assert(lattice->compare(successor1, successor2) == Lattice::UNKNOWN); - return std::make_tuple(lattice, successor1, successor2); - } - } else if (check && successors.getNumberOfSetBits() > 2) { - for (auto i = successors.getNextSetIndex(0); i < successors.size(); i = successors.getNextSetIndex(i+1)) { - for (auto j = successors.getNextSetIndex(i+1); j < successors.size(); j = successors.getNextSetIndex(j+1)) { - if (lattice->compare(i,j) == Lattice::UNKNOWN) { - return std::make_tuple(lattice, i, j); - } - } - } - - auto highest = successors.getNextSetIndex(0); - auto lowest = highest; - for (auto i = successors.getNextSetIndex(highest+1); i < successors.size(); i = successors.getNextSetIndex(i+1)) { - if (lattice->compare(i, highest) == Lattice::ABOVE) { - highest = i; - } - if (lattice->compare(lowest, i) == Lattice::ABOVE) { - lowest = i; - } + if (check) { + auto result = extendAllSuccAdded(lattice, stateNumber, successors); + if (std::get<1>(result) != successors.size()) { + return result; } - lattice->addBetween(stateNumber, lattice->getNode(highest), lattice->getNode(lowest)); } - // Checking for states which are already added to the lattice, and only have one successor left which haven't been added yet - bool checkOneSuccLeft = seenStates[stateNumber] && successors.getNumberOfSetBits() <= 2; - bool helper = true; - for (auto succIndex = successors.getNextSetIndex(0); (check || checkOneSuccLeft) && succIndex != numberOfStates; succIndex = successors.getNextSetIndex(++succIndex)) { - checkOneSuccLeft &= !(!helper && !seenStates[succIndex]); - helper &= seenStates[succIndex]; - } + auto succ1 = successors.getNextSetIndex(0); + auto succ2 = successors.getNextSetIndex(succ1 + 1); - checkOneSuccLeft &= !helper; + if (seenStates[stateNumber] && successors.size() == 2 + && (seenStates[succ1] || seenStates[succ2]) + && (!seenStates[succ1] || !seenStates[succ2])) { + if (!seenStates[succ1]) { + std::swap(succ1, succ2); + } - if (checkOneSuccLeft) { - // at most 2 successors - auto succ1 = successors.getNextSetIndex(0); - auto succ2 = successors.getNextSetIndex(succ1+1); - // Otherwise there is just one transition, this is already handled above - if (succ2 != numberOfStates) { - auto nodeCurr = lattice->getNode(stateNumber); - if (!seenStates[succ1]) { - std::swap(succ1, succ2); - } - assert (seenStates[succ1]); - auto nodeSucc = lattice->getNode(succ1); - auto compare = lattice->compare(stateNumber, succ1); - if (compare == Lattice::ABOVE) { - lattice->addBetween(succ2, lattice->getTop(), lattice->getNode(stateNumber)); - } else if (compare == Lattice::BELOW) { - lattice->addBetween(succ2, lattice->getNode(stateNumber), lattice->getBottom()); - } + auto compare = lattice->compare(stateNumber, succ1); + if (compare == Lattice::ABOVE) { + lattice->addBetween(succ2, lattice->getTop(), lattice->getNode(stateNumber)); + } else if (compare == Lattice::BELOW) { + lattice->addBetween(succ2, lattice->getNode(stateNumber), lattice->getBottom()); + } else { + // TODO: implement? + assert(false); } } } diff --git a/src/storm-pars/analysis/LatticeExtender.h b/src/storm-pars/analysis/LatticeExtender.h index 01b0554a8..e4cd8b0c4 100644 --- a/src/storm-pars/analysis/LatticeExtender.h +++ b/src/storm-pars/analysis/LatticeExtender.h @@ -54,7 +54,9 @@ namespace storm { std::map stateMap; -// storm::storage::BitVector initialMiddleStates; + void handleAssumption(Lattice* lattice, std::shared_ptr assumption); + + std::tuple extendAllSuccAdded(Lattice* lattice, uint_fast64_t stateNumber, storm::storage::BitVector successors); }; } } diff --git a/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp index 2e59d1b13..3880a525f 100644 --- a/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp +++ b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp @@ -66,7 +66,9 @@ TEST(AssumptionCheckerTest, Brp_no_bisimulation) { above.set(0); storm::storage::BitVector below(8); below.set(1); - auto dummyLattice = new storm::analysis::Lattice(above, below, 8); + storm::storage::BitVector initialMiddle(8); + + auto dummyLattice = new storm::analysis::Lattice(above, below, initialMiddle, 8); // Validate assumption EXPECT_FALSE(checker.validateAssumption(assumption, dummyLattice)); EXPECT_FALSE(checker.validated(assumption)); @@ -82,7 +84,8 @@ TEST(AssumptionCheckerTest, Brp_no_bisimulation) { above.set(12); below = storm::storage::BitVector(13); below.set(9); - dummyLattice = new storm::analysis::Lattice(above, below, 13); + initialMiddle = storm::storage::BitVector(13); + dummyLattice = new storm::analysis::Lattice(above, below, initialMiddle, 13); EXPECT_TRUE(checker.checkOnSamples(assumption)); EXPECT_TRUE(checker.validateAssumption(assumption, dummyLattice)); EXPECT_TRUE(checker.validated(assumption)); diff --git a/src/test/storm-pars/analysis/LatticeTest.cpp b/src/test/storm-pars/analysis/LatticeTest.cpp index 3b36a7ada..5fba6eac4 100644 --- a/src/test/storm-pars/analysis/LatticeTest.cpp +++ b/src/test/storm-pars/analysis/LatticeTest.cpp @@ -15,8 +15,9 @@ TEST(LatticeTest, Simple) { above.set(0); auto below = storm::storage::BitVector(numberOfStates); below.set(1); + auto initialMiddle = storm::storage::BitVector(numberOfStates); - auto lattice = storm::analysis::Lattice(above, below, numberOfStates); + auto lattice = storm::analysis::Lattice(above, below, initialMiddle, numberOfStates); EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(0,1)); EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(1,0)); EXPECT_EQ(nullptr, lattice.getNode(2)); @@ -80,8 +81,9 @@ TEST(LatticeTest, copy_lattice) { above.set(0); auto below = storm::storage::BitVector(numberOfStates); below.set(1); + auto initialMiddle = storm::storage::BitVector(numberOfStates); - auto lattice = storm::analysis::Lattice(above, below, numberOfStates); + auto lattice = storm::analysis::Lattice(above, below, initialMiddle, numberOfStates); lattice.add(2); lattice.add(3); lattice.addToNode(4, lattice.getNode(2)); diff --git a/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp index af9f6628f..12631b65a 100644 --- a/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp +++ b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp @@ -37,7 +37,8 @@ TEST(MonotonicityCheckerTest, Monotone_no_model) { above.set(1); auto below = storm::storage::BitVector(numberOfStates); below.set(0); - auto lattice = storm::analysis::Lattice(above, below, numberOfStates); + auto initialMiddle = storm::storage::BitVector(numberOfStates); + auto lattice = storm::analysis::Lattice(above, below, initialMiddle, numberOfStates); lattice.add(2); lattice.add(3); // Build map @@ -82,7 +83,8 @@ TEST(MonotonicityCheckerTest, Not_monotone_no_model) { above.set(1); auto below = storm::storage::BitVector(numberOfStates); below.set(0); - auto lattice = storm::analysis::Lattice(above, below, numberOfStates); + auto initialMiddle = storm::storage::BitVector(numberOfStates); + auto lattice = storm::analysis::Lattice(above, below, initialMiddle, numberOfStates); lattice.add(2); lattice.add(3); // Build map