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

Towards refactoring multi-objective preprocessing

main
TimQu 9 years ago
parent
b6d085a92d
commit
ee54c6cdac
5 changed files with 800 additions and 0 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. 64
      src/storm/modelchecker/multiobjective/Objective.h
  2. 448
      src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp
  3. 84
      src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h
  4. 73
      src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h
  5. 131
      src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h

64
src/storm/modelchecker/multiobjective/Objective.h
View File

@ -0,0 +1,64 @@
#pragma once
#include <boost/optional.hpp>
#include "storm/logic/Formula.h"
#include "storm/logic/Bound.h"
#include "storm/logic/TimeBound.h"
#include "storm/solver/OptimizationDirection.h"
namespace storm {
namespace modelchecker {
namespace multiobjective {
template <typename ValueType>
struct Objective {
// the original input formula
std::shared_ptr<storm::logic::Formula const> originalFormula;
// the name of the considered reward model in the preprocessedModel
boost::optional<std::string> rewardModelName;
// True iff the complementary event is considered.
// E.g. if we consider P<1-t [F !"safe"] instead of P>=t [ G "safe"]
bool considersComplementaryEvent;
// The probability/reward threshold for the preprocessed model (if originalFormula specifies one).
boost::optional<storm::logic::Bound> bound;
// The optimization direction for the preprocessed model
// if originalFormula does ot specifies one, the direction is derived from the bound.
storm::solver::OptimizationDirection optimizationDirection;
// Lower and upper time/step bouds
boost::optional<storm::logic::TimeBound> lowerTimeBound, upperTimeBound;
void printToStream(std::ostream& out) const {
out << originalFormula->toString();
out << " \t";
out << "direction: ";
out << optimizationDirection;
out << " \t";
out << "intern bound: ";
if (bound){
out << bound;
} else {
out << " -none- ";
}
out << " \t";
out << "time bounds: ";
if (lowerTimeBound && upperTimeBound) {
out << (lowerTimeBound->isStrict() ? "(" : "[") << lowerTimeBound->getBound() << "," << upperTimeBound->getBound() << (upperTimeBound->isStrict() ? ")" : "]");
} else if (lowerTimeBound) {
out << (lowerTimeBound->isStrict() ? ">" : ">=") << lowerTimeBound->getBound();
} else if (upperTimeBound) {
out << (upperTimeBound->isStrict() ? "<" : "<=") << upperTimeBound->getBound();
} else {
out << " -none- ";
}
out << " \t";
out << "intern reward model: " << *rewardModelName;
}
};
}
}
}

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

