3#include <boost/container/flat_map.hpp>
54namespace modelchecker {
57template<
typename ValueType,
typename SolutionType>
61 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
62 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"We do not support computing reward bounded values with interval models.");
75 std::vector<ValueType> x, b;
76 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> minMaxSolver;
84 std::vector<std::vector<ValueType>> cdfData;
89 uint64_t numCheckedEpochs = 0;
90 for (
auto const& epoch : epochOrder) {
95 rewardUnfolding.
setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(preciseEnv, dir, x, b, minMaxSolver, lowerBound, upperBound));
99 std::vector<ValueType> cdfEntry;
106 cdfData.push_back(std::move(cdfEntry));
115 std::map<storm::storage::sparse::state_type, ValueType> result;
116 for (
auto initState : initialStates) {
123 std::vector<std::string> headers;
125 headers.push_back(rewardUnfolding.
getDimension(i).formula->toString());
127 headers.push_back(
"Result");
128 storm::io::exportDataToCSVFile<ValueType, std::string, std::string>(
147template<
typename ValueType,
typename SolutionType>
151 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
152 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"We do not support next probabilities with reward models.");
159 multiplier->multiplyAndReduce(env, dir, result,
nullptr, result);
165template<
typename ValueType,
typename SolutionType = ValueType>
171 boost::optional<storm::storage::BitVector>
const& selectedChoices) {
179 validScheduler, selectedChoices);
185 std::vector<uint64_t> schedulerHint;
187 if (selectedChoices) {
189 for (
auto maybeState : maybeStates) {
190 auto choice = validScheduler.
getChoice(maybeState).getDeterministicChoice();
192 auto const origGlobalChoiceIndex = groupStart + choice;
193 STORM_LOG_ASSERT(selectedChoices->get(origGlobalChoiceIndex),
"The computed scheduler selects an illegal choice.");
195 for (
auto pos = selectedChoices->getNextUnsetIndex(groupStart); pos < origGlobalChoiceIndex; pos = selectedChoices->getNextUnsetIndex(pos + 1)) {
198 schedulerHint.push_back(choice);
201 for (
auto maybeState : maybeStates) {
202 schedulerHint.push_back(validScheduler.
getChoice(maybeState).getDeterministicChoice());
205 return schedulerHint;
208template<
typename ValueType>
285template<
typename ValueType,
typename SolutionType>
288 boost::optional<storm::storage::BitVector>
const& selectedChoices,
ModelCheckerHint const& hint,
289 bool skipECWithinMaybeStatesCheck) {
293 STORM_LOG_WARN(
"A scheduler hint was provided, but the solver requires a specific one. The provided scheduler hint will be ignored.");
295 auto const& schedulerHint = hint.template asExplicitModelCheckerHint<ValueType>().getSchedulerHint();
296 std::vector<uint64_t> hintChoices;
300 if (!skipECWithinMaybeStatesCheck) {
301 hintChoices.reserve(maybeStates.
size());
302 for (uint_fast64_t state = 0; state < maybeStates.
size(); ++state) {
303 hintChoices.push_back(schedulerHint.getChoice(state).getDeterministicChoice());
308 hintApplicable =
true;
311 if (hintApplicable) {
315 for (
auto state : maybeStates) {
316 uint_fast64_t hintChoice = schedulerHint.getChoice(state).getDeterministicChoice();
317 if (selectedChoices) {
319 uint_fast64_t lastChoice = firstChoice + hintChoice;
321 for (uint_fast64_t choice = selectedChoices->getNextSetIndex(firstChoice); choice < lastChoice;
322 choice = selectedChoices->getNextSetIndex(choice + 1)) {
326 hintChoices.push_back(hintChoice);
342template<
typename ValueType,
typename SolutionType>
347 boost::optional<storm::storage::BitVector>
const& selectedChoices = boost::none) {
361 bool hasSchedulerHint = hint.
isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasSchedulerHint();
369 "The solver requires to eliminate the end components although the solution is already assumed to be unique.");
370 STORM_LOG_DEBUG(
"Scheduling EC elimination, because the solver requires a unique solution.");
382 STORM_LOG_DEBUG(
"Computing valid scheduler, because the solver requires it.");
383 result.
schedulerHint = computeValidSchedulerHint<ValueType, SolutionType>(env, type, transitionMatrix, backwardTransitions, maybeStates, phiStates,
384 targetStates, selectedChoices);
410 STORM_LOG_TRACE(
"Warn A non-empty hint was provided, but its information will be disregarded.");
430template<
typename ValueType>
452template<
typename ValueType,
typename SolutionType>
457 std::vector<SolutionType> x =
459 : std::vector<SolutionType>(submatrix.getRowGroupCount(),
464 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType, SolutionType>> solver =
466 solver->setRequirementsChecked();
467 solver->setUncertaintyIsRobust(goal.isRobust());
482 solver->setTrackScheduler(produceScheduler);
485 solver->solveEquations(env, x, b);
490 auto resultIt = x.begin();
491 for (
auto const& entry : solver->getUpperBounds()) {
494 "Expecting result value for state " << std::distance(x.begin(), resultIt) <<
" to be <= " << entry <<
", but got " << *resultIt <<
".");
504 if (produceScheduler) {
505 result.
scheduler = std::move(solver->getSchedulerChoices());
516template<
typename ValueType>
519 result.
maybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getMaybeStates();
522 std::vector<ValueType>
const& resultsForNonMaybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getResultHint();
526 for (
auto state : nonMaybeStates) {
531 "Expected that the result hint specifies probabilities in {0,1} for non-maybe states");
539template<
typename ValueType,
typename SolutionType>
548 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
550 statesWithProbability01 =
553 statesWithProbability01 =
563template<
typename ValueType,
typename SolutionType>
570 return getQualitativeStateSetsUntilProbabilitiesFromHint<ValueType>(hint);
576template<
typename SolutionType,
bool subChoicesCoverOnlyMaybeStates = true>
579 if constexpr (subChoicesCoverOnlyMaybeStates) {
580 auto subChoiceIt = subChoices.begin();
581 for (
auto maybeState : maybeStates) {
582 scheduler.
setChoice(*subChoiceIt, maybeState);
585 assert(subChoiceIt == subChoices.end());
590 for (
auto maybeState : maybeStates) {
591 scheduler.
setChoice(subChoices[maybeState], maybeState);
596template<
typename ValueType,
typename SolutionType>
618template<
typename ValueType,
typename SolutionType>
623 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
650template<
typename ValueType,
typename SolutionType>
659 bool doDecomposition = !candidateStates.
empty();
662 if (doDecomposition) {
669 if (doDecomposition && !endComponentDecomposition.
empty()) {
673 submatrix, &b,
nullptr, produceScheduler);
683 if (!newRelevantValues.
empty()) {
697template<
typename ValueType,
typename SolutionType>
702 STORM_LOG_THROW(!qualitative || !produceScheduler, storm::exceptions::InvalidSettingsException,
703 "Cannot produce scheduler when performing qualitative model checking only.");
706 std::vector<SolutionType> result(transitionMatrix.
getRowGroupCount(), storm::utility::zero<SolutionType>());
718 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.
statesWithProbability1, storm::utility::one<SolutionType>());
721 bool maybeStatesNotRelevant = goal.hasRelevantValues() && goal.relevantValues().isDisjointFrom(qualitativeStateSets.
maybeStates);
724 std::unique_ptr<storm::storage::Scheduler<SolutionType>> scheduler;
725 if (produceScheduler) {
726 scheduler = std::make_unique<storm::storage::Scheduler<SolutionType>>(transitionMatrix.
getRowGroupCount());
728 if (maybeStatesNotRelevant) {
729 for (
auto state : qualitativeStateSets.
maybeStates) {
730 scheduler->setDontCare(state);
736 if (qualitative || maybeStatesNotRelevant) {
738 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.
maybeStates, storm::utility::convertNumber<SolutionType>(0.5));
750 std::vector<ValueType> b;
753 boost::optional<SparseMdpEndComponentInformation<ValueType>> ecInformation;
756 qualitativeStateSets, submatrix, b, produceScheduler);
767 if (ecInformation && ecInformation.get().getEliminatedEndComponents()) {
768 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
769 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"We do not support this end component with interval models.");
771 ecInformation.get().setValues(result, qualitativeStateSets.
maybeStates, resultForMaybeStates.
getValues());
772 if (produceScheduler) {
773 ecInformation.get().setScheduler(*scheduler, qualitativeStateSets.
maybeStates, transitionMatrix, backwardTransitions,
779 if constexpr (!std::is_same_v<ValueType, storm::Interval>) {
781 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.
maybeStates, resultForMaybeStates.
getValues());
785 result = resultForMaybeStates.
getValues();
787 if (produceScheduler) {
788 extractSchedulerChoices<SolutionType, !std::is_same_v<ValueType, storm::Interval>>(*scheduler, resultForMaybeStates.
getScheduler(),
796 if (produceScheduler) {
797 extendScheduler(*scheduler, goal, qualitativeStateSets, transitionMatrix, backwardTransitions, phiStates, psiStates);
801 STORM_LOG_ASSERT(!produceScheduler || scheduler,
"Expected that a scheduler was obtained.");
802 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isPartialScheduler(),
"Expected a fully defined scheduler");
803 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isDeterministicScheduler(),
"Expected a deterministic scheduler");
804 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isMemorylessScheduler(),
"Expected a memoryless scheduler");
810template<
typename ValueType,
typename SolutionType>
814 bool useMecBasedTechnique) {
815 if (useMecBasedTechnique) {
819 for (
auto const& mec : mecDecomposition) {
820 for (
auto const& stateActionsPair : mec) {
821 statesInPsiMecs.
set(stateActionsPair.first,
true);
825 return computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, psiStates, statesInPsiMecs, qualitative,
830 computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions,
832 for (
auto& element : result.values) {
833 element = storm::utility::one<SolutionType>() - element;
839template<
typename ValueType,
typename SolutionType>
840template<
typename RewardModelType>
843 RewardModelType
const& rewardModel, uint_fast64_t stepCount) {
844 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
845 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"We do not support instantenous rewards with interval models.");
848 STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException,
849 "Computing instantaneous rewards for a reward model that does not define any state-rewards. The result is trivially 0.");
851 std::vector<SolutionType> result(rewardModel.getStateRewardVector());
854 multiplier->repeatedMultiplyAndReduce(env, goal.direction(), result,
nullptr, stepCount);
860template<
typename ValueType,
typename SolutionType>
861template<
typename RewardModelType>
864 RewardModelType
const& rewardModel, uint_fast64_t stepBound) {
865 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
866 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"We do not support cumulative rewards with interval models.");
869 STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException,
"Missing reward model for formula. Skipping formula.");
872 std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix);
875 std::vector<SolutionType> result(transitionMatrix.
getRowGroupCount(), storm::utility::zero<SolutionType>());
878 multiplier->repeatedMultiplyAndReduce(env, goal.direction(), result, &totalRewardVector, stepBound);
884template<
typename ValueType,
typename SolutionType>
885template<
typename RewardModelType>
890 STORM_LOG_THROW(!rewardModel.hasNegativeRewards(), storm::exceptions::NotImplementedException,
891 "The reward model contains negative rewards. This is not implemented by the total rewards computation.");
893 if (goal.minimize()) {
897 for (uint64_t state = 0; state < transitionMatrix.
getRowGroupCount(); ++state) {
899 statesWithZeroRewardChoice.
set(state);
904 statesWithZeroRewardChoice, ~statesWithZeroRewardChoice,
false, 0, choicesWithoutReward);
906 auto result = computeReachabilityRewards(env, std::move(goal), transitionMatrix, backwardTransitions, rewardModel, rew0EStates, qualitative,
907 produceScheduler, hint);
908 if (result.scheduler) {
923 return computeReachabilityRewards(env, std::move(goal), transitionMatrix, backwardTransitions, rewardModel, rew0AStates, qualitative,
924 produceScheduler, hint);
927 STORM_LOG_ERROR_COND(!produceScheduler,
"Can not produce scheduler for this property (functionality not implemented");
932 for (
auto oldRew0AState : rew0AStates) {
933 newRew0AStates.
set(ecElimResult.oldToNewStateMapping[oldRew0AState]);
936 if (goal.hasRelevantValues()) {
938 for (
auto oldRelevantState : goal.relevantValues()) {
939 newRelevantValues.
set(ecElimResult.oldToNewStateMapping[oldRelevantState]);
941 goal.relevantValues() = std::move(newRelevantValues);
945 env, std::move(goal), ecElimResult.matrix, ecElimResult.matrix.transpose(
true),
947 std::vector<ValueType> result;
948 std::vector<ValueType> oldChoiceRewards = rewardModel.getTotalRewardVector(transitionMatrix);
949 result.reserve(rowCount);
950 for (uint64_t newState : maybeStates) {
951 for (auto newChoice : newTransitionMatrix.getRowGroupIndices(newState)) {
952 uint64_t oldChoice = ecElimResult.newToOldRowMapping[newChoice];
953 result.push_back(oldChoiceRewards[oldChoice]);
956 STORM_LOG_ASSERT(result.size() == rowCount,
"Unexpected size of reward vector.");
959 newRew0AStates, qualitative,
false,
962 for (
auto oldStateWithoutRew : statesWithoutReward) {
963 newStatesWithoutReward.
set(ecElimResult.oldToNewStateMapping[oldStateWithoutRew]);
965 return newStatesWithoutReward;
969 for (uint64_t newChoice = 0; newChoice < ecElimResult.matrix.getRowCount(); ++newChoice) {
970 if (choicesWithoutReward.get(ecElimResult.newToOldRowMapping[newChoice])) {
971 newChoicesWithoutReward.
set(newChoice);
974 return newChoicesWithoutReward;
977 std::vector<SolutionType> resultInEcQuotient = std::move(result.values);
978 result.values.resize(ecElimResult.oldToNewStateMapping.size());
985template<
typename ValueType,
typename SolutionType>
986template<
typename RewardModelType>
992 STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException,
"Reward model for formula is empty. Skipping formula.");
993 return computeReachabilityRewardsHelper(
994 env, std::move(goal), transitionMatrix, backwardTransitions,
996 return rewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates);
998 targetStates, qualitative, produceScheduler, [&]() {
return rewardModel.getStatesWithZeroReward(transitionMatrix); },
999 [&]() {
return rewardModel.getChoicesWithZeroReward(transitionMatrix); }, hint);
1002template<
typename ValueType,
typename SolutionType>
1007 return computeReachabilityRewardsHelper(
1008 env, std::move(goal), transitionMatrix, backwardTransitions,
1010 return std::vector<ValueType>(rowCount, storm::utility::one<ValueType>());
1016#ifdef STORM_HAVE_CARL
1017template<
typename ValueType,
typename SolutionType>
1023 STORM_LOG_THROW(!intervalRewardModel.
empty(), storm::exceptions::InvalidPropertyException,
"Missing reward model for formula. Skipping formula.");
1024 return computeReachabilityRewardsHelper(
1025 env, std::move(goal), transitionMatrix, backwardTransitions,
1027 std::vector<ValueType> result;
1028 result.reserve(rowCount);
1029 std::vector<storm::Interval> subIntervalVector = intervalRewardModel.
getTotalRewardVector(rowCount, transitionMatrix, maybeStates);
1030 for (
auto const& interval : subIntervalVector) {
1031 result.push_back(lowerBoundOfIntervals ? interval.lower() : interval.upper());
1035 targetStates, qualitative,
false,
1048std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeReachabilityRewards(
1052 STORM_LOG_THROW(
false, storm::exceptions::IllegalFunctionCallException,
"Computing reachability rewards is unsupported for this data type.");
1062template<
typename ValueType>
1066 result.
maybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getMaybeStates();
1069 std::vector<ValueType>
const& resultsForNonMaybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getResultHint();
1073 for (
auto state : nonMaybeStates) {
1078 "Expected that the result hint specifies probabilities in {0,infinity} for non-maybe states");
1085template<
typename ValueType,
typename SolutionType>
1104 trueStates, targetStates, zeroRewardChoicesGetter());
1107 zeroRewardStatesGetter(), targetStates);
1116template<
typename ValueType,
typename SolutionType>
1123 if (hint.
isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().getComputeOnlyMaybeStates()) {
1124 return getQualitativeStateSetsReachabilityRewardsFromHint<ValueType>(hint, targetStates);
1127 zeroRewardChoicesGetter);
1131template<
typename ValueType,
typename SolutionType>
1140 qualitativeStateSets.
rewardZeroStates, targetStates, scheduler, zeroRewardChoicesGetter());
1152template<
typename ValueType,
typename SolutionType>
1155 boost::optional<storm::storage::BitVector>
const& selectedChoices) {
1156 auto subChoiceIt = subChoices.begin();
1157 if (selectedChoices) {
1158 for (
auto maybeState : maybeStates) {
1161 uint_fast64_t selectedRowIndex = selectedChoices->getNextSetIndex(firstRowIndex);
1162 for (uint_fast64_t choice = 0; choice < *subChoiceIt; ++choice) {
1163 selectedRowIndex = selectedChoices->getNextSetIndex(selectedRowIndex + 1);
1165 scheduler.
setChoice(selectedRowIndex - firstRowIndex, maybeState);
1169 for (
auto maybeState : maybeStates) {
1170 scheduler.
setChoice(*subChoiceIt, maybeState);
1174 assert(subChoiceIt == subChoices.end());
1177template<
typename ValueType,
typename SolutionType>
1182 totalStateRewardVectorGetter,
1188 b = totalStateRewardVectorGetter(submatrix.
getRowCount(), transitionMatrix, qualitativeStateSets.
maybeStates);
1189 if (oneStepTargetProbabilities) {
1190 (*oneStepTargetProbabilities) =
1195 b = totalStateRewardVectorGetter(transitionMatrix.
getRowCount(), transitionMatrix,
1198 if (oneStepTargetProbabilities) {
1207template<
typename ValueType,
typename SolutionType>
1211 boost::optional<storm::storage::BitVector>
const& selectedChoices,
1213 totalStateRewardVectorGetter,
1215 bool produceScheduler) {
1220 std::vector<ValueType> rewardVector =
1224 for (
auto const& e : rewardVector) {
1226 zeroRewardChoices.
set(index);
1233 for (
auto state : qualitativeStateSets.
maybeStates) {
1234 bool keepState =
false;
1237 if (zeroRewardChoices.
get(row)) {
1244 candidateStates.
set(state,
false);
1252 bool doDecomposition = !candidateStates.
empty();
1255 if (doDecomposition) {
1257 endComponentDecomposition =
1263 if (doDecomposition && !endComponentDecomposition.
empty()) {
1266 endComponentDecomposition, transitionMatrix, qualitativeStateSets.
maybeStates,
1267 oneStepTargetProbabilities ? &qualitativeStateSets.
rewardZeroStates :
nullptr, selectedChoices ? &selectedChoices.get() :
nullptr, &rewardVector,
1268 submatrix, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() :
nullptr, &b, produceScheduler);
1278 if (!newRelevantValues.
empty()) {
1287 oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() :
nullptr);
1292template<
typename ValueType,
typename SolutionType>
1295 std::vector<ValueType>
const& oneStepTargetProbabilities) {
1296 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1297 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"We do not support computing upper reward bounds with interval models.");
1300 if (direction == storm::OptimizationDirection::Minimize) {
1310template<
typename ValueType,
typename SolutionType>
1311MDPSparseModelCheckingHelperReturnType<SolutionType> SparseMdpPrctlHelper<ValueType, SolutionType>::computeReachabilityRewardsHelper(
1315 totalStateRewardVectorGetter,
1320 std::vector<SolutionType> result(transitionMatrix.
getRowGroupCount(), storm::utility::zero<SolutionType>());
1323 QualitativeStateSetsReachabilityRewards qualitativeStateSets = getQualitativeStateSetsReachabilityRewards(
1324 goal, transitionMatrix, backwardTransitions, targetStates, hint, zeroRewardStatesGetter, zeroRewardChoicesGetter);
1326 STORM_LOG_INFO(
"Preprocessing: " << qualitativeStateSets.infinityStates.getNumberOfSetBits() <<
" states with reward infinity, "
1327 << qualitativeStateSets.rewardZeroStates.getNumberOfSetBits() <<
" states with reward zero ("
1328 << qualitativeStateSets.maybeStates.getNumberOfSetBits() <<
" states remaining).");
1333 std::unique_ptr<storm::storage::Scheduler<SolutionType>> scheduler;
1334 if (produceScheduler) {
1335 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1336 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"We do not support producing schedulers in this function with interval models.");
1338 scheduler = std::make_unique<storm::storage::Scheduler<SolutionType>>(transitionMatrix.
getRowGroupCount());
1346 if (qualitative || maybeStatesNotRelevant) {
1347 STORM_LOG_INFO(
"The rewards for the initial states were determined in a preprocessing step. No exact rewards were computed.");
1350 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.maybeStates, storm::utility::one<SolutionType>());
1352 if (!qualitativeStateSets.maybeStates.empty()) {
1356 boost::optional<storm::storage::BitVector> selectedChoices;
1357 if (!qualitativeStateSets.infinityStates.empty()) {
1358 selectedChoices = transitionMatrix.
getRowFilter(qualitativeStateSets.maybeStates, ~qualitativeStateSets.infinityStates);
1362 SparseMdpHintType<SolutionType> hintInformation = computeHints<ValueType, SolutionType>(
1363 env, SemanticSolutionType::ExpectedRewards, hint, goal.
direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates,
1364 ~qualitativeStateSets.rewardZeroStates, qualitativeStateSets.rewardZeroStates, produceScheduler, selectedChoices);
1368 std::vector<ValueType> b;
1372 boost::optional<std::vector<ValueType>> oneStepTargetProbabilities;
1373 if (hintInformation.getComputeUpperBounds()) {
1374 oneStepTargetProbabilities = std::vector<ValueType>();
1378 boost::optional<SparseMdpEndComponentInformation<ValueType>> ecInformation;
1379 if (hintInformation.getEliminateEndComponents()) {
1380 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1381 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"We do not support eliminating end components with interval models.");
1384 goal, transitionMatrix, backwardTransitions, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b,
1385 oneStepTargetProbabilities, produceScheduler);
1390 submatrix, b, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr);
1394 if (hintInformation.getComputeUpperBounds()) {
1395 STORM_LOG_ASSERT(oneStepTargetProbabilities,
"Expecting one step target probability vector to be available.");
1400 MaybeStateResult<SolutionType> resultForMaybeStates =
1404 if (ecInformation && ecInformation.get().getEliminatedEndComponents()) {
1405 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1406 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"We do not support eliminating end components with interval models.");
1408 ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
1409 if (produceScheduler) {
1410 ecInformation.get().setScheduler(*scheduler, qualitativeStateSets.maybeStates, transitionMatrix, backwardTransitions,
1411 resultForMaybeStates.getScheduler());
1416 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
1417 if (produceScheduler) {
1418 extractSchedulerChoices(*scheduler, transitionMatrix, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates,
1426 if (produceScheduler) {
1427 extendScheduler(*scheduler, goal, qualitativeStateSets, transitionMatrix, backwardTransitions, targetStates, zeroRewardChoicesGetter);
1431 STORM_LOG_ASSERT(!produceScheduler || scheduler,
"Expected that a scheduler was obtained.");
1432 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isPartialScheduler(),
"Expected a fully defined scheduler");
1433 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isDeterministicScheduler(),
"Expected a deterministic scheduler");
1434 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isMemorylessScheduler(),
"Expected a memoryless scheduler");
1436 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1437 return MDPSparseModelCheckingHelperReturnType<SolutionType>(std::move(result));
1439 return MDPSparseModelCheckingHelperReturnType<SolutionType>(std::move(result), std::move(scheduler));
1443template<
typename ValueType,
typename SolutionType>
1448 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1449 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"We do not support computing conditional probabilities with interval models.");
1451 std::chrono::high_resolution_clock::time_point start = std::chrono::high_resolution_clock::now();
1457 fixedTargetStates = targetStates;
1461 for (
auto const& mec : mecDecomposition) {
1462 for (
auto const& stateActionsPair : mec) {
1463 fixedTargetStates.
set(stateActionsPair.first);
1478 "Computing conditional probabilities in MDPs is only supported for models with exactly one initial state.");
1487 std::chrono::high_resolution_clock::time_point conditionStart = std::chrono::high_resolution_clock::now();
1488 std::vector<ValueType> conditionProbabilities =
1489 std::move(computeUntilProbabilities(env, OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, extendedConditionStates,
1492 std::chrono::high_resolution_clock::time_point conditionEnd = std::chrono::high_resolution_clock::now();
1494 << std::chrono::duration_cast<std::chrono::milliseconds>(conditionEnd - conditionStart).count() <<
"ms.");
1502 std::chrono::high_resolution_clock::time_point targetStart = std::chrono::high_resolution_clock::now();
1503 std::vector<ValueType> targetProbabilities = std::move(
1504 computeUntilProbabilities(env, OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, fixedTargetStates,
false,
false)
1506 std::chrono::high_resolution_clock::time_point targetEnd = std::chrono::high_resolution_clock::now();
1507 STORM_LOG_DEBUG(
"Computed probabilities to reach target in " << std::chrono::duration_cast<std::chrono::milliseconds>(targetEnd - targetStart).count()
1512 for (
auto const& element : conditionProbabilities) {
1514 statesWithProbabilityGreater0E.
set(state,
false);
1523 transitionMatrix, transitionMatrix.
getRowGroupIndices(), backwardTransitions, allStates, extendedConditionStates | fixedTargetStates);
1527 extendedConditionStates | fixedTargetStates | pureResetStates);
1536 uint_fast64_t currentRow = 0;
1537 for (
auto state : relevantStates) {
1539 if (fixedTargetStates.
get(state)) {
1541 builder.
addNextValue(currentRow, newGoalState, conditionProbabilities[state]);
1544 builder.
addNextValue(currentRow, newFailState, storm::utility::one<ValueType>() - conditionProbabilities[state]);
1547 }
else if (extendedConditionStates.
get(state)) {
1549 builder.
addNextValue(currentRow, newGoalState, targetProbabilities[state]);
1552 builder.
addNextValue(currentRow, newStopState, storm::utility::one<ValueType>() - targetProbabilities[state]);
1555 }
else if (pureResetStates.
get(state)) {
1556 builder.
addNextValue(currentRow, numberOfStatesBeforeRelevantStates[initialState], storm::utility::one<ValueType>());
1560 for (
auto const& successorEntry : transitionMatrix.
getRow(row)) {
1561 builder.
addNextValue(currentRow, numberOfStatesBeforeRelevantStates[successorEntry.getColumn()], successorEntry.getValue());
1565 if (problematicStates.
get(state)) {
1566 builder.
addNextValue(currentRow, numberOfStatesBeforeRelevantStates[initialState], storm::utility::one<ValueType>());
1574 builder.
addNextValue(currentRow, newGoalState, storm::utility::one<ValueType>());
1577 builder.
addNextValue(currentRow, newStopState, storm::utility::one<ValueType>());
1580 builder.
addNextValue(currentRow, numberOfStatesBeforeRelevantStates[initialState], storm::utility::one<ValueType>());
1583 std::chrono::high_resolution_clock::time_point end = std::chrono::high_resolution_clock::now();
1584 STORM_LOG_DEBUG(
"Computed transformed model in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() <<
"ms.");
1589 newGoalStates.
set(newGoalState);
1592 <<
" transitions.");
1600 std::chrono::high_resolution_clock::time_point conditionalStart = std::chrono::high_resolution_clock::now();
1601 std::vector<ValueType> goalProbabilities =
1602 std::move(computeUntilProbabilities(env, std::move(goal), newTransitionMatrix, newBackwardTransitions,
1605 std::chrono::high_resolution_clock::time_point conditionalEnd = std::chrono::high_resolution_clock::now();
1606 STORM_LOG_DEBUG(
"Computed conditional probabilities in transformed model in "
1607 << std::chrono::duration_cast<std::chrono::milliseconds>(conditionalEnd - conditionalStart).count() <<
"ms.");
1610 initialState, dir == OptimizationDirection::Maximize
1611 ? goalProbabilities[numberOfStatesBeforeRelevantStates[initialState]]
1612 : storm::utility::one<ValueType>() - goalProbabilities[numberOfStatesBeforeRelevantStates[initialState]]));
1620 uint_fast64_t stepCount);
1624 uint_fast64_t stepBound);
1634#ifdef STORM_HAVE_CARL
SolverEnvironment & solver()
storm::RationalNumber const & getPrecision() const
void setPrecision(storm::RationalNumber value)
MinMaxSolverEnvironment & minMax()
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.
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)
void oneMinus()
Flips the comparison type, the direction, and computes the new threshold as 1 - old threshold.
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.
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.
uint_fast64_t getNextSetIndex(uint_fast64_t startingIndex) const
Retrieves the index of the bit that is the next bit set to true in the bit vector.
bool empty() const
Retrieves whether no bits are set to true in this bit vector.
const_iterator begin() const
Returns an iterator to the indices of the set bits in the bit vector.
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.
uint_fast64_t getNumberOfSetBits() const
Returns the number of bits that are set to true in this bit vector.
std::vector< uint_fast64_t > getNumberOfSetBitsBeforeIndices() const
Retrieves a vector that holds at position i the number of bits set before index i.
bool get(uint_fast64_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 can be used to build a sparse matrix by adding value by value.
void addNextValue(index_type row, index_type column, value_type const &value)
Sets the matrix entry at the given row and column to the given value.
void newRowGroup(index_type startingRow)
Starts a new row group in the matrix.
SparseMatrix< value_type > build(index_type overriddenRowCount=0, index_type overriddenColumnCount=0, index_type overriddenRowGroupCount=0)
A class that holds a possibly non-square matrix in the compressed row storage format.
const_rows getRow(index_type row) const
Returns an object representing the given row.
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...
storm::storage::SparseMatrix< value_type > transpose(bool joinGroups=false, bool keepZeros=false) const
Transposes the matrix.
index_type getRowCount() const
Returns the number of rows of the matrix.
index_type getNonzeroEntryCount() const
Returns the cached number of nonzero entries in 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)
SettingsType const & getModule()
Get module.
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 getReachableStates(storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::BitVector const &initialStates, storm::storage::BitVector const &constraintStates, storm::storage::BitVector const &targetStates, bool useStepBound, uint_fast64_t maximalSteps, boost::optional< storm::storage::BitVector > const &choiceFilter)
Performs a forward depth-first search through the underlying graph structure to identify the states t...
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 performProb0A(storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
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