Return tuple and add assumptions

src/storm-pars-cli/storm-pars.cpp

@@ -612,15 +612,27 @@ namespace storm {
                 // Transform to Lattice
                 storm::utility::Stopwatch latticeWatch(true);
                 storm::analysis::LatticeExtender<storm::models::sparse::Model<ValueType>> extender = storm::analysis::LatticeExtender<storm::models::sparse::Model<ValueType>>(sparseModel);
-                storm::analysis::Lattice* lattice = extender.toLattice(formulas);
+                std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> criticalPair = extender.toLattice(formulas);
 
                 // Declare variables for all states
                 std::shared_ptr<storm::expressions::ExpressionManager> expressionManager(new storm::expressions::ExpressionManager());
-                for (uint_fast64_t i = 0; i < sparseModel.get()->getNumberOfStates(); ++i) {
+                for (uint_fast64_t i = 0; i < sparseModel->getNumberOfStates(); ++i) {
                     expressionManager->declareFreshIntegerVariable();
                 }
-//                std::set<storm::expressions::BinaryRelationExpression*> assumptions;
-//                extender.extendLattice(lattice, expressionManager, assumptions);
+
+                // Make assumptions
+                std::set<storm::expressions::BinaryRelationExpression*> assumptions;
+                while (std::get<1>(criticalPair) != sparseModel->getNumberOfStates()) {
+                    storm::expressions::Variable var1 = expressionManager->getVariable("_x" + std::to_string(std::get<1>(criticalPair)));
+                    storm::expressions::Variable var2 = expressionManager->getVariable("_x" + std::to_string(std::get<2>(criticalPair)));
+                    auto assumption = new storm::expressions::BinaryRelationExpression(*expressionManager, var1.getType(),
+                            var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
+                            storm::expressions::BinaryRelationExpression::RelationType::Greater);
+                    assumptions.insert(assumption);
+                    criticalPair = extender.extendLattice(std::get<0>(criticalPair), expressionManager, assumptions);
+                }
+                auto lattice = std::get<0>(criticalPair);
+
                 latticeWatch.stop();
                 STORM_PRINT(std::endl << "Time for lattice creation: " << latticeWatch << "." << std::endl << std::endl);
 
@@ -631,7 +643,7 @@ namespace storm {
                 myfile.close();
 
                 // Monotonicity?
-                auto matrix = sparseModel.get()->getTransitionMatrix();
+                auto matrix = sparseModel->getTransitionMatrix();
                 storm::utility::Stopwatch monotonicityWatch(true);
                 std::map<carl::Variable, std::pair<bool, bool>> varsMonotone = analyseMonotonicity<ValueType>(lattice, matrix);
                 monotonicityWatch.stop();

src/storm-pars/analysis/Lattice.h

@@ -11,9 +11,6 @@
 
 #include "storm/storage/BitVector.h"
 
-
-
-
 namespace storm {
             namespace analysis {
                 class Lattice {

src/storm-pars/analysis/LatticeExtender.cpp

@@ -30,7 +30,7 @@ namespace storm {
         }
 
         template <typename SparseModelType>
-        storm::analysis::Lattice* LatticeExtender<SparseModelType>::toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas) {
+        std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<SparseModelType>::toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas) {
             STORM_LOG_THROW((++formulas.begin()) == formulas.end(), storm::exceptions::NotSupportedException, "Only one formula allowed for monotonicity analysis");
             STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula()
                             && ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula()
@@ -77,14 +77,15 @@ namespace storm {
         }
 
         template <typename SparseModelType>
-        storm::analysis::Lattice* LatticeExtender<SparseModelType>::extendLattice(storm::analysis::Lattice* lattice) {
+        std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<SparseModelType>::extendLattice(storm::analysis::Lattice* lattice) {
             std::shared_ptr<storm::expressions::ExpressionManager> expressionManager(new storm::expressions::ExpressionManager());
             std::set<storm::expressions::BinaryRelationExpression*> assumptions;
             return this->extendLattice(lattice, expressionManager, assumptions);
         }
 
         template <typename SparseModelType>
-        storm::analysis::Lattice* LatticeExtender<SparseModelType>::extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::ExpressionManager> expressionManager, std::set<storm::expressions::BinaryRelationExpression*> assumptions) {
+        std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<SparseModelType>::extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::ExpressionManager> expressionManager, std::set<storm::expressions::BinaryRelationExpression*> assumptions) {
+            auto numberOfStates = this->model->getNumberOfStates();
             // First handle assumptions
             for (auto itr = assumptions.begin(); itr != assumptions.end(); ++itr) {
                 storm::expressions::BinaryRelationExpression expr = *(*itr);
@@ -114,8 +115,6 @@ namespace storm {
 
             // 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) {
@@ -155,17 +154,15 @@ namespace storm {
                             // the successors are at the same level
                             lattice->addToNode(stateNumber, lattice->getNode(successor1));
                         } else {
-                            // TODO: create critical pair
+                            return std::make_tuple(lattice, successor1, successor2);
                         }
                         seenStates.set(stateNumber);
                     }
                 }
             }
-            // TODO allow returning critical pair
-            return lattice;
+            return std::make_tuple(lattice, numberOfStates, numberOfStates);
         }
 
         template class LatticeExtender<storm::models::sparse::Model<storm::RationalFunction>>;
-//        template class LatticeExtender<storm::models::sparse::Mdp<storm::RationalFunction>>;
     }
 }

src/storm-pars/analysis/LatticeExtender.h

@@ -23,16 +23,16 @@ namespace storm {
         public:
             LatticeExtender(std::shared_ptr<SparseModelType> model);
 
-            storm::analysis::Lattice* toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas);
+            std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas);
 
-            storm::analysis::Lattice* extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::ExpressionManager> expressionManager, std::set<storm::expressions::BinaryRelationExpression*> assumptions);
+            std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::ExpressionManager> expressionManager, std::set<storm::expressions::BinaryRelationExpression*> assumptions);
 
         private:
             std::shared_ptr<SparseModelType> model;
 
             std::map<uint_fast64_t, storm::storage::BitVector> stateMap;
 
-            storm::analysis::Lattice* extendLattice(storm::analysis::Lattice* lattice);
+            std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> extendLattice(storm::analysis::Lattice* lattice);
 
         };
     }