@ -0,0 +1,448 @@
#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h"
#include <algorithm>
#include <storm/transformer/GoalStateMerger.h>
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/MarkovAutomaton.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/storage/MaximalEndComponentDecomposition.h"
#include "storm/storage/memorystructure/MemoryStructureBuilder.h"
#include "storm/storage/memorystructure/SparseModelMemoryProduct.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/transformer/SubsystemBuilder.h"
#include "storm/utility/macros.h"
#include "storm/utility/vector.h"
#include "storm/utility/graph.h"
#include "storm/utility/endComponents.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/UnexpectedException.h"
#include "storm/exceptions/NotImplementedException.h"
namespace storm {
namespace modelchecker {
namespace multiobjective {
template<typename SparseModelType>
typename SparseMultiObjectivePreprocessor<SparseModelType>::ReturnType SparseMultiObjectivePreprocessor<SparseModelType>::preprocess(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula) {
PreprocessorData data(originalModel);
//Invoke preprocessing on the individual objectives
for (auto const& subFormula : originalFormula.getSubformulas()) {
STORM_LOG_INFO("Preprocessing objective " << *subFormula<< ".");
data.objectives.push_back(std::make_shared<Objective<ValueType>>());
data.objectives.back()->originalFormula = subFormula;
data.finiteRewardCheckObjectives.resize(data.objectives.size(), false);
if (data.objectives.back()->originalFormula->isOperatorFormula()) {
preprocessOperatorFormula(data.objectives.back()->originalFormula->asOperatorFormula(), data);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the subformula " << *subFormula << " of " << originalFormula << " because it is not supported");
}
}
storm::storage::SparseModelMemoryProduct<ValueType> product = data.memory->product(originalModel);
std::shared_ptr<SparseModelType> preprocessedModel = std::dynamic_pointer_cast<SparseModelType>(product.build());
auto backwardTransitions = preprocessedModel->getBackwardTransitions();
bool endComponentAnalysisRequired = false;
for (auto& task : data.tasks) {
endComponentAnalysisRequired = endComponentAnalysisRequired || task->requiresEndComponentAnalysis();
}
if (endComponentAnalysisRequired) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "End component analysis required but currently not implemented.");
}
for (auto& task : data.tasks) {
task->perform(*preprocessedModel);
}
ReturnType result(originalFormula, originalModel);
for (auto& obj : data.objectives) {
result.objectives.push_back(std::move(*obj));
}
result.preprocessedModel = std::move(preprocessedModel);
result.queryType = ReturnType::QueryType::Achievability;
auto minMaxNonZeroRewardStates = getStatesWithNonZeroRewardMinMax(result, backwardTransitions);
auto finiteRewardStates = ensureRewardFiniteness(result, data.finiteRewardCheckObjectives, minMaxNonZeroRewardStates.first, backwardTransitions);
std::set<std::string> relevantRewardModels;
for (auto const& obj : result.objectives) {
relevantRewardModels.insert(*obj.rewardModelName);
}
// Build a subsystem that discards states that yield infinite reward for all schedulers.
// We can also merge the states that will have reward zero anyway.
storm::storage::BitVector zeroRewardStates = ~minMaxNonZeroRewardStates.second;
storm::transformer::GoalStateMerger<SparseModelType> merger(*result.preprocessedModel);
typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult = merger.mergeTargetAndSinkStates(finiteRewardStates, zeroRewardStates, storm::storage::BitVector(finiteRewardStates.size(), false), std::vector<std::string>(relevantRewardModels.begin(), relevantRewardModels.end()));
result.preprocessedModel = mergerResult.model;
result.possibleBottomStates = (~minMaxNonZeroRewardStates.first) % finiteRewardStates;
if (mergerResult.targetState) {
storm::storage::BitVector targetStateAsVector(result.preprocessedModel->getNumberOfStates(), false);
targetStateAsVector.set(*mergerResult.targetState, true);
result.possibleECChoices = 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);
}
assert(result.possibleBottomStates.size() == result.preprocessedModel->getNumberOfStates());
return result;
}
template <typename SparseModelType>
SparseMultiObjectivePreprocessor<SparseModelType>::PreprocessorData::PreprocessorData(SparseModelType const& model) : originalModel(model) {
storm::storage::MemoryStructureBuilder memoryBuilder(1);
memoryBuilder.setTransition(0,0, storm::logic::Formula::getTrueFormula());
memory = std::make_shared<storm::storage::MemoryStructure>(memoryBuilder.build());
// The memoryLabelPrefix should not be a prefix of a state label of the given model to ensure uniqueness of label names
memoryLabelPrefix = "mem";
while (true) {
bool prefixIsUnique = true;
for (auto const& label : originalModel.getStateLabeling().getLabels()) {
if (memoryLabelPrefix.size() <= label.size()) {
if (std::mismatch(memoryLabelPrefix.begin(), memoryLabelPrefix.end(), label.begin()).first == memoryLabelPrefix.end()) {
prefixIsUnique = false;
memoryLabelPrefix = "_" + memoryLabelPrefix;
break;
}
}
}
if (prefixIsUnique) {
break;
}
}
// The rewardModelNamePrefix should not be a prefix of a reward model name of the given model to ensure uniqueness of reward model names
rewardModelNamePrefix = "obj";
while (true) {
bool prefixIsUnique = true;
for (auto const& label : originalModel.getStateLabeling().getLabels()) {
if (memoryLabelPrefix.size() <= label.size()) {
if (std::mismatch(memoryLabelPrefix.begin(), memoryLabelPrefix.end(), label.begin()).first == memoryLabelPrefix.end()) {
prefixIsUnique = false;
memoryLabelPrefix = "_" + memoryLabelPrefix;
break;
}
}
}
if (prefixIsUnique) {
break;
}
}
}
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessOperatorFormula(storm::logic::OperatorFormula const& formula, PreprocessorData& data) {
Objective<ValueType>& objective = *data.objectives.back();
objective.considersComplementaryEvent = false;
if (formula.hasBound()) {
STORM_LOG_THROW(!formula.getBound().threshold.containsVariables(), storm::exceptions::InvalidPropertyException, "The formula " << formula << "considers a non-constant threshold");
objective.bound = formula.getBound();
if (storm::logic::isLowerBound(formula.getBound().comparisonType)) {
objective.optimizationDirection = storm::solver::OptimizationDirection::Maximize;
} else {
objective.optimizationDirection = storm::solver::OptimizationDirection::Minimize;
}
STORM_LOG_WARN_COND(!formula.hasOptimalityType() || formula.getOptimalityType() == objective.optimizationDirection, "Optimization direction of formula " << formula << " ignored as the formula also specifies a threshold.");
} else if (formula.hasOptimalityType()){
objective.optimizationDirection = formula.getOptimalityType();
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Current objective " << formula << " does not specify whether to minimize or maximize");
}
if (formula.isProbabilityOperatorFormula()){
preprocessProbabilityOperatorFormula(formula.asProbabilityOperatorFormula(), data);
} else if (formula.isRewardOperatorFormula()){
preprocessRewardOperatorFormula(formula.asRewardOperatorFormula(), data);
} else if (formula.isTimeOperatorFormula()){
preprocessTimeOperatorFormula(formula.asTimeOperatorFormula(), data);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the objective " << formula << " because it is not supported");
}
// Invert the bound and optimization direction (if necessary)
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);
}
objective.optimizationDirection = storm::solver::invert(objective.optimizationDirection);
}
}
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, PreprocessorData& data) {
if (formula.getSubformula().isUntilFormula()){
preprocessUntilFormula(formula.getSubformula().asUntilFormula(), data);
} else if (formula.getSubformula().isBoundedUntilFormula()){
preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), data);
} else if (formula.getSubformula().isGloballyFormula()){
preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), data);
} else if (formula.getSubformula().isEventuallyFormula()){
preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported.");
}
}
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, PreprocessorData& data) {
STORM_LOG_THROW((formula.hasRewardModelName() && data.originalModel.hasRewardModel(formula.getRewardModelName()))
|| (!formula.hasRewardModelName() && data.originalModel.hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model is not unique or the formula " << formula << " does not specify an existing reward model.");
std::string rewardModelName;
if (formula.hasRewardModelName()) {
rewardModelName = formula.getRewardModelName();
STORM_LOG_THROW(data.originalModel.hasRewardModel(rewardModelName), storm::exceptions::InvalidPropertyException, "The reward model specified by formula " << formula << " does not exist in the model");
} else {
STORM_LOG_THROW(data.originalModel.hasUniqueRewardModel(), storm::exceptions::InvalidOperationException, "The formula " << formula << " does not specify a reward model name and the reward model is not unique.");
rewardModelName = data.originalModel.getRewardModels().begin()->first;
}
if (formula.getSubformula().isEventuallyFormula()){
preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data, rewardModelName);
} else if (formula.getSubformula().isCumulativeRewardFormula()) {
preprocessCumulativeRewardFormula(formula.getSubformula().asCumulativeRewardFormula(), data, rewardModelName);
} else if (formula.getSubformula().isTotalRewardFormula()) {
preprocessTotalRewardFormula(data, rewardModelName);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported.");
}
}
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, PreprocessorData& data) {
// Time formulas are only supported for Markov automata
STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Time operator formulas are only supported for Markov automata.");
if (formula.getSubformula().isEventuallyFormula()){
preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported.");
}
}
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessUntilFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data) {
// Check if the formula is already satisfied in the initial state because then the transformation to expected rewards will fail.
if (!data.objectives.back()->lowerTimeBound) {
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(data.originalModel);
if (!(data.originalModel.getInitialStates() & mc.check(formula.getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()).empty()) {
// TODO: Handle this case more properly
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The Probability for the objective " << *data.objectives.back()->originalFormula << " is always one as the rhs of the until formula is true in the initial state. This (trivial) case is currently not implemented.");
}
}
// Create a memory structure that stores whether a non-PhiState or a PsiState has already been reached
storm::storage::MemoryStructureBuilder builder(2);
std::string relevantStatesLabel = data.memoryLabelPrefix + "_obj" + std::to_string(data.objectives.size()) + "_relevant";
builder.setLabel(0, relevantStatesLabel);
auto negatedLeftSubFormula = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getLeftSubformula().asSharedPointer());
auto targetFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::Or, negatedLeftSubFormula, formula.getRightSubformula().asSharedPointer());
builder.setTransition(0, 0, std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, targetFormula));
builder.setTransition(0, 1, targetFormula);
builder.setTransition(1, 1, storm::logic::Formula::getTrueFormula());
storm::storage::MemoryStructure objectiveMemory = builder.build();
data.memory = std::make_shared<storm::storage::MemoryStructure>(data.memory->product(objectiveMemory));
data.objectives.back()->rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size());
auto relevantStatesFormula = std::make_shared<storm::logic::AtomicLabelFormula>(relevantStatesLabel);
data.tasks.push_back(std::make_shared<SparseMultiObjectivePreprocessorReachProbToTotalRewTask<SparseModelType>>(data.objectives.back(), relevantStatesFormula, formula.getRightSubformula().asSharedPointer()));
}
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data) {
STORM_LOG_THROW(!data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.isStepBounded(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support STEP-bounded properties for Markov automata.");
if (formula.hasLowerBound()) {
STORM_LOG_THROW(!formula.getLowerBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The lower time bound for the formula " << formula << " still contains variables");
if (!storm::utility::isZero(formula.getLowerBound<double>()) || formula.isLowerBoundStrict()) {
data.objectives.back()->lowerTimeBound = storm::logic::TimeBound(formula.isLowerBoundStrict(), formula.getLowerBound());
}
}
if (formula.hasUpperBound()) {
STORM_LOG_THROW(!formula.getUpperBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The Upper time bound for the formula " << formula << " still contains variables");
if (!storm::utility::isInfinity(formula.getUpperBound<double>())) {
data.objectives.back()->upperTimeBound = storm::logic::TimeBound(formula.isUpperBoundStrict(), formula.getUpperBound());
}
}
preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data);
}
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, PreprocessorData& data) {
// The formula will be transformed to an until formula for the complementary event.
data.objectives.back()->considersComplementaryEvent = true;
auto negatedSubformula = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer());
preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), negatedSubformula), data);
}
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, PreprocessorData& data, boost::optional<std::string> const& optionalRewardModelName) {
if (formula.isReachabilityProbabilityFormula()){
preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), data);
return;
}
// Create a memory structure that stores whether a target state has already been reached
storm::storage::MemoryStructureBuilder builder(2);
// Get a unique label that is not already present in the model
std::string relevantStatesLabel = data.memoryLabelPrefix + "_obj" + std::to_string(data.objectives.size()) + "_relevant";
builder.setLabel(0, relevantStatesLabel);
builder.setTransition(0, 0, std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer()));
builder.setTransition(0, 1, formula.getSubformula().asSharedPointer());
builder.setTransition(1, 1, std::make_shared<storm::logic::BooleanLiteralFormula>(true));
storm::storage::MemoryStructure objectiveMemory = builder.build();
data.memory = std::make_shared<storm::storage::MemoryStructure>(data.memory->product(objectiveMemory));
auto relevantStatesFormula = std::make_shared<storm::logic::AtomicLabelFormula>(relevantStatesLabel);
data.objectives.back()->rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size());
data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true);
if (formula.isReachabilityRewardFormula()) {
assert(optionalRewardModelName.is_initialized());
data.tasks.push_back(std::make_shared<SparseMultiObjectivePreprocessorReachRewToTotalRewTask<SparseModelType>>(data.objectives.back(), relevantStatesFormula, optionalRewardModelName.get()));
data.finiteRewardCheckObjectives.set(data.objectives.size() - 1);
} else if (formula.isReachabilityTimeFormula() && data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton)) {
data.finiteRewardCheckObjectives.set(data.objectives.size() - 1);
data.tasks.push_back(std::make_shared<SparseMultiObjectivePreprocessorReachTimeToTotalRewTask<SparseModelType>>(data.objectives.back(), relevantStatesFormula));
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The formula " << formula << " neither considers reachability probabilities nor reachability rewards " << (data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) ? "nor reachability time" : "") << ". This is not supported.");
}
}
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, boost::optional<std::string> const& optionalRewardModelName) {
STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type.");
STORM_LOG_THROW(!formula.getBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The time bound for the formula " << formula << " still contains variables");
if (!storm::utility::isInfinity(formula.getBound<double>())) {
data.objectives.back()->upperTimeBound = storm::logic::TimeBound(formula.isBoundStrict(), formula.getBound());
}
}
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessTotalRewardFormula(PreprocessorData& data, boost::optional<std::string> const& optionalRewardModelName) {
assert(optionalRewardModelName.is_initialized());
data.objectives.back()->rewardModelName = *optionalRewardModelName;
data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true);
}
template<typename SparseModelType>
std::pair<storm::storage::BitVector, storm::storage::BitVector> SparseMultiObjectivePreprocessor<SparseModelType>::getStatesWithNonZeroRewardMinMax(ReturnType& result, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) {
uint_fast64_t stateCount = result.preprocessedModel->getNumberOfStates();
auto const& transitions = result.preprocessedModel->getTransitionMatrix();
std::vector<uint_fast64_t> const& groupIndices = transitions.getRowGroupIndices();
storm::storage::BitVector allStates(stateCount, true);
// Get the choices that yield non-zero reward
storm::storage::BitVector zeroRewardChoices(result.preprocessedModel->getNumberOfChoices(), true);
for (auto const& obj : result.objectives) {
auto const& rewModel = result.preprocessedModel->getRewardModel(*obj.rewardModelName);
zeroRewardChoices &= rewModel.getChoicesWithZeroReward(transitions);
}
// Get the states that have reward for at least one (or for all) choices assigned to it.
storm::storage::BitVector statesWithRewardForOneChoice = storm::storage::BitVector(stateCount, false);
storm::storage::BitVector statesWithRewardForAllChoices = storm::storage::BitVector(stateCount, true);
for (uint_fast64_t state = 0; state < stateCount; ++state) {
bool stateHasChoiceWithReward = false;
bool stateHasChoiceWithoutReward = false;
uint_fast64_t const& groupEnd = groupIndices[state + 1];
for (uint_fast64_t choice = groupIndices[state]; choice < groupEnd; ++choice) {
if (zeroRewardChoices.get(choice)) {
stateHasChoiceWithoutReward = true;
} else {
stateHasChoiceWithReward = true;
}
}
if (stateHasChoiceWithReward) {
statesWithRewardForOneChoice.set(state, true);
}
if (stateHasChoiceWithoutReward) {
statesWithRewardForAllChoices.set(state, false);
}
}
// get the states from which the minimal/maximal expected reward is always non-zero
storm::storage::BitVector minStates = storm::utility::graph::performProbGreater0A(transitions, groupIndices, backwardTransitions, allStates, statesWithRewardForAllChoices, false, 0, zeroRewardChoices);
storm::storage::BitVector maxStates = storm::utility::graph::performProbGreater0E(backwardTransitions, allStates, statesWithRewardForOneChoice);
STORM_LOG_ASSERT(minStates.isSubsetOf(maxStates), "The computed set of states with minimal non-zero expected rewards is not a subset of the states with maximal non-zero rewards.");
return std::make_pair(std::move(minStates), std::move(maxStates));
}
template<typename SparseModelType>
storm::storage::BitVector SparseMultiObjectivePreprocessor<SparseModelType>::ensureRewardFiniteness(ReturnType& result, storm::storage::BitVector const& finiteRewardCheckObjectives, storm::storage::BitVector const& nonZeroRewardMin, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) {
auto const& transitions = result.preprocessedModel->getTransitionMatrix();
std::vector<uint_fast64_t> const& groupIndices = transitions.getRowGroupIndices();
storm::storage::BitVector maxRewardsToCheck(result.preprocessedModel->getNumberOfChoices(), true);
bool hasMinRewardToCheck;
for (auto const& objIndex : finiteRewardCheckObjectives) {
auto const& rewModel = result.preprocessedModel->getRewardModel(result.objectives[objIndex].rewardModelName.get());
if (storm::solver::minimize(result.objectives[objIndex].optimizationDirection)) {
hasMinRewardToCheck = true;
} else {
maxRewardsToCheck &= rewModel.getChoicesWithZeroReward(transitions);
}
}
maxRewardsToCheck.complement();
// Assert reward finitiness for maximizing objectives under all schedulers
storm::storage::BitVector allStates(result.preprocessedModel->getNumberOfStates(), true);
if (storm::utility::endComponents::checkIfECWithChoiceExists(transitions, backwardTransitions, allStates, maxRewardsToCheck)) {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "At least one of the maximizing objectives induces infinite expected reward (or time). This is not supported");
}
// Assert that there is one scheduler under which all rewards are finite.
// This only has to be done if there are minimizing expected rewards that potentially can be infinite
storm::storage::BitVector finiteRewardStates;
if (hasMinRewardToCheck) {
finiteRewardStates = storm::utility::graph::performProb1E(transitions, groupIndices, backwardTransitions, allStates, ~nonZeroRewardMin);
if ((finiteRewardStates & result.preprocessedModel->getInitialStates()).empty()) {
// There is no scheduler that induces finite reward for the initial state
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "For every scheduler, at least one objective gets infinite reward.");
}
} else {
finiteRewardStates = allStates;
}
return finiteRewardStates;
}
template class SparseMultiObjectivePreprocessor<storm::models::sparse::Mdp<double>>;
template class SparseMultiObjectivePreprocessor<storm::models::sparse::MarkovAutomaton<double>>;
template class SparseMultiObjectivePreprocessor<storm::models::sparse::Mdp<storm::RationalNumber>>;
template class SparseMultiObjectivePreprocessor<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
}
}
}

