From 34c87453fb9b63c317bfd11ff5550f55df0c9801 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Fri, 31 Aug 2018 11:24:45 +0200 Subject: [PATCH] Implement extension of lattice with assumptions --- src/storm-pars-cli/storm-pars.cpp | 13 ++++- src/storm-pars/analysis/Lattice.cpp | 21 ++++++-- src/storm-pars/analysis/Lattice.h | 10 ++++ src/storm-pars/analysis/LatticeExtender.cpp | 54 +++++++++++++++++---- src/storm-pars/analysis/LatticeExtender.h | 5 +- 5 files changed, 86 insertions(+), 17 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 5700e52e0..b14285761 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -513,6 +513,7 @@ namespace storm { color = "color = blue, "; } } + myfile << "\t" << i << " -> " << first.getColumn() << "[" << color << "label=\"" << first.getValue() << "\"];" << std::endl; myfile << "\t" << i << " -> " << second.getColumn() << "[" << color << "label=\"" << second.getValue() << "\"];" @@ -610,13 +611,21 @@ namespace storm { // Transform to Lattice storm::utility::Stopwatch latticeWatch(true); - storm::analysis::LatticeExtender> extender = storm::analysis::LatticeExtender>(sparseModel); storm::analysis::Lattice* lattice = extender.toLattice(formulas); + + // Declare variables for all states + std::shared_ptr expressionManager(new storm::expressions::ExpressionManager()); + for (uint_fast64_t i = 0; i < sparseModel.get()->getNumberOfStates(); ++i) { + expressionManager->declareFreshIntegerVariable(); + } +// std::set assumptions; +// extender.extendLattice(lattice, expressionManager, assumptions); latticeWatch.stop(); STORM_PRINT(std::endl << "Time for lattice creation: " << latticeWatch << "." << std::endl << std::endl); - ofstream myfile; + // Write lattice to file + ofstream myfile; myfile.open ("lattice.dot"); lattice->toDotFile(myfile); myfile.close(); diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index 6e04d82c2..67205c4fe 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -61,6 +61,11 @@ namespace storm { below->above.insert(between); } + void Lattice::addRelationNodes(storm::analysis::Lattice::Node *above, storm::analysis::Lattice::Node * below) { + above->below.insert(below); + below->above.insert(above); + } + int Lattice::compare(uint_fast64_t state1, uint_fast64_t state2) { Node *node1 = getNode(state1); Node *node2 = getNode(state2); @@ -68,25 +73,33 @@ namespace storm { // TODO: Wat als above(node1, node2) en above(node2, node1), dan moeten ze samengevoegd? if (node1 != nullptr && node2 != nullptr) { if (node1 == node2) { - return 0; + return SAME; } if (above(node1, node2)) { - return 1; + return ABOVE; } if (above(node2, node1)) { - return 2; + return BELOW; } } - return -1; + return UNKNOWN; } Lattice::Node *Lattice::getNode(uint_fast64_t stateNumber) { return nodes.at(stateNumber); } + Lattice::Node *Lattice::getTop() { + return top; + } + + Lattice::Node *Lattice::getBottom() { + return bottom; + } + storm::storage::BitVector Lattice::getAddedStates() { return addedStates; } diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h index a5644db48..57fc43e13 100644 --- a/src/storm-pars/analysis/Lattice.h +++ b/src/storm-pars/analysis/Lattice.h @@ -63,6 +63,8 @@ namespace storm { */ void addRelation(Node* above, Node* between, Node* below); + void addRelationNodes(storm::analysis::Lattice::Node *above, storm::analysis::Lattice::Node * below); + /*! * Compares the level of the nodes of the states. * Behaviour unknown when one or more of the states doesnot occur at any Node in the Lattice. @@ -85,6 +87,10 @@ namespace storm { */ Node *getNode(uint_fast64_t state); + Node* getTop(); + + Node* getBottom(); + storm::storage::BitVector getAddedStates(); /*! @@ -101,6 +107,10 @@ namespace storm { */ void toDotFile(std::ostream &out); + static const int UNKNOWN = -1; + static const int BELOW = 2; + static const int ABOVE = 1; + static const int SAME = 0; private: std::vector nodes; diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp index d252149e3..921e66d42 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -36,7 +36,7 @@ namespace storm { && ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula() || (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()), storm::exceptions::NotSupportedException, "Expecting until formula"); - uint_fast64_t numberOfStates = this->model.get()->getNumberOfStates(); + uint_fast64_t numberOfStates = this->model->getNumberOfStates(); storm::modelchecker::SparsePropositionalModelChecker propositionalChecker(*model); storm::storage::BitVector phiStates; @@ -50,7 +50,7 @@ namespace storm { } // Get the maybeStates - std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->model.get()->getBackwardTransitions(), phiStates, psiStates); + std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->model->getBackwardTransitions(), phiStates, psiStates); storm::storage::BitVector topStates = statesWithProbability01.second; storm::storage::BitVector bottomStates = statesWithProbability01.first; @@ -58,7 +58,7 @@ namespace storm { STORM_LOG_THROW(bottomStates.begin() != bottomStates.end(), storm::exceptions::NotImplementedException, "Formula yields to no zero states"); // Transform to Lattice - auto matrix = this->model.get()->getTransitionMatrix(); + auto matrix = this->model->getTransitionMatrix(); for (uint_fast64_t i = 0; i < numberOfStates; ++i) { stateMap[i] = storm::storage::BitVector(numberOfStates, false); @@ -73,18 +73,51 @@ namespace storm { // Create the Lattice storm::analysis::Lattice *lattice = new storm::analysis::Lattice(topStates, bottomStates, numberOfStates); - return this->extendLattice(lattice, std::set({})); + return this->extendLattice(lattice); } template - storm::analysis::Lattice* LatticeExtender::extendLattice(storm::analysis::Lattice* lattice, std::set assumptions) { - uint_fast64_t numberOfStates = this->model.get()->getNumberOfStates(); + storm::analysis::Lattice* LatticeExtender::extendLattice(storm::analysis::Lattice* lattice) { + std::shared_ptr expressionManager(new storm::expressions::ExpressionManager()); + std::set assumptions; + return this->extendLattice(lattice, expressionManager, assumptions); + } - storm::storage::BitVector oldStates(numberOfStates); + template + storm::analysis::Lattice* LatticeExtender::extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr expressionManager, std::set assumptions) { + // First handle assumptions + for (auto itr = assumptions.begin(); itr != assumptions.end(); ++itr) { + storm::expressions::BinaryRelationExpression expr = *(*itr); + STORM_LOG_THROW(expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater, storm::exceptions::NotImplementedException, "Only greater assumptions allowed"); + if (expr.getFirstOperand()->isVariable() && expr.getSecondOperand()->isVariable()) { + storm::expressions::Variable largest = expr.getFirstOperand()->asVariableExpression().getVariable(); + storm::expressions::Variable smallest = expr.getSecondOperand()->asVariableExpression().getVariable(); + + if (lattice->compare(largest.getOffset(), smallest.getOffset()) != storm::analysis::Lattice::ABOVE) { + storm::analysis::Lattice::Node* n1 = lattice->getNode(largest.getOffset()); + storm::analysis::Lattice::Node* n2 = lattice->getNode(smallest.getOffset()); + + if (n1 != nullptr && n2 != nullptr) { + lattice->addRelationNodes(n1, n2); + } else if (n1 != nullptr) { + lattice->addBetween(smallest.getOffset(), n1, lattice->getBottom()); + } else if (n2 != nullptr) { + lattice->addBetween(largest.getOffset(), lattice->getTop(), n2); + } else { + lattice->add(largest.getOffset()); + lattice->addBetween(smallest.getOffset(), lattice->getNode(largest.getOffset()), + lattice->getBottom()); + } + } + } + } // Create a copy of the states already present in the lattice. storm::storage::BitVector seenStates = (lattice->getAddedStates()); + auto numberOfStates = this->model->getNumberOfStates(); + storm::storage::BitVector oldStates(numberOfStates); + while (oldStates != seenStates) { // As long as new states are added to the lattice, continue. oldStates = storm::storage::BitVector(seenStates); @@ -110,15 +143,15 @@ namespace storm { uint_fast64_t successor1 = successors.getNextSetIndex(0); uint_fast64_t successor2 = successors.getNextSetIndex(successor1 + 1); int compareResult = lattice->compare(successor1, successor2); - if (compareResult == 1) { + if (compareResult == storm::analysis::Lattice::ABOVE) { // successor 1 is closer to top than successor 2 lattice->addBetween(stateNumber, lattice->getNode(successor1), lattice->getNode(successor2)); - } else if (compareResult == 2) { + } else if (compareResult == storm::analysis::Lattice::BELOW) { // successor 2 is closer to top than successor 1 lattice->addBetween(stateNumber, lattice->getNode(successor2), lattice->getNode(successor1)); - } else if (compareResult == 0) { + } else if (compareResult == storm::analysis::Lattice::SAME) { // the successors are at the same level lattice->addToNode(stateNumber, lattice->getNode(successor1)); } else { @@ -128,6 +161,7 @@ namespace storm { } } } + // TODO allow returning critical pair return lattice; } diff --git a/src/storm-pars/analysis/LatticeExtender.h b/src/storm-pars/analysis/LatticeExtender.h index e52a3417d..37c39dc2a 100644 --- a/src/storm-pars/analysis/LatticeExtender.h +++ b/src/storm-pars/analysis/LatticeExtender.h @@ -25,12 +25,15 @@ namespace storm { storm::analysis::Lattice* toLattice(std::vector> formulas); - storm::analysis::Lattice* extendLattice(storm::analysis::Lattice* lattice, std::set assumptions); + storm::analysis::Lattice* extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr expressionManager, std::set assumptions); private: std::shared_ptr model; std::map stateMap; + + storm::analysis::Lattice* extendLattice(storm::analysis::Lattice* lattice); + }; } }