DeterministicSchedsObjectiveHelper: Compute tighter lower/upper bounds.

src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp

@@ -9,10 +9,10 @@ namespace storm {
         namespace multiobjective {
             
             template <typename ModelType, typename GeometryValueType>
-            DeterministicSchedsLpChecker<ModelType, GeometryValueType>::DeterministicSchedsLpChecker(ModelType const& model, std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives) : model(model) {
+            DeterministicSchedsLpChecker<ModelType, GeometryValueType>::DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives) : model(model) {
                 swInit.start();
                 initializeObjectiveHelper(objectives);
-                initializeLpModel();
+                initializeLpModel(env);
                 swInit.stop();
             }
             
@@ -22,8 +22,8 @@ namespace storm {
                 std::cout << "\t" << swInit << " seconds for initialization" << std::endl;
                 std::cout << "\t" << swCheck << " seconds for checking, including" << std::endl;
                 std::cout << "\t\t" << swLpBuild << " seconds for LP building" << std::endl;
-                std::cout << "\t\t" << swLpSolve << " seconds for LP solving" << std::endl;
-                std::cout << "\t\t" << swCheckVertices << " seconds for checking the vertices of the convex hull." << std::endl;
+                std::cout << "\t\t" << swLpSolve << " seconds for LP solving, including" << std::endl;
+                std::cout << "\t\t\t" << swCheckVertices << " seconds for finding the vertices of the convex hull." << std::endl;
                 std::cout << "\t" << swAux << " seconds for aux stuff" << std::endl;
             }
             
@@ -53,9 +53,10 @@ namespace storm {
             std::vector<GeometryValueType> DeterministicSchedsLpChecker<ModelType, GeometryValueType>::check(storm::Environment const& env) {
                 STORM_LOG_ASSERT(!currentWeightVector.empty(), "Checking invoked before specifying a weight vector.");
                 STORM_LOG_TRACE("Checking a vertex...");
-                swCheck.start(); swCheckVertices.start(); swLpSolve.start();
+                swCheck.start(); swLpSolve.start(); swCheckVertices.start();
                 lpModel->optimize();
-                swLpSolve.stop();
+                swCheckVertices.stop(); swLpSolve.stop();
+                STORM_LOG_TRACE("\t Done checking a vertex...");
                 STORM_LOG_ASSERT(!lpModel->isInfeasible(), "LP result is infeasable.");
                 STORM_LOG_ASSERT(!lpModel->isUnbounded(), "LP result is unbounded.");
                 
@@ -64,7 +65,7 @@ namespace storm {
                     newPoint.push_back(storm::utility::convertNumber<GeometryValueType>(lpModel->getContinuousValue(objVar)));
                 }
                 
-                swCheckVertices.stop(); swCheck.stop();
+                swCheck.stop();
                 return newPoint;
             }
 
@@ -95,7 +96,7 @@ namespace storm {
             }
             
             template <typename ModelType, typename GeometryValueType>
-            void DeterministicSchedsLpChecker<ModelType, GeometryValueType>::initializeLpModel() {
+            void DeterministicSchedsLpChecker<ModelType, GeometryValueType>::initializeLpModel(Environment const& env) {
                 uint64_t numStates = model.getNumberOfStates();
                 lpModel = storm::utility::solver::getLpSolver<ValueType>("model");
                 lpModel->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
@@ -128,7 +129,7 @@ namespace storm {
                     for (uint64_t state = 0; state < numStates; ++state) {
                         auto valIt = schedulerIndependentStates.find(state);
                         if (valIt == schedulerIndependentStates.end()) {
-                            stateVars.push_back(lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state), objectiveHelper[objIndex].getLowerValueBoundAtState(state), objectiveHelper[objIndex].getUpperValueBoundAtState(state)).getExpression());
+                            stateVars.push_back(lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state), objectiveHelper[objIndex].getLowerValueBoundAtState(env, state), objectiveHelper[objIndex].getUpperValueBoundAtState(env, state)).getExpression());
                         } else {
                             stateVars.push_back(lpModel->getConstant(valIt->second));
                         }
@@ -164,7 +165,7 @@ namespace storm {
                                 lpModel->addConstraint("", stateVars[state] == choiceValue);
                             } else {
                                 uint64_t globalChoiceIndex = model.getTransitionMatrix().getRowGroupIndices()[state] + choice;
-                                storm::expressions::Expression maxDiff = lpModel->getConstant(objectiveHelper[objIndex].getUpperValueBoundAtState(state) - objectiveHelper[objIndex].getLowerValueBoundAtState(state)) * (one - choiceVars[globalChoiceIndex]);
+                                storm::expressions::Expression maxDiff = lpModel->getConstant(objectiveHelper[objIndex].getUpperValueBoundAtState(env, state) - objectiveHelper[objIndex].getLowerValueBoundAtState(env, state)) * (one - choiceVars[globalChoiceIndex]);
                                 lpModel->addConstraint("", stateVars[state] - choiceValue <= maxDiff);
                                 lpModel->addConstraint("", choiceValue - stateVars[state] <= maxDiff);
                             }

src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h

@@ -24,7 +24,7 @@ namespace storm {
                 typedef typename std::shared_ptr<storm::storage::geometry::Polytope<GeometryValueType>> Polytope;
                 typedef typename std::vector<GeometryValueType> Point;
                 
-                DeterministicSchedsLpChecker(ModelType const& model, std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives);
+                DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives);
                 ~DeterministicSchedsLpChecker();
 
                 /*!
@@ -46,7 +46,7 @@ namespace storm {
 
             private:
                 void initializeObjectiveHelper(std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives);
-                void initializeLpModel();
+                void initializeLpModel(Environment const& env);
                 
                 void checkRecursive(storm::storage::geometry::PolytopeTree<GeometryValueType>& polytopeTree, GeometryValueType const& eps, std::vector<Point>& foundPoints, std::vector<Polytope>& infeasableAreas);
                 

src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp

@@ -3,12 +3,19 @@
 #include "storm/models/sparse/MarkovAutomaton.h"
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
+#include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"
 #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
 #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "storm/storage/BitVector.h"
 #include "storm/utility/graph.h"
 #include "storm/utility/FilteredRewardModel.h"
+#include "storm/utility/vector.h"
 #include "storm/logic/Formulas.h"
+#include "storm/logic/CloneVisitor.h"
+#include "storm/environment/solver/MinMaxSolverEnvironment.h"
+
 
 #include "storm/exceptions/UnexpectedException.h"
 namespace storm {
@@ -140,14 +147,66 @@ namespace storm {
                 return choiceValueOffsets.get();
             }
             
+            template <typename ValueType>
+            std::vector<ValueType> evaluateOperatorFormula(Environment const& env, storm::models::sparse::Mdp<ValueType> const& model, storm::logic::Formula const& formula) {
+                storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> mc(model);
+                storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> task(formula, false);
+                auto checkResult = mc.check(env, task);
+                STORM_LOG_THROW(checkResult && checkResult->isExplicitQuantitativeCheckResult(), storm::exceptions::UnexpectedException, "Unexpected type of check result for subformula " << formula << ".");
+                return checkResult->template asExplicitQuantitativeCheckResult<ValueType>().getValueVector();
+            }
+            
+            template <typename ValueType>
+            std::vector<ValueType> evaluateOperatorFormula(Environment const& env, storm::models::sparse::MarkovAutomaton<ValueType> const& model, storm::logic::Formula const& formula) {
+                storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>> mc(model);
+                storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> task(formula, false);
+                auto checkResult = mc.check(env, task);
+                STORM_LOG_THROW(checkResult && checkResult->isExplicitQuantitativeCheckResult(), storm::exceptions::UnexpectedException, "Unexpected type of check result for subformula " << formula << ".");
+                return checkResult->template asExplicitQuantitativeCheckResult<ValueType>().getValueVector();
+            }
+            
+            template <typename ModelType>
+            std::vector<typename ModelType::ValueType> computeValueBounds(Environment const& env, bool lowerValueBounds, ModelType const& model, storm::logic::Formula const& formula) {
+                // Change the optimization direction in the formula.
+                auto newFormula = storm::logic::CloneVisitor().clone(formula);
+                newFormula->asOperatorFormula().setOptimalityType(lowerValueBounds ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize);
+                // Create an environment where sound results are enforced
+                storm::Environment soundEnv(env);
+                soundEnv.solver().setForceSoundness(true);
+                auto result = evaluateOperatorFormula(soundEnv, model, *newFormula);
+                
+                auto eps = storm::utility::convertNumber<typename ModelType::ValueType>(soundEnv.solver().minMax().getPrecision());
+                // Add/substract eps to all entries to make up for precision errors
+                if (lowerValueBounds) {
+                    eps = -eps;
+                }
+                for (auto& v : result) {
+                    v += eps;
+                }
+                return result;
+            }
+            
             template <typename ModelType>
-            typename ModelType::ValueType const& DeterministicSchedsObjectiveHelper<ModelType>::getUpperValueBoundAtState(uint64_t state) const{
-                return objective.upperResultBound.get();
+            typename ModelType::ValueType const& DeterministicSchedsObjectiveHelper<ModelType>::getUpperValueBoundAtState(Environment const& env, uint64_t state) const{
+                //return objective.upperResultBound.get();
+                // TODO: try this.
+                if (!upperResultBounds) {
+                    upperResultBounds = computeValueBounds(env, false, model, *objective.formula);
+                    STORM_LOG_THROW(!storm::utility::vector::hasInfinityEntry(upperResultBounds.get()), storm::exceptions::NotSupportedException, "The upper bound for objective " << *objective.originalFormula << " is infinity at some state. This is not supported.");
+                }
+                return upperResultBounds.get()[state];
+                
             }
             
             template <typename ModelType>
-            typename ModelType::ValueType const& DeterministicSchedsObjectiveHelper<ModelType>::getLowerValueBoundAtState(uint64_t state) const{
-                return objective.lowerResultBound.get();
+            typename ModelType::ValueType const& DeterministicSchedsObjectiveHelper<ModelType>::getLowerValueBoundAtState(Environment const& env, uint64_t state) const{
+                // return objective.lowerResultBound.get();
+                //TODO: try this.
+                if (!lowerResultBounds) {
+                    lowerResultBounds = computeValueBounds(env, true, model, *objective.formula);
+                    STORM_LOG_THROW(!storm::utility::vector::hasInfinityEntry(lowerResultBounds.get()), storm::exceptions::NotSupportedException, "The lower bound for objective " << *objective.originalFormula << " is infinity at some state. This is not supported.");
+                }
+                return lowerResultBounds.get()[state];
             }
             
             template class DeterministicSchedsObjectiveHelper<storm::models::sparse::Mdp<double>>;

src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h

@@ -7,6 +7,9 @@
 
 
 namespace storm {
+    
+    class Environment;
+    
     namespace modelchecker {
         namespace multiobjective {
             
@@ -28,12 +31,15 @@ namespace storm {
                  */
                 std::map<uint64_t, ValueType> const& getChoiceValueOffsets() const;
 
-                ValueType const& getUpperValueBoundAtState(uint64_t state) const;
-                ValueType const& getLowerValueBoundAtState(uint64_t state) const;
+                ValueType const& getUpperValueBoundAtState(Environment const& env, uint64_t state) const;
+                ValueType const& getLowerValueBoundAtState(Environment const& env, uint64_t state) const;
             private:
                 
                 mutable boost::optional<std::map<uint64_t, ValueType>> schedulerIndependentStateValues;
                 mutable boost::optional<std::map<uint64_t, ValueType>> choiceValueOffsets;
+                mutable boost::optional<std::vector<ValueType>> lowerResultBounds;
+                mutable boost::optional<std::vector<ValueType>> upperResultBounds;
+                
                 
                 ModelType const& model;
                 Objective<ValueType> const& objective;

src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp

@@ -303,9 +303,9 @@ namespace storm {
             }
             
             template <class SparseModelType, typename GeometryValueType>
-            DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::DeterministicSchedsParetoExplorer(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) : model(preprocessorResult.preprocessedModel), objectives(preprocessorResult.objectives) {
+            DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::DeterministicSchedsParetoExplorer(Environment const& env, preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) : model(preprocessorResult.preprocessedModel), objectives(preprocessorResult.objectives) {
                 originalModelInitialState = *preprocessorResult.originalModel.getInitialStates().begin();
-                lpChecker = std::make_shared<DeterministicSchedsLpChecker<SparseModelType, GeometryValueType>>(*model, objectives);
+                lpChecker = std::make_shared<DeterministicSchedsLpChecker<SparseModelType, GeometryValueType>>(env, *model, objectives);
             }
 
             template <class SparseModelType, typename GeometryValueType>

src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h

@@ -138,7 +138,7 @@ namespace storm {
                 };
                 
                 
-                DeterministicSchedsParetoExplorer(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult);
+                DeterministicSchedsParetoExplorer(Environment const& env, preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult);
 
                 virtual std::unique_ptr<CheckResult> check(Environment const& env);
 

src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp

@@ -53,7 +53,7 @@ namespace storm {
                     {
                         if (env.modelchecker().multi().isSchedulerRestrictionSet()) {
                             STORM_LOG_THROW(preprocessorResult.queryType == preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Pareto, storm::exceptions::NotImplementedException, "Currently, only Pareto queries with scheduler restrictions are implemented.");
-                            auto explorer = DeterministicSchedsParetoExplorer<SparseModelType, storm::RationalNumber>(preprocessorResult);
+                            auto explorer = DeterministicSchedsParetoExplorer<SparseModelType, storm::RationalNumber>(env, preprocessorResult);
                             result = explorer.check(env);
                             if (env.modelchecker().multi().isExportPlotSet()) {
                                 explorer.exportPlotOfCurrentApproximation(env);