84
src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h
View File

@ -0,0 +1,84 @@
#pragma once
#include <memory>
#include <string>
#include "storm/logic/Formulas.h"
#include "storm/storage/BitVector.h"
#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h"
#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h"
#include "storm/storage/memorystructure/MemoryStructure.h"
namespace storm {
namespace modelchecker {
namespace multiobjective {
/*
* This class invokes the necessary preprocessing for the constraint based multi-objective model checking algorithm
*/
template <class SparseModelType>
class SparseMultiObjectivePreprocessor {
public:
typedef typename SparseModelType::ValueType ValueType;
typedef typename SparseModelType::RewardModelType RewardModelType;
typedef SparseMultiObjectivePreprocessorReturnType<SparseModelType> ReturnType;
/*!
* Preprocesses the given model w.r.t. the given formulas
* @param originalModel The considered model
* @param originalFormula the considered formula. The subformulas should only contain one OperatorFormula at top level.
*/
static ReturnType preprocess(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula);
private:
struct PreprocessorData {
SparseModelType const& originalModel;
std::vector<std::shared_ptr<CbObjective<ValueType>>> objectives;
std::vector<std::shared_ptr<SparseMultiObjectivePreprocessorTask<SparseModelType>>> tasks;
std::shared_ptr<storm::storage::MemoryStructure> memory;
// Indices of the objectives that require a check for finite reward
storm::storage::BitVector finiteRewardCheckObjectives;
std::string memoryLabelPrefix;
std::string rewardModelNamePrefix;
PreprocessorData(SparseModelType const& model);
};
/*!
* Apply the neccessary preprocessing for the given formula.
* @param formula the current (sub)formula
* @param data the current data. The currently processed objective is located at data.objectives.back()
* @param optionalRewardModelName the reward model name that is considered for the formula (if available)
*/
static void preprocessOperatorFormula(storm::logic::OperatorFormula const& formula, PreprocessorData& data);
static void preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, PreprocessorData& data);
static void preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, PreprocessorData& data);
static void preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, PreprocessorData& data);
static void preprocessUntilFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data);
static void preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data);
static void preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, PreprocessorData& data);
static void preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, PreprocessorData& data, boost::optional<std::string> const& optionalRewardModelName = boost::none);
static void preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, boost::optional<std::string> const& optionalRewardModelName = boost::none);
static void preprocessTotalRewardFormula(PreprocessorData& data, boost::optional<std::string> const& optionalRewardModelName = boost::none); // The total reward formula itself does not need to be provided as it is unique.
/*!
* Computes the set of states that have a non-zero reward w.r.t. all objectives, assuming that the objectives are all minimizing and maximizing, respectively.
*/
static std::pair<storm::storage::BitVector, storm::storage::BitVector> getStatesWithNonZeroRewardMinMax(ReturnType& result, storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
/*!
* Checks whether the occurring expected rewards are finite. If not, the input is rejected.
* Returns the set of states for which a scheduler exists that induces finite reward for all objectives
*/
static storm::storage::BitVector ensureRewardFiniteness(ReturnType& result, storm::storage::BitVector const& finiteRewardCheckObjectives, storm::storage::BitVector const& nonZeroRewardMin, storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
};
}
}
}

