WIP: Check assumptions on samples

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

@@ -543,6 +543,12 @@ namespace storm {
                 storm::utility::Stopwatch latticeWatch(true);
                 storm::analysis::LatticeExtender<ValueType> *extender = new storm::analysis::LatticeExtender<ValueType>(sparseModel);
                 std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> criticalPair = extender->toLattice(formulas);
+                // TODO check not mdp
+                auto dtmcModel = model->as<storm::models::sparse::Dtmc<ValueType>>();
+                // TODO check formula type
+                auto assumptionChecker = storm::analysis::AssumptionChecker<ValueType>(formulas[0], dtmcModel, 3);
+                auto assumptionMaker = storm::analysis::AssumptionMaker<ValueType>(extender, &assumptionChecker, sparseModel->getNumberOfStates());
+
                 std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result = assumptionMaker.startMakingAssumptions(std::get<0>(criticalPair), std::get<1>(criticalPair), std::get<2>(criticalPair));
 
 

src/storm-pars/analysis/AssumptionChecker.cpp

@@ -0,0 +1,72 @@
+//
+// Created by Jip Spel on 12.09.18.
+//
+
+#include <storm-pars/utility/ModelInstantiator.h>
+#include <storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h>
+#include <storm/exceptions/NotSupportedException.h>
+#include "AssumptionChecker.h"
+#include "storm/modelchecker/CheckTask.h"
+#include "storm/environment/Environment.h"
+#include "storm/modelchecker/results/CheckResult.h"
+#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+
+
+
+
+namespace storm {
+    namespace analysis {
+        template <typename ValueType>
+        AssumptionChecker<ValueType>::AssumptionChecker(std::shared_ptr<storm::logic::Formula const> formula, std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples) {
+            this->formula = formula;
+
+            auto instantiator = storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<ValueType>, storm::models::sparse::Dtmc<double>>(*model.get());
+            auto matrix = model->getTransitionMatrix();
+            std::set<storm::RationalFunctionVariable> variables =  storm::models::sparse::getProbabilityParameters(*model);
+
+
+            for (auto i = 0; i < numberOfSamples; ++i) {
+                auto valuation = storm::utility::parametric::Valuation<ValueType>();
+                for (auto itr = variables.begin(); itr != variables.end(); ++itr) {
+                    auto val = std::pair<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient>((*itr), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(boost::lexical_cast<std::string>((i+1)/(double (numberOfSamples + 1)))));
+                    valuation.insert(val);
+                }
+                storm::models::sparse::Dtmc<double> sampleModel = instantiator.instantiate(valuation);
+                auto checker = storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>>(sampleModel);
+                std::unique_ptr<storm::modelchecker::CheckResult> checkResult;
+                if (formula->isProbabilityOperatorFormula() &&
+                    formula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) {
+                    const storm::modelchecker::CheckTask<storm::logic::UntilFormula, double> checkTask = storm::modelchecker::CheckTask<storm::logic::UntilFormula, double>(
+                            (*formula).asProbabilityOperatorFormula().getSubformula().asUntilFormula());
+                    checkResult = checker.computeUntilProbabilities(Environment(), checkTask);
+                } else if (formula->isProbabilityOperatorFormula() &&
+                           formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()) {
+                    const storm::modelchecker::CheckTask<storm::logic::EventuallyFormula, double> checkTask = storm::modelchecker::CheckTask<storm::logic::EventuallyFormula, double>(
+                            (*formula).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula());
+                    checkResult = checker.computeReachabilityProbabilities(Environment(), checkTask);
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
+                                    "Expecting until or eventually formula");
+                }
+                auto quantitativeResult = checkResult->asExplicitQuantitativeCheckResult<double>();
+                std::vector<double> values = quantitativeResult.getValueVector();
+                results.push_back(values);
+            }
+            this->numberOfStates = model->getNumberOfStates();
+            this->initialStates = model->getInitialStates();
+        }
+
+        template <typename ValueType>
+        bool AssumptionChecker<ValueType>::checkOnSamples(uint_fast64_t val1, uint_fast64_t val2) {
+            bool result = true;
+            for (auto itr = results.begin(); result && itr != results.end(); ++itr) {
+                // TODO: als expressie
+                auto values = (*itr);
+                result &= (values[val1] >= values[val2]);
+            }
+            return result;
+        }
+
+        template class AssumptionChecker<storm::RationalFunction>;
+    }
+}

