sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

constraint based achievability queries

main
TimQu 8 years ago
parent
5c338b0092
commit
9c8531d40a
5 changed files with 201 additions and 5 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 21
      src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp
  2. 146
      src/storm/modelchecker/multiobjective/constraintBased/SparseCbAchievabilityQuery.cpp
  3. 27
      src/storm/modelchecker/multiobjective/constraintBased/SparseCbAchievabilityQuery.h
  4. 5
      src/storm/modelchecker/multiobjective/constraintBased/SparseCbQuery.cpp
  5. 7
      src/storm/modelchecker/multiobjective/constraintBased/SparseCbQuery.h

21
src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp
View File

@ -147,11 +147,25 @@ namespace storm {
if (objective.considersComplementaryEvent) {
if (objective.bound) {
objective.bound->threshold = objective.bound->threshold.getManager().rational(storm::utility::one<storm::RationalNumber>()) - 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<typename SparseModelType>
@ -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());

146
src/storm/modelchecker/multiobjective/constraintBased/SparseCbAchievabilityQuery.cpp
View File

@ -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 <class SparseModelType>
SparseCbAchievabilityQuery<SparseModelType>::SparseCbAchievabilityQuery(SparseMultiObjectivePreprocessorReturnType<SparseModelType>& preprocessorResult) : SparseCbQuery<SparseModelType>(preprocessorResult) {
STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorReturnType<SparseModelType>::QueryType::Achievability, "Invalid query Type");
solver = storm::utility::solver::SmtSolverFactory().create(*this->expressionManager);
}
template <class SparseModelType>
@ -35,8 +39,148 @@ namespace storm {
template <class SparseModelType>
bool SparseCbAchievabilityQuery<SparseModelType>::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 <class SparseModelType>
void SparseCbAchievabilityQuery<SparseModelType>::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<ValueType>());
storm::expressions::Expression one = this->expressionManager->rational(storm::utility::one<ValueType>());
// 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<ValueType> 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 <class SparseModelType>
void SparseCbAchievabilityQuery<SparseModelType>::addObjectiveConstraints() {
storm::expressions::Expression zero = this->expressionManager->rational(storm::utility::zero<ValueType>());
for (Objective<ValueType> 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<ValueType> 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<double> SparseCbAchievabilityQuery<storm::models::sparse::Mdp<double>>::getActionBasedExpectedRewards(std::string const& rewardModelName) const {
return this->preprocessedModel.getRewardModel(rewardModelName).getTotalRewardVector(this->preprocessedModel.getTransitionMatrix());
}
template <>
std::vector<double> SparseCbAchievabilityQuery<storm::models::sparse::MarkovAutomaton<double>>::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<double> result = rewModel.hasStateActionRewards() ? rewModel.getStateActionRewardVector() : std::vector<double>(this->preprocessedModel.getNumberOfChoices(), storm::utility::zero<ValueType>());
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<storm::RationalNumber> SparseCbAchievabilityQuery<storm::models::sparse::Mdp<storm::RationalNumber>>::getActionBasedExpectedRewards(std::string const& rewardModelName) const {
return this->preprocessedModel.getRewardModel(rewardModelName).getTotalRewardVector(this->preprocessedModel.getTransitionMatrix());
}
#ifdef STORM_HAVE_CARL
template class SparseCbAchievabilityQuery<storm::models::sparse::Mdp<double>>;

27
src/storm/modelchecker/multiobjective/constraintBased/SparseCbAchievabilityQuery.h
View File

@ -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<SparseModelType> {
public:
typedef typename SparseModelType::ValueType ValueType;
SparseCbAchievabilityQuery(SparseMultiObjectivePreprocessorReturnType<SparseModelType>& 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<ValueType> getActionBasedExpectedRewards(std::string const& rewardModelName) const;
std::vector<storm::expressions::Variable> expectedChoiceVariables;
std::vector<storm::expressions::Variable> bottomStateVariables;
std::unique_ptr<storm::solver::SmtSolver> solver;
};
}

5
src/storm/modelchecker/multiobjective/constraintBased/SparseCbQuery.cpp
View File

@ -20,8 +20,9 @@ namespace storm {
template <class SparseModelType>
SparseCbQuery<SparseModelType>::SparseCbQuery(SparseMultiObjectivePreprocessorReturnType<SparseModelType>& 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<storm::expressions::ExpressionManager>();
}

7
src/storm/modelchecker/multiobjective/constraintBased/SparseCbQuery.h
View File

@ -1,7 +1,10 @@
#pragma once
#include <memory>
#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<Objective<typename SparseModelType::ValueType>> objectives;
std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
storm::storage::BitVector possibleBottomStates;
};
}

Write Preview
Loading…
Cancel
Save