73
src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h
View File

@ -0,0 +1,73 @@
#pragma once
#include <vector>
#include <memory>
#include <boost/optional.hpp>
#include "storm/logic/Formulas.h"
#include "storm/modelchecker/multiobjective/constraintbased/CbObjective.h"
#include "storm/exceptions/UnexpectedException.h"
namespace storm {
namespace modelchecker {
namespace multiobjective {
template <class SparseModelType>
struct SparseCbPreprocessorReturnType {
enum class QueryType { Achievability };
storm::logic::MultiObjectiveFormula const& originalFormula;
SparseModelType const& originalModel;
std::shared_ptr<SparseModelType> preprocessedModel;
QueryType queryType;
// The (preprocessed) objectives
std::vector<CbObjective<typename SparseModelType::ValueType>> objectives;
// The states for which there is a scheduler such that all objectives have value zero
storm::storage::BitVector possibleBottomStates;
// Overapproximation of the set of choices that are part of an end component.
storm::storage::BitVector possibleECChoices;
SparseCbPreprocessorReturnType(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel) : originalFormula(originalFormula), originalModel(originalModel) {
// Intentionally left empty
}
void printToStream(std::ostream& out) const {
out << std::endl;
out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
out << " Multi-objective Query " << std::endl;
out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
out << std::endl;
out << "Original Formula: " << std::endl;
out << "--------------------------------------------------------------" << std::endl;
out << "\t" << originalFormula << std::endl;
out << std::endl;
out << "Objectives:" << std::endl;
out << "--------------------------------------------------------------" << std::endl;
for (auto const& obj : objectives) {
obj.printToStream(out);
}
out << "--------------------------------------------------------------" << std::endl;
out << std::endl;
out << "Original Model Information:" << std::endl;
originalModel.printModelInformationToStream(out);
out << std::endl;
out << "Preprocessed Model Information:" << std::endl;
preprocessedModel.printModelInformationToStream(out);
out << std::endl;
out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
}
friend std::ostream& operator<<(std::ostream& out, SparseCbPreprocessorReturnType<SparseModelType> const& ret) {
ret.printToStream(out);
return out;
}
};
}
}
}

