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

Multi-objective model checking: adapted data structures to allow more general objectives

main
TimQu 8 years ago
parent
d35a5e4bdd
commit
defcd7d5d7
11 changed files with 260 additions and 284 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. 48
      src/storm/modelchecker/multiobjective/Objective.h
  2. 190
      src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp
  3. 19
      src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h
  4. 16
      src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h
  5. 14
      src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp
  6. 34
      src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp
  7. 31
      src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp
  8. 13
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp
  9. 18
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp
  10. 6
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp
  11. 35
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp

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

@ -13,57 +13,27 @@ namespace storm {
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;
// The preprocessed (simplified) formula
std::shared_ptr<storm::logic::OperatorFormula const> formula;
// 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/reward bouds
boost::optional<storm::logic::TimeBound> lowerTimeBound, upperTimeBound;
boost::optional<storm::logic::TimeBoundReference> timeBoundReference;
// Limitations for the quantitative objective value (e.g. 0 <= value <= 1 for probabilities).
// Can be used to guide the underlying solver
boost::optional<ValueType> lowerResultBound, upperResultBound;
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 << "Original: " << *originalFormula;
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: ";
if (rewardModelName) {
out << *rewardModelName;
} else {
out << " -none- ";
out << "Preprocessed: " << *formula;
if (considersComplementaryEvent) {
out << " (Complementary event)";
}
out << " \t";
out << "result bounds: ";

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

@ -113,80 +113,81 @@ namespace storm {
Objective<ValueType>& objective = *data.objectives.back();
objective.considersComplementaryEvent = false;
// Check whether the complementary event is considered
objective.considersComplementaryEvent = formula.isProbabilityOperatorFormula() && formula.getSubformula().isGloballyFormula();
storm::logic::OperatorInformation opInfo;
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)
opInfo.bound = formula.getBound();
// Invert the bound (if necessary)
if (objective.considersComplementaryEvent) {
if (objective.bound) {
objective.bound->threshold = objective.bound->threshold.getManager().rational(storm::utility::one<storm::RationalNumber>()) - objective.bound->threshold;
switch (objective.bound->comparisonType) {
opInfo.bound->threshold = opInfo.bound->threshold.getManager().rational(storm::utility::one<storm::RationalNumber>()) - opInfo.bound->threshold;
switch (opInfo.bound->comparisonType) {
case storm::logic::ComparisonType::Greater:
objective.bound->comparisonType = storm::logic::ComparisonType::Less;
opInfo.bound->comparisonType = storm::logic::ComparisonType::Less;
break;
case storm::logic::ComparisonType::GreaterEqual:
objective.bound->comparisonType = storm::logic::ComparisonType::LessEqual;
opInfo.bound->comparisonType = storm::logic::ComparisonType::LessEqual;
break;
case storm::logic::ComparisonType::Less:
objective.bound->comparisonType = storm::logic::ComparisonType::Greater;
opInfo.bound->comparisonType = storm::logic::ComparisonType::Greater;
break;
case storm::logic::ComparisonType::LessEqual:
objective.bound->comparisonType = storm::logic::ComparisonType::GreaterEqual;
opInfo.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);
if (storm::logic::isLowerBound(opInfo.bound->comparisonType)) {
opInfo.optimalityType = storm::solver::OptimizationDirection::Maximize;
} else {
opInfo.optimalityType = storm::solver::OptimizationDirection::Minimize;
}
STORM_LOG_WARN_COND(!formula.hasOptimalityType(), "Optimization direction of formula " << formula << " ignored as the formula also specifies a threshold.");
} else if (formula.hasOptimalityType()){
opInfo.optimalityType = formula.getOptimalityType();
// Invert the optimality type (if necessary)
if (objective.considersComplementaryEvent) {
opInfo.optimalityType = storm::solver::invert(opInfo.optimalityType.get());
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Objective " << formula << " does not specify whether to minimize or maximize");
}
if (formula.isProbabilityOperatorFormula()){
preprocessProbabilityOperatorFormula(formula.asProbabilityOperatorFormula(), opInfo, data);
} else if (formula.isRewardOperatorFormula()){
preprocessRewardOperatorFormula(formula.asRewardOperatorFormula(), opInfo, data);
} else if (formula.isTimeOperatorFormula()){
preprocessTimeOperatorFormula(formula.asTimeOperatorFormula(), opInfo, data);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the objective " << formula << " because it is not supported");
}
}
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, PreprocessorData& data) {
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) {
// Probabilities are between zero and one
data.objectives.back()->lowerResultBound = storm::utility::zero<ValueType>();
data.objectives.back()->upperResultBound = storm::utility::one<ValueType>();
if (formula.getSubformula().isUntilFormula()){
preprocessUntilFormula(formula.getSubformula().asUntilFormula(), data);
preprocessUntilFormula(formula.getSubformula().asUntilFormula(), opInfo, data);
} else if (formula.getSubformula().isBoundedUntilFormula()){
preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), data);
preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), opInfo, data);
} else if (formula.getSubformula().isGloballyFormula()){
preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), data);
preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), opInfo, data);
} else if (formula.getSubformula().isEventuallyFormula()){
preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data);
preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), opInfo, 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) {
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, 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.");
@ -203,43 +204,39 @@ namespace storm {
data.objectives.back()->lowerResultBound = storm::utility::zero<ValueType>();
if (formula.getSubformula().isEventuallyFormula()){
preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data, rewardModelName);
preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), opInfo, data, rewardModelName);
} else if (formula.getSubformula().isCumulativeRewardFormula()) {
preprocessCumulativeRewardFormula(formula.getSubformula().asCumulativeRewardFormula(), data, rewardModelName);
preprocessCumulativeRewardFormula(formula.getSubformula().asCumulativeRewardFormula(), opInfo, data, rewardModelName);
} else if (formula.getSubformula().isTotalRewardFormula()) {
preprocessTotalRewardFormula(data, rewardModelName);
preprocessTotalRewardFormula(opInfo, 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) {
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, 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.");
data.objectives.back()->lowerResultBound = storm::utility::zero<ValueType>();
if (formula.getSubformula().isEventuallyFormula()){
preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data);
preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), opInfo, 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) {
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessUntilFormula(storm::logic::UntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, std::shared_ptr<storm::logic::Formula const> subformula) {
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(data.originalModel);
storm::storage::BitVector rightSubformulaResult = mc.check(formula.getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
storm::storage::BitVector leftSubformulaResult = mc.check(formula.getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
// 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) {
if (!(data.originalModel.getInitialStates() & rightSubformulaResult).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.");
}
}
STORM_LOG_THROW((data.originalModel.getInitialStates() & rightSubformulaResult).empty(), 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<ValueType, RewardModelType> builder(2, data.originalModel);
@ -255,7 +252,11 @@ namespace storm {
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());
std::string rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size());
if (subformula == nullptr) {
subformula = std::make_shared<storm::logic::TotalRewardFormula>();
}
data.objectives.back()->formula = std::make_shared<storm::logic::RewardOperatorFormula>(subformula, rewardModelName, opInfo);
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()));
@ -263,38 +264,37 @@ namespace storm {
}
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data) {
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());
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) {
// Check how to handle this query
if (!formula.getTimeBoundReference().isRewardBound() && (!formula.hasLowerBound() || (!formula.isLowerBoundStrict() && storm::utility::isZero(formula.template getLowerBound<storm::RationalNumber>())))) {
std::shared_ptr<storm::logic::Formula const> subformula;
if (!formula.hasUpperBound()) {
// The formula is actually unbounded
subformula = std::make_shared<storm::logic::TotalRewardFormula>();
} else {
STORM_LOG_THROW(!data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || formula.getTimeBoundReference().isTimeBound(), storm::exceptions::InvalidPropertyException, "Bounded until formulas for Markov Automata are only allowed when time bounds are considered.");
storm::logic::TimeBound bound(formula.isUpperBoundStrict(), formula.getUpperBound());
subformula = std::make_shared<storm::logic::CumulativeRewardFormula>(bound, formula.getTimeBoundReference().getType());
}
preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), opInfo, data, subformula);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Property " << formula << "is not supported");
}
data.objectives.back()->timeBoundReference = formula.getTimeBoundReference();
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;
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) {
// The formula is transformed to an until formula for the complementary event.
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);
preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), negatedSubformula), opInfo, data);
}
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, PreprocessorData& data, boost::optional<std::string> const& optionalRewardModelName) {
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional<std::string> const& optionalRewardModelName) {
if (formula.isReachabilityProbabilityFormula()){
preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), data);
preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), opInfo, data);
return;
}
@ -318,7 +318,9 @@ namespace storm {
auto relevantStatesFormula = std::make_shared<storm::logic::AtomicLabelFormula>(relevantStatesLabel);
data.objectives.back()->rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size());
std::string auxRewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size());
auto totalRewardFormula = std::make_shared<storm::logic::TotalRewardFormula>();
data.objectives.back()->formula = std::make_shared<storm::logic::RewardOperatorFormula>(totalRewardFormula, auxRewardModelName, opInfo);
data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true);
if (formula.isReachabilityRewardFormula()) {
@ -334,23 +336,19 @@ namespace storm {
}
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, boost::optional<std::string> const& optionalRewardModelName) {
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, storm::logic::OperatorInformation const& opInfo, 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());
}
assert(optionalRewardModelName.is_initialized());
data.objectives.back()->rewardModelName = *optionalRewardModelName;
storm::logic::TimeBound bound(formula.isBoundStrict(), formula.getBound());
auto cumulativeRewardFormula = std::make_shared<storm::logic::CumulativeRewardFormula>(bound, storm::logic::TimeBoundType::Steps);
data.objectives.back()->formula = std::make_shared<storm::logic::RewardOperatorFormula>(cumulativeRewardFormula, *optionalRewardModelName, opInfo);
}
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessTotalRewardFormula(PreprocessorData& data, boost::optional<std::string> const& optionalRewardModelName) {
assert(optionalRewardModelName.is_initialized());
data.objectives.back()->rewardModelName = *optionalRewardModelName;
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessTotalRewardFormula(storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional<std::string> const& optionalRewardModelName) {
auto totalRewardFormula = std::make_shared<storm::logic::TotalRewardFormula>();
data.objectives.back()->formula = std::make_shared<storm::logic::RewardOperatorFormula>(totalRewardFormula, *optionalRewardModelName, opInfo);
data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true);
}
@ -372,9 +370,10 @@ namespace storm {
std::set<std::string> relevantRewardModels;
for (auto const& obj : result.objectives) {
relevantRewardModels.insert(*obj.rewardModelName);
if (obj.timeBoundReference && obj.timeBoundReference->isRewardBound()) {
relevantRewardModels.insert(obj.timeBoundReference->getRewardName());
if (obj.formula->isRewardOperatorFormula()) {
relevantRewardModels.insert(obj.formula->asRewardOperatorFormula().getRewardModelName());
} else {
STORM_LOG_ASSERT(false, "Unknown formula type.");
}
}
@ -407,7 +406,7 @@ namespace storm {
typename SparseMultiObjectivePreprocessor<SparseModelType>::ReturnType::QueryType SparseMultiObjectivePreprocessor<SparseModelType>::getQueryType(std::vector<Objective<ValueType>> const& objectives) {
uint_fast64_t numOfObjectivesWithThreshold = 0;
for (auto& obj : objectives) {
if (obj.bound) {
if (obj.formula->hasBound()) {
++numOfObjectivesWithThreshold;
}
}
@ -434,8 +433,12 @@ namespace storm {
// 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);
if (obj.formula->isRewardOperatorFormula()) {
auto const& rewModel = result.preprocessedModel->getRewardModel(obj.formula->asRewardOperatorFormula().getRewardModelName());
zeroRewardChoices &= rewModel.getChoicesWithZeroReward(transitions);
} else {
STORM_LOG_ASSERT(false, "Unknown formula type.");
}
}
// Get the states that have reward for at least one (or for all) choices assigned to it.
@ -476,8 +479,9 @@ namespace storm {
storm::storage::BitVector maxRewardsToCheck(result.preprocessedModel->getNumberOfChoices(), true);
bool hasMinRewardToCheck = false;
for (auto const& objIndex : finiteRewardCheckObjectives) {
auto const& rewModel = result.preprocessedModel->getRewardModel(result.objectives[objIndex].rewardModelName.get());
if (storm::solver::minimize(result.objectives[objIndex].optimizationDirection)) {
STORM_LOG_ASSERT(result.objectives[objIndex].formula->isRewardOperatorFormula(), "Objective needs to be checked for finite reward but has no reward operator.");
auto const& rewModel = result.preprocessedModel->getRewardModel(result.objectives[objIndex].formula->asRewardOperatorFormula().getRewardModelName());
if (storm::solver::minimize(result.objectives[objIndex].formula->getOptimalityType())) {
hasMinRewardToCheck = true;
} else {
maxRewardsToCheck &= rewModel.getChoicesWithZeroReward(transitions);

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

@ -50,19 +50,20 @@ namespace storm {
/*!
* Apply the neccessary preprocessing for the given formula.
* @param formula the current (sub)formula
* @param opInfo the information of the resulting operator 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.
static void preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data);
static void preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data);
static void preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data);
static void preprocessUntilFormula(storm::logic::UntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, std::shared_ptr<storm::logic::Formula const> subformula = nullptr);
static void preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data);
static void preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data);
static void preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional<std::string> const& optionalRewardModelName = boost::none);
static void preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional<std::string> const& optionalRewardModelName = boost::none);
static void preprocessTotalRewardFormula(storm::logic::OperatorInformation const& opInfo, 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.
/*!

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

@ -58,8 +58,9 @@ namespace storm {
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)));
STORM_LOG_ASSERT(this->objective->formula->isRewardOperatorFormula(), "No reward operator formula.");
STORM_LOG_ASSERT(this->objective->formula->asRewardOperatorFormula().hasRewardModelName(), "No reward model name has been specified");
preprocessedModel.addRewardModel(this->objective->formula->asRewardOperatorFormula().getRewardModelName(), typename SparseModelType::RewardModelType(boost::none, std::move(objectiveRewards)));
}
private:
@ -91,8 +92,9 @@ namespace storm {
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));
STORM_LOG_ASSERT(this->objective->formula->isRewardOperatorFormula(), "No reward operator formula.");
STORM_LOG_ASSERT(this->objective->formula->asRewardOperatorFormula().hasRewardModelName(), "No reward model name has been specified");
preprocessedModel.addRewardModel(this->objective->formula->asRewardOperatorFormula().getRewardModelName(), std::move(objectiveRewards));
}
private:
@ -117,8 +119,10 @@ namespace storm {
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)));
STORM_LOG_ASSERT(this->objective->formula->isRewardOperatorFormula(), "No reward operator formula.");
STORM_LOG_ASSERT(this->objective->formula->asRewardOperatorFormula().hasRewardModelName(), "No reward model name has been specified");
preprocessedModel.addRewardModel(this->objective->formula->asRewardOperatorFormula().getRewardModelName(), typename SparseModelType::RewardModelType(std::move(timeRewards)));
}
private:

14
src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp
View File

@ -134,10 +134,10 @@ namespace storm {
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_LOG_THROW(obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isTotalRewardFormula(), storm::exceptions::InvalidOperationException, "Constraint-based solver only supports total-reward objectives. Got " << *obj.formula << " instead.");
STORM_LOG_THROW(obj.formula->hasBound(), storm::exceptions::InvalidOperationException, "Invoked achievability query but no bound was specified for at least one objective.");
STORM_LOG_THROW(obj.formula->asRewardOperatorFormula().hasRewardModelName(), storm::exceptions::InvalidOperationException, "Expected reward operator with a reward model name. Got " << *obj.formula << " instead.");
std::vector<ValueType> rewards = getActionBasedExpectedRewards(obj.formula->asRewardOperatorFormula().getRewardModelName());
storm::expressions::Expression objValue = zero;
for (uint_fast64_t choice = 0; choice < rewards.size(); ++choice) {
if (!storm::utility::isZero(rewards[choice])) {
@ -145,9 +145,8 @@ namespace storm {
}
}
// 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) {
storm::expressions::Expression threshold = this->expressionManager->rational(obj.formula->getThreshold().evaluateAsRational());
switch (obj.formula->getBound().comparisonType) {
case storm::logic::ComparisonType::Greater:
solver->add( objValue > threshold);
break;
@ -165,7 +164,6 @@ namespace storm {
}
}
}
}
template <>
std::vector<double> SparseCbAchievabilityQuery<storm::models::sparse::Mdp<double>>::getActionBasedExpectedRewards(std::string const& rewardModelName) const {

34
src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp
View File

@ -8,9 +8,11 @@
#include "storm/utility/macros.h"
#include "storm/utility/vector.h"
#include "storm/solver/GmmxxLinearEquationSolver.h"
#include "storm/logic/Formulas.h"
#include "storm/exceptions/InvalidOperationException.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/UnexpectedException.h"
namespace storm {
namespace modelchecker {
@ -26,7 +28,11 @@ namespace storm {
// Set the (discretized) state action rewards.
this->discreteActionRewards.resize(objectives.size());
for (auto objIndex : this->objectivesWithNoUpperTimeBound) {
typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(*this->objectives[objIndex].rewardModelName);
auto const& formula = *objectives[objIndex].formula;
STORM_LOG_THROW(formula.isRewardOperatorFormula() && formula.asRewardOperatorFormula().hasRewardModelName(), storm::exceptions::UnexpectedException, "Unexpected type of operator formula: " << formula);
STORM_LOG_THROW(formula.getSubformula().isTotalRewardFormula() || (formula.getSubformula().isCumulativeRewardFormula() && formula.getSubformula().asCumulativeRewardFormula().isTimeBounded()), storm::exceptions::UnexpectedException, "Unexpected type of sub-formula: " << formula.getSubformula());
STORM_LOG_WARN_COND(!formula.getSubformula().isCumulativeRewardFormula() || (objectives[objIndex].originalFormula->isProbabilityOperatorFormula() && objectives[objIndex].originalFormula->asProbabilityOperatorFormula().getSubformula().isBoundedUntilFormula()), "Objective " << objectives[objIndex].originalFormula << " was simplified to a cumulative reward formula. Correctness of the algorithm is unknown for this type of property.");
typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(formula.asRewardOperatorFormula().getRewardModelName());
STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected.");
this->discreteActionRewards[objIndex] = rewModel.hasStateActionRewards() ? rewModel.getStateActionRewardVector() : std::vector<ValueType>(this->model.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>());
if (rewModel.hasStateRewards()) {
@ -41,10 +47,6 @@ namespace storm {
template <class SparseMaModelType>
void SparseMaPcaaWeightVectorChecker<SparseMaModelType>::boundedPhase(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) {
for (auto const& obj : this->objectives) {
STORM_LOG_THROW(!obj.timeBoundReference || obj.timeBoundReference->isTimeBound(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking of Markov automata is only supported for time-bounded formulass.");
}
// Split the preprocessed model into transitions from/to probabilistic/Markovian states.
SubModel MS = createSubModel(true, weightedRewardVector);
SubModel PS = createSubModel(false, weightedRewardVector);
@ -124,7 +126,7 @@ namespace storm {
if (this->objectivesWithNoUpperTimeBound.get(objIndex)) {
storm::utility::vector::selectVectorValues(objVector, result.choices, this->discreteActionRewards[objIndex]);
} else {
typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(*this->objectives[objIndex].rewardModelName);
typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(this->objectives[objIndex].formula->asRewardOperatorFormula().getRewardModelName());
STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected.");
STORM_LOG_ASSERT(!rewModel.hasStateRewards(), "State rewards for bounded objectives for MAs are not expected (bounded rewards are not supported).");
if (rewModel.hasStateActionRewards()) {
@ -164,10 +166,9 @@ namespace storm {
std::vector<VT> eToPowerOfMinusMaxRateTimesBound;
VT smallestNonZeroBound = storm::utility::zero<VT>();
for (auto const& obj : this->objectives) {
if(obj.upperTimeBound){
STORM_LOG_THROW(!obj.upperTimeBound->getBound().containsVariables(), storm::exceptions::InvalidOperationException, "The time bound '" << obj.upperTimeBound->getBound() << " contains undefined variables");
timeBounds.push_back(storm::utility::convertNumber<VT>(obj.upperTimeBound->getBound().evaluateAsRational()));
STORM_LOG_ASSERT(!storm::utility::isZero(timeBounds.back()), "Got zero-valued upper time bound.");
if (obj.formula->getSubformula().isCumulativeRewardFormula()) {
timeBounds.push_back(obj.formula->getSubformula().asCumulativeRewardFormula().template getBound<VT>());
STORM_LOG_THROW(!storm::utility::isZero(timeBounds.back()), storm::exceptions::InvalidPropertyException, "Got zero-valued upper time bound. This is not suppoted.");
eToPowerOfMinusMaxRateTimesBound.push_back(std::exp(-maxRate * timeBounds.back()));
smallestNonZeroBound = storm::utility::isZero(smallestNonZeroBound) ? timeBounds.back() : std::min(smallestNonZeroBound, timeBounds.back());
} else {
@ -260,11 +261,10 @@ namespace storm {
VT const maxRate = this->model.getMaximalExitRate();
for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
auto const& obj = this->objectives[objIndex];
STORM_LOG_THROW(!obj.lowerTimeBound, storm::exceptions::InvalidPropertyException, "Lower time bounds are not supported by this model checker");
VT errorTowardsZero = storm::utility::zero<VT>();
VT errorAwayFromZero = storm::utility::zero<VT>();
if(obj.upperTimeBound) {
VT timeBound = storm::utility::convertNumber<VT>(obj.upperTimeBound->getBound().evaluateAsRational());
if (obj.formula->getSubformula().isCumulativeRewardFormula()) {
VT timeBound = obj.formula->getSubformula().asCumulativeRewardFormula().template getBound<VT>();
uint_fast64_t digitizedBound = storm::utility::convertNumber<uint_fast64_t>(timeBound/digitizationConstant);
auto timeBoundIt = upperTimeBounds.insert(std::make_pair(digitizedBound, storm::storage::BitVector(this->objectives.size(), false))).first;
timeBoundIt->second.set(objIndex);
@ -272,7 +272,7 @@ namespace storm {
digitizationError -= std::exp(-maxRate * timeBound) * storm::utility::pow(storm::utility::one<VT>() + maxRate * digitizationConstant, digitizedBound);
errorAwayFromZero += digitizationError;
}
if (storm::solver::maximize(obj.optimizationDirection)) {
if (storm::solver::maximize(obj.formula->getOptimalityType())) {
this->offsetsToUnderApproximation[objIndex] = -errorTowardsZero;
this->offsetsToOverApproximation[objIndex] = errorAwayFromZero;
} else {
@ -328,7 +328,7 @@ namespace storm {
consideredObjectives |= upperTimeBoundIt->second;
for (auto objIndex : upperTimeBoundIt->second) {
// This objective now plays a role in the weighted sum
ValueType factor = storm::solver::minimize(this->objectives[objIndex].optimizationDirection) ? -weightVector[objIndex] : weightVector[objIndex];
ValueType factor = storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType()) ? -weightVector[objIndex] : weightVector[objIndex];
storm::utility::vector::addScaledVector(MS.weightedRewardVector, MS.objectiveRewardVectors[objIndex], factor);
storm::utility::vector::addScaledVector(PS.weightedRewardVector, PS.objectiveRewardVectors[objIndex], factor);
}
@ -349,7 +349,7 @@ namespace storm {
// In this case there is no need to perform the computation on the individual objectives
optimalChoicesAtCurrentEpoch = newChoices;
PS.objectiveSolutionVectors[*consideredObjectives.begin()] = PS.weightedSolutionVector;
if (storm::solver::minimize(this->objectives[*consideredObjectives.begin()].optimizationDirection)) {
if (storm::solver::minimize(this->objectives[*consideredObjectives.begin()].formula->getOptimalityType())) {
storm::utility::vector::scaleVectorInPlace(PS.objectiveSolutionVectors[*consideredObjectives.begin()], -storm::utility::one<ValueType>());
}
} else {
@ -396,7 +396,7 @@ namespace storm {
if (consideredObjectives.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*consideredObjectives.begin()])) {
// In this case there is no need to perform the computation on the individual objectives
MS.objectiveSolutionVectors[*consideredObjectives.begin()] = MS.weightedSolutionVector;
if (storm::solver::minimize(this->objectives[*consideredObjectives.begin()].optimizationDirection)) {
if (storm::solver::minimize(this->objectives[*consideredObjectives.begin()].formula->getOptimalityType())) {
storm::utility::vector::scaleVectorInPlace(MS.objectiveSolutionVectors[*consideredObjectives.begin()], -storm::utility::one<ValueType>());
}
} else {

31
src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp
View File

@ -5,6 +5,7 @@
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/utility/macros.h"
#include "storm/utility/vector.h"
#include "storm/logic/Formulas.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/IllegalArgumentException.h"
#include "storm/exceptions/NotSupportedException.h"
@ -21,24 +22,22 @@ namespace storm {
storm::storage::BitVector const& possibleECActions,
storm::storage::BitVector const& possibleBottomStates) :
SparsePcaaWeightVectorChecker<SparseMdpModelType>(model, objectives, possibleECActions, possibleBottomStates) {
// set the state action rewards
// set the state action rewards. Also do some sanity checks on the objectives.
for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
typename SparseMdpModelType::RewardModelType const& rewModel = this->model.getRewardModel(*this->objectives[objIndex].rewardModelName);
STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Reward model has transition rewards which is not expected.");
auto const& formula = *objectives[objIndex].formula;
STORM_LOG_THROW(formula.isRewardOperatorFormula() && formula.asRewardOperatorFormula().hasRewardModelName(), storm::exceptions::UnexpectedException, "Unexpected type of operator formula: " << formula);
STORM_LOG_THROW(formula.getSubformula().isCumulativeRewardFormula() || formula.getSubformula().isTotalRewardFormula(), storm::exceptions::UnexpectedException, "Unexpected type of sub-formula: " << formula.getSubformula());
typename SparseMdpModelType::RewardModelType const& rewModel = this->model.getRewardModel(formula.asRewardOperatorFormula().getRewardModelName());
STORM_LOG_THROW(!rewModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Reward model has transition rewards which is not expected.");
this->discreteActionRewards[objIndex] = rewModel.getTotalRewardVector(this->model.getTransitionMatrix());
}
}
template <class SparseMdpModelType>
void SparseMdpPcaaWeightVectorChecker<SparseMdpModelType>::boundedPhase(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) {
// Check whether reward bounded objectives occur.
// Currently, only step bounds are considered.
// TODO: Check whether reward bounded objectives occur.
bool containsRewardBoundedObjectives = false;
for (auto const& obj : this->objectives) {
if (obj.timeBoundReference && obj.timeBoundReference->isRewardBound()) {
containsRewardBoundedObjectives = true;
break;
}
}
if (containsRewardBoundedObjectives) {
boundedPhaseWithRewardBounds(weightVector, weightedRewardVector);
@ -56,12 +55,10 @@ namespace storm {
// Get for each occurring timeBound the indices of the objectives with that bound.
std::map<uint_fast64_t, storm::storage::BitVector, std::greater<uint_fast64_t>> stepBounds;
for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
auto const& obj = this->objectives[objIndex];
STORM_LOG_THROW(!obj.lowerTimeBound, storm::exceptions::InvalidPropertyException, "Lower step bounds are not supported by this model checker");
if (obj.upperTimeBound) {
STORM_LOG_THROW(!obj.upperTimeBound->getBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The step bound '" << obj.upperTimeBound->getBound() << " contains undefined variables");
uint_fast64_t stepBound = (uint_fast64_t) obj.upperTimeBound->getBound().evaluateAsInt();
if (obj.upperTimeBound->isStrict()) {
if (this->objectives[objIndex].formula->getSubformula().isCumulativeRewardFormula()) {
auto const& subformula = this->objectives[objIndex].formula->getSubformula().asCumulativeRewardFormula();
uint_fast64_t stepBound = subformula.template getBound<uint_fast64_t>();
if (subformula.isBoundStrict()) {
--stepBound;
}
auto stepBoundIt = stepBounds.insert(std::make_pair(stepBound, storm::storage::BitVector(this->objectives.size(), false))).first;
@ -85,7 +82,7 @@ namespace storm {
consideredObjectives |= stepBoundIt->second;
for(auto objIndex : stepBoundIt->second) {
// This objective now plays a role in the weighted sum
ValueType factor = storm::solver::minimize(this->objectives[objIndex].optimizationDirection) ? -weightVector[objIndex] : weightVector[objIndex];
ValueType factor = storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType()) ? -weightVector[objIndex] : weightVector[objIndex];
storm::utility::vector::addScaledVector(weightedRewardVector, this->discreteActionRewards[objIndex], factor);
}
++stepBoundIt;

13
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp
View File

@ -32,17 +32,16 @@ namespace storm {
thresholds.reserve(this->objectives.size());
strictThresholds = storm::storage::BitVector(this->objectives.size(), false);
for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
auto const& obj = this->objectives[objIndex];
STORM_LOG_ASSERT(obj.bound.is_initialized(), "Achievability query invoked but there is an objective without bound.");
STORM_LOG_THROW(!obj.bound->threshold.containsVariables(), storm::exceptions::InvalidOperationException, "There is an objective whose bound contains undefined variables.");
thresholds.push_back(storm::utility::convertNumber<GeometryValueType>(obj.bound->threshold.evaluateAsRational()));
if (storm::solver::minimize(obj.optimizationDirection)) {
STORM_LOG_ASSERT(!storm::logic::isLowerBound(obj.bound->comparisonType), "Minimizing objective should not specify an upper bound.");
auto const& formula = *this->objectives[objIndex].formula;
STORM_LOG_ASSERT(formula.hasBound(), "Achievability query invoked but there is an objective without bound.");
thresholds.push_back(formula.template getThresholdAs<GeometryValueType>());
if (storm::solver::minimize(formula.getOptimalityType())) {
STORM_LOG_ASSERT(!storm::logic::isLowerBound(formula.getBound().comparisonType), "Minimizing objective should not specify an upper bound.");
// Values for minimizing objectives will be negated in order to convert them to maximizing objectives.
// Hence, we also negate the threshold
thresholds.back() *= -storm::utility::one<GeometryValueType>();
}
strictThresholds.set(objIndex, storm::logic::isStrict(obj.bound->comparisonType));
strictThresholds.set(objIndex, storm::logic::isStrict(formula.getBound().comparisonType));
}
}

18
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp
View File

@ -24,7 +24,7 @@ namespace storm {
STORM_LOG_ASSERT(preprocessorResult.queryType == SparseMultiObjectivePreprocessorReturnType<SparseModelType>::QueryType::Quantitative, "Invalid query Type");
for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
if (!this->objectives[objIndex].bound.is_initialized()) {
if (!this->objectives[objIndex].formula->hasBound()) {
indexOfOptimizingObjective = objIndex;
break;
}
@ -43,17 +43,17 @@ namespace storm {
std::vector<storm::storage::geometry::Halfspace<GeometryValueType>> thresholdConstraints;
thresholdConstraints.reserve(this->objectives.size() - 1);
for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
auto const& obj = this->objectives[objIndex];
if (obj.bound) {
STORM_LOG_THROW(!obj.bound->threshold.containsVariables(), storm::exceptions::InvalidOperationException, "There is an objective whose bound contains undefined variables.");
thresholds.push_back(storm::utility::convertNumber<GeometryValueType>(obj.bound->threshold.evaluateAsRational()));
if (storm::solver::minimize(obj.optimizationDirection)) {
STORM_LOG_ASSERT(!storm::logic::isLowerBound(obj.bound->comparisonType), "Minimizing objective should not specify an upper bound.");
auto const& formula = *this->objectives[objIndex].formula;
if (formula.hasBound()) {
thresholds.push_back(formula.template getThresholdAs<GeometryValueType>());
if (storm::solver::minimize(formula.getOptimalityType())) {
STORM_LOG_ASSERT(!storm::logic::isLowerBound(formula.getBound().comparisonType), "Minimizing objective should not specify an upper bound.");
// Values for minimizing objectives will be negated in order to convert them to maximizing objectives.
// Hence, we also negate the threshold
thresholds.back() *= -storm::utility::one<GeometryValueType>();
}
strictThresholds.set(objIndex, storm::logic::isStrict(obj.bound->comparisonType));
strictThresholds.set(objIndex, storm::logic::isStrict(formula.getBound().comparisonType));
WeightVector normalVector(this->objectives.size(), storm::utility::zero<GeometryValueType>());
normalVector[objIndex] = -storm::utility::one<GeometryValueType>();
thresholdConstraints.emplace_back(std::move(normalVector), -thresholds.back());
@ -74,7 +74,7 @@ namespace storm {
// transform the obtained result for the preprocessed model to a result w.r.t. the original model and return the checkresult
auto const& obj = this->objectives[indexOfOptimizingObjective];
if (storm::solver::maximize(obj.optimizationDirection)) {
if (storm::solver::maximize(obj.formula->getOptimalityType())) {
if (obj.considersComplementaryEvent) {
result = storm::utility::one<GeometryValueType>() - result;
}

6
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp
View File

@ -107,7 +107,7 @@ namespace storm {
step.upperBoundPoint = storm::utility::vector::convertNumericVector<GeometryValueType>(weightVectorChecker->getOverApproximationOfInitialStateResults());
// For the minimizing objectives, we need to scale the corresponding entries with -1 as we want to consider the downward closure
for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
if (storm::solver::minimize(this->objectives[objIndex].optimizationDirection)) {
if (storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) {
step.lowerBoundPoint[objIndex] *= -storm::utility::one<GeometryValueType>();
step.upperBoundPoint[objIndex] *= -storm::utility::one<GeometryValueType>();
}
@ -161,7 +161,7 @@ namespace storm {
result.reserve(point.size());
for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
auto const& obj = this->objectives[objIndex];
if (storm::solver::maximize(obj.optimizationDirection)) {
if (storm::solver::maximize(obj.formula->getOptimalityType())) {
if (obj.considersComplementaryEvent) {
result.push_back(storm::utility::one<GeometryValueType>() - point[objIndex]);
} else {
@ -192,7 +192,7 @@ namespace storm {
transformationVector.reserve(numObjectives);
for(uint_fast64_t objIndex = 0; objIndex < numObjectives; ++objIndex) {
auto const& obj = this->objectives[objIndex];
if (storm::solver::maximize(obj.optimizationDirection)) {
if (storm::solver::maximize(obj.formula->getOptimalityType())) {
if (obj.considersComplementaryEvent) {
transformationMatrix[objIndex][objIndex] = -storm::utility::one<GeometryValueType>();
transformationVector.push_back(storm::utility::one<GeometryValueType>());

35
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
View File

@ -12,6 +12,7 @@
#include "storm/utility/graph.h"
#include "storm/utility/macros.h"
#include "storm/utility/vector.h"
#include "storm/logic/Formulas.h"
#include "storm/exceptions/IllegalFunctionCallException.h"
#include "storm/exceptions/UnexpectedException.h"
@ -42,10 +43,11 @@ namespace storm {
// set data for unbounded objectives
for(uint_fast64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) {
auto const& obj = objectives[objIndex];
if (!obj.upperTimeBound) {
auto const& formula = *objectives[objIndex].formula;
if (formula.getSubformula().isTotalRewardFormula()) {
objectivesWithNoUpperTimeBound.set(objIndex, true);
actionsWithoutRewardInUnboundedPhase &= model.getRewardModel(*obj.rewardModelName).getChoicesWithZeroReward(model.getTransitionMatrix());
STORM_LOG_ASSERT(formula.isRewardOperatorFormula() && formula.asRewardOperatorFormula().hasRewardModelName(), "Unexpected type of operator formula.");
actionsWithoutRewardInUnboundedPhase &= model.getRewardModel(formula.asRewardOperatorFormula().getRewardModelName()).getChoicesWithZeroReward(model.getTransitionMatrix());
}
}
}
@ -59,26 +61,27 @@ namespace storm {
boost::optional<ValueType> weightedLowerResultBound = storm::utility::zero<ValueType>();
boost::optional<ValueType> weightedUpperResultBound = storm::utility::zero<ValueType>();
for (auto objIndex : objectivesWithNoUpperTimeBound) {
if (storm::solver::minimize(objectives[objIndex].optimizationDirection)) {
if (objectives[objIndex].lowerResultBound && weightedUpperResultBound) {
weightedUpperResultBound.get() -= weightVector[objIndex] * objectives[objIndex].lowerResultBound.get();
auto const& obj = objectives[objIndex];
if (storm::solver::minimize(objectives[objIndex].formula->getOptimalityType())) {
if (obj.lowerResultBound && weightedUpperResultBound) {
weightedUpperResultBound.get() -= weightVector[objIndex] * obj.lowerResultBound.get();
} else {
weightedUpperResultBound = boost::none;
}
if (objectives[objIndex].upperResultBound && weightedLowerResultBound) {
weightedLowerResultBound.get() -= weightVector[objIndex] * objectives[objIndex].upperResultBound.get();
if (obj.upperResultBound && weightedLowerResultBound) {
weightedLowerResultBound.get() -= weightVector[objIndex] * obj.upperResultBound.get();
} else {
weightedLowerResultBound = boost::none;
}
storm::utility::vector::addScaledVector(weightedRewardVector, discreteActionRewards[objIndex], -weightVector[objIndex]);
} else {
if (objectives[objIndex].lowerResultBound && weightedLowerResultBound) {
weightedLowerResultBound.get() += weightVector[objIndex] * objectives[objIndex].lowerResultBound.get();
if (obj.lowerResultBound && weightedLowerResultBound) {
weightedLowerResultBound.get() += weightVector[objIndex] * obj.lowerResultBound.get();
} else {
weightedLowerResultBound = boost::none;
}
if (objectives[objIndex].upperResultBound && weightedUpperResultBound) {
weightedUpperResultBound.get() += weightVector[objIndex] * objectives[objIndex].upperResultBound.get();
if (obj.upperResultBound && weightedUpperResultBound) {
weightedUpperResultBound.get() += weightVector[objIndex] * obj.upperResultBound.get();
} else {
weightedUpperResultBound = boost::none;
}
@ -91,7 +94,7 @@ namespace storm {
unboundedIndividualPhase(weightVector);
// Only invoke boundedPhase if necessarry, i.e., if there is at least one objective with a time bound
for (auto const& obj : this->objectives) {
if(obj.lowerTimeBound || obj.upperTimeBound) {
if (!obj.formula->getSubformula().isTotalRewardFormula()) {
boundedPhase(weightVector, weightedRewardVector);
break;
}
@ -141,7 +144,7 @@ namespace storm {
storm::storage::Scheduler<typename SparsePcaaWeightVectorChecker<SparseModelType>::ValueType> SparsePcaaWeightVectorChecker<SparseModelType>::computeScheduler() const {
STORM_LOG_THROW(this->checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before.");
for (auto const& obj : this->objectives) {
STORM_LOG_THROW(!obj.lowerTimeBound && !obj.upperTimeBound, storm::exceptions::NotImplementedException, "Scheduler retrival is not implemented for timeBounded objectives.");
STORM_LOG_THROW(obj.formula->getSubformula().isTotalRewardFormula(), storm::exceptions::NotImplementedException, "Scheduler retrival is only implemented for objectives without time-bound.");
}
storm::storage::Scheduler<ValueType> result(this->optimalChoices.size());
@ -202,7 +205,7 @@ namespace storm {
if (objectivesWithNoUpperTimeBound.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*objectivesWithNoUpperTimeBound.begin()])) {
uint_fast64_t objIndex = *objectivesWithNoUpperTimeBound.begin();
objectiveResults[objIndex] = weightedResult;
if (storm::solver::minimize(objectives[objIndex].optimizationDirection)) {
if (storm::solver::minimize(objectives[objIndex].formula->getOptimalityType())) {
storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], -storm::utility::one<ValueType>());
}
for (uint_fast64_t objIndex2 = 0; objIndex2 < objectives.size(); ++objIndex2) {
@ -235,7 +238,7 @@ namespace storm {
if (!storm::utility::isZero(weightVector[objIndex])) {
objectiveResults[objIndex] = weightedSumOfUncheckedObjectives;
ValueType scalingFactor = storm::utility::one<ValueType>() / sumOfWeightsOfUncheckedObjectives;
if (storm::solver::minimize(obj.optimizationDirection)) {
if (storm::solver::minimize(obj.formula->getOptimalityType())) {
scalingFactor *= -storm::utility::one<ValueType>();
}
storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], scalingFactor);

Write Preview
Loading…
Cancel
Save