diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index bb93e0eaf..f9f370aaa 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -147,11 +147,25 @@ namespace storm { if (objective.considersComplementaryEvent) { if (objective.bound) { objective.bound->threshold = objective.bound->threshold.getManager().rational(storm::utility::one()) - objective.bound->threshold; - objective.bound->comparisonType = storm::logic::invert(objective.bound->comparisonType); + switch (objective.bound->comparisonType) { + case storm::logic::ComparisonType::Greater: + objective.bound->comparisonType = storm::logic::ComparisonType::Less; + break; + case storm::logic::ComparisonType::GreaterEqual: + objective.bound->comparisonType = storm::logic::ComparisonType::LessEqual; + break; + case storm::logic::ComparisonType::Less: + objective.bound->comparisonType = storm::logic::ComparisonType::Greater; + break; + case storm::logic::ComparisonType::LessEqual: + objective.bound->comparisonType = storm::logic::ComparisonType::GreaterEqual; + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Current objective " << formula << " has unexpected comparison type"); + } } objective.optimizationDirection = storm::solver::invert(objective.optimizationDirection); } - } template @@ -365,10 +379,13 @@ namespace storm { if (mergerResult.targetState) { storm::storage::BitVector targetStateAsVector(result.preprocessedModel->getNumberOfStates(), false); targetStateAsVector.set(*mergerResult.targetState, true); + // The overapproximation for the possible ec choices consists of the states that can reach the target states with prob. 0 and the target state itself. result.possibleECChoices = result.preprocessedModel->getTransitionMatrix().getRowIndicesOfRowGroups(storm::utility::graph::performProb0E(*result.preprocessedModel, result.preprocessedModel->getBackwardTransitions(), storm::storage::BitVector(targetStateAsVector.size(), true), targetStateAsVector)); result.possibleECChoices.set(result.preprocessedModel->getTransitionMatrix().getRowGroupIndices()[*mergerResult.targetState], true); // There is an additional state in the result result.possibleBottomStates.resize(result.possibleBottomStates.size() + 1, true); + } else { + result.possibleECChoices = storm::storage::BitVector(result.preprocessedModel->getNumberOfChoices(), true); } assert(result.possibleBottomStates.size() == result.preprocessedModel->getNumberOfStates()); diff --git a/src/storm/modelchecker/multiobjective/constraintBased/SparseCbAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/constraintBased/SparseCbAchievabilityQuery.cpp index 4aefe2d8d..fcecefebc 100644 --- a/src/storm/modelchecker/multiobjective/constraintBased/SparseCbAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/constraintBased/SparseCbAchievabilityQuery.cpp @@ -7,11 +7,15 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" +#include "storm/utility/solver.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/MultiObjectiveSettings.h" +#include "storm/storage/expressions/Expressions.h" #include "storm/exceptions/InvalidOperationException.h" +#include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/UnexpectedException.h" namespace storm { namespace modelchecker { @@ -21,7 +25,7 @@ namespace storm { template SparseCbAchievabilityQuery::SparseCbAchievabilityQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult) : SparseCbQuery(preprocessorResult) { STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorReturnType::QueryType::Achievability, "Invalid query Type"); - + solver = storm::utility::solver::SmtSolverFactory().create(*this->expressionManager); } template @@ -35,8 +39,148 @@ namespace storm { template bool SparseCbAchievabilityQuery::checkAchievability() { + + //this->preprocessedModel.writeDotToStream(std::cout); + + initializeConstraintSystem(); + solver->push(); + addObjectiveConstraints(); + solver->push(); + + storm::solver::SmtSolver::CheckResult result = solver->check(); + switch(result) { + case storm::solver::SmtSolver::CheckResult::Sat: + // std::cout << std::endl << "Satisfying assignment: " << std::endl << solver->getModelAsValuation().toString(true) << std::endl; + return true; + case storm::solver::SmtSolver::CheckResult::Unsat: + // std::cout << std::endl << "Unsatisfiability core: {" << std::endl; + // for (auto const& expr : solver->getUnsatCore()) { + // std::cout << "\t " << expr << std::endl; + // } + // std::cout << "}" << std::endl; + return false; + default: + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "SMT solver yielded an unexpected result"); + } + return false; } + + template + void SparseCbAchievabilityQuery::initializeConstraintSystem() { + uint_fast64_t numStates = this->preprocessedModel.getNumberOfStates(); + uint_fast64_t numChoices = this->preprocessedModel.getNumberOfChoices(); + uint_fast64_t numBottomStates = this->possibleBottomStates.getNumberOfSetBits(); + + storm::expressions::Expression zero = this->expressionManager->rational(storm::utility::zero()); + storm::expressions::Expression one = this->expressionManager->rational(storm::utility::one()); + + // Declare the variables for the choices and bottom states + expectedChoiceVariables.reserve(numChoices); + for (uint_fast64_t choice = 0; choice < numChoices; ++choice) { + expectedChoiceVariables.push_back(this->expressionManager->declareRationalVariable("y" + std::to_string(choice))); + } + bottomStateVariables.reserve(numBottomStates); + for (uint_fast64_t bottomState = 0; bottomState < numBottomStates; ++bottomState) { + bottomStateVariables.push_back(this->expressionManager->declareRationalVariable("z" + std::to_string(bottomState))); + } + + // assert that the values are greater zero and that the bottom state values sum up to one + for (auto& var : expectedChoiceVariables) { + solver->add(var.getExpression() >= zero); + } + storm::expressions::Expression bottomStateSum = zero; + for (auto& var : bottomStateVariables) { + solver->add(var.getExpression() >= zero); + bottomStateSum = bottomStateSum + var.getExpression(); + } + solver->add(bottomStateSum == one); + + // assert that the "incoming" value of each state equals the "outgoing" value + storm::storage::SparseMatrix backwardsTransitions = this->preprocessedModel.getTransitionMatrix().transpose(); + auto bottomStateVariableIt = bottomStateVariables.begin(); + for (uint_fast64_t state = 0; state < numStates; ++state) { + // get the "incomming" value + storm::expressions::Expression value = this->preprocessedModel.getInitialStates().get(state) ? one : zero; + for (auto const& backwardsEntry : backwardsTransitions.getRow(state)) { + value = value + (this->expressionManager->rational(backwardsEntry.getValue()) * expectedChoiceVariables[backwardsEntry.getColumn()].getExpression()); + } + + // subtract the "outgoing" value + for (uint_fast64_t choice = this->preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; choice < this->preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) { + value = value - expectedChoiceVariables[choice]; + } + if (this->possibleBottomStates.get(state)) { + value = value - (*bottomStateVariableIt); + ++bottomStateVariableIt; + } + solver->add(value == zero); + } + assert(bottomStateVariableIt == bottomStateVariables.end()); + + } + + template + void SparseCbAchievabilityQuery::addObjectiveConstraints() { + storm::expressions::Expression zero = this->expressionManager->rational(storm::utility::zero()); + for (Objective const& obj : this->objectives) { + if (obj.rewardModelName) { + STORM_LOG_THROW(obj.bound, storm::exceptions::InvalidOperationException, "Invoked achievability query but no bound was specified for at least one objective."); + STORM_LOG_THROW(!obj.lowerTimeBound && !obj.upperTimeBound, storm::exceptions::NotSupportedException, "Constraint based method currently does not support step bounds"); + std::vector rewards = getActionBasedExpectedRewards(*obj.rewardModelName); + storm::expressions::Expression objValue = zero; + for (uint_fast64_t choice = 0; choice < rewards.size(); ++choice) { + if (!storm::utility::isZero(rewards[choice])) { + objValue = objValue + (this->expressionManager->rational(rewards[choice]) * expectedChoiceVariables[choice].getExpression()); + } + } + // We need to actually evaluate the threshold as rational number. Otherwise a threshold like '<=16/9' might be considered as 1 due to integer division + STORM_LOG_THROW(!obj.bound->threshold.containsVariables(), storm::exceptions::InvalidOperationException, "The threshold for one objective still contains undefined variables"); + storm::expressions::Expression threshold = this->expressionManager->rational(obj.bound->threshold.evaluateAsRational()); + switch (obj.bound->comparisonType) { + case storm::logic::ComparisonType::Greater: + solver->add( objValue > threshold); + break; + case storm::logic::ComparisonType::GreaterEqual: + solver->add( objValue >= threshold); + break; + case storm::logic::ComparisonType::Less: + solver->add( objValue < threshold); + break; + case storm::logic::ComparisonType::LessEqual: + solver->add( objValue <= threshold); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "One or more objectives have an invalid comparison type"); + } + } + } + } + + template <> + std::vector SparseCbAchievabilityQuery>::getActionBasedExpectedRewards(std::string const& rewardModelName) const { + return this->preprocessedModel.getRewardModel(rewardModelName).getTotalRewardVector(this->preprocessedModel.getTransitionMatrix()); + } + + template <> + std::vector SparseCbAchievabilityQuery>::getActionBasedExpectedRewards(std::string const& rewardModelName) const { + auto const& rewModel = this->preprocessedModel.getRewardModel(rewardModelName); + STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected."); + std::vector result = rewModel.hasStateActionRewards() ? rewModel.getStateActionRewardVector() : std::vector(this->preprocessedModel.getNumberOfChoices(), storm::utility::zero()); + if(rewModel.hasStateRewards()) { + // Note that state rewards are earned over time and thus play no role for probabilistic states + for(auto markovianState : this->preprocessedModel.getMarkovianStates()) { + result[this->preprocessedModel.getTransitionMatrix().getRowGroupIndices()[markovianState]] += rewModel.getStateReward(markovianState) / this->preprocessedModel.getExitRate(markovianState); + } + } + return result; + } + + template <> + std::vector SparseCbAchievabilityQuery>::getActionBasedExpectedRewards(std::string const& rewardModelName) const { + return this->preprocessedModel.getRewardModel(rewardModelName).getTotalRewardVector(this->preprocessedModel.getTransitionMatrix()); + } + #ifdef STORM_HAVE_CARL template class SparseCbAchievabilityQuery>; diff --git a/src/storm/modelchecker/multiobjective/constraintBased/SparseCbAchievabilityQuery.h b/src/storm/modelchecker/multiobjective/constraintBased/SparseCbAchievabilityQuery.h index a5f754a9b..24e3c3374 100644 --- a/src/storm/modelchecker/multiobjective/constraintBased/SparseCbAchievabilityQuery.h +++ b/src/storm/modelchecker/multiobjective/constraintBased/SparseCbAchievabilityQuery.h @@ -1,7 +1,11 @@ #pragma once + #include "storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h" +#include "storm/solver/SmtSolver.h" +#include "storm/storage/expressions/Variable.h" + namespace storm { namespace modelchecker { namespace multiobjective { @@ -13,6 +17,8 @@ namespace storm { class SparseCbAchievabilityQuery : public SparseCbQuery { public: + typedef typename SparseModelType::ValueType ValueType; + SparseCbAchievabilityQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult); virtual ~SparseCbAchievabilityQuery() = default; @@ -29,6 +35,27 @@ namespace storm { */ bool checkAchievability(); + + /* + * Adds variable y_i for each choice i and z_j for each possible bottom state j and asserts that for every solution of the + * constraint system there is a scheduler under which + * * if choice i yields reward for an expected value objective, then y_i is the expected number of times choice i is taken. + * * z_j/(z_j + Sum_{i in Choices(j)} y_i) is a lower bound for the probability that starting from j no more reward is collected + */ + void initializeConstraintSystem(); + + // Adds the thresholds of the objective values + void addObjectiveConstraints(); + + // Returns the action based rewards for the given reward model name. + std::vector getActionBasedExpectedRewards(std::string const& rewardModelName) const; + + + std::vector expectedChoiceVariables; + std::vector bottomStateVariables; + + + std::unique_ptr solver; }; } diff --git a/src/storm/modelchecker/multiobjective/constraintBased/SparseCbQuery.cpp b/src/storm/modelchecker/multiobjective/constraintBased/SparseCbQuery.cpp index 919ada311..3d277dc4a 100644 --- a/src/storm/modelchecker/multiobjective/constraintBased/SparseCbQuery.cpp +++ b/src/storm/modelchecker/multiobjective/constraintBased/SparseCbQuery.cpp @@ -20,8 +20,9 @@ namespace storm { template SparseCbQuery::SparseCbQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult) : originalModel(preprocessorResult.originalModel), originalFormula(preprocessorResult.originalFormula), - preprocessedModel(std::move(*preprocessorResult.preprocessedModel)), objectives(std::move(preprocessorResult.objectives)) { - + preprocessedModel(std::move(*preprocessorResult.preprocessedModel)), objectives(std::move(preprocessorResult.objectives)), + possibleBottomStates(std::move(preprocessorResult.possibleBottomStates)) { + expressionManager = std::make_shared(); } diff --git a/src/storm/modelchecker/multiobjective/constraintBased/SparseCbQuery.h b/src/storm/modelchecker/multiobjective/constraintBased/SparseCbQuery.h index f8324f0fe..d3bc42c91 100644 --- a/src/storm/modelchecker/multiobjective/constraintBased/SparseCbQuery.h +++ b/src/storm/modelchecker/multiobjective/constraintBased/SparseCbQuery.h @@ -1,7 +1,10 @@ #pragma once +#include + #include "storm/modelchecker/results/CheckResult.h" #include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h" +#include "storm/storage/expressions/ExpressionManager.h" namespace storm { namespace modelchecker { @@ -32,6 +35,10 @@ namespace storm { SparseModelType preprocessedModel; std::vector> objectives; + std::shared_ptr expressionManager; + + storm::storage::BitVector possibleBottomStates; + }; }