131
src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h
View File

@ -0,0 +1,131 @@
#pragma once
#include <boost/optional.hpp>
#include <memory>
#include "storm/logic/Formula.h"
#include "storm/logic/Bound.h"
#include "storm/solver/OptimizationDirection.h"
#include "storm/modelchecker/multiobjective/Objective.h"
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/MarkovAutomaton.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/utility/vector.h"
namespace storm {
namespace modelchecker {
namespace multiobjective {
template <typename SparseModelType>
class SparseMultiObjectivePreprocessorTask {
public:
SparseMultiObjectivePreprocessorTask(std::shared_ptr<Objective<typename SparseModelType::ValueType>> const& objective) : objective(objective) {
// intentionally left empty
}
virtual void perform(SparseModelType& preprocessedModel) const = 0;
virtual bool requiresEndComponentAnalysis() const {
return false;
}
protected:
std::shared_ptr<Objective<typename SparseModelType::ValueType>> objective;
};
// Transforms reachability probabilities to total expected rewards by adding a rewardModel
// such that one reward is given whenever a goal state is reached from a relevant state
template <typename SparseModelType>
class SparseMultiObjectivePreprocessorReachProbToTotalRewTask : public SparseMultiObjectivePreprocessorTask<SparseModelType> {
public:
SparseMultiObjectivePreprocessorReachProbToTotalRewTask(std::shared_ptr<Objective<typename SparseModelType::ValueType>> const& objective, std::shared_ptr<storm::logic::Formula const> const& relevantStateFormula, std::shared_ptr<storm::logic::Formula const> const& goalStateFormula) : SparseMultiObjectivePreprocessorTask<SparseModelType>(objective), relevantStateFormula(relevantStateFormula), goalStateFormula(goalStateFormula) {
// Intentionally left empty
}
virtual void perform(SparseModelType& preprocessedModel) const override {
// build stateAction reward vector that gives (one*transitionProbability) reward whenever a transition leads from a relevantState to a goalState
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(preprocessedModel);
storm::storage::BitVector relevantStates = mc.check(*relevantStateFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
storm::storage::BitVector goalStates = mc.check(*goalStateFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
std::vector<typename SparseModelType::ValueType> objectiveRewards(preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero<typename SparseModelType::ValueType>());
for (auto const& state : relevantStates) {
for (uint_fast64_t row = preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; row < preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++row) {
objectiveRewards[row] = preprocessedModel.getTransitionMatrix().getConstrainedRowSum(row, goalStates);
}
}
STORM_LOG_ASSERT(this->objective->rewardModelName.is_initialized(), "No reward model name has been specified");
preprocessedModel.addRewardModel(this->objective->rewardModelName.get(), typename SparseModelType::RewardModelType(boost::none, std::move(objectiveRewards)));
}
private:
std::shared_ptr<storm::logic::Formula const> relevantStateFormula;
std::shared_ptr<storm::logic::Formula const> goalStateFormula;
};
// Transforms expected reachability rewards to total expected rewards by adding a rewardModel
// such that non-relevant states get reward zero
template <typename SparseModelType>
class SparseMultiObjectivePreprocessorReachRewToTotalRewTask : public SparseMultiObjectivePreprocessorTask<SparseModelType> {
public:
SparseMultiObjectivePreprocessorReachRewToTotalRewTask(std::shared_ptr<Objective<typename SparseModelType::ValueType>> const& objective, std::shared_ptr<storm::logic::Formula const> const& relevantStateFormula, std::string const& originalRewardModelName) : SparseMultiObjectivePreprocessorTask<SparseModelType>(objective), relevantStateFormula(relevantStateFormula), originalRewardModelName(originalRewardModelName) {
// Intentionally left empty
}
virtual void perform(SparseModelType& preprocessedModel) const override {
// build stateAction reward vector that only gives reward for relevant states
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(preprocessedModel);
storm::storage::BitVector nonRelevantStates = ~mc.check(*relevantStateFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
typename SparseModelType::RewardModelType objectiveRewards = preprocessedModel.getRewardModel(originalRewardModelName);
objectiveRewards.reduceToStateBasedRewards(preprocessedModel.getTransitionMatrix(), false);
if (objectiveRewards.hasStateRewards()) {
storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), nonRelevantStates, storm::utility::zero<typename SparseModelType::ValueType>());
}
if (objectiveRewards.hasStateActionRewards()) {
for (auto state : nonRelevantStates) {
std::fill_n(objectiveRewards.getStateActionRewardVector().begin() + preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state], preprocessedModel.getTransitionMatrix().getRowGroupSize(state), storm::utility::zero<typename SparseModelType::ValueType>());
}
}
STORM_LOG_ASSERT(this->objective->rewardModelName.is_initialized(), "No reward model name has been specified");
preprocessedModel.addRewardModel(this->objective->rewardModelName.get(), std::move(objectiveRewards));
}
private:
std::shared_ptr<storm::logic::Formula const> relevantStateFormula;
std::string originalRewardModelName;
};
// Transforms expected reachability time to total expected rewards by adding a rewardModel
// such that every time step done from a relevant state yields one reward
template <typename SparseModelType>
class SparseMultiObjectivePreprocessorReachTimeToTotalRewTask : public SparseMultiObjectivePreprocessorTask<SparseModelType> {
public:
SparseMultiObjectivePreprocessorReachTimeToTotalRewTask(std::shared_ptr<Objective<typename SparseModelType::ValueType>> const& objective, std::shared_ptr<storm::logic::Formula const> const& relevantStateFormula) : SparseMultiObjectivePreprocessorTask<SparseModelType>(objective), relevantStateFormula(relevantStateFormula) {
// Intentionally left empty
}
virtual void perform(SparseModelType& preprocessedModel) const override {
// build stateAction reward vector that only gives reward for relevant states
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(preprocessedModel);
storm::storage::BitVector relevantStates = mc.check(*relevantStateFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
std::vector<typename SparseModelType::ValueType> timeRewards(preprocessedModel.getNumberOfStates(), storm::utility::zero<typename SparseModelType::ValueType>());
storm::utility::vector::setVectorValues(timeRewards, dynamic_cast<storm::models::sparse::MarkovAutomaton<typename SparseModelType::ValueType> const&>(preprocessedModel).getMarkovianStates() & relevantStates, storm::utility::one<typename SparseModelType::ValueType>());
STORM_LOG_ASSERT(this->objective->rewardModelName.is_initialized(), "No reward model name has been specified");
preprocessedModel.addRewardModel(this->objective->rewardModelName.get(), typename SparseModelType::RewardModelType(std::move(timeRewards)));
}
private:
std::shared_ptr<storm::logic::Formula const> relevantStateFormula;
};
}
}
}
Write Preview
Loading…
Cancel
Save