src/storm-pars/analysis/AssumptionChecker.h

@@ -0,0 +1,35 @@
+//
+// Created by Jip Spel on 12.09.18.
+//
+
+#ifndef STORM_ASSUMPTIONCHECKER_H
+#define STORM_ASSUMPTIONCHECKER_H
+
+#include <storm/logic/Formula.h>
+#include <storm/models/sparse/Dtmc.h>
+#include "storm/environment/Environment.h"
+
+namespace storm {
+    namespace analysis {
+        template<typename ValueType>
+        class AssumptionChecker {
+        public:
+            AssumptionChecker(std::shared_ptr<storm::logic::Formula const> formula, std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples);
+
+            bool checkOnSamples(uint_fast64_t val1, uint_fast64_t val2);
+        private:
+            std::shared_ptr<storm::logic::Formula const> formula;
+
+            std::vector<storm::models::sparse::Dtmc<double>> sampleModels;
+
+            std::vector<std::vector<double>> results;
+
+            uint_fast64_t numberOfStates;
+
+            storm::storage::BitVector initialStates;
+        };
+    }
+}
+
+
+#endif //STORM_ASSUMPTIONCHECKER_H

src/storm-pars/analysis/AssumptionMaker.cpp

@@ -7,9 +7,10 @@
 namespace storm {
     namespace analysis {
         template<typename ValueType>
-        AssumptionMaker<ValueType>::AssumptionMaker(storm::analysis::LatticeExtender<ValueType>* latticeExtender, uint_fast64_t numberOfStates) {
+        AssumptionMaker<ValueType>::AssumptionMaker(storm::analysis::LatticeExtender<ValueType>* latticeExtender, storm::analysis::AssumptionChecker<ValueType>* assumptionChecker, uint_fast64_t numberOfStates) {
             this->latticeExtender = latticeExtender;
             this->numberOfStates = numberOfStates;
+            this->assumptionChecker = assumptionChecker;
             this->expressionManager = std::make_shared<storm::expressions::ExpressionManager>(storm::expressions::ExpressionManager());
             for (uint_fast64_t i = 0; i < this->numberOfStates; ++i) {
                 expressionManager->declareIntegerVariable(std::to_string(i));
@@ -27,15 +28,20 @@ namespace storm {
             } else {
                 storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(critical1));
                 storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(critical2));
-                std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions;
 
-                auto latticeCopy = new Lattice(lattice);
-                std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptionsCopy = std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(assumptions);
-                auto myMap = createAssumptions(var1, var2, latticeCopy, assumptionsCopy);
-                result.insert(myMap.begin(), myMap.end());
-
-                myMap = createAssumptions(var2, var1, lattice, assumptions);
-                result.insert(myMap.begin(), myMap.end());
+                if (assumptionChecker->checkOnSamples(critical1, critical2)) {
+                    auto latticeCopy = new Lattice(lattice);
+                    std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions;
+                    auto myMap = createAssumptions(var1, var2, latticeCopy, assumptions);
+                    result.insert(myMap.begin(), myMap.end());
+                }
+                if (assumptionChecker->checkOnSamples(critical2, critical1)) {
+                    std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions;
+                    auto myMap = createAssumptions(var2, var1, lattice, assumptions);
+                    result.insert(myMap.begin(), myMap.end());
+                } else {
+                    delete lattice;
+                }
             }
             return result;
         }
@@ -43,22 +49,30 @@ namespace storm {
         template<typename ValueType>
         std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> AssumptionMaker<ValueType>::runRecursive(storm::analysis::Lattice* lattice, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions) {
             std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
-            std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> criticalPair = this->latticeExtender->extendLattice(lattice, assumptions);
+            std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> criticalTriple = this->latticeExtender->extendLattice(lattice, assumptions);
 
-            if (std::get<1>(criticalPair) == numberOfStates) {
+            if (std::get<1>(criticalTriple) == numberOfStates) {
                 result.insert(std::pair<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(lattice, assumptions));
             } else {
-                storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(std::get<1>(criticalPair)));
-                storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(std::get<2>(criticalPair)));
+                auto val1 = std::get<1>(criticalTriple);
+                auto val2 = std::get<2>(criticalTriple);
+                storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(val1));
+                storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(val2));
 
-                auto latticeCopy = new Lattice(lattice);
-                std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptionsCopy = std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(assumptions);
-                auto myMap = createAssumptions(var1, var2, latticeCopy, assumptionsCopy);
-                result.insert(myMap.begin(), myMap.end());
-                myMap = createAssumptions(var2, var1, lattice, assumptions);
-                result.insert(myMap.begin(), myMap.end());
-            }
+                if (assumptionChecker->checkOnSamples(val1, val2)) {
+                    auto latticeCopy = new Lattice(lattice);
+                    std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptionsCopy = std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(assumptions);
+                    auto myMap = createAssumptions(var1, var2, latticeCopy, assumptionsCopy);
+                    result.insert(myMap.begin(), myMap.end());
+                }
 
+                if (assumptionChecker->checkOnSamples(val2, val1)) {
+                    auto myMap = createAssumptions(var2, var1, lattice, assumptions);
+                    result.insert(myMap.begin(), myMap.end());
+                } else {
+                    delete lattice;
+                }
+            }
             return result;
         }
 
