3#include <boost/container/flat_map.hpp>
56namespace modelchecker {
59template<
typename ValueType,
typename SolutionType>
63 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
64 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"We do not support computing reward bounded values with interval models.");
77 std::vector<ValueType> x, b;
78 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> minMaxSolver;
81 initEpoch, storm::utility::convertNumber<ValueType>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()));
86 std::vector<std::vector<ValueType>> cdfData;
91 uint64_t numCheckedEpochs = 0;
92 for (
auto const& epoch : epochOrder) {
97 rewardUnfolding.
setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(preciseEnv, dir, x, b, minMaxSolver, lowerBound, upperBound));
99 if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportCdfSet() &&
101 std::vector<ValueType> cdfEntry;
108 cdfData.push_back(std::move(cdfEntry));
117 std::map<storm::storage::sparse::state_type, ValueType> result;
118 for (
auto initState : initialStates) {
124 if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportCdfSet()) {
125 std::vector<std::string> headers;
127 headers.push_back(rewardUnfolding.
getDimension(i).formula->toString());
129 headers.push_back(
"Result");
130 storm::io::exportDataToCSVFile<ValueType, std::string, std::string>(
131 storm::settings::getModule<storm::settings::modules::IOSettings>().getExportCdfDirectory() +
"cdf.csv", cdfData, headers);
134 if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
149template<
typename ValueType,
typename SolutionType>
153 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
154 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"We do not support next probabilities with reward models.");
161 multiplier->multiplyAndReduce(env, dir, result,
nullptr, result);
167template<
typename ValueType,
typename SolutionType = ValueType>
173 boost::optional<storm::storage::BitVector>
const& selectedChoices) {
181 validScheduler, selectedChoices);
187 std::vector<uint64_t> schedulerHint;
189 if (selectedChoices) {
191 for (
auto maybeState : maybeStates) {
192 auto choice = validScheduler.
getChoice(maybeState).getDeterministicChoice();
194 auto const origGlobalChoiceIndex = groupStart + choice;
195 STORM_LOG_ASSERT(selectedChoices->get(origGlobalChoiceIndex),
"The computed scheduler selects an illegal choice.");
197 for (
auto pos = selectedChoices->getNextUnsetIndex(groupStart); pos < origGlobalChoiceIndex; pos = selectedChoices->getNextUnsetIndex(pos + 1)) {
200 schedulerHint.push_back(choice);
203 for (
auto maybeState : maybeStates) {
204 schedulerHint.push_back(validScheduler.
getChoice(maybeState).getDeterministicChoice());
207 return schedulerHint;
210template<
typename ValueType>
287template<
typename ValueType,
typename SolutionType>
290 boost::optional<storm::storage::BitVector>
const& selectedChoices,
ModelCheckerHint const& hint,
291 bool skipECWithinMaybeStatesCheck) {
295 STORM_LOG_WARN(
"A scheduler hint was provided, but the solver requires a specific one. The provided scheduler hint will be ignored.");
297 auto const& schedulerHint = hint.template asExplicitModelCheckerHint<ValueType>().getSchedulerHint();
298 std::vector<uint64_t> hintChoices;
302 if (!skipECWithinMaybeStatesCheck) {
303 hintChoices.reserve(maybeStates.
size());
304 for (uint_fast64_t state = 0; state < maybeStates.
size(); ++state) {
305 hintChoices.push_back(schedulerHint.getChoice(state).getDeterministicChoice());
310 hintApplicable =
true;
313 if (hintApplicable) {
317 for (
auto state : maybeStates) {
318 uint_fast64_t hintChoice = schedulerHint.getChoice(state).getDeterministicChoice();
319 if (selectedChoices) {
321 uint_fast64_t lastChoice = firstChoice + hintChoice;
323 for (uint_fast64_t choice = selectedChoices->getNextSetIndex(firstChoice); choice < lastChoice;
324 choice = selectedChoices->getNextSetIndex(choice + 1)) {
328 hintChoices.push_back(hintChoice);
344template<
typename ValueType,
typename SolutionType>
349 boost::optional<storm::storage::BitVector>
const& selectedChoices = boost::none) {
363 bool hasSchedulerHint = hint.
isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasSchedulerHint();
371 "The solver requires to eliminate the end components although the solution is already assumed to be unique.");
372 STORM_LOG_DEBUG(
"Scheduling EC elimination, because the solver requires a unique solution.");
384 STORM_LOG_DEBUG(
"Computing valid scheduler, because the solver requires it.");
385 result.
schedulerHint = computeValidSchedulerHint<ValueType, SolutionType>(env, type, transitionMatrix, backwardTransitions, maybeStates, phiStates,
386 targetStates, selectedChoices);
412 STORM_LOG_TRACE(
"Warn A non-empty hint was provided, but its information will be disregarded.");
432template<
typename ValueType>
454template<
typename ValueType,
typename SolutionType>
459 std::vector<SolutionType> x =
461 : std::vector<SolutionType>(submatrix.getRowGroupCount(),
466 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType, SolutionType>> solver =
468 solver->setRequirementsChecked();
469 solver->setUncertaintyIsRobust(goal.isRobust());
484 solver->setTrackScheduler(produceScheduler);
487 solver->solveEquations(env, x, b);
492 uint64_t relevantState = solver->hasRelevantValues() ? solver->getRelevantValues().getNextSetIndex(0ull) : 0ull;
493 std::function<void()> getNextRelevantStateIndex;
494 if (solver->hasRelevantValues()) {
496 getNextRelevantStateIndex = [&relevantState, &relevantValues]() { relevantState = relevantValues.
getNextSetIndex(++relevantState); };
498 getNextRelevantStateIndex = [&relevantState]() { ++relevantState; };
500 for (; relevantState < solver->getUpperBounds().size(); getNextRelevantStateIndex()) {
502 solver->getUpperBounds().at(relevantState) + storm::utility::convertNumber<ValueType>(env.
solver().
minMax().
getPrecision()),
503 "Expecting result value for state " << relevantState <<
" to be <= " << solver->getUpperBounds().at(relevantState) <<
", but got "
504 << x.at(relevantState) <<
".");
513 if (produceScheduler) {
514 result.
scheduler = std::move(solver->getSchedulerChoices());
525template<
typename ValueType>
528 result.
maybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getMaybeStates();
531 std::vector<ValueType>
const& resultsForNonMaybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getResultHint();
535 for (
auto state : nonMaybeStates) {
540 "Expected that the result hint specifies probabilities in {0,1} for non-maybe states");
548template<
typename ValueType,
typename SolutionType>
557 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
559 statesWithProbability01 =
562 statesWithProbability01 =
572template<
typename ValueType,
typename SolutionType>
579 return getQualitativeStateSetsUntilProbabilitiesFromHint<ValueType>(hint);
585template<
typename SolutionType,
bool subChoicesCoverOnlyMaybeStates = true>
588 if constexpr (subChoicesCoverOnlyMaybeStates) {
589 auto subChoiceIt = subChoices.begin();
590 for (
auto maybeState : maybeStates) {
591 scheduler.
setChoice(*subChoiceIt, maybeState);
594 assert(subChoiceIt == subChoices.end());
599 for (
auto maybeState : maybeStates) {
600 scheduler.
setChoice(subChoices[maybeState], maybeState);
605template<
typename ValueType,
typename SolutionType>
627template<
typename ValueType,
typename SolutionType>
632 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
659template<
typename ValueType,
typename SolutionType>
668 bool doDecomposition = !candidateStates.
empty();
671 if (doDecomposition) {
678 if (doDecomposition && !endComponentDecomposition.
empty()) {
682 submatrix, &b,
nullptr, produceScheduler);
692 if (!newRelevantValues.
empty()) {
706template<
typename ValueType,
typename SolutionType>
711 STORM_LOG_THROW(!qualitative || !produceScheduler, storm::exceptions::InvalidSettingsException,
712 "Cannot produce scheduler when performing qualitative model checking only.");
715 std::vector<SolutionType> result(transitionMatrix.
getRowGroupCount(), storm::utility::zero<SolutionType>());
727 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.
statesWithProbability1, storm::utility::one<SolutionType>());
730 bool maybeStatesNotRelevant = goal.hasRelevantValues() && goal.relevantValues().isDisjointFrom(qualitativeStateSets.
maybeStates);
733 std::unique_ptr<storm::storage::Scheduler<SolutionType>> scheduler;
734 if (produceScheduler) {
735 scheduler = std::make_unique<storm::storage::Scheduler<SolutionType>>(transitionMatrix.
getRowGroupCount());
737 if (maybeStatesNotRelevant) {
738 for (
auto state : qualitativeStateSets.
maybeStates) {
739 scheduler->setDontCare(state);
745 if (qualitative || maybeStatesNotRelevant) {
747 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.
maybeStates, storm::utility::convertNumber<SolutionType>(0.5));
759 std::vector<ValueType> b;
762 boost::optional<SparseMdpEndComponentInformation<ValueType>> ecInformation;
765 qualitativeStateSets, submatrix, b, produceScheduler);
776 if (ecInformation && ecInformation.get().getEliminatedEndComponents()) {
777 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
778 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"We do not support this end component with interval models.");
780 ecInformation.get().setValues(result, qualitativeStateSets.
maybeStates, resultForMaybeStates.
getValues());
781 if (produceScheduler) {
782 ecInformation.get().setScheduler(*scheduler, qualitativeStateSets.
maybeStates, transitionMatrix, backwardTransitions,
788 if constexpr (!std::is_same_v<ValueType, storm::Interval>) {
790 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.
maybeStates, resultForMaybeStates.
getValues());
794 result = resultForMaybeStates.
getValues();
796 if (produceScheduler) {
797 extractSchedulerChoices<SolutionType, !std::is_same_v<ValueType, storm::Interval>>(*scheduler, resultForMaybeStates.
getScheduler(),
805 if (produceScheduler) {
806 extendScheduler(*scheduler, goal, qualitativeStateSets, transitionMatrix, backwardTransitions, phiStates, psiStates);
810 STORM_LOG_ASSERT(!produceScheduler || scheduler,
"Expected that a scheduler was obtained.");
811 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isPartialScheduler(),
"Expected a fully defined scheduler");
812 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isDeterministicScheduler(),
"Expected a deterministic scheduler");
813 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isMemorylessScheduler(),
"Expected a memoryless scheduler");
819template<
typename ValueType,
typename SolutionType>
823 bool useMecBasedTechnique) {
824 if (useMecBasedTechnique) {
828 for (
auto const& mec : mecDecomposition) {
829 for (
auto const& stateActionsPair : mec) {
830 statesInPsiMecs.
set(stateActionsPair.first,
true);
834 return computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, psiStates, statesInPsiMecs, qualitative,
839 computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions,
841 for (
auto& element : result.values) {
842 element = storm::utility::one<SolutionType>() - element;
848template<
typename ValueType,
typename SolutionType>
849template<
typename RewardModelType>
852 RewardModelType
const& rewardModel, uint_fast64_t stepCount) {
853 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
854 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"We do not support instantenous rewards with interval models.");
857 STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException,
858 "Computing instantaneous rewards for a reward model that does not define any state-rewards. The result is trivially 0.");
860 std::vector<SolutionType> result(rewardModel.getStateRewardVector());
863 multiplier->repeatedMultiplyAndReduce(env, goal.direction(), result,
nullptr, stepCount);
869template<
typename ValueType,
typename SolutionType>
870template<
typename RewardModelType>
873 RewardModelType
const& rewardModel, uint_fast64_t stepBound) {
874 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
875 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"We do not support cumulative rewards with interval models.");
878 STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException,
"Missing reward model for formula. Skipping formula.");
881 std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix);
884 std::vector<SolutionType> result(transitionMatrix.
getRowGroupCount(), storm::utility::zero<SolutionType>());
887 multiplier->repeatedMultiplyAndReduce(env, goal.direction(), result, &totalRewardVector, stepBound);
893template<
typename ValueType,
typename SolutionType>
894template<
typename RewardModelType>
899 STORM_LOG_THROW(!rewardModel.hasNegativeRewards(), storm::exceptions::NotImplementedException,
900 "The reward model contains negative rewards. This is not implemented by the total rewards computation.");
902 if (goal.minimize()) {
906 for (uint64_t state = 0; state < transitionMatrix.
getRowGroupCount(); ++state) {
908 statesWithZeroRewardChoice.
set(state);
913 statesWithZeroRewardChoice, ~statesWithZeroRewardChoice,
false, 0, choicesWithoutReward);
915 auto result = computeReachabilityRewards(env, std::move(goal), transitionMatrix, backwardTransitions, rewardModel, rew0EStates, qualitative,
916 produceScheduler, hint);
917 if (result.scheduler) {
932 return computeReachabilityRewards(env, std::move(goal), transitionMatrix, backwardTransitions, rewardModel, rew0AStates, qualitative,
933 produceScheduler, hint);
936 STORM_LOG_ERROR_COND(!produceScheduler,
"Can not produce scheduler for this property (functionality not implemented");
941 for (
auto oldRew0AState : rew0AStates) {
942 newRew0AStates.
set(ecElimResult.oldToNewStateMapping[oldRew0AState]);
945 if (goal.hasRelevantValues()) {
947 for (
auto oldRelevantState : goal.relevantValues()) {
948 newRelevantValues.
set(ecElimResult.oldToNewStateMapping[oldRelevantState]);
950 goal.relevantValues() = std::move(newRelevantValues);
954 env, std::move(goal), ecElimResult.matrix, ecElimResult.matrix.transpose(
true),
956 std::vector<ValueType> result;
957 std::vector<ValueType> oldChoiceRewards = rewardModel.getTotalRewardVector(transitionMatrix);
958 result.reserve(rowCount);
959 for (uint64_t newState : maybeStates) {
960 for (auto newChoice : newTransitionMatrix.getRowGroupIndices(newState)) {
961 uint64_t oldChoice = ecElimResult.newToOldRowMapping[newChoice];
962 result.push_back(oldChoiceRewards[oldChoice]);
965 STORM_LOG_ASSERT(result.size() == rowCount,
"Unexpected size of reward vector.");
968 newRew0AStates, qualitative,
false,
971 for (
auto oldStateWithoutRew : statesWithoutReward) {
972 newStatesWithoutReward.
set(ecElimResult.oldToNewStateMapping[oldStateWithoutRew]);
974 return newStatesWithoutReward;
978 for (uint64_t newChoice = 0; newChoice < ecElimResult.matrix.getRowCount(); ++newChoice) {
979 if (choicesWithoutReward.get(ecElimResult.newToOldRowMapping[newChoice])) {
980 newChoicesWithoutReward.
set(newChoice);
983 return newChoicesWithoutReward;
986 std::vector<SolutionType> resultInEcQuotient = std::move(result.values);
987 result.values.resize(ecElimResult.oldToNewStateMapping.size());
994template<
typename ValueType,
typename SolutionType>
995template<
typename RewardModelType>
998 RewardModelType
const& rewardModel, uint_fast64_t stepBound, ValueType discountFactor) {
1000 STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException,
"Missing reward model for formula. Skipping formula.");
1003 std::vector<SolutionType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix);
1006 std::vector<SolutionType> result(transitionMatrix.
getRowGroupCount(), storm::utility::zero<ValueType>());
1009 multiplier->repeatedMultiplyAndReduceWithFactor(env, goal.direction(), result, &totalRewardVector, stepBound, discountFactor);
1014template<
typename ValueType,
typename SolutionType>
1015template<
typename RewardModelType>
1022 "Exact solving of discounted total reward objectives is currently not supported.");
1024 std::vector<ValueType> b;
1026 std::vector<SolutionType> x = std::vector<SolutionType>(transitionMatrix.
getRowGroupCount(), storm::utility::zero<SolutionType>());
1027 b = rewardModel.getTotalRewardVector(transitionMatrix);
1032 std::unique_ptr<storm::storage::Scheduler<SolutionType>> scheduler;
1033 if (produceScheduler) {
1034 scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(discountingHelper.
computeScheduler());
1036 STORM_LOG_ASSERT(!produceScheduler || scheduler,
"Expected that a scheduler was obtained.");
1037 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isPartialScheduler(),
"Expected a fully defined scheduler");
1038 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isDeterministicScheduler(),
"Expected a deterministic scheduler");
1039 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isMemorylessScheduler(),
"Expected a memoryless scheduler");
1043template<
typename ValueType,
typename SolutionType>
1044template<
typename RewardModelType>
1050 STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException,
"Reward model for formula is empty. Skipping formula.");
1051 return computeReachabilityRewardsHelper(
1052 env, std::move(goal), transitionMatrix, backwardTransitions,
1054 return rewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates);
1056 targetStates, qualitative, produceScheduler, [&]() {
return rewardModel.getStatesWithZeroReward(transitionMatrix); },
1057 [&]() {
return rewardModel.getChoicesWithZeroReward(transitionMatrix); }, hint);
1060template<
typename ValueType,
typename SolutionType>
1065 return computeReachabilityRewardsHelper(
1066 env, std::move(goal), transitionMatrix, backwardTransitions,
1068 return std::vector<ValueType>(rowCount, storm::utility::one<ValueType>());
1074#ifdef STORM_HAVE_CARL
1075template<
typename ValueType,
typename SolutionType>
1081 STORM_LOG_THROW(!intervalRewardModel.
empty(), storm::exceptions::InvalidPropertyException,
"Missing reward model for formula. Skipping formula.");
1082 return computeReachabilityRewardsHelper(
1083 env, std::move(goal), transitionMatrix, backwardTransitions,
1085 std::vector<ValueType> result;
1086 result.reserve(rowCount);
1087 std::vector<storm::Interval> subIntervalVector = intervalRewardModel.
getTotalRewardVector(rowCount, transitionMatrix, maybeStates);
1088 for (
auto const& interval : subIntervalVector) {
1089 result.push_back(lowerBoundOfIntervals ? interval.lower() : interval.upper());
1093 targetStates, qualitative,
false,
1106std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeReachabilityRewards(
1110 STORM_LOG_THROW(
false, storm::exceptions::IllegalFunctionCallException,
"Computing reachability rewards is unsupported for this data type.");
1120template<
typename ValueType>
1124 result.
maybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getMaybeStates();
1127 std::vector<ValueType>
const& resultsForNonMaybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getResultHint();
1131 for (
auto state : nonMaybeStates) {
1136 "Expected that the result hint specifies probabilities in {0,infinity} for non-maybe states");
1143template<
typename ValueType,
typename SolutionType>
1159 if (storm::settings::getModule<storm::settings::modules::ModelCheckerSettings>().isFilterRewZeroSet()) {
1162 trueStates, targetStates, zeroRewardChoicesGetter());
1165 zeroRewardStatesGetter(), targetStates);
1174template<
typename ValueType,
typename SolutionType>
1181 if (hint.
isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().getComputeOnlyMaybeStates()) {
1182 return getQualitativeStateSetsReachabilityRewardsFromHint<ValueType>(hint, targetStates);
1185 zeroRewardChoicesGetter);
1189template<
typename ValueType,
typename SolutionType>
1198 qualitativeStateSets.
rewardZeroStates, targetStates, scheduler, zeroRewardChoicesGetter());
1210template<
typename ValueType,
typename SolutionType>
1213 boost::optional<storm::storage::BitVector>
const& selectedChoices) {
1214 auto subChoiceIt = subChoices.begin();
1215 if (selectedChoices) {
1216 for (
auto maybeState : maybeStates) {
1219 uint_fast64_t selectedRowIndex = selectedChoices->getNextSetIndex(firstRowIndex);
1220 for (uint_fast64_t choice = 0; choice < *subChoiceIt; ++choice) {
1221 selectedRowIndex = selectedChoices->getNextSetIndex(selectedRowIndex + 1);
1223 scheduler.
setChoice(selectedRowIndex - firstRowIndex, maybeState);
1227 for (
auto maybeState : maybeStates) {
1228 scheduler.
setChoice(*subChoiceIt, maybeState);
1232 assert(subChoiceIt == subChoices.end());
1235template<
typename ValueType,
typename SolutionType>
1240 totalStateRewardVectorGetter,
1246 b = totalStateRewardVectorGetter(submatrix.
getRowCount(), transitionMatrix, qualitativeStateSets.
maybeStates);
1247 if (oneStepTargetProbabilities) {
1248 (*oneStepTargetProbabilities) =
1253 b = totalStateRewardVectorGetter(transitionMatrix.
getRowCount(), transitionMatrix,
1256 if (oneStepTargetProbabilities) {
1265template<
typename ValueType,
typename SolutionType>
1269 boost::optional<storm::storage::BitVector>
const& selectedChoices,
1271 totalStateRewardVectorGetter,
1273 bool produceScheduler) {
1278 std::vector<ValueType> rewardVector =
1282 for (
auto const& e : rewardVector) {
1284 zeroRewardChoices.
set(index);
1291 for (
auto state : qualitativeStateSets.
maybeStates) {
1292 bool keepState =
false;
1295 if (zeroRewardChoices.
get(row)) {
1302 candidateStates.
set(state,
false);
1310 bool doDecomposition = !candidateStates.
empty();
1313 if (doDecomposition) {
1315 endComponentDecomposition =
1321 if (doDecomposition && !endComponentDecomposition.
empty()) {
1324 endComponentDecomposition, transitionMatrix, qualitativeStateSets.
maybeStates,
1325 oneStepTargetProbabilities ? &qualitativeStateSets.
rewardZeroStates :
nullptr, selectedChoices ? &selectedChoices.get() :
nullptr, &rewardVector,
1326 submatrix, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() :
nullptr, &b, produceScheduler);
1336 if (!newRelevantValues.
empty()) {
1345 oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() :
nullptr);
1350template<
typename ValueType,
typename SolutionType>
1353 std::vector<ValueType>
const& oneStepTargetProbabilities) {
1354 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1355 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"We do not support computing upper reward bounds with interval models.");
1358 if (direction == storm::OptimizationDirection::Minimize) {
1368template<
typename ValueType,
typename SolutionType>
1369MDPSparseModelCheckingHelperReturnType<SolutionType> SparseMdpPrctlHelper<ValueType, SolutionType>::computeReachabilityRewardsHelper(
1373 totalStateRewardVectorGetter,
1378 std::vector<SolutionType> result(transitionMatrix.
getRowGroupCount(), storm::utility::zero<SolutionType>());
1381 QualitativeStateSetsReachabilityRewards qualitativeStateSets = getQualitativeStateSetsReachabilityRewards(
1382 goal, transitionMatrix, backwardTransitions, targetStates, hint, zeroRewardStatesGetter, zeroRewardChoicesGetter);
1384 STORM_LOG_INFO(
"Preprocessing: " << qualitativeStateSets.infinityStates.getNumberOfSetBits() <<
" states with reward infinity, "
1385 << qualitativeStateSets.rewardZeroStates.getNumberOfSetBits() <<
" states with reward zero ("
1386 << qualitativeStateSets.maybeStates.getNumberOfSetBits() <<
" states remaining).");
1391 std::unique_ptr<storm::storage::Scheduler<SolutionType>> scheduler;
1392 if (produceScheduler) {
1393 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1394 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"We do not support producing schedulers in this function with interval models.");
1396 scheduler = std::make_unique<storm::storage::Scheduler<SolutionType>>(transitionMatrix.
getRowGroupCount());
1404 if (qualitative || maybeStatesNotRelevant) {
1405 STORM_LOG_INFO(
"The rewards for the initial states were determined in a preprocessing step. No exact rewards were computed.");
1408 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.maybeStates, storm::utility::one<SolutionType>());
1410 if (!qualitativeStateSets.maybeStates.empty()) {
1414 boost::optional<storm::storage::BitVector> selectedChoices;
1415 if (!qualitativeStateSets.infinityStates.empty()) {
1416 selectedChoices = transitionMatrix.
getRowFilter(qualitativeStateSets.maybeStates, ~qualitativeStateSets.infinityStates);
1420 SparseMdpHintType<SolutionType> hintInformation = computeHints<ValueType, SolutionType>(
1421 env, SemanticSolutionType::ExpectedRewards, hint, goal.
direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates,
1422 ~qualitativeStateSets.rewardZeroStates, qualitativeStateSets.rewardZeroStates, produceScheduler, selectedChoices);
1426 std::vector<ValueType> b;
1430 boost::optional<std::vector<ValueType>> oneStepTargetProbabilities;
1431 if (hintInformation.getComputeUpperBounds()) {
1432 oneStepTargetProbabilities = std::vector<ValueType>();
1436 boost::optional<SparseMdpEndComponentInformation<ValueType>> ecInformation;
1437 if (hintInformation.getEliminateEndComponents()) {
1438 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1439 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"We do not support eliminating end components with interval models.");
1442 goal, transitionMatrix, backwardTransitions, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b,
1443 oneStepTargetProbabilities, produceScheduler);
1448 submatrix, b, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr);
1452 if (hintInformation.getComputeUpperBounds()) {
1453 STORM_LOG_ASSERT(oneStepTargetProbabilities,
"Expecting one step target probability vector to be available.");
1458 MaybeStateResult<SolutionType> resultForMaybeStates =
1462 if (ecInformation && ecInformation.get().getEliminatedEndComponents()) {
1463 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1464 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"We do not support eliminating end components with interval models.");
1466 ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
1467 if (produceScheduler) {
1468 ecInformation.get().setScheduler(*scheduler, qualitativeStateSets.maybeStates, transitionMatrix, backwardTransitions,
1469 resultForMaybeStates.getScheduler());
1474 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
1475 if (produceScheduler) {
1476 extractSchedulerChoices(*scheduler, transitionMatrix, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates,
1484 if (produceScheduler) {
1485 extendScheduler(*scheduler, goal, qualitativeStateSets, transitionMatrix, backwardTransitions, targetStates, zeroRewardChoicesGetter);
1489 STORM_LOG_ASSERT(!produceScheduler || scheduler,
"Expected that a scheduler was obtained.");
1490 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isPartialScheduler(),
"Expected a fully defined scheduler");
1491 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isDeterministicScheduler(),
"Expected a deterministic scheduler");
1492 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isMemorylessScheduler(),
"Expected a memoryless scheduler");
1494 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1495 return MDPSparseModelCheckingHelperReturnType<SolutionType>(std::move(result));
1497 return MDPSparseModelCheckingHelperReturnType<SolutionType>(std::move(result), std::move(scheduler));
1501template class SparseMdpPrctlHelper<double>;
1505 uint_fast64_t stepCount);
1509 uint_fast64_t stepBound);
1510template std::vector<double> SparseMdpPrctlHelper<double>::computeDiscountedCumulativeRewards(
1513template MDPSparseModelCheckingHelperReturnType<double> SparseMdpPrctlHelper<double>::computeReachabilityRewards(
1517template MDPSparseModelCheckingHelperReturnType<double> SparseMdpPrctlHelper<double>::computeTotalRewards(
1520 bool produceScheduler, ModelCheckerHint
const& hint);
1521template MDPSparseModelCheckingHelperReturnType<double> SparseMdpPrctlHelper<double>::computeDiscountedTotalRewards(
1524 bool produceScheduler,
double discountFactor, ModelCheckerHint
const& hint);
1526#ifdef STORM_HAVE_CARL
1527template class SparseMdpPrctlHelper<storm::RationalNumber>;
1528template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeInstantaneousRewards(
1531template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeCumulativeRewards(
1534template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeDiscountedCumulativeRewards(
1537template MDPSparseModelCheckingHelperReturnType<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeReachabilityRewards(
1541 bool produceScheduler, ModelCheckerHint
const& hint);
1542template MDPSparseModelCheckingHelperReturnType<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeTotalRewards(
1546 ModelCheckerHint
const& hint);
1547template MDPSparseModelCheckingHelperReturnType<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeDiscountedTotalRewards(
1551 storm::RationalNumber discountFactor, ModelCheckerHint
const& hint);
1554template class SparseMdpPrctlHelper<storm::Interval, double>;
1555template std::vector<double> SparseMdpPrctlHelper<storm::Interval, double>::computeInstantaneousRewards(
1558template std::vector<double> SparseMdpPrctlHelper<storm::Interval, double>::computeCumulativeRewards(
1561template MDPSparseModelCheckingHelperReturnType<double> SparseMdpPrctlHelper<storm::Interval, double>::computeReachabilityRewards(
1565template MDPSparseModelCheckingHelperReturnType<double> SparseMdpPrctlHelper<storm::Interval, double>::computeTotalRewards(
1568 bool qualitative,
bool produceScheduler, ModelCheckerHint
const& hint);
SolverEnvironment & solver()
storm::RationalNumber const & getPrecision() const
void setPrecision(storm::RationalNumber value)
MinMaxSolverEnvironment & minMax()
bool isForceExact() const
This class contains information that might accelerate the model checking process.
virtual bool isExplicitModelCheckerHint() const
ExplicitModelCheckerHint< ValueType > & asExplicitModelCheckerHint()
virtual bool isEmpty() const
ValueType computeUpperBound()
Computes an upper bound on the expected rewards.
storm::storage::Scheduler< ValueType > computeScheduler() const
Retrieves the generated scheduler.
bool solveWithDiscountedValueIteration(Environment const &env, std::optional< OptimizationDirection > dir, std::vector< ValueType > &x, std::vector< ValueType > const &b) const
std::vector< ValueType > computeUpperBounds()
Computes upper bounds on the expected rewards.
static MDPSparseModelCheckingHelperReturnType< SolutionType > computeGloballyProbabilities(Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &psiStates, bool qualitative, bool produceScheduler, bool useMecBasedTechnique=false)
static MDPSparseModelCheckingHelperReturnType< SolutionType > computeTotalRewards(Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, RewardModelType const &rewardModel, bool qualitative, bool produceScheduler, ModelCheckerHint const &hint=ModelCheckerHint())
static std::vector< SolutionType > computeCumulativeRewards(Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, RewardModelType const &rewardModel, uint_fast64_t stepBound)
static std::vector< SolutionType > computeInstantaneousRewards(Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, RewardModelType const &rewardModel, uint_fast64_t stepCount)
static std::map< storm::storage::sparse::state_type, SolutionType > computeRewardBoundedValues(Environment const &env, OptimizationDirection dir, rewardbounded::MultiDimensionalRewardUnfolding< ValueType, true > &rewardUnfolding, storm::storage::BitVector const &initialStates)
static std::vector< SolutionType > computeNextProbabilities(Environment const &env, OptimizationDirection dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::BitVector const &nextStates)
static MDPSparseModelCheckingHelperReturnType< SolutionType > computeUntilProbabilities(Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool qualitative, bool produceScheduler, ModelCheckerHint const &hint=ModelCheckerHint())
bool hasBottomDimension(Epoch const &epoch) const
uint64_t const & getDimensionCount() const
uint64_t getDimensionOfEpoch(Epoch const &epoch, uint64_t const &dimension) const
Epoch getStartEpoch(bool setUnknownDimsToBottom=false)
Retrieves the desired epoch that needs to be analyzed to compute the reward bounded values.
SolutionType getInitialStateResult(Epoch const &epoch)
Dimension< ValueType > const & getDimension(uint64_t dim) const
EpochManager const & getEpochManager() const
EpochModel< ValueType, SingleObjectiveMode > & setCurrentEpoch(Epoch const &epoch)
std::vector< Epoch > getEpochComputationOrder(Epoch const &startEpoch, bool stopAtComputedEpochs=false)
Computes a sequence of epochs that need to be analyzed to get a result at the start epoch.
ValueType getRequiredEpochModelPrecision(Epoch const &startEpoch, ValueType const &precision)
Returns the precision required for the analyzis of each epoch model in order to achieve the given ove...
boost::optional< ValueType > getLowerObjectiveBound(uint64_t objectiveIndex=0)
void setSolutionForCurrentEpoch(std::vector< SolutionType > &&inStateSolutions)
boost::optional< ValueType > getUpperObjectiveBound(uint64_t objectiveIndex=0)
Returns an upper/lower bound for the objective result in every state (if this bound could be computed...
bool empty() const
Retrieves whether the reward model is empty, i.e.
std::vector< ValueType > getTotalRewardVector(storm::storage::SparseMatrix< MatrixValueType > const &transitionMatrix) const
Creates a vector representing the complete reward vector based on the state-, state-action- and trans...
storm::storage::BitVector getChoicesWithFilter(storm::storage::SparseMatrix< MatrixValueType > const &transitionMatrix, std::function< bool(ValueType const &)> const &filter) const
Returns the set of choices for which all associated rewards (state, action or transition rewards) sat...
storm::storage::BitVector getStatesWithFilter(storm::storage::SparseMatrix< MatrixValueType > const &transitionMatrix, std::function< bool(ValueType const &)> const &filter) const
Returns the set of states for which all associated rewards (state, action or transition rewards) sati...
MinMaxLinearEquationSolverRequirements getRequirements(Environment const &env, bool hasUniqueSolution=false, bool hasNoEndComponents=false, boost::optional< storm::solver::OptimizationDirection > const &direction=boost::none, bool hasInitialScheduler=false, bool trackScheduler=false) const
Retrieves the requirements of the solver that would be created when calling create() right now.
SolverRequirement const & validInitialScheduler() const
void clearValidInitialScheduler()
void clearUniqueSolution()
bool hasEnabledRequirement() const
SolverRequirement const & uniqueSolution() const
bool hasEnabledCriticalRequirement() const
std::string getEnabledRequirementsAsString() const
Returns a string that enumerates the enabled requirements.
SolverRequirement const & upperBounds() const
std::unique_ptr< Multiplier< ValueType > > create(Environment const &env, storm::storage::SparseMatrix< ValueType > const &matrix)
bool hasRelevantValues() const
void restrictRelevantValues(storm::storage::BitVector const &filter)
storm::storage::BitVector & relevantValues()
void setRelevantValues(storm::storage::BitVector &&values)
OptimizationDirection direction() const
A bit vector that is internally represented as a vector of 64-bit values.
void complement()
Negates all bits in the bit vector.
uint64_t getNextSetIndex(uint64_t startingIndex) const
Retrieves the index of the bit that is the next bit set to true in the bit vector.
bool isDisjointFrom(BitVector const &other) const
Checks whether none of the bits that are set in the current bit vector are also set in the given bit ...
bool full() const
Retrieves whether all bits are set in this bit vector.
bool empty() const
Retrieves whether no bits are set to true in this bit vector.
uint64_t getNumberOfSetBits() const
Returns the number of bits that are set to true in this bit vector.
void set(uint64_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.
bool get(uint64_t index) const
Retrieves the truth value of the bit at the given index and performs a bound check.
bool empty() const
Checks if the decomposition is empty.
std::size_t size() const
Retrieves the number of blocks of this decomposition.
This class represents the decomposition of a nondeterministic model into its maximal end components.
std::string statistics(uint64_t totalNumberOfStates) const
Returns a string containing statistics about the MEC decomposition, e.g., the number of (trivial/non-...
This class defines which action is chosen in a particular state of a non-deterministic model.
SchedulerChoice< ValueType > const & getChoice(uint_fast64_t modelState, uint_fast64_t memoryState=0) const
Gets the choice defined by the scheduler for the given model and memory state.
void setChoice(SchedulerChoice< ValueType > const &choice, uint_fast64_t modelState, uint_fast64_t memoryState=0)
Sets the choice defined by the scheduler for the given state.
A class that holds a possibly non-square matrix in the compressed row storage format.
SparseMatrix getSubmatrix(bool useGroups, storm::storage::BitVector const &rowConstraint, storm::storage::BitVector const &columnConstraint, bool insertDiagonalEntries=false, storm::storage::BitVector const &makeZeroColumns=storm::storage::BitVector()) const
Creates a submatrix of the current matrix by dropping all rows and columns whose bits are not set to ...
std::vector< value_type > getConstrainedRowSumVector(storm::storage::BitVector const &rowConstraint, storm::storage::BitVector const &columnConstraint) const
Computes a vector whose i-th entry is the sum of the entries in the i-th selected row where only thos...
SparseMatrix< ValueType > transposeSelectedRowsFromRowGroups(std::vector< uint64_t > const &rowGroupChoices, bool keepZeros=false) const
Transposes the matrix w.r.t.
index_type getRowGroupCount() const
Returns the number of row groups in the matrix.
index_type getColumnCount() const
Returns the number of columns of the matrix.
std::vector< index_type > const & getRowGroupIndices() const
Returns the grouping of rows of this matrix.
std::vector< value_type > getConstrainedRowGroupSumVector(storm::storage::BitVector const &rowGroupConstraint, storm::storage::BitVector const &columnConstraint) const
Computes a vector whose entries represent the sums of selected columns for all rows in selected row g...
index_type getRowCount() const
Returns the number of rows of the matrix.
storm::storage::BitVector getRowFilter(storm::storage::BitVector const &groupConstraint) const
Returns a bitvector representing the set of rows, with all indices set that correspond to one of the ...
SparseMatrix filterEntries(storm::storage::BitVector const &rowFilter) const
Returns a copy of this matrix that only considers entries in the selected rows.
A class that provides convenience operations to display run times.
bool updateProgress(uint64_t count)
Updates the progress to the current count and prints it if the delay passed.
void setMaxCount(uint64_t maxCount)
Sets the maximal possible count.
void startNewMeasurement(uint64_t startCount)
Starts a new measurement, dropping all progress information collected so far.
A class that provides convenience operations to display run times.
void start()
Start stopwatch (again) and start measuring time.
void stop()
Stop stopwatch and add measured time to total time.
#define STORM_LOG_INFO(message)
#define STORM_LOG_WARN(message)
#define STORM_LOG_DEBUG(message)
#define STORM_LOG_TRACE(message)
#define STORM_LOG_ASSERT(cond, message)
#define STORM_LOG_ERROR_COND(cond, message)
#define STORM_LOG_THROW(cond, exception, message)
#define STORM_PRINT_AND_LOG(message)
void extractSchedulerChoices(storm::storage::Scheduler< SolutionType > &scheduler, std::vector< uint64_t > const &subChoices, storm::storage::BitVector const &maybeStates)
boost::optional< SparseMdpEndComponentInformation< ValueType > > computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(storm::solver::SolveGoal< ValueType, SolutionType > &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, QualitativeStateSetsUntilProbabilities const &qualitativeStateSets, storm::storage::SparseMatrix< ValueType > &submatrix, std::vector< ValueType > &b, bool produceScheduler)
QualitativeStateSetsReachabilityRewards computeQualitativeStateSetsReachabilityRewards(storm::solver::SolveGoal< ValueType, SolutionType > const &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &targetStates, std::function< storm::storage::BitVector()> const &zeroRewardStatesGetter, std::function< storm::storage::BitVector()> const &zeroRewardChoicesGetter)
QualitativeStateSetsUntilProbabilities computeQualitativeStateSetsUntilProbabilities(storm::solver::SolveGoal< ValueType, SolutionType > const &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
void extractValueAndSchedulerHint(SparseMdpHintType< SolutionType > &hintStorage, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &maybeStates, boost::optional< storm::storage::BitVector > const &selectedChoices, ModelCheckerHint const &hint, bool skipECWithinMaybeStatesCheck)
std::vector< uint_fast64_t > computeValidSchedulerHint(Environment const &env, SemanticSolutionType const &type, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &maybeStates, storm::storage::BitVector const &filterStates, storm::storage::BitVector const &targetStates, boost::optional< storm::storage::BitVector > const &selectedChoices)
SparseMdpHintType< SolutionType > computeHints(Environment const &env, SemanticSolutionType const &type, ModelCheckerHint const &hint, storm::OptimizationDirection const &dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &maybeStates, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &targetStates, bool produceScheduler, boost::optional< storm::storage::BitVector > const &selectedChoices=boost::none)
QualitativeStateSetsUntilProbabilities getQualitativeStateSetsUntilProbabilitiesFromHint(ModelCheckerHint const &hint)
std::vector< ValueType > computeUpperRewardBounds(storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< ValueType > const &rewards, std::vector< ValueType > const &oneStepTargetProbabilities)
QualitativeStateSetsReachabilityRewards getQualitativeStateSetsReachabilityRewards(storm::solver::SolveGoal< ValueType, SolutionType > const &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &targetStates, ModelCheckerHint const &hint, std::function< storm::storage::BitVector()> const &zeroRewardStatesGetter, std::function< storm::storage::BitVector()> const &zeroRewardChoicesGetter)
void computeFixedPointSystemUntilProbabilities(storm::solver::SolveGoal< ValueType, SolutionType > &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, QualitativeStateSetsUntilProbabilities const &qualitativeStateSets, storm::storage::SparseMatrix< ValueType > &submatrix, std::vector< ValueType > &b)
MaybeStateResult< SolutionType > computeValuesForMaybeStates(Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > &&submatrix, std::vector< ValueType > const &b, bool produceScheduler, SparseMdpHintType< SolutionType > &hint)
void extendScheduler(storm::storage::Scheduler< SolutionType > &scheduler, storm::solver::SolveGoal< ValueType, SolutionType > const &goal, QualitativeStateSetsUntilProbabilities const &qualitativeStateSets, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
QualitativeStateSetsReachabilityRewards getQualitativeStateSetsReachabilityRewardsFromHint(ModelCheckerHint const &hint, storm::storage::BitVector const &targetStates)
boost::optional< SparseMdpEndComponentInformation< ValueType > > computeFixedPointSystemReachabilityRewardsEliminateEndComponents(storm::solver::SolveGoal< ValueType, SolutionType > &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, QualitativeStateSetsReachabilityRewards const &qualitativeStateSets, boost::optional< storm::storage::BitVector > const &selectedChoices, std::function< std::vector< ValueType >(uint_fast64_t, storm::storage::SparseMatrix< ValueType > const &, storm::storage::BitVector const &)> const &totalStateRewardVectorGetter, storm::storage::SparseMatrix< ValueType > &submatrix, std::vector< ValueType > &b, boost::optional< std::vector< ValueType > > &oneStepTargetProbabilities, bool produceScheduler)
QualitativeStateSetsUntilProbabilities getQualitativeStateSetsUntilProbabilities(storm::solver::SolveGoal< ValueType, SolutionType > const &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, ModelCheckerHint const &hint)
void computeFixedPointSystemReachabilityRewards(storm::solver::SolveGoal< ValueType, SolutionType > &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, QualitativeStateSetsReachabilityRewards const &qualitativeStateSets, boost::optional< storm::storage::BitVector > const &selectedChoices, std::function< std::vector< ValueType >(uint_fast64_t, storm::storage::SparseMatrix< ValueType > const &, storm::storage::BitVector const &)> const &totalStateRewardVectorGetter, storm::storage::SparseMatrix< ValueType > &submatrix, std::vector< ValueType > &b, std::vector< ValueType > *oneStepTargetProbabilities=nullptr)
std::unique_ptr< storm::solver::MinMaxLinearEquationSolver< ValueType, SolutionType > > configureMinMaxLinearEquationSolver(Environment const &env, SolveGoal< ValueType, SolutionType > &&goal, storm::solver::MinMaxLinearEquationSolverFactory< ValueType, SolutionType > const &factory, MatrixType &&matrix)
std::pair< storm::storage::BitVector, storm::storage::BitVector > performProb01Max(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)
void computeSchedulerStayingInStates(storm::storage::BitVector const &states, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::Scheduler< SchedulerValueType > &scheduler, boost::optional< storm::storage::BitVector > const &rowFilter)
Computes a scheduler for the given states that chooses an action that stays completely in the very sa...
void computeSchedulerProbGreater0E(storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::storage::Scheduler< SchedulerValueType > &scheduler, boost::optional< storm::storage::BitVector > const &rowFilter)
Computes a scheduler for the ProbGreater0E-States such that in the induced system the given psiStates...
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...
void computeSchedulerProb1E(storm::storage::BitVector const &prob1EStates, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::storage::Scheduler< SchedulerValueType > &scheduler, boost::optional< storm::storage::BitVector > const &rowFilter)
Computes a scheduler for the given prob1EStates such that in the induced system the given psiStates a...
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 performProb1(storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &, storm::storage::BitVector const &psiStates, storm::storage::BitVector const &statesWithProbabilityGreater0)
Computes the set of states of the given model for which all paths lead to the given set of target sta...
storm::storage::BitVector performProb0E(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 0 of satisfying phi until psi under at least one po...
void computeSchedulerProb0E(storm::storage::BitVector const &prob0EStates, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::Scheduler< SchedulerValueType > &scheduler)
Computes a scheduler for the given states that have a scheduler that has a probability 0.
std::pair< storm::storage::BitVector, storm::storage::BitVector > performProb01Min(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)
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...
void computeSchedulerRewInf(storm::storage::BitVector const &rewInfStates, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::Scheduler< SchedulerValueType > &scheduler)
Computes a scheduler for the given states that have a scheduler that has a reward infinity.
bool isTerminate()
Check whether the program should terminate (due to some abort signal).
void setVectorValues(std::vector< T > &vector, storm::storage::BitVector const &positions, std::vector< T > const &values)
Sets the provided values at the provided positions in the given vector.
void setAllValues(std::vector< T > &vec, storm::storage::BitVector const &positions, T const &positiveValue=storm::utility::one< T >(), T const &negativeValue=storm::utility::zero< T >())
void selectVectorValues(std::vector< T > &vector, storm::storage::BitVector const &positions, std::vector< T > const &values)
Selects the elements from a vector at the specified positions and writes them consecutively into anot...
void filterVectorInPlace(std::vector< Type > &v, storm::storage::BitVector const &filter)
std::vector< Type > filterVector(std::vector< Type > const &in, storm::storage::BitVector const &filter)
bool isOne(ValueType const &a)
bool isZero(ValueType const &a)
bool isInfinity(ValueType const &a)
bool hasScheduler() const
boost::optional< std::vector< uint64_t > > scheduler
MaybeStateResult(std::vector< ValueType > &&values)
std::vector< uint64_t > const & getScheduler() const
std::vector< ValueType > values
std::vector< ValueType > const & getValues() const
storm::storage::BitVector rewardZeroStates
storm::storage::BitVector infinityStates
storm::storage::BitVector maybeStates
storm::storage::BitVector statesWithProbability0
storm::storage::BitVector statesWithProbability1
storm::storage::BitVector maybeStates
ValueType const & getUpperResultBound() const
boost::optional< std::vector< uint64_t > > schedulerHint
std::vector< ValueType > & getValueHint()
bool hasNoEndComponents() const
boost::optional< ValueType > lowerResultBound
ValueType const & getLowerResultBound() const
boost::optional< ValueType > upperResultBound
bool hasValueHint() const
std::vector< uint64_t > & getSchedulerHint()
bool hasUniqueSolution() const
bool getEliminateEndComponents() const
boost::optional< std::vector< ValueType > > valueHint
bool getComputeUpperBounds()
bool hasUpperResultBound() const
std::vector< ValueType > const & getUpperResultBounds() const
std::vector< ValueType > & getUpperResultBounds()
boost::optional< std::vector< ValueType > > upperResultBounds
bool hasSchedulerHint() const
bool hasLowerResultBound() const
bool eliminateEndComponents
bool hasUpperResultBounds() const