24namespace modelchecker {
25namespace multiobjective {
26namespace preprocessing {
28template<
typename SparseModelType>
32 auto backwardTransitions = preprocessorResult.
preprocessedModel->getBackwardTransitions();
34 setReward0States(result, preprocessorResult, backwardTransitions);
35 checkRewardFiniteness(result, preprocessorResult, backwardTransitions);
40template<
typename SparseModelType>
44 uint_fast64_t stateCount = preprocessorResult.
preprocessedModel->getNumberOfStates();
45 auto const& transitions = preprocessorResult.
preprocessedModel->getTransitionMatrix();
46 std::vector<uint_fast64_t>
const& groupIndices = transitions.getRowGroupIndices();
53 for (
auto const& obj : preprocessorResult.objectives) {
54 if (obj.formula->isRewardOperatorFormula()) {
55 auto const& rewModel = preprocessorResult.
preprocessedModel->getRewardModel(obj.formula->asRewardOperatorFormula().getRewardModelName());
56 if (obj.formula->getSubformula().isLongRunAverageRewardFormula()) {
57 zeroLraRewardChoices &= rewModel.getChoicesWithZeroReward(transitions);
58 }
else if (obj.formula->getSubformula().isTotalRewardFormula()) {
59 zeroTotalRewardChoices &= rewModel.getChoicesWithZeroReward(transitions);
62 "Analyzing subformula " << obj.formula->getSubformula() <<
" is not supported properly.");
63 zeroCumulativeRewardChoices &= rewModel.getChoicesWithZeroReward(transitions);
69 auto statesWithTotalRewardForAllChoices = transitions.getRowGroupFilter(~zeroTotalRewardChoices,
true);
71 statesWithTotalRewardForAllChoices,
false, 0, zeroTotalRewardChoices);
72 result.totalReward0EStates.complement();
76 auto statesWithoutLraReward = transitions.getRowGroupFilter(zeroLraRewardChoices,
true);
79 result.reward0AStates =
82 auto statesWithTotalOrCumulativeReward = transitions.getRowGroupFilter(~(zeroTotalRewardChoices & zeroCumulativeRewardChoices),
false);
84 assert(result.reward0AStates.isSubsetOf(result.totalReward0EStates));
87template<
typename SparseModelType>
88void SparseMultiObjectiveRewardAnalysis<SparseModelType>::checkRewardFiniteness(
93 auto const& transitions = preprocessorResult.
preprocessedModel->getTransitionMatrix();
94 std::vector<uint_fast64_t>
const& groupIndices = transitions.getRowGroupIndices();
101 for (
auto objIndex : preprocessorResult.maybeInfiniteRewardObjectives) {
103 "Objective needs to be checked for finite reward but has no reward operator.");
105 preprocessorResult.
objectives[objIndex].formula->asRewardOperatorFormula().getRewardModelName());
106 auto irrelevantChoices = rewModel.getChoicesWithZeroReward(transitions);
108 if (preprocessorResult.
objectives[objIndex].formula->getSubformula().isCumulativeRewardFormula()) {
109 auto const& timeBoundReference =
110 preprocessorResult.
objectives[objIndex].formula->getSubformula().asCumulativeRewardFormula().getTimeBoundReference();
112 assert(timeBoundReference.isRewardBound());
113 auto const& rewModelOfBound = preprocessorResult.
preprocessedModel->getRewardModel(timeBoundReference.getRewardName());
114 irrelevantChoices |= ~rewModelOfBound.getChoicesWithZeroReward(transitions);
118 bool const negativeRewards = rewModel.hasNegativeRewards();
119 bool const positiveRewards = rewModel.hasPositiveRewards();
120 bool const hasMixedSignRewards = negativeRewards && positiveRewards;
122 if (hasMixedSignRewards || (maximizing && !negativeRewards) || (!maximizing && !positiveRewards)) {
123 attractingInfRewardChoices &= irrelevantChoices;
125 drainingInfRewardChoices &= irrelevantChoices;
128 attractingInfRewardChoices.complement();
129 drainingInfRewardChoices.complement();
139 result.totalRewardLessInfinityEStates =
141 if ((result.totalRewardLessInfinityEStates.get() & preprocessorResult.
preprocessedModel->getInitialStates()).empty()) {
149 result.totalRewardLessInfinityEStates = allStates;
153template<
typename SparseModelType>
158 "Tried to find an upper result bound for an objective, but a result bound is already there.");
161 auto const& transitions = model.getTransitionMatrix();
163 if (objective.
formula->isRewardOperatorFormula()) {
164 auto const& rewModel = model.getRewardModel(objective.
formula->asRewardOperatorFormula().getRewardModelName());
165 auto actionRewards = rewModel.getTotalRewardVector(transitions);
167 if (objective.
formula->getSubformula().isTotalRewardFormula() || objective.
formula->getSubformula().isCumulativeRewardFormula()) {
173 auto nonZeroRewardStates = rewModel.getStatesWithZeroReward(transitions);
174 nonZeroRewardStates.complement();
177 auto zeroRewardChoices = rewModel.getChoicesWithZeroReward(transitions);
182 allStates.
resize(ecElimRes.matrix.getRowGroupCount());
184 std::vector<ValueType> rew0StateProbs;
185 rew0StateProbs.reserve(ecElimRes.matrix.getRowCount());
186 for (uint64_t state = 0; state < allStates.
size(); ++state) {
187 for (uint64_t choice = ecElimRes.matrix.getRowGroupIndices()[state]; choice < ecElimRes.matrix.getRowGroupIndices()[state + 1]; ++choice) {
189 bool isOutChoice =
false;
190 uint64_t originalModelChoice = ecElimRes.newToOldRowMapping[choice];
191 for (
auto const& entry : transitions.getRow(originalModelChoice)) {
192 if (!expRewGreater0EStates.get(entry.getColumn())) {
194 outStates.
set(state,
true);
195 rew0StateProbs.push_back(storm::utility::one<ValueType>() - ecElimRes.matrix.getRowSum(choice));
201 rew0StateProbs.push_back(storm::utility::zero<ValueType>());
210 std::vector<ValueType> rewards;
211 rewards.reserve(ecElimRes.matrix.getRowCount());
212 for (
auto row : ecElimRes.newToOldRowMapping) {
213 rewards.push_back(actionRewards[row]);
ValueType computeUpperBound()
Computes an upper bound on the expected rewards.
static ReturnType analyze(storm::modelchecker::multiobjective::preprocessing::SparseMultiObjectivePreprocessorResult< SparseModelType > const &preprocessorResult)
Analyzes the reward objectives of the multi objective query.
static void computeUpperResultBound(SparseModelType const &model, storm::modelchecker::multiobjective::Objective< ValueType > &objective, storm::storage::SparseMatrix< ValueType > const &backwardTransitions)
Tries to finds an upper bound for the expected reward of the objective (assuming it considers an expe...
A bit vector that is internally represented as a vector of 64-bit values.
bool full() const
Retrieves whether all bits are set in this bit vector.
void resize(uint_fast64_t newLength, bool init=false)
Resizes the bit vector to hold the given new number of bits.
void set(uint_fast64_t index, bool value=true)
Sets the given truth value at the given index.
size_t size() const
Retrieves the number of bits this bit vector can store.
A class that holds a possibly non-square matrix in the compressed row storage format.
#define STORM_LOG_INFO(message)
#define STORM_LOG_WARN(message)
#define STORM_LOG_ASSERT(cond, message)
#define STORM_LOG_WARN_COND(cond, message)
#define STORM_LOG_INFO_COND(cond, message)
bool constexpr maximize(OptimizationDirection d)
storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound, uint_fast64_t maximalSteps, boost::optional< storm::storage::BitVector > const &choiceConstraint)
Computes the sets of states that have probability greater 0 of satisfying phi until psi under any pos...
storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel< T, RM > const &model, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Computes the sets of states that have probability 1 of satisfying phi until psi under all possible re...
storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound, uint_fast64_t maximalSteps)
Computes the sets of states that have probability greater 0 of satisfying phi until psi under at leas...
storm::storage::BitVector performProb0A(storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
bool checkIfECWithChoiceExists(storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &subsystem, storm::storage::BitVector const &choices)
Checks whether there is an End Component that.
storm::storage::BitVector performProb1E(storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, boost::optional< storm::storage::BitVector > const &choiceConstraint)
Computes the sets of states that have probability 1 of satisfying phi until psi under at least one po...
bool isZero(ValueType const &a)
boost::optional< ValueType > upperResultBound
std::shared_ptr< storm::logic::OperatorFormula const > formula
std::shared_ptr< SparseModelType > preprocessedModel
std::vector< Objective< typename SparseModelType::ValueType > > objectives