@@ -67,11 +81,13 @@ namespace storm {
             std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption1
                 = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, var1.getType(),
                         var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
-                        storm::expressions::BinaryRelationExpression::RelationType::Greater));
+                        storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual));
             assumptions.insert(assumption1);
             return (runRecursive(lattice, assumptions));
         }
 
+
+
         template class AssumptionMaker<storm::RationalFunction>;
     }
 }

src/storm-pars/analysis/AssumptionMaker.h

@@ -6,8 +6,11 @@
 #define STORM_ASSUMPTIONMAKER_H
 
 #include "Lattice.h"
+#include "AssumptionChecker.h"
 #include "storm/storage/expressions/BinaryRelationExpression.h"
 #include "LatticeExtender.h"
+#include "storm-pars/utility/ModelInstantiator.h"
+
 
 namespace storm {
     namespace analysis {
@@ -15,7 +18,7 @@ namespace storm {
         template<typename ValueType>
         class AssumptionMaker {
         public:
-            AssumptionMaker(storm::analysis::LatticeExtender<ValueType>* latticeExtender, uint_fast64_t numberOfStates);
+            AssumptionMaker(storm::analysis::LatticeExtender<ValueType>* latticeExtender, storm::analysis::AssumptionChecker<ValueType>* checker, uint_fast64_t numberOfStates);
 
             std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> startMakingAssumptions(storm::analysis::Lattice* lattice, uint_fast64_t critical1, uint_fast64_t critical2);
 
@@ -29,6 +32,8 @@ namespace storm {
             std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
 
             uint_fast64_t numberOfStates;
+
+            storm::analysis::AssumptionChecker<ValueType>* assumptionChecker;
         };
     }
 }

src/storm-pars/analysis/LatticeExtender.cpp

@@ -34,7 +34,7 @@ namespace storm {
             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()
-                                || (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()), storm::exceptions::NotSupportedException, "Expecting until formula");
+                                || (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()), storm::exceptions::NotSupportedException, "Expecting until or eventually formula");
 
             uint_fast64_t numberOfStates = this->model->getNumberOfStates();
 
@@ -86,7 +86,7 @@ namespace storm {
             // 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");
+                STORM_LOG_THROW(expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual, 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();

src/storm-pars/analysis/MonotonicityChecker.cpp

@@ -156,6 +156,4 @@ namespace storm {
         };
         template class MonotonicityChecker<storm::RationalFunction>;
     }
-
 }
-