61 changed files with 3155 additions and 1171 deletions
-
6src/storm/cli/cli.cpp
-
36src/storm/cli/entrypoints.h
-
4src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
-
19src/storm/modelchecker/multiobjective/MultiObjectiveModelCheckingMethod.cpp
-
13src/storm/modelchecker/multiobjective/MultiObjectiveModelCheckingMethod.h
-
82src/storm/modelchecker/multiobjective/Objective.h
-
504src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp
-
95src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h
-
43src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h
-
131src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h
-
218src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp
-
63src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h
-
38src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp
-
46src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h
-
122src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp
-
19src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.h
-
88src/storm/modelchecker/multiobjective/pcaa.cpp
-
20src/storm/modelchecker/multiobjective/pcaa.h
-
72src/storm/modelchecker/multiobjective/pcaa/PcaaObjective.h
-
43src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp
-
9src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h
-
30src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp
-
17src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h
-
21src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp
-
2src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h
-
4src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp
-
2src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h
-
416src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp
-
82src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h
-
82src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp
-
2src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h
-
76src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp
-
16src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h
-
147src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
-
65src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h
-
4src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
-
4src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
-
33src/storm/models/sparse/StandardRewardModel.cpp
-
9src/storm/models/sparse/StandardRewardModel.h
-
19src/storm/settings/modules/MultiObjectiveSettings.cpp
-
7src/storm/settings/modules/MultiObjectiveSettings.h
-
6src/storm/storage/SparseMatrix.cpp
-
137src/storm/storage/memorystructure/MemoryStructure.cpp
-
68src/storm/storage/memorystructure/MemoryStructure.h
-
36src/storm/storage/memorystructure/MemoryStructureBuilder.cpp
-
49src/storm/storage/memorystructure/MemoryStructureBuilder.h
-
330src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp
-
72src/storm/storage/memorystructure/SparseModelMemoryProduct.h
-
308src/storm/transformer/GoalStateMerger.cpp
-
41src/storm/transformer/GoalStateMerger.h
-
69src/storm/transformer/SparseParametricDtmcSimplifier.cpp
-
92src/storm/transformer/SparseParametricMdpSimplifier.cpp
-
12src/storm/transformer/SparseParametricModelSimplifier.cpp
-
5src/storm/transformer/SparseParametricModelSimplifier.h
-
195src/storm/utility/graph.cpp
-
17src/storm/utility/graph.h
-
17src/storm/utility/storm.h
-
35src/test/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp
-
28src/test/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp
-
74src/test/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp
-
26src/test/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp
@ -0,0 +1,19 @@ |
|||
#include "storm/modelchecker/multiobjective/MultiObjectiveModelCheckingMethod.h"
|
|||
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace multiobjective { |
|||
|
|||
std::string toString(MultiObjectiveMethod m) { |
|||
switch (m) { |
|||
case MultiObjectiveMethod::Pcaa: |
|||
return "Pareto Curve Approximation Algorithm"; |
|||
case MultiObjectiveMethod::ConstraintBased: |
|||
return "Constraint Based Algorithm"; |
|||
} |
|||
return "invalid"; |
|||
} |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,13 @@ |
|||
#pragma once |
|||
|
|||
#include "storm/utility/ExtendSettingEnumWithSelectionField.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace multiobjective { |
|||
ExtendEnumsWithSelectionField(MultiObjectiveMethod, Pcaa, ConstraintBased) |
|||
} |
|||
} |
|||
} |
|||
|
|||
|
|||
@ -0,0 +1,82 @@ |
|||
#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; |
|||
|
|||
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 << " \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 << " \t"; |
|||
out << "result bounds: "; |
|||
if (lowerResultBound && upperResultBound) { |
|||
out << "[" << *lowerResultBound << ", " << *upperResultBound << "]"; |
|||
} else if (lowerResultBound) { |
|||
out << ">=" << *lowerResultBound; |
|||
} else if (upperResultBound) { |
|||
out << "<=" << *upperResultBound; |
|||
} else { |
|||
out << " -none- "; |
|||
} |
|||
} |
|||
}; |
|||
} |
|||
} |
|||
} |
|||
|
|||
@ -0,0 +1,504 @@ |
|||
#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/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"); |
|||
} |
|||
} |
|||
|
|||
// Incorporate the required memory into the state space
|
|||
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(); |
|||
|
|||
// compute the end components of the model (if required)
|
|||
bool endComponentAnalysisRequired = false; |
|||
for (auto& task : data.tasks) { |
|||
endComponentAnalysisRequired = endComponentAnalysisRequired || task->requiresEndComponentAnalysis(); |
|||
} |
|||
if (endComponentAnalysisRequired) { |
|||
// TODO
|
|||
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "End component analysis required but currently not implemented."); |
|||
} |
|||
|
|||
for (auto& task : data.tasks) { |
|||
task->perform(*preprocessedModel); |
|||
} |
|||
|
|||
// Build the actual result
|
|||
return buildResult(originalModel, originalFormula, data, preprocessedModel, backwardTransitions); |
|||
} |
|||
|
|||
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; |
|||
switch (objective.bound->comparisonType) { |
|||
case storm::logic::ComparisonType::Greater: |
|||
objective.bound->comparisonType = storm::logic::ComparisonType::Less; |
|||
break; |
|||
case storm::logic::ComparisonType::GreaterEqual: |
|||
objective.bound->comparisonType = storm::logic::ComparisonType::LessEqual; |
|||
break; |
|||
case storm::logic::ComparisonType::Less: |
|||
objective.bound->comparisonType = storm::logic::ComparisonType::Greater; |
|||
break; |
|||
case storm::logic::ComparisonType::LessEqual: |
|||
objective.bound->comparisonType = storm::logic::ComparisonType::GreaterEqual; |
|||
break; |
|||
default: |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Current objective " << formula << " has unexpected comparison type"); |
|||
} |
|||
} |
|||
objective.optimizationDirection = storm::solver::invert(objective.optimizationDirection); |
|||
} |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, 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); |
|||
} 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; |
|||
} |
|||
|
|||
data.objectives.back()->lowerResultBound = storm::utility::zero<ValueType>(); |
|||
|
|||
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."); |
|||
|
|||
data.objectives.back()->lowerResultBound = storm::utility::zero<ValueType>(); |
|||
|
|||
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()); |
|||
} |
|||
|
|||
assert(optionalRewardModelName.is_initialized()); |
|||
data.objectives.back()->rewardModelName = *optionalRewardModelName; |
|||
|
|||
} |
|||
|
|||
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> |
|||
typename SparseMultiObjectivePreprocessor<SparseModelType>::ReturnType SparseMultiObjectivePreprocessor<SparseModelType>::buildResult(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula, PreprocessorData& data, std::shared_ptr<SparseModelType> const& preprocessedModel, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) { |
|||
|
|||
ReturnType result(originalFormula, originalModel); |
|||
|
|||
result.preprocessedModel = preprocessedModel; |
|||
|
|||
for (auto& obj : data.objectives) { |
|||
result.objectives.push_back(std::move(*obj)); |
|||
} |
|||
|
|||
result.queryType = getQueryType(result.objectives); |
|||
|
|||
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::storage::BitVector maybeStates = finiteRewardStates & ~zeroRewardStates; |
|||
storm::transformer::GoalStateMerger<SparseModelType> merger(*result.preprocessedModel); |
|||
typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult = merger.mergeTargetAndSinkStates(maybeStates, zeroRewardStates, storm::storage::BitVector(maybeStates.size(), false), std::vector<std::string>(relevantRewardModels.begin(), relevantRewardModels.end())); |
|||
|
|||
result.preprocessedModel = mergerResult.model; |
|||
result.possibleBottomStates = (~minMaxNonZeroRewardStates.first) % maybeStates; |
|||
if (mergerResult.targetState) { |
|||
storm::storage::BitVector targetStateAsVector(result.preprocessedModel->getNumberOfStates(), false); |
|||
targetStateAsVector.set(*mergerResult.targetState, true); |
|||
// The overapproximation for the possible ec choices consists of the states that can reach the target states with prob. 0 and the target state itself.
|
|||
result.possibleECChoices = result.preprocessedModel->getTransitionMatrix().getRowFilter(storm::utility::graph::performProb0E(*result.preprocessedModel, result.preprocessedModel->getBackwardTransitions(), storm::storage::BitVector(targetStateAsVector.size(), true), targetStateAsVector)); |
|||
result.possibleECChoices.set(result.preprocessedModel->getTransitionMatrix().getRowGroupIndices()[*mergerResult.targetState], true); |
|||
// There is an additional state in the result
|
|||
result.possibleBottomStates.resize(result.possibleBottomStates.size() + 1, true); |
|||
} else { |
|||
result.possibleECChoices = storm::storage::BitVector(result.preprocessedModel->getNumberOfChoices(), true); |
|||
} |
|||
assert(result.possibleBottomStates.size() == result.preprocessedModel->getNumberOfStates()); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
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) { |
|||
++numOfObjectivesWithThreshold; |
|||
} |
|||
} |
|||
if (numOfObjectivesWithThreshold == objectives.size()) { |
|||
return ReturnType::QueryType::Achievability; |
|||
} else if (numOfObjectivesWithThreshold + 1 == objectives.size()) { |
|||
// Note: We do not want to consider a Pareto query when the total number of objectives is one.
|
|||
return ReturnType::QueryType::Quantitative; |
|||
} else if (numOfObjectivesWithThreshold == 0) { |
|||
return ReturnType::QueryType::Pareto; |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Invalid Multi-objective query: The numer of qualitative objectives should be either 0 (Pareto query), 1 (quantitative query), or #objectives (achievability query)."); |
|||
} |
|||
} |
|||
|
|||
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 = 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)) { |
|||
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::graph::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>>; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,95 @@ |
|||
#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<Objective<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. |
|||
|
|||
|
|||
/*! |
|||
* Builds the result from preprocessing |
|||
*/ |
|||
static ReturnType buildResult(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula, PreprocessorData& data, std::shared_ptr<SparseModelType> const& preprocessedModel, storm::storage::SparseMatrix<ValueType> const& backwardTransitions); |
|||
|
|||
/*! |
|||
* Returns the query type |
|||
*/ |
|||
static typename ReturnType::QueryType getQueryType(std::vector<Objective<ValueType>> const& objectives); |
|||
|
|||
|
|||
/*! |
|||
* 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); |
|||
|
|||
}; |
|||
} |
|||
} |
|||
} |
|||
|
|||
@ -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; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
} |
|||
|
|||
@ -0,0 +1,218 @@ |
|||
#include "storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h"
|
|||
|
|||
#include "storm/adapters/CarlAdapter.h"
|
|||
#include "storm/models/sparse/Mdp.h"
|
|||
#include "storm/models/sparse/MarkovAutomaton.h"
|
|||
#include "storm/models/sparse/StandardRewardModel.h"
|
|||
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
|
|||
#include "storm/utility/constants.h"
|
|||
#include "storm/utility/vector.h"
|
|||
#include "storm/utility/solver.h"
|
|||
#include "storm/utility/Stopwatch.h"
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/settings/modules/GeneralSettings.h"
|
|||
#include "storm/settings/modules/CoreSettings.h"
|
|||
#include "storm/settings/modules/MultiObjectiveSettings.h"
|
|||
#include "storm/storage/expressions/Expressions.h"
|
|||
|
|||
#include "storm/exceptions/InvalidOperationException.h"
|
|||
#include "storm/exceptions/NotSupportedException.h"
|
|||
#include "storm/exceptions/UnexpectedException.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace multiobjective { |
|||
|
|||
|
|||
template <class SparseModelType> |
|||
SparseCbAchievabilityQuery<SparseModelType>::SparseCbAchievabilityQuery(SparseMultiObjectivePreprocessorReturnType<SparseModelType>& preprocessorResult) : SparseCbQuery<SparseModelType>(preprocessorResult) { |
|||
STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorReturnType<SparseModelType>::QueryType::Achievability, "Invalid query Type"); |
|||
solver = storm::utility::solver::SmtSolverFactory().create(*this->expressionManager); |
|||
} |
|||
|
|||
template <class SparseModelType> |
|||
std::unique_ptr<CheckResult> SparseCbAchievabilityQuery<SparseModelType>::check() { |
|||
|
|||
bool result = this->checkAchievability(); |
|||
|
|||
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(this->originalModel.getInitialStates().getNextSetIndex(0), result)); |
|||
|
|||
} |
|||
|
|||
template <class SparseModelType> |
|||
bool SparseCbAchievabilityQuery<SparseModelType>::checkAchievability() { |
|||
STORM_LOG_INFO("Building constraint system to check achievability."); |
|||
//this->preprocessedModel.writeDotToStream(std::cout);
|
|||
storm::utility::Stopwatch swInitialization(true); |
|||
initializeConstraintSystem(); |
|||
STORM_LOG_INFO("Constraint system consists of " << expectedChoiceVariables.size() << " + " << bottomStateVariables.size() << " variables"); |
|||
addObjectiveConstraints(); |
|||
swInitialization.stop(); |
|||
|
|||
storm::utility::Stopwatch swCheck(true); |
|||
STORM_LOG_INFO("Invoking SMT Solver."); |
|||
storm::solver::SmtSolver::CheckResult result = solver->check(); |
|||
swCheck.stop(); |
|||
|
|||
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) { |
|||
STORM_PRINT_AND_LOG("Building the constraintsystem took " << swInitialization << " seconds and checking the SMT formula took " << swCheck << " seconds." << std::endl); |
|||
} |
|||
|
|||
switch(result) { |
|||
case storm::solver::SmtSolver::CheckResult::Sat: |
|||
// std::cout << std::endl << "Satisfying assignment: " << std::endl << solver->getModelAsValuation().toString(true) << std::endl;
|
|||
return true; |
|||
case storm::solver::SmtSolver::CheckResult::Unsat: |
|||
// std::cout << std::endl << "Unsatisfiability core: {" << std::endl;
|
|||
// for (auto const& expr : solver->getUnsatCore()) {
|
|||
// std::cout << "\t " << expr << std::endl;
|
|||
// }
|
|||
// std::cout << "}" << std::endl;
|
|||
return false; |
|||
default: |
|||
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "SMT solver yielded an unexpected result"); |
|||
} |
|||
|
|||
return false; |
|||
} |
|||
|
|||
template <class SparseModelType> |
|||
void SparseCbAchievabilityQuery<SparseModelType>::initializeConstraintSystem() { |
|||
uint_fast64_t numStates = this->preprocessedModel.getNumberOfStates(); |
|||
uint_fast64_t numChoices = this->preprocessedModel.getNumberOfChoices(); |
|||
uint_fast64_t numBottomStates = this->possibleBottomStates.getNumberOfSetBits(); |
|||
|
|||
storm::expressions::Expression zero = this->expressionManager->rational(storm::utility::zero<ValueType>()); |
|||
storm::expressions::Expression one = this->expressionManager->rational(storm::utility::one<ValueType>()); |
|||
|
|||
// Declare the variables for the choices and bottom states
|
|||
expectedChoiceVariables.reserve(numChoices); |
|||
for (uint_fast64_t choice = 0; choice < numChoices; ++choice) { |
|||
expectedChoiceVariables.push_back(this->expressionManager->declareRationalVariable("y" + std::to_string(choice))); |
|||
} |
|||
bottomStateVariables.reserve(numBottomStates); |
|||
for (uint_fast64_t bottomState = 0; bottomState < numBottomStates; ++bottomState) { |
|||
bottomStateVariables.push_back(this->expressionManager->declareRationalVariable("z" + std::to_string(bottomState))); |
|||
} |
|||
|
|||
// assert that the values are greater zero and that the bottom state values sum up to one
|
|||
for (auto& var : expectedChoiceVariables) { |
|||
solver->add(var.getExpression() >= zero); |
|||
} |
|||
storm::expressions::Expression bottomStateSum = zero; |
|||
for (auto& var : bottomStateVariables) { |
|||
solver->add(var.getExpression() >= zero); |
|||
bottomStateSum = bottomStateSum + var.getExpression(); |
|||
} |
|||
solver->add(bottomStateSum == one); |
|||
|
|||
// assert that the "incoming" value of each state equals the "outgoing" value
|
|||
storm::storage::SparseMatrix<ValueType> backwardsTransitions = this->preprocessedModel.getTransitionMatrix().transpose(); |
|||
auto bottomStateVariableIt = bottomStateVariables.begin(); |
|||
for (uint_fast64_t state = 0; state < numStates; ++state) { |
|||
// get the "incomming" value
|
|||
storm::expressions::Expression value = this->preprocessedModel.getInitialStates().get(state) ? one : zero; |
|||
for (auto const& backwardsEntry : backwardsTransitions.getRow(state)) { |
|||
value = value + (this->expressionManager->rational(backwardsEntry.getValue()) * expectedChoiceVariables[backwardsEntry.getColumn()].getExpression()); |
|||
} |
|||
|
|||
// subtract the "outgoing" value
|
|||
for (uint_fast64_t choice = this->preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; choice < this->preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) { |
|||
value = value - expectedChoiceVariables[choice]; |
|||
} |
|||
if (this->possibleBottomStates.get(state)) { |
|||
value = value - (*bottomStateVariableIt); |
|||
++bottomStateVariableIt; |
|||
} |
|||
solver->add(value == zero); |
|||
} |
|||
assert(bottomStateVariableIt == bottomStateVariables.end()); |
|||
|
|||
} |
|||
|
|||
template <class SparseModelType> |
|||
void SparseCbAchievabilityQuery<SparseModelType>::addObjectiveConstraints() { |
|||
storm::expressions::Expression zero = this->expressionManager->rational(storm::utility::zero<ValueType>()); |
|||
for (Objective<ValueType> const& obj : this->objectives) { |
|||
if (obj.rewardModelName) { |
|||
STORM_LOG_THROW(obj.bound, storm::exceptions::InvalidOperationException, "Invoked achievability query but no bound was specified for at least one objective."); |
|||
STORM_LOG_THROW(!obj.lowerTimeBound && !obj.upperTimeBound, storm::exceptions::NotSupportedException, "Constraint based method currently does not support step bounds"); |
|||
std::vector<ValueType> rewards = getActionBasedExpectedRewards(*obj.rewardModelName); |
|||
storm::expressions::Expression objValue = zero; |
|||
for (uint_fast64_t choice = 0; choice < rewards.size(); ++choice) { |
|||
if (!storm::utility::isZero(rewards[choice])) { |
|||
objValue = objValue + (this->expressionManager->rational(rewards[choice]) * expectedChoiceVariables[choice].getExpression()); |
|||
} |
|||
} |
|||
// We need to actually evaluate the threshold as rational number. Otherwise a threshold like '<=16/9' might be considered as 1 due to integer division
|
|||
STORM_LOG_THROW(!obj.bound->threshold.containsVariables(), storm::exceptions::InvalidOperationException, "The threshold for one objective still contains undefined variables"); |
|||
storm::expressions::Expression threshold = this->expressionManager->rational(obj.bound->threshold.evaluateAsRational()); |
|||
switch (obj.bound->comparisonType) { |
|||
case storm::logic::ComparisonType::Greater: |
|||
solver->add( objValue > threshold); |
|||
break; |
|||
case storm::logic::ComparisonType::GreaterEqual: |
|||
solver->add( objValue >= threshold); |
|||
break; |
|||
case storm::logic::ComparisonType::Less: |
|||
solver->add( objValue < threshold); |
|||
break; |
|||
case storm::logic::ComparisonType::LessEqual: |
|||
solver->add( objValue <= threshold); |
|||
break; |
|||
default: |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "One or more objectives have an invalid comparison type"); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
template <> |
|||
std::vector<double> SparseCbAchievabilityQuery<storm::models::sparse::Mdp<double>>::getActionBasedExpectedRewards(std::string const& rewardModelName) const { |
|||
return this->preprocessedModel.getRewardModel(rewardModelName).getTotalRewardVector(this->preprocessedModel.getTransitionMatrix()); |
|||
} |
|||
|
|||
template <> |
|||
std::vector<double> SparseCbAchievabilityQuery<storm::models::sparse::MarkovAutomaton<double>>::getActionBasedExpectedRewards(std::string const& rewardModelName) const { |
|||
auto const& rewModel = this->preprocessedModel.getRewardModel(rewardModelName); |
|||
STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected."); |
|||
std::vector<double> result = rewModel.hasStateActionRewards() ? rewModel.getStateActionRewardVector() : std::vector<double>(this->preprocessedModel.getNumberOfChoices(), storm::utility::zero<ValueType>()); |
|||
if(rewModel.hasStateRewards()) { |
|||
// Note that state rewards are earned over time and thus play no role for probabilistic states
|
|||
for(auto markovianState : this->preprocessedModel.getMarkovianStates()) { |
|||
result[this->preprocessedModel.getTransitionMatrix().getRowGroupIndices()[markovianState]] += rewModel.getStateReward(markovianState) / this->preprocessedModel.getExitRate(markovianState); |
|||
} |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
template <> |
|||
std::vector<storm::RationalNumber> SparseCbAchievabilityQuery<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::getActionBasedExpectedRewards(std::string const& rewardModelName) const { |
|||
auto const& rewModel = this->preprocessedModel.getRewardModel(rewardModelName); |
|||
STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected."); |
|||
std::vector<storm::RationalNumber> result = rewModel.hasStateActionRewards() ? rewModel.getStateActionRewardVector() : std::vector<storm::RationalNumber>(this->preprocessedModel.getNumberOfChoices(), storm::utility::zero<ValueType>()); |
|||
if(rewModel.hasStateRewards()) { |
|||
// Note that state rewards are earned over time and thus play no role for probabilistic states
|
|||
for(auto markovianState : this->preprocessedModel.getMarkovianStates()) { |
|||
result[this->preprocessedModel.getTransitionMatrix().getRowGroupIndices()[markovianState]] += rewModel.getStateReward(markovianState) / this->preprocessedModel.getExitRate(markovianState); |
|||
} |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
template <> |
|||
std::vector<storm::RationalNumber> SparseCbAchievabilityQuery<storm::models::sparse::Mdp<storm::RationalNumber>>::getActionBasedExpectedRewards(std::string const& rewardModelName) const { |
|||
return this->preprocessedModel.getRewardModel(rewardModelName).getTotalRewardVector(this->preprocessedModel.getTransitionMatrix()); |
|||
} |
|||
|
|||
|
|||
#ifdef STORM_HAVE_CARL
|
|||
template class SparseCbAchievabilityQuery<storm::models::sparse::Mdp<double>>; |
|||
template class SparseCbAchievabilityQuery<storm::models::sparse::MarkovAutomaton<double>>; |
|||
|
|||
template class SparseCbAchievabilityQuery<storm::models::sparse::Mdp<storm::RationalNumber>>; |
|||
template class SparseCbAchievabilityQuery<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>; |
|||
#endif
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,63 @@ |
|||
#pragma once |
|||
|
|||
|
|||
#include "storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h" |
|||
|
|||
#include "storm/solver/SmtSolver.h" |
|||
#include "storm/storage/expressions/Variable.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace multiobjective { |
|||
|
|||
/* |
|||
* This class represents an achievability query for the constraint based approach (using SMT or LP solvers). |
|||
*/ |
|||
template <class SparseModelType> |
|||
class SparseCbAchievabilityQuery : public SparseCbQuery<SparseModelType> { |
|||
public: |
|||
|
|||
typedef typename SparseModelType::ValueType ValueType; |
|||
|
|||
SparseCbAchievabilityQuery(SparseMultiObjectivePreprocessorReturnType<SparseModelType>& preprocessorResult); |
|||
|
|||
virtual ~SparseCbAchievabilityQuery() = default; |
|||
|
|||
/* |
|||
* Invokes the computation and retrieves the result |
|||
*/ |
|||
virtual std::unique_ptr<CheckResult> check() override; |
|||
|
|||
private: |
|||
|
|||
/* |
|||
* Returns whether the given thresholds are achievable. |
|||
*/ |
|||
bool checkAchievability(); |
|||
|
|||
|
|||
/* |
|||
* Adds variable y_i for each choice i and z_j for each possible bottom state j and asserts that for every solution of the |
|||
* constraint system there is a scheduler under which |
|||
* * if choice i yields reward for an expected value objective, then y_i is the expected number of times choice i is taken. |
|||
* * z_j/(z_j + Sum_{i in Choices(j)} y_i) is a lower bound for the probability that starting from j no more reward is collected |
|||
*/ |
|||
void initializeConstraintSystem(); |
|||
|
|||
// Adds the thresholds of the objective values |
|||
void addObjectiveConstraints(); |
|||
|
|||
// Returns the action based rewards for the given reward model name. |
|||
std::vector<ValueType> getActionBasedExpectedRewards(std::string const& rewardModelName) const; |
|||
|
|||
|
|||
std::vector<storm::expressions::Variable> expectedChoiceVariables; |
|||
std::vector<storm::expressions::Variable> bottomStateVariables; |
|||
|
|||
|
|||
std::unique_ptr<storm::solver::SmtSolver> solver; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,38 @@ |
|||
#include "storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h"
|
|||
|
|||
#include "storm/adapters/CarlAdapter.h"
|
|||
#include "storm/models/sparse/Mdp.h"
|
|||
#include "storm/models/sparse/MarkovAutomaton.h"
|
|||
#include "storm/models/sparse/StandardRewardModel.h"
|
|||
#include "storm/modelchecker/multiobjective/Objective.h"
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/settings/modules/MultiObjectiveSettings.h"
|
|||
#include "storm/utility/constants.h"
|
|||
#include "storm/utility/vector.h"
|
|||
|
|||
#include "storm/exceptions/UnexpectedException.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace multiobjective { |
|||
|
|||
|
|||
template <class SparseModelType> |
|||
SparseCbQuery<SparseModelType>::SparseCbQuery(SparseMultiObjectivePreprocessorReturnType<SparseModelType>& preprocessorResult) : |
|||
originalModel(preprocessorResult.originalModel), originalFormula(preprocessorResult.originalFormula), |
|||
preprocessedModel(std::move(*preprocessorResult.preprocessedModel)), objectives(std::move(preprocessorResult.objectives)), |
|||
possibleBottomStates(std::move(preprocessorResult.possibleBottomStates)) { |
|||
expressionManager = std::make_shared<storm::expressions::ExpressionManager>(); |
|||
} |
|||
|
|||
|
|||
#ifdef STORM_HAVE_CARL
|
|||
template class SparseCbQuery<storm::models::sparse::Mdp<double>>; |
|||
template class SparseCbQuery<storm::models::sparse::MarkovAutomaton<double>>; |
|||
|
|||
template class SparseCbQuery<storm::models::sparse::Mdp<storm::RationalNumber>>; |
|||
template class SparseCbQuery<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>; |
|||
#endif
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,46 @@ |
|||
#pragma once |
|||
|
|||
#include <memory> |
|||
|
|||
#include "storm/modelchecker/results/CheckResult.h" |
|||
#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h" |
|||
#include "storm/storage/expressions/ExpressionManager.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace multiobjective { |
|||
|
|||
/* |
|||
* This class represents a multi-objective query for the constraint based approach (using SMT or LP solvers). |
|||
*/ |
|||
template <class SparseModelType> |
|||
class SparseCbQuery { |
|||
public: |
|||
|
|||
|
|||
virtual ~SparseCbQuery() = default; |
|||
|
|||
/* |
|||
* Invokes the computation and retrieves the result |
|||
*/ |
|||
virtual std::unique_ptr<CheckResult> check() = 0; |
|||
|
|||
protected: |
|||
|
|||
SparseCbQuery(SparseMultiObjectivePreprocessorReturnType<SparseModelType>& preprocessorResult); |
|||
|
|||
SparseModelType const& originalModel; |
|||
storm::logic::MultiObjectiveFormula const& originalFormula; |
|||
|
|||
SparseModelType preprocessedModel; |
|||
std::vector<Objective<typename SparseModelType::ValueType>> objectives; |
|||
|
|||
std::shared_ptr<storm::expressions::ExpressionManager> expressionManager; |
|||
|
|||
storm::storage::BitVector possibleBottomStates; |
|||
|
|||
}; |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,122 @@ |
|||
#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h"
|
|||
|
|||
#include "storm/utility/macros.h"
|
|||
|
|||
#include "storm/models/sparse/Mdp.h"
|
|||
#include "storm/models/sparse/MarkovAutomaton.h"
|
|||
#include "storm/models/sparse/StandardRewardModel.h"
|
|||
#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h"
|
|||
#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h"
|
|||
#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h"
|
|||
#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h"
|
|||
#include "storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h"
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/settings/modules/MultiObjectiveSettings.h"
|
|||
#include "storm/settings/modules/CoreSettings.h"
|
|||
#include "storm/utility/Stopwatch.h"
|
|||
|
|||
#include "storm/exceptions/InvalidArgumentException.h"
|
|||
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace multiobjective { |
|||
|
|||
template<typename SparseModelType> |
|||
std::unique_ptr<CheckResult> performMultiObjectiveModelChecking(SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection) { |
|||
storm::utility::Stopwatch swTotal(true); |
|||
storm::utility::Stopwatch swPreprocessing(true); |
|||
STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "Multi-objective Model checking on model with multiple initial states is not supported."); |
|||
|
|||
// If we consider an MA, ensure that it is closed
|
|||
if(model.isOfType(storm::models::ModelType::MarkovAutomaton)) { |
|||
STORM_LOG_THROW(dynamic_cast<storm::models::sparse::MarkovAutomaton<typename SparseModelType::ValueType> const *>(&model)->isClosed(), storm::exceptions::InvalidArgumentException, "Unable to check multi-objective formula on non-closed Markov automaton."); |
|||
} |
|||
|
|||
// Preprocess the model
|
|||
auto preprocessorResult = SparseMultiObjectivePreprocessor<SparseModelType>::preprocess(model, formula); |
|||
swPreprocessing.stop(); |
|||
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) { |
|||
STORM_PRINT_AND_LOG("Preprocessing done in " << swPreprocessing << " seconds." << std::endl << " Result: " << preprocessorResult << std::endl); |
|||
} else { |
|||
STORM_LOG_INFO("Preprocessing done in " << swPreprocessing << " seconds." << std::endl << " Result: " << preprocessorResult << std::endl); |
|||
} |
|||
|
|||
// Get the solution method
|
|||
MultiObjectiveMethod method; |
|||
if (methodSelection == MultiObjectiveMethodSelection::FROMSETTINGS) { |
|||
method = storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getMultiObjectiveMethod(); |
|||
} else { |
|||
method = convert(methodSelection); |
|||
} |
|||
|
|||
// Invoke the analysis
|
|||
storm::utility::Stopwatch swAnalysis(true); |
|||
std::unique_ptr<CheckResult> result; |
|||
switch (method) { |
|||
case MultiObjectiveMethod::Pcaa: |
|||
{ |
|||
std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>> query; |
|||
switch (preprocessorResult.queryType) { |
|||
case SparseMultiObjectivePreprocessorReturnType<SparseModelType>::QueryType::Achievability: |
|||
query = std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>> (new SparsePcaaAchievabilityQuery<SparseModelType, storm::RationalNumber>(preprocessorResult)); |
|||
break; |
|||
case SparseMultiObjectivePreprocessorReturnType<SparseModelType>::QueryType::Quantitative: |
|||
query = std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>> (new SparsePcaaQuantitativeQuery<SparseModelType, storm::RationalNumber>(preprocessorResult)); |
|||
break; |
|||
case SparseMultiObjectivePreprocessorReturnType<SparseModelType>::QueryType::Pareto: |
|||
query = std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>> (new SparsePcaaParetoQuery<SparseModelType, storm::RationalNumber>(preprocessorResult)); |
|||
break; |
|||
default: |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The multi-objective query type is not supported for the selected solution method '" << toString(method) << "'."); |
|||
break; |
|||
} |
|||
|
|||
result = query->check(); |
|||
|
|||
if(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().isExportPlotSet()) { |
|||
query->exportPlotOfCurrentApproximation(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getExportPlotDirectory()); |
|||
} |
|||
break; |
|||
} |
|||
case MultiObjectiveMethod::ConstraintBased: |
|||
{ |
|||
std::unique_ptr<SparseCbQuery<SparseModelType>> query; |
|||
switch (preprocessorResult.queryType) { |
|||
case SparseMultiObjectivePreprocessorReturnType<SparseModelType>::QueryType::Achievability: |
|||
query = std::unique_ptr<SparseCbQuery<SparseModelType>> (new SparseCbAchievabilityQuery<SparseModelType>(preprocessorResult)); |
|||
break; |
|||
default: |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The multi-objective query type is not supported for the selected solution method '" << toString(method) << "'."); |
|||
break; |
|||
} |
|||
|
|||
result = query->check(); |
|||
|
|||
if(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().isExportPlotSet()) { |
|||
STORM_LOG_ERROR("Can not export plot for the constrained based solver."); |
|||
} |
|||
break; |
|||
} |
|||
default: |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The multi-objective solution method '" << toString(method) << "' is not supported."); |
|||
} |
|||
swAnalysis.stop(); |
|||
|
|||
swTotal.stop(); |
|||
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) { |
|||
STORM_PRINT_AND_LOG("Solving multi-objective query took " << swTotal << " seconds (consisting of " << swPreprocessing << " seconds for preprocessing and " << swAnalysis << " seconds for analyzing the preprocessed model)." << std::endl); |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
|
|||
template std::unique_ptr<CheckResult> performMultiObjectiveModelChecking<storm::models::sparse::Mdp<double>>(storm::models::sparse::Mdp<double> const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); |
|||
template std::unique_ptr<CheckResult> performMultiObjectiveModelChecking<storm::models::sparse::MarkovAutomaton<double>>(storm::models::sparse::MarkovAutomaton<double> const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); |
|||
template std::unique_ptr<CheckResult> performMultiObjectiveModelChecking<storm::models::sparse::Mdp<storm::RationalNumber>>(storm::models::sparse::Mdp<storm::RationalNumber> const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); |
|||
template std::unique_ptr<CheckResult> performMultiObjectiveModelChecking<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>(storm::models::sparse::MarkovAutomaton<storm::RationalNumber> const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,19 @@ |
|||
#pragma once |
|||
|
|||
#include <memory> |
|||
|
|||
#include "storm/modelchecker/results/CheckResult.h" |
|||
#include "storm/modelchecker/multiobjective/MultiObjectiveModelCheckingMethod.h" |
|||
#include "storm/logic/Formulas.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace multiobjective { |
|||
|
|||
|
|||
template<typename SparseModelType> |
|||
std::unique_ptr<CheckResult> performMultiObjectiveModelChecking(SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection = MultiObjectiveMethodSelection::FROMSETTINGS); |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -1,88 +0,0 @@ |
|||
#include "storm/modelchecker/multiobjective/pcaa.h"
|
|||
|
|||
#include "storm/utility/macros.h"
|
|||
|
|||
#include "storm/models/sparse/Mdp.h"
|
|||
#include "storm/models/sparse/MarkovAutomaton.h"
|
|||
#include "storm/models/sparse/StandardRewardModel.h"
|
|||
#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h"
|
|||
#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h"
|
|||
#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h"
|
|||
#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h"
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/settings/modules/MultiObjectiveSettings.h"
|
|||
#include "storm/settings/modules/CoreSettings.h"
|
|||
#include "storm/utility/Stopwatch.h"
|
|||
|
|||
#include "storm/exceptions/InvalidArgumentException.h"
|
|||
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace multiobjective { |
|||
|
|||
template<typename SparseModelType> |
|||
std::unique_ptr<CheckResult> performPcaa(SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula) { |
|||
storm::utility::Stopwatch swTotal(true); |
|||
storm::utility::Stopwatch swPreprocessing(true); |
|||
STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "Multi-objective Model checking on model with multiple initial states is not supported."); |
|||
|
|||
#ifdef STORM_HAVE_CARL
|
|||
|
|||
// If we consider an MA, ensure that it is closed
|
|||
if(model.isOfType(storm::models::ModelType::MarkovAutomaton)) { |
|||
STORM_LOG_THROW(dynamic_cast<storm::models::sparse::MarkovAutomaton<typename SparseModelType::ValueType> const *>(&model)->isClosed(), storm::exceptions::InvalidArgumentException, "Unable to check multi-objective formula on non-closed Markov automaton."); |
|||
} |
|||
|
|||
auto preprocessorResult = SparsePcaaPreprocessor<SparseModelType>::preprocess(model, formula); |
|||
swPreprocessing.stop(); |
|||
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) { |
|||
STORM_PRINT_AND_LOG("Preprocessing done in " << swPreprocessing << " seconds." << std::endl << " Result: " << preprocessorResult << std::endl); |
|||
} else { |
|||
STORM_LOG_INFO("Preprocessing done in " << swPreprocessing << " seconds." << std::endl << " Result: " << preprocessorResult << std::endl); |
|||
} |
|||
storm::utility::Stopwatch swValueIterations(true); |
|||
std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>> query; |
|||
switch (preprocessorResult.queryType) { |
|||
case SparsePcaaPreprocessorReturnType<SparseModelType>::QueryType::Achievability: |
|||
query = std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>> (new SparsePcaaAchievabilityQuery<SparseModelType, storm::RationalNumber>(preprocessorResult)); |
|||
break; |
|||
case SparsePcaaPreprocessorReturnType<SparseModelType>::QueryType::Quantitative: |
|||
query = std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>> (new SparsePcaaQuantitativeQuery<SparseModelType, storm::RationalNumber>(preprocessorResult)); |
|||
break; |
|||
case SparsePcaaPreprocessorReturnType<SparseModelType>::QueryType::Pareto: |
|||
query = std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>> (new SparsePcaaParetoQuery<SparseModelType, storm::RationalNumber>(preprocessorResult)); |
|||
break; |
|||
default: |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unsupported multi-objective Query Type."); |
|||
break; |
|||
} |
|||
|
|||
auto result = query->check(); |
|||
swValueIterations.stop(); |
|||
swTotal.stop(); |
|||
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) { |
|||
STORM_PRINT_AND_LOG("Solving multi-objective query took " << swTotal << " seconds (consisting of " << swPreprocessing << " seconds for preprocessing and " << swValueIterations << " seconds for value iteration-based exploration of achievable points)." << std::endl); |
|||
} |
|||
|
|||
|
|||
if(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().isExportPlotSet()) { |
|||
query->exportPlotOfCurrentApproximation(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getExportPlotDirectory()); |
|||
} |
|||
return result; |
|||
#else
|
|||
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Multi-objective model checking requires carl."); |
|||
return nullptr; |
|||
#endif
|
|||
} |
|||
|
|||
template std::unique_ptr<CheckResult> performPcaa<storm::models::sparse::Mdp<double>>(storm::models::sparse::Mdp<double> const& model, storm::logic::MultiObjectiveFormula const& formula); |
|||
template std::unique_ptr<CheckResult> performPcaa<storm::models::sparse::MarkovAutomaton<double>>(storm::models::sparse::MarkovAutomaton<double> const& model, storm::logic::MultiObjectiveFormula const& formula); |
|||
#ifdef STORM_HAVE_CARL
|
|||
template std::unique_ptr<CheckResult> performPcaa<storm::models::sparse::Mdp<storm::RationalNumber>>(storm::models::sparse::Mdp<storm::RationalNumber> const& model, storm::logic::MultiObjectiveFormula const& formula); |
|||
template std::unique_ptr<CheckResult> performPcaa<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>(storm::models::sparse::MarkovAutomaton<storm::RationalNumber> const& model, storm::logic::MultiObjectiveFormula const& formula); |
|||
#endif
|
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -1,20 +0,0 @@ |
|||
#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_H_ |
|||
#define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_H_ |
|||
|
|||
#include <memory> |
|||
|
|||
#include "storm/modelchecker/results/CheckResult.h" |
|||
#include "storm/logic/Formulas.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace multiobjective { |
|||
|
|||
template<typename SparseModelType> |
|||
std::unique_ptr<CheckResult> performPcaa(SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula); |
|||
|
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_H_ */ |
|||
@ -1,72 +0,0 @@ |
|||
#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_PCAAOBJECTIVE_H_ |
|||
#define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_PCAAOBJECTIVE_H_ |
|||
|
|||
#include <iomanip> |
|||
#include <boost/optional.hpp> |
|||
|
|||
#include "storm/logic/Formulas.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace multiobjective { |
|||
template <typename ValueType> |
|||
struct PcaaObjective { |
|||
// the original input formula |
|||
std::shared_ptr<storm::logic::Formula const> originalFormula; |
|||
|
|||
// the name of the considered reward model in the preprocessedModel |
|||
std::string rewardModelName; |
|||
|
|||
// true if all rewards for this objective are positive, false if all rewards are negative. |
|||
bool rewardsArePositive; |
|||
|
|||
// transformation from the values of the preprocessed model to the ones for the actual input model, i.e., |
|||
// x is achievable in the preprocessed model iff factor*x + offset is achievable in the original model |
|||
ValueType toOriginalValueTransformationFactor; |
|||
ValueType toOriginalValueTransformationOffset; |
|||
|
|||
// The probability/reward threshold for the preprocessed model (if originalFormula specifies one). |
|||
// This is always a lower bound. |
|||
boost::optional<ValueType> threshold; |
|||
// True iff the specified threshold is strict, i.e., > |
|||
bool thresholdIsStrict = false; |
|||
|
|||
// The time bound(s) for the formula (if given by the originalFormula) |
|||
boost::optional<storm::expressions::Expression> lowerTimeBound; |
|||
boost::optional<storm::expressions::Expression> upperTimeBound; |
|||
bool lowerTimeBoundStrict = false; |
|||
bool upperTimeBoundStrict = false; |
|||
|
|||
void printToStream(std::ostream& out) const { |
|||
out << std::setw(30) << originalFormula->toString(); |
|||
out << " \t(toOrigVal:" << std::setw(3) << toOriginalValueTransformationFactor << "*x +" << std::setw(3) << toOriginalValueTransformationOffset << ", \t"; |
|||
out << "intern threshold:"; |
|||
if(threshold){ |
|||
out << (thresholdIsStrict ? " >" : ">="); |
|||
out << std::setw(5) << (*threshold) << ","; |
|||
} else { |
|||
out << " none,"; |
|||
} |
|||
out << " \t"; |
|||
out << "intern reward model: " << std::setw(10) << rewardModelName; |
|||
out << (rewardsArePositive ? " (positive)" : " (negative)") << ", \t"; |
|||
out << "time bounds:"; |
|||
if(lowerTimeBound) { |
|||
if(upperTimeBound) { |
|||
out << (lowerTimeBoundStrict ? "(" : "[") << *lowerTimeBound << ", " << *upperTimeBound << (upperTimeBoundStrict ? ")" : "]"); |
|||
} else { |
|||
out << (lowerTimeBoundStrict ? " >" : ">=") << std::setw(5) << *lowerTimeBound; |
|||
} |
|||
} else if (upperTimeBound) { |
|||
out << (upperTimeBoundStrict ? " <" : "<=") << std::setw(5) << *upperTimeBound; |
|||
} else { |
|||
out << " none"; |
|||
} |
|||
out << ")" << std::endl; |
|||
} |
|||
}; |
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_OBJECTIVE_H_ */ |
|||
@ -1,416 +0,0 @@ |
|||
#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.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/transformer/StateDuplicator.h"
|
|||
#include "storm/transformer/SubsystemBuilder.h"
|
|||
#include "storm/utility/macros.h"
|
|||
#include "storm/utility/vector.h"
|
|||
#include "storm/utility/graph.h"
|
|||
|
|||
#include "storm/exceptions/InvalidPropertyException.h"
|
|||
#include "storm/exceptions/UnexpectedException.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace multiobjective { |
|||
|
|||
template<typename SparseModelType> |
|||
typename SparsePcaaPreprocessor<SparseModelType>::ReturnType SparsePcaaPreprocessor<SparseModelType>::preprocess(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula) { |
|||
|
|||
ReturnType result(originalFormula, originalModel, SparseModelType(originalModel)); |
|||
result.newToOldStateIndexMapping = storm::utility::vector::buildVectorForRange(0, originalModel.getNumberOfStates()); |
|||
|
|||
//Invoke preprocessing on the individual objectives
|
|||
for(auto const& subFormula : originalFormula.getSubformulas()){ |
|||
STORM_LOG_INFO("Preprocessing objective " << *subFormula<< "."); |
|||
result.objectives.emplace_back(); |
|||
PcaaObjective<ValueType>& currentObjective = result.objectives.back(); |
|||
currentObjective.originalFormula = subFormula; |
|||
if(currentObjective.originalFormula->isOperatorFormula()) { |
|||
preprocessOperatorFormula(currentObjective.originalFormula->asOperatorFormula(), result, currentObjective); |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the subformula " << *subFormula << " of " << originalFormula << " because it is not supported"); |
|||
} |
|||
} |
|||
// Set the query type. In case of a quantitative query, also set the index of the objective to be optimized.
|
|||
// Note: If there are only zero (or one) objectives left, we should not consider a pareto query!
|
|||
storm::storage::BitVector objectivesWithoutThreshold(result.objectives.size()); |
|||
for(uint_fast64_t objIndex = 0; objIndex < result.objectives.size(); ++objIndex) { |
|||
objectivesWithoutThreshold.set(objIndex, !result.objectives[objIndex].threshold); |
|||
} |
|||
uint_fast64_t numOfObjectivesWithoutThreshold = objectivesWithoutThreshold.getNumberOfSetBits(); |
|||
if(numOfObjectivesWithoutThreshold == 0) { |
|||
result.queryType = ReturnType::QueryType::Achievability; |
|||
} else if (numOfObjectivesWithoutThreshold == 1) { |
|||
result.queryType = ReturnType::QueryType::Quantitative; |
|||
result.indexOfOptimizingObjective = objectivesWithoutThreshold.getNextSetIndex(0); |
|||
} else if (numOfObjectivesWithoutThreshold == result.objectives.size()) { |
|||
result.queryType = ReturnType::QueryType::Pareto; |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The number of objectives without threshold is not valid. It should be either 0 (achievability query), 1 (quantitative query), or " << result.objectives.size() << " (Pareto Query). Got " << numOfObjectivesWithoutThreshold << " instead."); |
|||
} |
|||
|
|||
//We can remove the original reward models to save some memory
|
|||
std::set<std::string> origRewardModels = originalFormula.getReferencedRewardModels(); |
|||
for (auto const& rewModel : origRewardModels){ |
|||
result.preprocessedModel.removeRewardModel(rewModel); |
|||
} |
|||
|
|||
//Get actions to which a positive or negative reward is assigned for at least one objective
|
|||
result.actionsWithPositiveReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false); |
|||
result.actionsWithNegativeReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false); |
|||
for(uint_fast64_t objIndex = 0; objIndex < result.objectives.size(); ++objIndex) { |
|||
if(!result.objectives[objIndex].upperTimeBound) { |
|||
if(result.objectives[objIndex].rewardsArePositive) { |
|||
result.actionsWithPositiveReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix())); |
|||
} else { |
|||
result.actionsWithNegativeReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix())); |
|||
} |
|||
} |
|||
} |
|||
|
|||
// Analyze End components and ensure reward finiteness.
|
|||
// Note that this is only necessary if there is at least one objective with no upper time bound
|
|||
for (auto const& obj : result.objectives) { |
|||
if(!obj.upperTimeBound) { |
|||
auto backwardTransitions = result.preprocessedModel.getBackwardTransitions(); |
|||
analyzeEndComponents(result, backwardTransitions); |
|||
ensureRewardFiniteness(result, backwardTransitions); |
|||
break; |
|||
} |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::updatePreprocessedModel(ReturnType& result, SparseModelType& newPreprocessedModel, std::vector<uint_fast64_t>& newToOldStateIndexMapping) { |
|||
result.preprocessedModel = std::move(newPreprocessedModel); |
|||
// the given newToOldStateIndexMapping reffers to the indices of the former preprocessedModel as 'old indices'
|
|||
for(auto & preprocessedModelStateIndex : newToOldStateIndexMapping){ |
|||
preprocessedModelStateIndex = result.newToOldStateIndexMapping[preprocessedModelStateIndex]; |
|||
} |
|||
result.newToOldStateIndexMapping = std::move(newToOldStateIndexMapping); |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessOperatorFormula(storm::logic::OperatorFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective) { |
|||
|
|||
// Get a unique name for the new reward model.
|
|||
currentObjective.rewardModelName = "objective" + std::to_string(result.objectives.size()); |
|||
while(result.preprocessedModel.hasRewardModel(currentObjective.rewardModelName)){ |
|||
currentObjective.rewardModelName = "_" + currentObjective.rewardModelName; |
|||
} |
|||
|
|||
currentObjective.toOriginalValueTransformationFactor = storm::utility::one<ValueType>(); |
|||
currentObjective.toOriginalValueTransformationOffset = storm::utility::zero<ValueType>(); |
|||
currentObjective.rewardsArePositive = true; |
|||
|
|||
bool formulaMinimizes = false; |
|||
if(formula.hasBound()) { |
|||
currentObjective.threshold = formula.template getThresholdAs<ValueType>(); |
|||
currentObjective.thresholdIsStrict = storm::logic::isStrict(formula.getBound().comparisonType); |
|||
//Note that we minimize for upper bounds since we are looking for the EXISTENCE of a satisfying scheduler
|
|||
formulaMinimizes = !storm::logic::isLowerBound(formula.getBound().comparisonType); |
|||
} else if (formula.hasOptimalityType()){ |
|||
formulaMinimizes = storm::solver::minimize(formula.getOptimalityType()); |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Current objective " << formula << " does not specify whether to minimize or maximize"); |
|||
} |
|||
if(formulaMinimizes) { |
|||
// We negate all the values so we can consider the maximum for this objective
|
|||
// Thus, all objectives will be maximized.
|
|||
currentObjective.rewardsArePositive = false; |
|||
currentObjective.toOriginalValueTransformationFactor = -storm::utility::one<ValueType>(); |
|||
} |
|||
|
|||
if(formula.isProbabilityOperatorFormula()){ |
|||
preprocessProbabilityOperatorFormula(formula.asProbabilityOperatorFormula(), result, currentObjective); |
|||
} else if(formula.isRewardOperatorFormula()){ |
|||
preprocessRewardOperatorFormula(formula.asRewardOperatorFormula(), result, currentObjective); |
|||
} else if(formula.isTimeOperatorFormula()){ |
|||
preprocessTimeOperatorFormula(formula.asTimeOperatorFormula(), result, currentObjective); |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the objective " << formula << " because it is not supported"); |
|||
} |
|||
|
|||
// Transform the threshold for the preprocessed Model
|
|||
if(currentObjective.threshold) { |
|||
currentObjective.threshold = (currentObjective.threshold.get() - currentObjective.toOriginalValueTransformationOffset) / currentObjective.toOriginalValueTransformationFactor; |
|||
} |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective) { |
|||
|
|||
if(formula.getSubformula().isUntilFormula()){ |
|||
preprocessUntilFormula(formula.getSubformula().asUntilFormula(), result, currentObjective); |
|||
} else if(formula.getSubformula().isBoundedUntilFormula()){ |
|||
preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), result, currentObjective); |
|||
} else if(formula.getSubformula().isGloballyFormula()){ |
|||
preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), result, currentObjective); |
|||
} else if(formula.getSubformula().isEventuallyFormula()){ |
|||
preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective); |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); |
|||
} |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective) { |
|||
// Check if the reward model is uniquely specified
|
|||
STORM_LOG_THROW((formula.hasRewardModelName() && result.preprocessedModel.hasRewardModel(formula.getRewardModelName())) |
|||
|| result.preprocessedModel.hasUniqueRewardModel(), storm::exceptions::InvalidPropertyException, "The reward model is not unique and the formula " << formula << " does not specify a reward model."); |
|||
|
|||
if(formula.getSubformula().isEventuallyFormula()){ |
|||
preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective, formula.getOptionalRewardModelName()); |
|||
} else if(formula.getSubformula().isCumulativeRewardFormula()) { |
|||
preprocessCumulativeRewardFormula(formula.getSubformula().asCumulativeRewardFormula(), result, currentObjective, formula.getOptionalRewardModelName()); |
|||
} else if(formula.getSubformula().isTotalRewardFormula()) { |
|||
preprocessTotalRewardFormula(result, currentObjective, formula.getOptionalRewardModelName()); |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); |
|||
} |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective) { |
|||
// Time formulas are only supported for Markov automata
|
|||
STORM_LOG_THROW(result.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(), result, currentObjective); |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); |
|||
} |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessUntilFormula(storm::logic::UntilFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective) { |
|||
CheckTask<storm::logic::Formula, ValueType> phiTask(formula.getLeftSubformula()); |
|||
CheckTask<storm::logic::Formula, ValueType> psiTask(formula.getRightSubformula()); |
|||
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(result.preprocessedModel); |
|||
STORM_LOG_THROW(mc.canHandle(phiTask) && mc.canHandle(psiTask), storm::exceptions::InvalidPropertyException, "The subformulas of " << formula << " should be propositional."); |
|||
storm::storage::BitVector phiStates = mc.check(phiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector(); |
|||
storm::storage::BitVector psiStates = mc.check(psiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector(); |
|||
|
|||
if(!(psiStates & result.preprocessedModel.getInitialStates()).empty() && !currentObjective.lowerTimeBound) { |
|||
// The probability is always one as the initial state is a target state.
|
|||
// For this special case, the transformation to an expected reward objective fails.
|
|||
// We could handle this with further preprocessing steps but as this case is boring anyway, we simply reject the input.
|
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The Probability for the objective " << currentObjective.originalFormula << " is always one as the rhs of the until formula is true in the initial state. Please omit this objective."); |
|||
} |
|||
|
|||
auto duplicatorResult = storm::transformer::StateDuplicator<SparseModelType>::transform(result.preprocessedModel, ~phiStates | psiStates); |
|||
updatePreprocessedModel(result, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping); |
|||
|
|||
storm::storage::BitVector newPsiStates(result.preprocessedModel.getNumberOfStates(), false); |
|||
for(auto const& oldPsiState : psiStates){ |
|||
//note that psiStates are always located in the second copy
|
|||
newPsiStates.set(duplicatorResult.secondCopyOldToNewStateIndexMapping[oldPsiState], true); |
|||
} |
|||
|
|||
// build stateAction reward vector that gives (one*transitionProbability) reward whenever a transition leads from the firstCopy to a psiState
|
|||
std::vector<ValueType> objectiveRewards(result.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>()); |
|||
for (auto const& firstCopyState : duplicatorResult.firstCopy) { |
|||
for (uint_fast64_t row = result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[firstCopyState]; row < result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[firstCopyState + 1]; ++row) { |
|||
objectiveRewards[row] = result.preprocessedModel.getTransitionMatrix().getConstrainedRowSum(row, newPsiStates); |
|||
} |
|||
} |
|||
if(!currentObjective.rewardsArePositive) { |
|||
storm::utility::vector::scaleVectorInPlace(objectiveRewards, -storm::utility::one<ValueType>()); |
|||
} |
|||
result.preprocessedModel.addRewardModel(currentObjective.rewardModelName, RewardModelType(boost::none, objectiveRewards)); |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective) { |
|||
STORM_LOG_THROW(!result.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()) { |
|||
currentObjective.lowerTimeBound = formula.getLowerBound(); |
|||
currentObjective.lowerTimeBoundStrict = formula.isLowerBoundStrict(); |
|||
} |
|||
if (formula.hasUpperBound()) { |
|||
currentObjective.upperTimeBound = formula.getUpperBound(); |
|||
currentObjective.upperTimeBoundStrict = formula.isUpperBoundStrict(); |
|||
} |
|||
preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), result, currentObjective); |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective) { |
|||
// The formula will be transformed to an until formula for the complementary event.
|
|||
// If the original formula minimizes, the complementary one will maximize and vice versa.
|
|||
// Hence, the decision whether to consider positive or negative rewards flips.
|
|||
currentObjective.rewardsArePositive = !currentObjective.rewardsArePositive; |
|||
// To transform from the value of the preprocessed model back to the value of the original model, we have to add 1 to the result.
|
|||
// The transformation factor has already been set correctly.
|
|||
currentObjective.toOriginalValueTransformationOffset = storm::utility::one<ValueType>(); |
|||
|
|||
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), result, currentObjective); |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective, boost::optional<std::string> const& optionalRewardModelName) { |
|||
if(formula.isReachabilityProbabilityFormula()){ |
|||
preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), result, currentObjective); |
|||
return; |
|||
} |
|||
|
|||
CheckTask<storm::logic::Formula, ValueType> targetTask(formula.getSubformula()); |
|||
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(result.preprocessedModel); |
|||
STORM_LOG_THROW(mc.canHandle(targetTask), storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " should be propositional."); |
|||
storm::storage::BitVector targetStates = mc.check(targetTask)->asExplicitQualitativeCheckResult().getTruthValuesVector(); |
|||
|
|||
auto duplicatorResult = storm::transformer::StateDuplicator<SparseModelType>::transform(result.preprocessedModel, targetStates); |
|||
updatePreprocessedModel(result, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping); |
|||
|
|||
// Add a reward model that gives zero reward to the actions of states of the second copy.
|
|||
RewardModelType objectiveRewards(boost::none); |
|||
if(formula.isReachabilityRewardFormula()) { |
|||
objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); |
|||
objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false); |
|||
if(objectiveRewards.hasStateRewards()) { |
|||
storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), duplicatorResult.secondCopy, storm::utility::zero<ValueType>()); |
|||
} |
|||
if(objectiveRewards.hasStateActionRewards()) { |
|||
for(auto secondCopyState : duplicatorResult.secondCopy) { |
|||
std::fill_n(objectiveRewards.getStateActionRewardVector().begin() + result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[secondCopyState], result.preprocessedModel.getTransitionMatrix().getRowGroupSize(secondCopyState), storm::utility::zero<ValueType>()); |
|||
} |
|||
} |
|||
} else if(formula.isReachabilityTimeFormula() && result.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton)) { |
|||
objectiveRewards = RewardModelType(std::vector<ValueType>(result.preprocessedModel.getNumberOfStates(), storm::utility::zero<ValueType>())); |
|||
storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), dynamic_cast<storm::models::sparse::MarkovAutomaton<ValueType>*>(&result.preprocessedModel)->getMarkovianStates() & duplicatorResult.firstCopy, storm::utility::one<ValueType>()); |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The formula " << formula << " neither considers reachability probabilities nor reachability rewards " << (result.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton) ? "nor reachability time" : "") << ". This is not supported."); |
|||
} |
|||
if(!currentObjective.rewardsArePositive){ |
|||
if(objectiveRewards.hasStateRewards()) { |
|||
storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one<ValueType>()); |
|||
} |
|||
if(objectiveRewards.hasStateActionRewards()) { |
|||
storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one<ValueType>()); |
|||
} |
|||
} |
|||
result.preprocessedModel.addRewardModel(currentObjective.rewardModelName, std::move(objectiveRewards)); |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective, boost::optional<std::string> const& optionalRewardModelName) { |
|||
STORM_LOG_THROW(result.originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type."); |
|||
currentObjective.upperTimeBound = formula.getBound(); |
|||
currentObjective.upperTimeBoundStrict = formula.isBoundStrict(); |
|||
|
|||
RewardModelType objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); |
|||
objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false); |
|||
if(!currentObjective.rewardsArePositive){ |
|||
if(objectiveRewards.hasStateRewards()) { |
|||
storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one<ValueType>()); |
|||
} |
|||
if(objectiveRewards.hasStateActionRewards()) { |
|||
storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one<ValueType>()); |
|||
} |
|||
} |
|||
result.preprocessedModel.addRewardModel(currentObjective.rewardModelName, std::move(objectiveRewards)); |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::preprocessTotalRewardFormula(ReturnType& result, PcaaObjective<ValueType>& currentObjective, boost::optional<std::string> const& optionalRewardModelName) { |
|||
RewardModelType objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); |
|||
objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false); |
|||
if(!currentObjective.rewardsArePositive){ |
|||
if(objectiveRewards.hasStateRewards()) { |
|||
storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one<ValueType>()); |
|||
} |
|||
if(objectiveRewards.hasStateActionRewards()) { |
|||
storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one<ValueType>()); |
|||
} |
|||
} |
|||
result.preprocessedModel.addRewardModel(currentObjective.rewardModelName, std::move(objectiveRewards)); |
|||
} |
|||
|
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::analyzeEndComponents(ReturnType& result, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) { |
|||
|
|||
result.ecActions = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false); |
|||
std::vector<storm::storage::MaximalEndComponent> ecs; |
|||
auto mecDecomposition = storm::storage::MaximalEndComponentDecomposition<ValueType>(result.preprocessedModel.getTransitionMatrix(), backwardTransitions); |
|||
STORM_LOG_ASSERT(!mecDecomposition.empty(), "Empty maximal end component decomposition."); |
|||
ecs.reserve(mecDecomposition.size()); |
|||
for(auto& mec : mecDecomposition) { |
|||
for(auto const& stateActionsPair : mec) { |
|||
for(auto const& action : stateActionsPair.second) { |
|||
result.ecActions.set(action); |
|||
} |
|||
} |
|||
ecs.push_back(std::move(mec)); |
|||
} |
|||
|
|||
result.possiblyRecurrentStates = storm::storage::BitVector(result.preprocessedModel.getNumberOfStates(), false); |
|||
storm::storage::BitVector neutralActions = ~(result.actionsWithNegativeReward | result.actionsWithPositiveReward); |
|||
storm::storage::BitVector statesInCurrentECWithNeutralAction(result.preprocessedModel.getNumberOfStates(), false); |
|||
for(uint_fast64_t ecIndex = 0; ecIndex < ecs.size(); ++ecIndex) { //we will insert new ecs in the vector (thus no iterators for the loop)
|
|||
bool currentECIsNeutral = true; |
|||
for(auto const& stateActionsPair : ecs[ecIndex]) { |
|||
bool stateHasNeutralActionWithinEC = false; |
|||
for(auto const& action : stateActionsPair.second) { |
|||
stateHasNeutralActionWithinEC |= neutralActions.get(action); |
|||
} |
|||
statesInCurrentECWithNeutralAction.set(stateActionsPair.first, stateHasNeutralActionWithinEC); |
|||
currentECIsNeutral &= stateHasNeutralActionWithinEC; |
|||
} |
|||
if(currentECIsNeutral) { |
|||
result.possiblyRecurrentStates |= statesInCurrentECWithNeutralAction; |
|||
}else{ |
|||
// Check if the ec contains neutral sub ecs. This is done by adding the subECs to our list of ECs
|
|||
// A neutral subEC only consist of states that can stay in statesInCurrentECWithNeutralAction
|
|||
statesInCurrentECWithNeutralAction = storm::utility::graph::performProb0E(result.preprocessedModel.getTransitionMatrix(), result.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), backwardTransitions,statesInCurrentECWithNeutralAction, ~statesInCurrentECWithNeutralAction); |
|||
auto subECs = storm::storage::MaximalEndComponentDecomposition<ValueType>(result.preprocessedModel.getTransitionMatrix(), backwardTransitions, statesInCurrentECWithNeutralAction); |
|||
ecs.reserve(ecs.size() + subECs.size()); |
|||
for(auto& ec : subECs){ |
|||
ecs.push_back(std::move(ec)); |
|||
} |
|||
} |
|||
statesInCurrentECWithNeutralAction.clear(); |
|||
} |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
void SparsePcaaPreprocessor<SparseModelType>::ensureRewardFiniteness(ReturnType& result, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) { |
|||
STORM_LOG_THROW((result.actionsWithPositiveReward & result.ecActions).empty(), storm::exceptions::InvalidPropertyException, "Infinite reward: There is one maximizing objective for which infinite reward is possible. This is not supported."); |
|||
|
|||
//Check whether the states that can be visited inf. often are reachable with prob. 1 under some scheduler
|
|||
storm::storage::BitVector statesReachingNegativeRewardsFinitelyOftenForSomeScheduler = storm::utility::graph::performProb1E(result.preprocessedModel.getTransitionMatrix(), result.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), backwardTransitions, storm::storage::BitVector(result.preprocessedModel.getNumberOfStates(), true), result.possiblyRecurrentStates); |
|||
STORM_LOG_THROW(!(statesReachingNegativeRewardsFinitelyOftenForSomeScheduler & result.preprocessedModel.getInitialStates()).empty(), storm::exceptions::InvalidPropertyException, "Infinite Rewards: For every scheduler, the induced reward for one or more of the objectives that minimize rewards is infinity."); |
|||
|
|||
if(!statesReachingNegativeRewardsFinitelyOftenForSomeScheduler.full()) { |
|||
// Remove the states that for any scheduler have one objective with infinite expected reward.
|
|||
auto subsystemBuilderResult = storm::transformer::SubsystemBuilder<SparseModelType>::transform(result.preprocessedModel, statesReachingNegativeRewardsFinitelyOftenForSomeScheduler, storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), true)); |
|||
updatePreprocessedModel(result, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping); |
|||
result.ecActions = result.ecActions % subsystemBuilderResult.keptActions; |
|||
result.actionsWithPositiveReward = result.actionsWithPositiveReward % subsystemBuilderResult.keptActions; |
|||
result.actionsWithNegativeReward = result.actionsWithNegativeReward % subsystemBuilderResult.keptActions; |
|||
result.possiblyRecurrentStates = result.possiblyRecurrentStates % statesReachingNegativeRewardsFinitelyOftenForSomeScheduler; |
|||
} |
|||
} |
|||
|
|||
|
|||
|
|||
template class SparsePcaaPreprocessor<storm::models::sparse::Mdp<double>>; |
|||
template class SparsePcaaPreprocessor<storm::models::sparse::MarkovAutomaton<double>>; |
|||
|
|||
#ifdef STORM_HAVE_CARL
|
|||
template class SparsePcaaPreprocessor<storm::models::sparse::Mdp<storm::RationalNumber>>; |
|||
template class SparsePcaaPreprocessor<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>; |
|||
#endif
|
|||
} |
|||
} |
|||
} |
|||
@ -1,82 +0,0 @@ |
|||
#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSOR_H_ |
|||
#define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSOR_H_ |
|||
|
|||
#include <memory> |
|||
|
|||
#include "storm/logic/Formulas.h" |
|||
#include "storm/storage/BitVector.h" |
|||
#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessorReturnType.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace multiobjective { |
|||
|
|||
/* |
|||
* This class invokes the necessary preprocessing for the Pareto Curve Approximation Algorithm (PCAA) |
|||
*/ |
|||
template <class SparseModelType> |
|||
class SparsePcaaPreprocessor { |
|||
public: |
|||
typedef typename SparseModelType::ValueType ValueType; |
|||
typedef typename SparseModelType::RewardModelType RewardModelType; |
|||
typedef SparsePcaaPreprocessorReturnType<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, i.e., the formula is simple. |
|||
*/ |
|||
static ReturnType preprocess(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula); |
|||
|
|||
private: |
|||
/*! |
|||
* Initializes the returned Information |
|||
* @param originalModel The considered model |
|||
* @param originalFormula the considered formula |
|||
*/ |
|||
static ReturnType initializeResult(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel); |
|||
|
|||
/*! |
|||
* Updates the preprocessed model stored in the given result to the given model. |
|||
* The given newToOldStateIndexMapping should give for each state in the newPreprocessedModel |
|||
* the index of the state in the current result.preprocessedModel. |
|||
*/ |
|||
static void updatePreprocessedModel(ReturnType& result, SparseModelType& newPreprocessedModel, std::vector<uint_fast64_t>& newToOldStateIndexMapping); |
|||
|
|||
/*! |
|||
* Apply the neccessary preprocessing for the given formula. |
|||
* @param formula the current (sub)formula |
|||
* @param result the information collected so far |
|||
* @param currentObjective the currently considered objective. The given formula should be a a (sub)formula of this objective |
|||
* @param optionalRewardModelName the reward model name that is considered for the formula (if available) |
|||
*/ |
|||
static void preprocessOperatorFormula(storm::logic::OperatorFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective); |
|||
static void preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective); |
|||
static void preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective); |
|||
static void preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective); |
|||
static void preprocessUntilFormula(storm::logic::UntilFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective); |
|||
static void preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective); |
|||
static void preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective); |
|||
static void preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective, boost::optional<std::string> const& optionalRewardModelName = boost::none); |
|||
static void preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective, boost::optional<std::string> const& optionalRewardModelName = boost::none); |
|||
static void preprocessTotalRewardFormula(ReturnType& result, PcaaObjective<ValueType>& currentObjective, boost::optional<std::string> const& optionalRewardModelName = boost::none); // The total reward formula itself does not need to be provided as it is unique. |
|||
|
|||
/*! |
|||
* Analyzes the end components of the preprocessed model. That is: |
|||
* -get the set of actions that are part of an end component |
|||
* -Find the states that can be visited infinitely often without inducing infinite reward |
|||
*/ |
|||
static void analyzeEndComponents(ReturnType& result, storm::storage::SparseMatrix<ValueType> const& backwardTransitions); |
|||
|
|||
/*! |
|||
* Checks whether the occurring expected rewards are finite. If not, the input is rejected. |
|||
* Also removes all states for which no finite reward wrt. all objectives is possible |
|||
*/ |
|||
static void ensureRewardFiniteness(ReturnType& result, storm::storage::SparseMatrix<ValueType> const& backwardTransitions); |
|||
|
|||
}; |
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSOR_H_ */ |
|||
@ -0,0 +1,137 @@ |
|||
#include "storm/storage/memorystructure/MemoryStructure.h"
|
|||
|
|||
#include <iostream>
|
|||
|
|||
#include "storm/logic/Formulas.h"
|
|||
#include "storm/utility/macros.h"
|
|||
#include "storm/storage/memorystructure/SparseModelMemoryProduct.h"
|
|||
|
|||
#include "storm/exceptions/InvalidOperationException.h"
|
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
|
|||
MemoryStructure::MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling) : transitions(transitionMatrix), stateLabeling(memoryStateLabeling) { |
|||
// intentionally left empty
|
|||
} |
|||
|
|||
MemoryStructure::MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling) : transitions(std::move(transitionMatrix)), stateLabeling(std::move(memoryStateLabeling)) { |
|||
// intentionally left empty
|
|||
} |
|||
|
|||
MemoryStructure::TransitionMatrix const& MemoryStructure::getTransitionMatrix() const { |
|||
return transitions; |
|||
} |
|||
|
|||
storm::models::sparse::StateLabeling const& MemoryStructure::getStateLabeling() const { |
|||
return stateLabeling; |
|||
} |
|||
|
|||
uint_fast64_t MemoryStructure::getNumberOfStates() const { |
|||
return transitions.size(); |
|||
} |
|||
|
|||
MemoryStructure MemoryStructure::product(MemoryStructure const& rhs) const { |
|||
uint_fast64_t lhsNumStates = this->getTransitionMatrix().size(); |
|||
uint_fast64_t rhsNumStates = rhs.getTransitionMatrix().size(); |
|||
uint_fast64_t resNumStates = lhsNumStates * rhsNumStates; |
|||
|
|||
// Transition matrix
|
|||
TransitionMatrix resultTransitions(resNumStates, std::vector<std::shared_ptr<storm::logic::Formula const>>(resNumStates)); |
|||
uint_fast64_t resState = 0; |
|||
for (uint_fast64_t lhsState = 0; lhsState < lhsNumStates; ++lhsState) { |
|||
for (uint_fast64_t rhsState = 0; rhsState < rhsNumStates; ++rhsState) { |
|||
assert (resState == (lhsState * rhsNumStates) + rhsState); |
|||
auto& resStateTransitions = resultTransitions[resState]; |
|||
for (uint_fast64_t lhsTransitionTarget = 0; lhsTransitionTarget < lhsNumStates; ++lhsTransitionTarget) { |
|||
auto& lhsTransition = this->getTransitionMatrix()[lhsState][lhsTransitionTarget]; |
|||
if (lhsTransition) { |
|||
for (uint_fast64_t rhsTransitionTarget = 0; rhsTransitionTarget < rhsNumStates; ++rhsTransitionTarget) { |
|||
auto& rhsTransition = rhs.getTransitionMatrix()[rhsState][rhsTransitionTarget]; |
|||
if (rhsTransition) { |
|||
uint_fast64_t resTransitionTarget = (lhsTransitionTarget * rhsNumStates) + rhsTransitionTarget; |
|||
resStateTransitions[resTransitionTarget] = std::make_shared<storm::logic::BinaryBooleanStateFormula const>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, lhsTransition,rhsTransition); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
++resState; |
|||
} |
|||
} |
|||
|
|||
// State Labels
|
|||
storm::models::sparse::StateLabeling resultLabeling(resNumStates); |
|||
for (std::string lhsLabel : this->getStateLabeling().getLabels()) { |
|||
storm::storage::BitVector const& lhsLabeledStates = this->getStateLabeling().getStates(lhsLabel); |
|||
storm::storage::BitVector resLabeledStates(resNumStates, false); |
|||
for (auto const& lhsState : lhsLabeledStates) { |
|||
for (uint_fast64_t rhsState = 0; rhsState < rhsNumStates; ++rhsState) { |
|||
resState = (lhsState * rhsNumStates) + rhsState; |
|||
resLabeledStates.set(resState, true); |
|||
} |
|||
} |
|||
resultLabeling.addLabel(lhsLabel, std::move(resLabeledStates)); |
|||
} |
|||
for (std::string rhsLabel : rhs.getStateLabeling().getLabels()) { |
|||
STORM_LOG_THROW(!resultLabeling.containsLabel(rhsLabel), storm::exceptions::InvalidOperationException, "Failed to build the product of two memory structures: State labelings are not disjoint as both structures contain the label " << rhsLabel << "."); |
|||
storm::storage::BitVector const& rhsLabeledStates = rhs.getStateLabeling().getStates(rhsLabel); |
|||
storm::storage::BitVector resLabeledStates(resNumStates, false); |
|||
for (auto const& rhsState : rhsLabeledStates) { |
|||
for (uint_fast64_t lhsState = 0; lhsState < lhsNumStates; ++lhsState) { |
|||
resState = (lhsState * rhsNumStates) + rhsState; |
|||
resLabeledStates.set(resState, true); |
|||
} |
|||
} |
|||
resultLabeling.addLabel(rhsLabel, std::move(resLabeledStates)); |
|||
} |
|||
//return MemoryStructure(std::move(resultTransitions), std::move(resultLabeling));
|
|||
|
|||
MemoryStructure res(std::move(resultTransitions), std::move(resultLabeling)); |
|||
return res; |
|||
|
|||
} |
|||
|
|||
template <typename ValueType> |
|||
SparseModelMemoryProduct<ValueType> MemoryStructure::product(storm::models::sparse::Model<ValueType> const& sparseModel) const { |
|||
return SparseModelMemoryProduct<ValueType>(sparseModel, *this); |
|||
} |
|||
|
|||
std::string MemoryStructure::toString() const { |
|||
std::stringstream stream; |
|||
|
|||
stream << "Memory Structure with " << getNumberOfStates() << " states: " << std::endl; |
|||
|
|||
for (uint_fast64_t state = 0; state < getNumberOfStates(); ++state) { |
|||
stream << "State " << state << ": Labels = {"; |
|||
bool firstLabel = true; |
|||
for (auto const& label : getStateLabeling().getLabelsOfState(state)) { |
|||
if (!firstLabel) { |
|||
stream << ", "; |
|||
} |
|||
firstLabel = false; |
|||
stream << label; |
|||
} |
|||
stream << "}, Transitions: " << std::endl; |
|||
for (uint_fast64_t transitionTarget = 0; transitionTarget < getNumberOfStates(); ++transitionTarget) { |
|||
stream << "\t From " << state << " to " << transitionTarget << ": \t"; |
|||
auto const& transition = getTransitionMatrix()[state][transitionTarget]; |
|||
if (transition) { |
|||
stream << *transition; |
|||
} else { |
|||
stream << "false"; |
|||
} |
|||
stream << std::endl; |
|||
} |
|||
} |
|||
|
|||
return stream.str(); |
|||
} |
|||
|
|||
template SparseModelMemoryProduct<double> MemoryStructure::product(storm::models::sparse::Model<double> const& sparseModel) const; |
|||
template SparseModelMemoryProduct<storm::RationalNumber> MemoryStructure::product(storm::models::sparse::Model<storm::RationalNumber> const& sparseModel) const; |
|||
|
|||
|
|||
} |
|||
} |
|||
|
|||
|
|||
@ -0,0 +1,68 @@ |
|||
#pragma once |
|||
|
|||
#include <vector> |
|||
#include <memory> |
|||
|
|||
#include "storm/logic/Formula.h" |
|||
#include "storm/models/sparse/StateLabeling.h" |
|||
#include "storm/models/sparse/Model.h" |
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
|
|||
template <typename ValueType> |
|||
class SparseModelMemoryProduct; |
|||
|
|||
/*! |
|||
* This class represents a (deterministic) memory structure that can be used to encode certain events |
|||
* (such as reaching a set of goal states) into the state space of the model. |
|||
*/ |
|||
class MemoryStructure { |
|||
public: |
|||
|
|||
typedef std::vector<std::vector<std::shared_ptr<storm::logic::Formula const>>> TransitionMatrix; |
|||
|
|||
/*! |
|||
* Creates a memory structure with the given transition matrix and the given memory state labeling. |
|||
* The initial state is always the state with index 0. |
|||
* The transition matrix is assumed to contain propositional state formulas. The entry |
|||
* transitionMatrix[m][n] specifies the set of model states which trigger a transition from memory |
|||
* state m to memory state n. |
|||
* Transitions are assumed to be deterministic and complete, i.e., the formulas in |
|||
* transitionMatrix[m] form a partition of the state space of the considered model. |
|||
* |
|||
* @param transitionMatrix The transition matrix |
|||
* @param memoryStateLabeling A labeling of the memory states to specify, e.g., accepting states |
|||
*/ |
|||
MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling); |
|||
MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling); |
|||
|
|||
TransitionMatrix const& getTransitionMatrix() const; |
|||
storm::models::sparse::StateLabeling const& getStateLabeling() const; |
|||
uint_fast64_t getNumberOfStates() const; |
|||
|
|||
/*! |
|||
* Builds the product of this memory structure and the given memory structure. |
|||
* The resulting memory structure will have the state labels of both given structures. |
|||
* Throws an exception if the state labelings are not disjoint. |
|||
*/ |
|||
MemoryStructure product(MemoryStructure const& rhs) const; |
|||
|
|||
/*! |
|||
* Builds the product of this memory structure and the given sparse model. |
|||
* An exception is thrown if the state labelings of this memory structure and the given model are not disjoint. |
|||
*/ |
|||
template <typename ValueType> |
|||
SparseModelMemoryProduct<ValueType> product(storm::models::sparse::Model<ValueType> const& sparseModel) const; |
|||
|
|||
std::string toString() const; |
|||
|
|||
private: |
|||
TransitionMatrix transitions; |
|||
storm::models::sparse::StateLabeling stateLabeling; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
|
|||
|
|||
@ -0,0 +1,36 @@ |
|||
#include "storm/storage/memorystructure/MemoryStructureBuilder.h"
|
|||
|
|||
#include "storm/logic/FragmentSpecification.h"
|
|||
#include "storm/utility/macros.h"
|
|||
|
|||
#include "storm/exceptions/InvalidOperationException.h"
|
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
|
|||
MemoryStructureBuilder::MemoryStructureBuilder(uint_fast64_t const& numberOfStates) : transitions(numberOfStates, std::vector<std::shared_ptr<storm::logic::Formula const>>(numberOfStates)), stateLabeling(numberOfStates) { |
|||
// Intentionally left empty
|
|||
} |
|||
|
|||
void MemoryStructureBuilder::setTransition(uint_fast64_t const& startState, uint_fast64_t const& goalState, std::shared_ptr<storm::logic::Formula const> formula) { |
|||
STORM_LOG_THROW(startState < transitions.size(), storm::exceptions::InvalidOperationException, "Invalid index of start state: " << startState << ". There are only " << transitions.size() << " states in this memory structure."); |
|||
STORM_LOG_THROW(goalState < transitions.size(), storm::exceptions::InvalidOperationException, "Invalid index of goal state: " << startState << ". There are only " << transitions.size() << " states in this memory structure."); |
|||
STORM_LOG_THROW(formula->isInFragment(storm::logic::propositional()), storm::exceptions::InvalidOperationException, "The formula '" << *formula << "' is not propositional"); |
|||
|
|||
transitions[startState][goalState] = formula; |
|||
} |
|||
|
|||
void MemoryStructureBuilder::setLabel(uint_fast64_t const& state, std::string const& label) { |
|||
STORM_LOG_THROW(state < transitions.size(), storm::exceptions::InvalidOperationException, "Can not add label to state with index " << state << ". There are only " << transitions.size() << " states in this memory structure."); |
|||
if (!stateLabeling.containsLabel(label)) { |
|||
stateLabeling.addLabel(label); |
|||
} |
|||
stateLabeling.addLabelToState(label, state); |
|||
} |
|||
|
|||
MemoryStructure MemoryStructureBuilder::build() { |
|||
return MemoryStructure(std::move(transitions), std::move(stateLabeling)); |
|||
} |
|||
|
|||
} |
|||
} |
|||
@ -0,0 +1,49 @@ |
|||
#pragma once |
|||
|
|||
#include <vector> |
|||
#include <memory> |
|||
|
|||
#include "storm/logic/Formula.h" |
|||
#include "storm/models/sparse/StateLabeling.h" |
|||
#include "storm/storage/memorystructure/MemoryStructure.h" |
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
|
|||
|
|||
class MemoryStructureBuilder { |
|||
public: |
|||
|
|||
/*! |
|||
* Initializes a new builder for a memory structure |
|||
* @param numberOfStates The number of states the resulting memory structure should have |
|||
*/ |
|||
MemoryStructureBuilder(uint_fast64_t const& numberOfStates); |
|||
|
|||
/*! |
|||
* Specifies a transition. The formula should be a propositional formula |
|||
*/ |
|||
void setTransition(uint_fast64_t const& startState, uint_fast64_t const& goalState, std::shared_ptr<storm::logic::Formula const> formula); |
|||
|
|||
/*! |
|||
* Sets a label to the given state. |
|||
*/ |
|||
void setLabel(uint_fast64_t const& state, std::string const& label); |
|||
|
|||
/*! |
|||
* Builds the memory structure. |
|||
* @note Calling this invalidates this builder. |
|||
* @note When calling this method, the specified transitions should be deterministic and complete. This is not checked. |
|||
*/ |
|||
MemoryStructure build(); |
|||
|
|||
|
|||
private: |
|||
MemoryStructure::TransitionMatrix transitions; |
|||
storm::models::sparse::StateLabeling stateLabeling; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
|
|||
|
|||
@ -0,0 +1,330 @@ |
|||
#include "storm/storage/memorystructure/SparseModelMemoryProduct.h"
|
|||
|
|||
#include <boost/optional.hpp>
|
|||
|
|||
#include "storm/models/sparse/Dtmc.h"
|
|||
#include "storm/models/sparse/Mdp.h"
|
|||
#include "storm/models/sparse/Ctmc.h"
|
|||
#include "storm/models/sparse/MarkovAutomaton.h"
|
|||
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
|
|||
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
|
|||
#include "storm/utility/constants.h"
|
|||
#include "storm/utility/macros.h"
|
|||
|
|||
#include "storm/exceptions/InvalidOperationException.h"
|
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
|
|||
template <typename ValueType> |
|||
SparseModelMemoryProduct<ValueType>::SparseModelMemoryProduct(storm::models::sparse::Model<ValueType> const& sparseModel, storm::storage::MemoryStructure const& memoryStructure) : model(sparseModel), memory(memoryStructure) { |
|||
// intentionally left empty
|
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType>> SparseModelMemoryProduct<ValueType>::build() { |
|||
uint_fast64_t modelStateCount = model.getNumberOfStates(); |
|||
uint_fast64_t memoryStateCount = memory.getNumberOfStates(); |
|||
|
|||
std::vector<uint_fast64_t> memorySuccessors = computeMemorySuccessors(); |
|||
|
|||
// Get the initial states and reachable states. A stateIndex s corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount)
|
|||
storm::storage::BitVector initialStates(modelStateCount * memoryStateCount, false); |
|||
for (auto const& modelInit : model.getInitialStates()) { |
|||
// Note: The initial state of a memory structure is always 0.
|
|||
initialStates.set(modelInit * memoryStateCount + memorySuccessors[modelInit * memoryStateCount], true); |
|||
} |
|||
storm::storage::BitVector reachableStates = computeReachableStates(memorySuccessors, initialStates); |
|||
// Compute the mapping to the states of the result
|
|||
uint_fast64_t reachableStateCount = 0; |
|||
toResultStateMapping = std::vector<uint_fast64_t> (model.getNumberOfStates() * memory.getNumberOfStates(), std::numeric_limits<uint_fast64_t>::max()); |
|||
for (auto const& reachableState : reachableStates) { |
|||
toResultStateMapping[reachableState] = reachableStateCount; |
|||
++reachableStateCount; |
|||
} |
|||
|
|||
// Build the model components
|
|||
storm::storage::SparseMatrix<ValueType> transitionMatrix = model.getTransitionMatrix().hasTrivialRowGrouping() ? |
|||
buildDeterministicTransitionMatrix(reachableStates, memorySuccessors) : |
|||
buildNondeterministicTransitionMatrix(reachableStates, memorySuccessors); |
|||
storm::models::sparse::StateLabeling labeling = buildStateLabeling(transitionMatrix); |
|||
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels = buildRewardModels(transitionMatrix, memorySuccessors); |
|||
|
|||
// Add the label for the initial states. We need to translate the state indices w.r.t. the set of reachable states.
|
|||
labeling.addLabel("init", initialStates % reachableStates); |
|||
|
|||
return buildResult(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels)); |
|||
|
|||
} |
|||
|
|||
template <typename ValueType> |
|||
uint_fast64_t const& SparseModelMemoryProduct<ValueType>::getResultState(uint_fast64_t const& modelState, uint_fast64_t const& memoryState) const { |
|||
return toResultStateMapping[modelState * memory.getNumberOfStates() + memoryState]; |
|||
} |
|||
|
|||
|
|||
template <typename ValueType> |
|||
std::vector<uint_fast64_t> SparseModelMemoryProduct<ValueType>::computeMemorySuccessors() const { |
|||
uint_fast64_t modelStateCount = model.getNumberOfStates(); |
|||
uint_fast64_t memoryStateCount = memory.getNumberOfStates(); |
|||
std::vector<uint_fast64_t> result(modelStateCount * memoryStateCount, std::numeric_limits<uint_fast64_t>::max()); |
|||
|
|||
storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<ValueType>> mc(model); |
|||
for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { |
|||
for (uint_fast64_t transitionGoal = 0; transitionGoal < memoryStateCount; ++transitionGoal) { |
|||
auto const& transition = memory.getTransitionMatrix()[memoryState][transitionGoal]; |
|||
if (transition) { |
|||
auto mcResult = mc.check(*transition); |
|||
for (auto const& modelState : mcResult->asExplicitQualitativeCheckResult().getTruthValuesVector()) { |
|||
result[modelState * memoryStateCount + memoryState] = transitionGoal; |
|||
} |
|||
} |
|||
} |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
storm::storage::BitVector SparseModelMemoryProduct<ValueType>::computeReachableStates(std::vector<uint_fast64_t> const& memorySuccessors, storm::storage::BitVector const& initialStates) const { |
|||
uint_fast64_t memoryStateCount = memory.getNumberOfStates(); |
|||
// Explore the reachable states via DFS.
|
|||
// A state s on the stack corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount)
|
|||
storm::storage::BitVector reachableStates = initialStates; |
|||
std::vector<uint_fast64_t> stack(reachableStates.begin(), reachableStates.end()); |
|||
while (!stack.empty()) { |
|||
uint_fast64_t stateIndex = stack.back(); |
|||
stack.pop_back(); |
|||
uint_fast64_t modelState = stateIndex / memoryStateCount; |
|||
uint_fast64_t memoryState = stateIndex % memoryStateCount; |
|||
|
|||
for (auto const& modelTransition : model.getTransitionMatrix().getRowGroup(modelState)) { |
|||
if (!storm::utility::isZero(modelTransition.getValue())) { |
|||
uint_fast64_t successorModelState = modelTransition.getColumn(); |
|||
uint_fast64_t successorMemoryState = memorySuccessors[successorModelState * memoryStateCount + memoryState]; |
|||
uint_fast64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState; |
|||
if (!reachableStates.get(successorStateIndex)) { |
|||
reachableStates.set(successorStateIndex, true); |
|||
stack.push_back(successorStateIndex); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
return reachableStates; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType>::buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector<uint_fast64_t> const& memorySuccessors) const { |
|||
uint_fast64_t memoryStateCount = memory.getNumberOfStates(); |
|||
uint_fast64_t numResStates = reachableStates.getNumberOfSetBits(); |
|||
uint_fast64_t numResTransitions = 0; |
|||
for (auto const& stateIndex : reachableStates) { |
|||
numResTransitions += model.getTransitionMatrix().getRow(stateIndex / memoryStateCount).getNumberOfEntries(); |
|||
} |
|||
|
|||
storm::storage::SparseMatrixBuilder<ValueType> builder(numResStates, numResStates, numResTransitions, true); |
|||
uint_fast64_t currentRow = 0; |
|||
for (auto const& stateIndex : reachableStates) { |
|||
uint_fast64_t modelState = stateIndex / memoryStateCount; |
|||
uint_fast64_t memoryState = stateIndex % memoryStateCount; |
|||
for (auto const& entry : model.getTransitionMatrix().getRow(modelState)) { |
|||
uint_fast64_t const& successorMemoryState = memorySuccessors[entry.getColumn() * memoryStateCount + memoryState]; |
|||
builder.addNextValue(currentRow, getResultState(entry.getColumn(), successorMemoryState), entry.getValue()); |
|||
} |
|||
++currentRow; |
|||
} |
|||
|
|||
return builder.build(); |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType>::buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector<uint_fast64_t> const& memorySuccessors) const { |
|||
uint_fast64_t memoryStateCount = memory.getNumberOfStates(); |
|||
uint_fast64_t numResStates = reachableStates.getNumberOfSetBits(); |
|||
uint_fast64_t numResChoices = 0; |
|||
uint_fast64_t numResTransitions = 0; |
|||
for (auto const& stateIndex : reachableStates) { |
|||
uint_fast64_t modelState = stateIndex / memoryStateCount; |
|||
for (uint_fast64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRow < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRow) { |
|||
++numResChoices; |
|||
numResTransitions += model.getTransitionMatrix().getRow(modelRow).getNumberOfEntries(); |
|||
} |
|||
} |
|||
|
|||
storm::storage::SparseMatrixBuilder<ValueType> builder(numResChoices, numResStates, numResTransitions, true, true, numResStates); |
|||
uint_fast64_t currentRow = 0; |
|||
for (auto const& stateIndex : reachableStates) { |
|||
uint_fast64_t modelState = stateIndex / memoryStateCount; |
|||
uint_fast64_t memoryState = stateIndex % memoryStateCount; |
|||
builder.newRowGroup(currentRow); |
|||
for (uint_fast64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRow < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRow) { |
|||
for (auto const& entry : model.getTransitionMatrix().getRow(modelRow)) { |
|||
uint_fast64_t const& successorMemoryState = memorySuccessors[entry.getColumn() * memoryStateCount + memoryState]; |
|||
builder.addNextValue(currentRow, getResultState(entry.getColumn(), successorMemoryState), entry.getValue()); |
|||
} |
|||
++currentRow; |
|||
} |
|||
} |
|||
|
|||
return builder.build(); |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
storm::models::sparse::StateLabeling SparseModelMemoryProduct<ValueType>::buildStateLabeling(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix) const { |
|||
uint_fast64_t modelStateCount = model.getNumberOfStates(); |
|||
uint_fast64_t memoryStateCount = memory.getNumberOfStates(); |
|||
|
|||
uint_fast64_t numResStates = resultTransitionMatrix.getRowGroupCount(); |
|||
storm::models::sparse::StateLabeling resultLabeling(numResStates); |
|||
|
|||
for (std::string modelLabel : model.getStateLabeling().getLabels()) { |
|||
if (modelLabel != "init") { |
|||
storm::storage::BitVector resLabeledStates(numResStates, false); |
|||
for (auto const& modelState : model.getStateLabeling().getStates(modelLabel)) { |
|||
for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { |
|||
uint_fast64_t const& resState = getResultState(modelState, memoryState); |
|||
// Check if the state exists in the result (i.e. if it is reachable)
|
|||
if (resState < numResStates) { |
|||
resLabeledStates.set(resState, true); |
|||
} |
|||
} |
|||
} |
|||
resultLabeling.addLabel(modelLabel, std::move(resLabeledStates)); |
|||
} |
|||
} |
|||
for (std::string memoryLabel : memory.getStateLabeling().getLabels()) { |
|||
STORM_LOG_THROW(!resultLabeling.containsLabel(memoryLabel), storm::exceptions::InvalidOperationException, "Failed to build the product of model and memory structure: State labelings are not disjoint as both structures contain the label " << memoryLabel << "."); |
|||
storm::storage::BitVector resLabeledStates(numResStates, false); |
|||
for (auto const& memoryState : memory.getStateLabeling().getStates(memoryLabel)) { |
|||
for (uint_fast64_t modelState = 0; modelState < modelStateCount; ++modelState) { |
|||
uint_fast64_t const& resState = getResultState(modelState, memoryState); |
|||
// Check if the state exists in the result (i.e. if it is reachable)
|
|||
if (resState < numResStates) { |
|||
resLabeledStates.set(resState, true); |
|||
} |
|||
} |
|||
} |
|||
resultLabeling.addLabel(memoryLabel, std::move(resLabeledStates)); |
|||
} |
|||
return resultLabeling; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> SparseModelMemoryProduct<ValueType>::buildRewardModels(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix, std::vector<uint_fast64_t> const& memorySuccessors) const { |
|||
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> result; |
|||
uint_fast64_t memoryStateCount = memory.getNumberOfStates(); |
|||
uint_fast64_t numResStates = resultTransitionMatrix.getRowGroupCount(); |
|||
|
|||
for (auto const& rewardModel : model.getRewardModels()) { |
|||
boost::optional<std::vector<ValueType>> stateRewards; |
|||
if (rewardModel.second.hasStateRewards()) { |
|||
stateRewards = std::vector<ValueType>(numResStates, storm::utility::zero<ValueType>()); |
|||
uint_fast64_t modelState = 0; |
|||
for (auto const& modelStateReward : rewardModel.second.getStateRewardVector()) { |
|||
if (!storm::utility::isZero(modelStateReward)) { |
|||
for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { |
|||
uint_fast64_t const& resState = getResultState(modelState, memoryState); |
|||
// Check if the state exists in the result (i.e. if it is reachable)
|
|||
if (resState < numResStates) { |
|||
stateRewards.get()[resState] = modelStateReward; |
|||
} |
|||
} |
|||
} |
|||
++modelState; |
|||
} |
|||
} |
|||
boost::optional<std::vector<ValueType>> stateActionRewards; |
|||
if (rewardModel.second.hasStateActionRewards()) { |
|||
stateActionRewards = std::vector<ValueType>(resultTransitionMatrix.getRowCount(), storm::utility::zero<ValueType>()); |
|||
uint_fast64_t modelState = 0; |
|||
uint_fast64_t modelRow = 0; |
|||
for (auto const& modelStateActionReward : rewardModel.second.getStateActionRewardVector()) { |
|||
if (!storm::utility::isZero(modelStateActionReward)) { |
|||
while (modelRow >= model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]) { |
|||
++modelState; |
|||
} |
|||
uint_fast64_t rowOffset = modelRow - model.getTransitionMatrix().getRowGroupIndices()[modelState]; |
|||
for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { |
|||
uint_fast64_t const& resState = getResultState(modelState, memoryState); |
|||
// Check if the state exists in the result (i.e. if it is reachable)
|
|||
if (resState < numResStates) { |
|||
stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset] = modelStateActionReward; |
|||
} |
|||
} |
|||
} |
|||
++modelRow; |
|||
} |
|||
} |
|||
boost::optional<storm::storage::SparseMatrix<ValueType>> transitionRewards; |
|||
if (rewardModel.second.hasTransitionRewards()) { |
|||
storm::storage::SparseMatrixBuilder<ValueType> builder(resultTransitionMatrix.getRowCount(), resultTransitionMatrix.getColumnCount()); |
|||
uint_fast64_t stateIndex = 0; |
|||
for (auto const& resState : toResultStateMapping) { |
|||
if (resState < numResStates) { |
|||
uint_fast64_t modelState = stateIndex / memoryStateCount; |
|||
uint_fast64_t memoryState = stateIndex % memoryStateCount; |
|||
uint_fast64_t rowGroupSize = resultTransitionMatrix.getRowGroupSize(resState); |
|||
for (uint_fast64_t rowOffset = 0; rowOffset < rowGroupSize; ++rowOffset) { |
|||
uint_fast64_t resRowIndex = resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset; |
|||
uint_fast64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + rowOffset; |
|||
for (auto const& entry : rewardModel.second.getTransitionRewardMatrix().getRow(modelRowIndex)) { |
|||
uint_fast64_t const& successorMemoryState = memorySuccessors[entry.getColumn() * memoryStateCount + memoryState]; |
|||
builder.addNextValue(resRowIndex, getResultState(entry.getColumn(), successorMemoryState), entry.getValue()); |
|||
} |
|||
} |
|||
} |
|||
++stateIndex; |
|||
} |
|||
transitionRewards = builder.build(); |
|||
} |
|||
result.insert(std::make_pair(rewardModel.first, storm::models::sparse::StandardRewardModel<ValueType>(std::move(stateRewards), std::move(stateActionRewards), std::move(transitionRewards)))); |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType>> SparseModelMemoryProduct<ValueType>::buildResult(storm::storage::SparseMatrix<ValueType>&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>>&& rewardModels) const { |
|||
switch (model.getType()) { |
|||
case storm::models::ModelType::Dtmc: |
|||
return std::make_shared<storm::models::sparse::Dtmc<ValueType>> (std::move(matrix), std::move(labeling), std::move(rewardModels)); |
|||
case storm::models::ModelType::Mdp: |
|||
return std::make_shared<storm::models::sparse::Mdp<ValueType>> (std::move(matrix), std::move(labeling), std::move(rewardModels)); |
|||
case storm::models::ModelType::Ctmc: |
|||
return std::make_shared<storm::models::sparse::Ctmc<ValueType>> (std::move(matrix), std::move(labeling), std::move(rewardModels)); |
|||
case storm::models::ModelType::MarkovAutomaton: |
|||
{ |
|||
// We also need to translate the exit rates and the Markovian states
|
|||
uint_fast64_t numResStates = matrix.getRowGroupCount(); |
|||
uint_fast64_t memoryStateCount = memory.getNumberOfStates(); |
|||
std::vector<ValueType> resultExitRates; |
|||
resultExitRates.reserve(matrix.getRowGroupCount()); |
|||
storm::storage::BitVector resultMarkovianStates(numResStates, false); |
|||
auto const& modelExitRates = dynamic_cast<storm::models::sparse::MarkovAutomaton<ValueType> const&>(model).getExitRates(); |
|||
auto const& modelMarkovianStates = dynamic_cast<storm::models::sparse::MarkovAutomaton<ValueType> const&>(model).getMarkovianStates(); |
|||
|
|||
uint_fast64_t stateIndex = 0; |
|||
for (auto const& resState : toResultStateMapping) { |
|||
if (resState < numResStates) { |
|||
assert(resState == resultExitRates.size()); |
|||
uint_fast64_t modelState = stateIndex / memoryStateCount; |
|||
resultExitRates.push_back(modelExitRates[modelState]); |
|||
if (modelMarkovianStates.get(modelState)) { |
|||
resultMarkovianStates.set(resState, true); |
|||
} |
|||
} |
|||
++stateIndex; |
|||
} |
|||
return std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>> (std::move(matrix), std::move(labeling), std::move(resultMarkovianStates), std::move(resultExitRates), true, std::move(rewardModels)); |
|||
} |
|||
default: |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Memory Structure Product for Model Type " << model.getType() << " is not supported"); |
|||
} |
|||
} |
|||
|
|||
template class SparseModelMemoryProduct<double>; |
|||
template class SparseModelMemoryProduct<storm::RationalNumber>; |
|||
template class SparseModelMemoryProduct<storm::RationalFunction>; |
|||
|
|||
} |
|||
} |
|||
|
|||
|
|||
@ -0,0 +1,72 @@ |
|||
#pragma once |
|||
|
|||
#include <memory> |
|||
#include <string> |
|||
#include <unordered_map> |
|||
|
|||
#include "storm/storage/BitVector.h" |
|||
#include "storm/storage/memorystructure/MemoryStructure.h" |
|||
#include "storm/models/sparse/Model.h" |
|||
#include "storm/models/sparse/StandardRewardModel.h" |
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
/*! |
|||
* This class builds the product of the given sparse model and the given memory structure. |
|||
* This is similar to the well-known product of a model with a deterministic rabin automaton. |
|||
* Note: we already do one memory-structure-step for the initial state, i.e., if s is an initial state of |
|||
* the given model and s satisfies memoryStructure.getTransitionMatrix[0][n], then (s,n) will be the corresponding |
|||
* initial state of the resulting model. |
|||
* |
|||
* The states of the resulting sparse model will have the original state labels plus the labels of this |
|||
* memory structure. |
|||
* An exception is thrown if the state labelings are not disjoint. |
|||
*/ |
|||
template <typename ValueType> |
|||
class SparseModelMemoryProduct { |
|||
public: |
|||
|
|||
SparseModelMemoryProduct(storm::models::sparse::Model<ValueType> const& sparseModel, storm::storage::MemoryStructure const& memoryStructure); |
|||
|
|||
// Invokes the building of the product |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType>> build(); |
|||
|
|||
// Retrieves the state of the resulting model that represents the given memory and model state. |
|||
// An invalid index is returned, if the specifyied state does not exist (i.e., if it is not reachable). |
|||
uint_fast64_t const& getResultState(uint_fast64_t const& modelState, uint_fast64_t const& memoryState) const; |
|||
|
|||
private: |
|||
|
|||
// Computes for each pair of memory and model state the successor memory state |
|||
// The resulting vector maps (modelState * memoryStateCount) + memoryState to the corresponding successor state of the memory structure |
|||
std::vector<uint_fast64_t> computeMemorySuccessors() const; |
|||
|
|||
// Computes the reachable states of the resulting model |
|||
storm::storage::BitVector computeReachableStates(std::vector<uint_fast64_t> const& memorySuccessors, storm::storage::BitVector const& initialStates) const; |
|||
|
|||
// Methods that build the model components |
|||
// Matrix for deterministic models |
|||
storm::storage::SparseMatrix<ValueType> buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector<uint_fast64_t> const& memorySuccessors) const; |
|||
// Matrix for nondeterministic models |
|||
storm::storage::SparseMatrix<ValueType> buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector<uint_fast64_t> const& memorySuccessors) const; |
|||
// State labeling. Note: DOES NOT ADD A LABEL FOR THE INITIAL STATES |
|||
storm::models::sparse::StateLabeling buildStateLabeling(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix) const; |
|||
// Reward models |
|||
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> buildRewardModels(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix, std::vector<uint_fast64_t> const& memorySuccessors) const; |
|||
|
|||
// Builds the resulting model |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildResult(storm::storage::SparseMatrix<ValueType>&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>>&& rewardModels) const; |
|||
|
|||
|
|||
// Maps (modelState * memoryStateCount) + memoryState to the state in the result that represents (memoryState,modelState) |
|||
std::vector<uint_fast64_t> toResultStateMapping; |
|||
|
|||
|
|||
storm::models::sparse::Model<ValueType> const& model; |
|||
storm::storage::MemoryStructure const& memory; |
|||
|
|||
}; |
|||
} |
|||
} |
|||
|
|||
|
|||
@ -0,0 +1,35 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h"
|
|||
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
|
|||
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
|
|||
#include "storm/models/sparse/MarkovAutomaton.h"
|
|||
#include "storm/settings/modules/GeneralSettings.h"
|
|||
#include "storm/settings/modules/MultiObjectiveSettings.h"
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/utility/storm.h"
|
|||
|
|||
|
|||
TEST(SparseMaCbMultiObjectiveModelCheckerTest, server) { |
|||
|
|||
std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/server.ma"; |
|||
std::string formulasAsString = "multi(T>=5/3 [ F \"error\" ], P>=7/12 [ F \"processB\" ]) "; // true
|
|||
formulasAsString += "; multi(T>=16/9 [ F \"error\" ], P>=7/12 [ F \"processB\" ]) "; // false
|
|||
|
|||
storm::prism::Program program = storm::parseProgram(programFile); |
|||
program = storm::utility::prism::preprocess(program, ""); |
|||
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>> ma = storm::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>(); |
|||
uint_fast64_t const initState = *ma->getInitialStates().begin(); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result; |
|||
|
|||
result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); |
|||
ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); |
|||
EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); |
|||
|
|||
result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); |
|||
ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); |
|||
EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); |
|||
} |
|||
@ -0,0 +1,74 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h"
|
|||
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
|
|||
#include "storm/models/sparse/Mdp.h"
|
|||
#include "storm/settings/modules/GeneralSettings.h"
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/utility/storm.h"
|
|||
|
|||
|
|||
TEST(SparseMdpCbMultiObjectiveModelCheckerTest, consensus) { |
|||
|
|||
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_consensus2_3_2.nm"; |
|||
std::string formulasAsString = "multi(Pmax=? [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ]) "; // numerical
|
|||
formulasAsString += "; \n multi(P>=0.1 [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ])"; // achievability (true)
|
|||
formulasAsString += "; \n multi(P>=0.11 [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ])"; // achievability (false)
|
|||
|
|||
// programm, model, formula
|
|||
storm::prism::Program program = storm::parseProgram(programFile); |
|||
program = storm::utility::prism::preprocess(program, ""); |
|||
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp = storm::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>(); |
|||
uint_fast64_t const initState = *mdp->getInitialStates().begin();; |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result; |
|||
|
|||
result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); |
|||
ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); |
|||
EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); |
|||
|
|||
result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[2]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); |
|||
ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); |
|||
EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); |
|||
|
|||
} |
|||
|
|||
|
|||
TEST(SparseMdpCbMultiObjectiveModelCheckerTest, zeroconf) { |
|||
|
|||
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_zeroconf4.nm"; |
|||
std::string formulasAsString = "multi(P>=0.0003 [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ]) "; // numerical
|
|||
|
|||
// programm, model, formula
|
|||
storm::prism::Program program = storm::parseProgram(programFile); |
|||
program = storm::utility::prism::preprocess(program, ""); |
|||
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp = storm::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>(); |
|||
uint_fast64_t const initState = *mdp->getInitialStates().begin(); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); |
|||
ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); |
|||
EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); |
|||
} |
|||
|
|||
/* This test takes a little bit too long ...
|
|||
TEST(SparseMdpCbMultiObjectiveModelCheckerTest, team3with3objectives) { |
|||
|
|||
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm"; |
|||
std::string formulasAsString = "multi(P>=0.75 [ F \"task1_compl\" ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F \"task2_compl\" ])"; // numerical
|
|||
|
|||
// programm, model, formula
|
|||
storm::prism::Program program = storm::parseProgram(programFile); |
|||
program = storm::utility::prism::preprocess(program, ""); |
|||
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp = storm::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>(); |
|||
uint_fast64_t const initState = *mdp->getInitialStates().begin(); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); |
|||
ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); |
|||
EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); |
|||
} |
|||
*/ |
|||
|
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue