AssumptionChecker for mdp

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

@@ -543,14 +543,21 @@ 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
+                std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
+                if (model->isOfType(storm::models::ModelType::Dtmc)) {
                     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(), parSettings.isValidateAssumptionsSet());
+                    result = assumptionMaker.makeAssumptions(std::get<0>(criticalPair), std::get<1>(criticalPair), std::get<2>(criticalPair));
+                } else if (model->isOfType(storm::models::ModelType::Dtmc)) {
+                    auto mdpModel = model->as<storm::models::sparse::Mdp<ValueType>>();
+                    auto assumptionChecker = storm::analysis::AssumptionChecker<ValueType>(formulas[0], mdpModel, 3);
+                    auto assumptionMaker = storm::analysis::AssumptionMaker<ValueType>(extender, &assumptionChecker, sparseModel->getNumberOfStates(), parSettings.isValidateAssumptionsSet());
+                    result = assumptionMaker.makeAssumptions(std::get<0>(criticalPair), std::get<1>(criticalPair), std::get<2>(criticalPair));
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform monotonicity analysis on the provided model type.");
+                }
 
-                std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result = assumptionMaker.makeAssumptions(
-                        std::get<0>(criticalPair), std::get<1>(criticalPair), std::get<2>(criticalPair));
 
                 latticeWatch.stop();
                 STORM_PRINT(std::endl << "Time for lattice creation: " << latticeWatch << "." << std::endl << std::endl);

src/storm-pars/analysis/AssumptionChecker.cpp

@@ -9,6 +9,7 @@
 #include "storm/exceptions/NotSupportedException.h"
 #include "storm/modelchecker/CheckTask.h"
 #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
 #include "storm/modelchecker/results/CheckResult.h"
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "storm/storage/expressions/SimpleValuation.h"
@@ -56,6 +57,45 @@ namespace storm {
             }
         }
 
+        template <typename ValueType>
+        AssumptionChecker<ValueType>::AssumptionChecker(std::shared_ptr<storm::logic::Formula const> formula, std::shared_ptr<storm::models::sparse::Mdp<ValueType>> model, uint_fast64_t numberOfSamples) {
+            this->formula = formula;
+            this->matrix = model->getTransitionMatrix();
+
+            // Create sample points
+            auto instantiator = storm::utility::ModelInstantiator<storm::models::sparse::Mdp<ValueType>, storm::models::sparse::Mdp<double>>(*model);
+            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) {
+                    // TODO: Type
+                    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::Mdp<double> sampleModel = instantiator.instantiate(valuation);
+                auto checker = storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<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);
+            }
+        }
+
         template <typename ValueType>
         bool AssumptionChecker<ValueType>::checkOnSamples(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
             bool result = true;

src/storm-pars/analysis/AssumptionChecker.h

@@ -7,6 +7,7 @@
 
 #include "storm/logic/Formula.h"
 #include "storm/models/sparse/Dtmc.h"
+#include "storm/models/sparse/Mdp.h"
 #include "storm/environment/Environment.h"
 #include "storm/storage/expressions/BinaryRelationExpression.h"
 #include "Lattice.h"
@@ -20,11 +21,20 @@ namespace storm {
              * Constructs an AssumptionChecker based on the number of samples, for the given formula and model.
              *
              * @param formula The formula to check.
-             * @param model The model to check the formula on.
+             * @param model The dtmc model to check the formula on.
              * @param numberOfSamples Number of sample points.
              */
             AssumptionChecker(std::shared_ptr<storm::logic::Formula const> formula, std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples);
 
+            /*!
+             * Constructs an AssumptionChecker based on the number of samples, for the given formula and model.
+             *
+             * @param formula The formula to check.
+             * @param model The mdp model to check the formula on.
+             * @param numberOfSamples Number of sample points.
+             */
+            AssumptionChecker(std::shared_ptr<storm::logic::Formula const> formula, std::shared_ptr<storm::models::sparse::Mdp<ValueType>> model, uint_fast64_t numberOfSamples);
+
             /*!
              * Checks if the assumption holds at the sample points of the AssumptionChecker.
              *