Check assumptions on a region

src/storm-pars/analysis/MonotonicityChecker.cpp

@@ -15,14 +15,20 @@
 #include "storm/utility/Stopwatch.h"
 #include "storm/models/ModelType.h"
 
+#include "storm/api/verification.h"
+#include "storm-pars/api/storm-pars.h"
+
 #include "storm/modelchecker/results/CheckResult.h"
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h"
+
 #include "storm/solver/Z3SmtSolver.h"
 #include "storm/storage/expressions/ExpressionManager.h"
 
 #include "storm/storage/expressions/RationalFunctionToExpression.h"
 
 
+
 namespace storm {
     namespace analysis {
         template <typename ValueType>
@@ -51,6 +57,73 @@ namespace storm {
             return checkMonotonicity(map, matrix);
         }
 
+        template <typename ValueType>
+        std::vector<storm::storage::ParameterRegion<ValueType>> MonotonicityChecker<ValueType>::checkAssumptionsOnRegion(std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions) {
+            assert (formulas[0]->isProbabilityOperatorFormula());
+            assert (formulas[0]->asProbabilityOperatorFormula().getSubformula().isUntilFormula() || formulas[0]->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula());
+            Environment env = Environment();
+            std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
+            bool generateSplitEstimates = false;
+            bool allowModelSimplification = false;
+            auto task = storm::api::createTask<ValueType>(formulas[0], true);
+            // TODO: storm::RationalNumber or double?
+
+            // TODO: Also allow different models
+            STORM_LOG_THROW (sparseModel->isOfType(storm::models::ModelType::Dtmc), storm::exceptions::NotImplementedException,
+                             "Checking assumptions on a region not implemented for this type of model");
+            auto modelChecker = storm::api::initializeParameterLiftingDtmcModelChecker<ValueType, storm::RationalNumber>(env, sparseModel, task, generateSplitEstimates, allowModelSimplification);
+
+            std::stack<std::pair<storm::storage::ParameterRegion<ValueType>, int>> regions;
+            std::vector<storm::storage::ParameterRegion<ValueType>> satRegions;
+            std::string regionText = "";
+            auto parameters = storm::models::sparse::getProbabilityParameters(*sparseModel);
+            for (auto itr = parameters.begin(); itr != parameters.end(); ++itr) {
+                if (regionText != "") {
+                    regionText += ",";
+                }
+                // TODO: region bounds
+                regionText += "0.1 <= " + itr->name() + " <= 0.9";
+            }
+
+            auto initialRegion = storm::api::parseRegion<ValueType>(regionText, parameters);
+            regions.push(std::pair<storm::storage::ParameterRegion<ValueType>, int>(initialRegion,0));
+            while (!regions.empty()) {
+                auto lastElement = regions.top();
+                regions.pop();
+                storm::storage::ParameterRegion<ValueType> currentRegion = lastElement.first;
+
+                // TODO: depth
+                if (lastElement.second < 5) {
+                    auto upperBound = modelChecker->getBound(env, currentRegion, storm::solver::OptimizationDirection::Maximize);
+                    auto lowerBound = modelChecker->getBound(env, currentRegion, storm::solver::OptimizationDirection::Minimize);
+                    std::vector<storm::RationalNumber> valuesUpper = upperBound->template asExplicitQuantitativeCheckResult<storm::RationalNumber>().getValueVector();
+                    std::vector<storm::RationalNumber> valuesLower = lowerBound->template asExplicitQuantitativeCheckResult<storm::RationalNumber>().getValueVector();
+                    bool assumptionsHold = true;
+                    for (auto itr = assumptions.begin(); assumptionsHold && itr != assumptions.end(); ++itr) {
+                        auto assumption = *itr;
+                        assert (assumption->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual);
+                        auto state1 = std::stoi(assumption->getFirstOperand()->asVariableExpression().getVariableName());
+                        auto state2 = std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName());
+                        assumptionsHold &= valuesLower[state1] >= valuesUpper[state2];
+                    }
+                    if (!assumptionsHold) {
+                        std::vector<storm::storage::ParameterRegion<ValueType>> newRegions;
+                        currentRegion.split(currentRegion.getCenterPoint(), newRegions);
+                        for (auto itr = newRegions.begin(); itr != newRegions.end(); ++itr) {
+                            regions.push(std::pair<storm::storage::ParameterRegion<ValueType>, int>(*itr,
+                                                                                                    lastElement.second +
+                                                                                                    1));
+                        }
+                    } else {
+                        satRegions.push_back(currentRegion);
+                    }
+                }
+            }
+            return satRegions;
+        }
+
+
+
         template <typename ValueType>
         std::map<storm::analysis::Lattice*, std::map<carl::Variable, std::pair<bool, bool>>> MonotonicityChecker<ValueType>::checkMonotonicity(std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix) {
             storm::utility::Stopwatch finalCheckWatch(true);
@@ -74,35 +147,36 @@ namespace storm {
 
                     outfile.open(filename, std::ios_base::app);
                     auto assumptions = itr->second;
+                    bool validSomewhere = true;
                     if (assumptions.size() > 0) {
-                        STORM_PRINT("Given assumptions: " << std::endl);
+                        auto regions = checkAssumptionsOnRegion(assumptions);
+                        if (regions.size() > 0) {
+                            STORM_PRINT("For regions: " << std::endl);
+                        }
                         bool first = true;
-                        for (auto itr2 = assumptions.begin(); itr2 != assumptions.end(); ++itr2) {
-                            if (!first) {
-                                STORM_PRINT(" ^ ");
-                                outfile << (" ^ ");
-                            } else {
+                        for (auto itr2 = regions.begin(); itr2 != regions.end(); ++itr2) {
+                            if (first) {
                                 STORM_PRINT("    ");
                                 first = false;
                             }
-
-                            std::shared_ptr<storm::expressions::BinaryRelationExpression> expression = *itr2;
-                            auto var1 = expression->getFirstOperand();
-                            auto var2 = expression->getSecondOperand();
-                            STORM_PRINT(*expression);
-                            outfile << (*expression);
+                            STORM_PRINT(*itr2);
+                            outfile << (*itr2);
                         }
-                        STORM_PRINT(std::endl);
-                        outfile << ", ";
-                    } else {
+                        if (regions.size() > 0) {
+                            STORM_PRINT(std::endl);
+                            outfile << ", ";
+                        }
+                    }
+
+                    if (validSomewhere && assumptions.size() == 0) {
                         outfile << "No assumptions, ";
                     }
 
 
-                    if (varsMonotone.size() == 0) {
+                    if (validSomewhere && varsMonotone.size() == 0) {
                         STORM_PRINT("Result is constant" << std::endl);
                         outfile << "No params";
-                    } else {
+                    } else if (validSomewhere) {
                         auto itr2 = varsMonotone.begin();
                         while (itr2 != varsMonotone.end()) {
                             if (resultCheckOnSamples.find(itr2->first) != resultCheckOnSamples.end() &&
@@ -121,6 +195,7 @@ namespace storm {
                                     STORM_PRINT("  - Monotone decreasing in: " << itr2->first << std::endl);
                                     outfile << "D " << itr2->first;
                                 } else {
+
                                     STORM_PRINT(
                                             "  - Do not know if monotone incr/decreasing in: " << itr2->first << std::endl);
                                     outfile << "? " << itr2->first;

src/storm-pars/analysis/MonotonicityChecker.h

@@ -17,6 +17,7 @@
 #include "storm/models/sparse/Mdp.h"
 #include "storm/logic/Formula.h"
 #include "storm/storage/SparseMatrix.h"
+#include "storm-pars/api/region.h"
 
 namespace storm {
     namespace analysis {
@@ -61,6 +62,8 @@ namespace storm {
 
             std::pair<bool, bool> checkDerivative(ValueType derivative);
 
+            std::vector<storm::storage::ParameterRegion<ValueType>> checkAssumptionsOnRegion(std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions);
+
             std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> extendLatticeWithAssumptions(storm::analysis::Lattice* lattice, storm::analysis::AssumptionMaker<ValueType>* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions);
 
             std::shared_ptr<storm::models::ModelBase> model;

src/storm-pars/api/region.h

@@ -79,14 +79,14 @@ namespace storm {
             STORM_LOG_THROW(res.size() == 1, storm::exceptions::InvalidOperationException, "Parsed " << res.size() << " regions but exactly one was expected.");
             return res.front();
         }
-        
+
         template <typename ParametricType, typename ConstantType>
         std::shared_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeParameterLiftingRegionModelChecker(Environment const& env, std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task, bool generateSplitEstimates = false, bool allowModelSimplification = true) {
-            
+
             STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually...");
 
             std::shared_ptr<storm::models::sparse::Model<ParametricType>> consideredModel = model;
-            
+
             // Treat continuous time models
             if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) {
                     STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model...");
@@ -94,7 +94,7 @@ namespace storm {
                     consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector);
                     STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed.");
             }
-            
+
             // Obtain the region model checker
             std::shared_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> checker;
             if (consideredModel->isOfType(storm::models::ModelType::Dtmc)) {
@@ -104,11 +104,41 @@ namespace storm {
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type.");
             }
-            
+
             checker->specify(env, consideredModel, task, generateSplitEstimates, allowModelSimplification);
-            
+
             return checker;
         }
+
+        // TODO: make more generic
+        template <typename ParametricType, typename ConstantType>
+        std::shared_ptr<storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ParametricType>, ConstantType>> initializeParameterLiftingDtmcModelChecker(Environment const& env, std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task, bool generateSplitEstimates = false, bool allowModelSimplification = true) {
+
+            STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually...");
+
+            std::shared_ptr<storm::models::sparse::Model<ParametricType>> consideredModel = model;
+
+            // Treat continuous time models
+            if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) {
+                STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model...");
+                std::vector<std::shared_ptr<storm::logic::Formula const>> taskFormulaAsVector { task.getFormula().asSharedPointer() };
+                consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector);
+                STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed.");
+            }
+
+            // Obtain the region model checker
+            std::shared_ptr<storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ParametricType>, ConstantType>> checker;
+            if (consideredModel->isOfType(storm::models::ModelType::Dtmc)) {
+                checker = std::make_shared<storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ParametricType>, ConstantType>>();
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type.");
+            }
+
+            checker->specify(env, consideredModel, task, generateSplitEstimates, allowModelSimplification);
+
+            return checker;
+        }
+
         
         template <typename ParametricType, typename ImpreciseType, typename PreciseType>
         std::shared_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeValidatingRegionModelChecker(Environment const& env, std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task, bool generateSplitEstimates = false, bool allowModelSimplification = true) {