diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp index f621a78b6..da5815cc4 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp @@ -9,10 +9,10 @@ namespace storm { namespace multiobjective { template - DeterministicSchedsLpChecker::DeterministicSchedsLpChecker(ModelType const& model, std::vector> const& objectives) : model(model) { + DeterministicSchedsLpChecker::DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector> 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 DeterministicSchedsLpChecker::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(lpModel->getContinuousValue(objVar))); } - swCheckVertices.stop(); swCheck.stop(); + swCheck.stop(); return newPoint; } @@ -95,7 +96,7 @@ namespace storm { } template - void DeterministicSchedsLpChecker::initializeLpModel() { + void DeterministicSchedsLpChecker::initializeLpModel(Environment const& env) { uint64_t numStates = model.getNumberOfStates(); lpModel = storm::utility::solver::getLpSolver("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); } diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h index 3a88b0940..a1352e3d1 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h @@ -24,7 +24,7 @@ namespace storm { typedef typename std::shared_ptr> Polytope; typedef typename std::vector Point; - DeterministicSchedsLpChecker(ModelType const& model, std::vector> const& objectives); + DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector> const& objectives); ~DeterministicSchedsLpChecker(); /*! @@ -46,7 +46,7 @@ namespace storm { private: void initializeObjectiveHelper(std::vector> const& objectives); - void initializeLpModel(); + void initializeLpModel(Environment const& env); void checkRecursive(storm::storage::geometry::PolytopeTree& polytopeTree, GeometryValueType const& eps, std::vector& foundPoints, std::vector& infeasableAreas); diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp index 67bc9d24d..c31fecd78 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp +++ b/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 + std::vector evaluateOperatorFormula(Environment const& env, storm::models::sparse::Mdp const& model, storm::logic::Formula const& formula) { + storm::modelchecker::SparseMdpPrctlModelChecker> mc(model); + storm::modelchecker::CheckTask 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().getValueVector(); + } + + template + std::vector evaluateOperatorFormula(Environment const& env, storm::models::sparse::MarkovAutomaton const& model, storm::logic::Formula const& formula) { + storm::modelchecker::SparseMarkovAutomatonCslModelChecker> mc(model); + storm::modelchecker::CheckTask 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().getValueVector(); + } + + template + std::vector 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(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::ValueType const& DeterministicSchedsObjectiveHelper::getUpperValueBoundAtState(uint64_t state) const{ - return objective.upperResultBound.get(); + typename ModelType::ValueType const& DeterministicSchedsObjectiveHelper::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::ValueType const& DeterministicSchedsObjectiveHelper::getLowerValueBoundAtState(uint64_t state) const{ - return objective.lowerResultBound.get(); + typename ModelType::ValueType const& DeterministicSchedsObjectiveHelper::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>; diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h index 5bb778c87..58dd28768 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h +++ b/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 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> schedulerIndependentStateValues; mutable boost::optional> choiceValueOffsets; + mutable boost::optional> lowerResultBounds; + mutable boost::optional> upperResultBounds; + ModelType const& model; Objective const& objective; diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp index 1b5662e99..034fbe6fe 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp @@ -303,9 +303,9 @@ namespace storm { } template - DeterministicSchedsParetoExplorer::DeterministicSchedsParetoExplorer(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult) : model(preprocessorResult.preprocessedModel), objectives(preprocessorResult.objectives) { + DeterministicSchedsParetoExplorer::DeterministicSchedsParetoExplorer(Environment const& env, preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult) : model(preprocessorResult.preprocessedModel), objectives(preprocessorResult.objectives) { originalModelInitialState = *preprocessorResult.originalModel.getInitialStates().begin(); - lpChecker = std::make_shared>(*model, objectives); + lpChecker = std::make_shared>(env, *model, objectives); } template diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h index bbf074b5c..0fe5dc408 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h @@ -138,7 +138,7 @@ namespace storm { }; - DeterministicSchedsParetoExplorer(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult); + DeterministicSchedsParetoExplorer(Environment const& env, preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult); virtual std::unique_ptr check(Environment const& env); diff --git a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp index 68e9fcd5e..8c395ec5c 100644 --- a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp +++ b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp @@ -53,7 +53,7 @@ namespace storm { { if (env.modelchecker().multi().isSchedulerRestrictionSet()) { STORM_LOG_THROW(preprocessorResult.queryType == preprocessing::SparseMultiObjectivePreprocessorResult::QueryType::Pareto, storm::exceptions::NotImplementedException, "Currently, only Pareto queries with scheduler restrictions are implemented."); - auto explorer = DeterministicSchedsParetoExplorer(preprocessorResult); + auto explorer = DeterministicSchedsParetoExplorer(env, preprocessorResult); result = explorer.check(env); if (env.modelchecker().multi().isExportPlotSet()) { explorer.exportPlotOfCurrentApproximation(env);