45namespace modelchecker {
51 std::shared_ptr<storm::logic::OperatorFormula const> ) {
52 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"The specified property is not supported by this value type.");
53 return std::map<storm::storage::sparse::state_type, storm::RationalFunction>();
56template<
typename ValueType,
typename RewardModelType>
72 std::vector<ValueType> x, b;
73 std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> linEqSolver;
77 initEpoch, storm::utility::convertNumber<ValueType>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()));
81 std::vector<std::vector<ValueType>> cdfData;
90 uint64_t numCheckedEpochs = 0;
91 for (
auto const& epoch : epochOrder) {
96 rewardUnfolding.
setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(preciseEnv, x, b, linEqSolver, lowerBound, upperBound));
98 if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportCdfSet() &&
100 std::vector<ValueType> cdfEntry;
107 cdfData.push_back(std::move(cdfEntry));
116 std::map<storm::storage::sparse::state_type, ValueType> result;
123 if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportCdfSet()) {
124 std::vector<std::string> headers;
126 headers.push_back(rewardUnfolding.
getDimension(i).formula->toString());
128 headers.push_back(
"Result");
129 storm::io::exportDataToCSVFile<ValueType, std::string, std::string>(
130 storm::settings::getModule<storm::settings::modules::IOSettings>().getExportCdfDirectory() +
"cdf.csv", cdfData, headers);
133 if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
147template<
typename ValueType,
typename RewardModelType>
152 std::vector<ValueType> result(transitionMatrix.
getRowCount(), storm::utility::zero<ValueType>());
159 maybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getMaybeStates();
162 std::vector<ValueType>
const& resultsForNonMaybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getResultHint();
165 for (
auto state : nonMaybeStates) {
167 statesWithProbability1.
set(state,
true);
168 result[state] = storm::utility::one<ValueType>();
171 "Expected that the result hint specifies probabilities in {0,1} for non-maybe states");
176 <<
" states remaining).");
179 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
182 statesWithProbability1 = std::move(statesWithProbability01.second);
183 maybeStates = ~(statesWithProbability0 | statesWithProbability1);
187 <<
" states remaining).");
190 storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability0, storm::utility::zero<ValueType>());
191 storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability1, storm::utility::one<ValueType>());
195 bool maybeStatesNotRelevant = goal.hasRelevantValues() && goal.relevantValues().isDisjointFrom(maybeStates);
198 if (qualitative || maybeStatesNotRelevant) {
200 storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, storm::utility::convertNumber<ValueType>(0.5));
202 if (!maybeStates.
empty()) {
207 bool convertToEquationSystem =
212 if (convertToEquationSystem) {
221 std::vector<ValueType> x;
225 x = std::vector<ValueType>(maybeStates.
getNumberOfSetBits(), storm::utility::convertNumber<ValueType>(0.5));
233 goal.restrictRelevantValues(maybeStates);
234 std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver =
236 solver->setBounds(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
237 solver->solveEquations(env, x, b);
240 storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, x);
246template<
typename ValueType,
typename RewardModelType>
250 uint_fast64_t numberOfStates = transitionMatrix.
getRowCount();
251 std::vector<ValueType> result(numberOfStates, storm::utility::zero<ValueType>());
257 if (!relevantStates.
empty()) {
260 bool convertToEquationSystem =
271 submatrix = submatrix.
getSubmatrix(
true, relevantStates, relevantStates, convertToEquationSystem);
273 if (convertToEquationSystem) {
282 std::vector<ValueType> x = std::vector<ValueType>(relevantStates.
getNumberOfSetBits(), storm::utility::convertNumber<ValueType>(0.5));
285 std::vector<ValueType> b(relevantStates.
getNumberOfSetBits(), storm::utility::zero<ValueType>());
288 ValueType initDist = storm::utility::one<ValueType>() / storm::utility::convertNumber<ValueType>(initialStates.
getNumberOfSetBits());
289 for (
auto state : relevantStates) {
290 if (initialStates.
get(state)) {
297 goal.restrictRelevantValues(relevantStates);
298 std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver =
300 solver->setBounds(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
301 solver->solveEquations(env, x, b);
304 storm::utility::vector::setVectorValues<ValueType>(result, relevantStates, x);
309template<
typename ValueType,
typename RewardModelType>
314 std::vector<ValueType> result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions,
316 for (
auto& entry : result) {
317 entry = storm::utility::one<ValueType>() - entry;
322template<
typename ValueType,
typename RewardModelType>
326 std::vector<ValueType> result(transitionMatrix.
getRowCount());
331 multiplier->multiply(env, result,
nullptr, result);
335template<
typename ValueType,
typename RewardModelType>
338 RewardModelType
const& rewardModel, uint_fast64_t stepBound) {
340 std::vector<ValueType> result(transitionMatrix.
getRowCount());
343 std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix);
347 multiplier->repeatedMultiply(env, result, &totalRewardVector, stepBound);
352template<
typename ValueType,
typename RewardModelType>
355 RewardModelType
const& rewardModel, uint_fast64_t stepCount) {
357 STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException,
358 "Computing instantaneous rewards for a reward model that does not define any state-rewards. The result is trivially 0.");
361 std::vector<ValueType> result = rewardModel.getStateRewardVector();
365 multiplier->repeatedMultiply(env, result,
nullptr, stepCount);
370template<
typename ValueType,
typename RewardModelType>
379 return computeReachabilityRewards(env, std::move(goal), transitionMatrix, backwardTransitions, rewardModel, rew0States, qualitative, hint);
387 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"The specified property is not supported by this value type.");
391template<
typename ValueType,
typename RewardModelType>
394 RewardModelType
const& rewardModel, uint_fast64_t stepBound, ValueType discountFactor) {
396 STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException,
"Missing reward model for formula. Skipping formula.");
399 std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix);
402 std::vector<ValueType> result(transitionMatrix.
getRowGroupCount(), storm::utility::zero<ValueType>());
405 multiplier->repeatedMultiplyWithFactor(env, result, &totalRewardVector, stepBound, discountFactor);
417 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"The specified property is not supported by this value type.");
421template<
typename ValueType,
typename RewardModelType>
428 "Exact solving of discounted total reward objectives is currently not supported.");
431 std::vector<ValueType> b;
433 std::vector<ValueType> x = std::vector<ValueType>(transitionMatrix.
getRowGroupCount(), storm::utility::zero<ValueType>());
434 b = rewardModel.getTotalRewardVector(transitionMatrix);
437 return std::vector<ValueType>(std::move(x));
440template<
typename ValueType,
typename RewardModelType>
445 return computeReachabilityRewards(
446 env, std::move(goal), transitionMatrix, backwardTransitions,
448 return rewardModel.getTotalRewardVector(numberOfRows, transitionMatrix, maybeStates);
450 targetStates, qualitative, [&]() {
return rewardModel.getStatesWithZeroReward(transitionMatrix); }, hint);
453template<
typename ValueType,
typename RewardModelType>
458 return computeReachabilityRewards(
459 env, std::move(goal), transitionMatrix, backwardTransitions,
461 std::vector<ValueType> result(numberOfRows);
468template<
typename ValueType,
typename RewardModelType>
473 return computeReachabilityRewards(
474 env, std::move(goal), transitionMatrix, backwardTransitions,
476 return std::vector<ValueType>(numberOfRows, storm::utility::one<ValueType>());
482template<
typename ValueType>
484 std::vector<ValueType>
const& oneStepTargetProbabilities) {
486 std::vector<ValueType> bounds = dsmpi.computeUpperBounds();
492 std::vector<storm::RationalFunction>
const& ,
493 std::vector<storm::RationalFunction>
const& ) {
494 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Computing upper reward bounds is not supported for rational functions.");
497template<
typename ValueType,
typename RewardModelType>
502 totalStateRewardVectorGetter,
505 std::vector<ValueType> result(transitionMatrix.
getRowCount(), storm::utility::zero<ValueType>());
509 if (storm::settings::getModule<storm::settings::modules::ModelCheckerSettings>().isFilterRewZeroSet()) {
512 rew0States = targetStates;
518 maybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getMaybeStates();
522 <<
" states remaining).");
527 maybeStates = ~(rew0States | infinityStates);
530 <<
" states with reward zero (" << maybeStates.
getNumberOfSetBits() <<
" states remaining).");
536 bool maybeStatesNotRelevant = goal.hasRelevantValues() && goal.relevantValues().isDisjointFrom(maybeStates);
539 if (qualitative || maybeStatesNotRelevant) {
542 storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, storm::utility::one<ValueType>());
544 if (!maybeStates.
empty()) {
547 bool convertToEquationSystem =
556 std::vector<ValueType> x;
560 x = std::vector<ValueType>(submatrix.
getColumnCount(), storm::utility::one<ValueType>());
564 std::vector<ValueType> b = totalStateRewardVectorGetter(submatrix.
getRowCount(), transitionMatrix, maybeStates);
567 boost::optional<std::vector<ValueType>> upperRewardBounds;
577 if (convertToEquationSystem) {
583 goal.restrictRelevantValues(maybeStates);
584 std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver =
586 solver->setLowerBound(storm::utility::zero<ValueType>());
587 if (upperRewardBounds) {
588 solver->setUpperBounds(std::move(upperRewardBounds.get()));
592 solver->solveEquations(env, x, b);
595 storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, x);
601template<
typename ValueType,
typename RewardModelType>
602typename SparseDtmcPrctlHelper<ValueType, RewardModelType>::BaierTransformedModel SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeBaierTransformation(
605 boost::optional<std::vector<ValueType>>
const& stateRewards) {
606 BaierTransformedModel result;
609 std::vector<ValueType> probabilitiesToReachConditionStates =
614 uint_fast64_t state = 0;
615 uint_fast64_t beforeStateIndex = 0;
616 for (
auto const& value : probabilitiesToReachConditionStates) {
617 if (value == storm::utility::zero<ValueType>()) {
618 result.beforeStates.set(state,
false);
620 probabilitiesToReachConditionStates[beforeStateIndex] = value;
625 probabilitiesToReachConditionStates.resize(beforeStateIndex);
627 if (targetStates.
empty()) {
628 result.noTargetStates =
true;
630 }
else if (!result.beforeStates.empty()) {
637 std::vector<uint_fast64_t> numberOfBeforeStatesUpToState = result.beforeStates.getNumberOfSetBitsBeforeIndices();
640 uint_fast64_t normalStatesOffset = result.beforeStates.getNumberOfSetBits();
644 bool addDeadlockState =
false;
645 uint_fast64_t deadlockState = normalStatesOffset + statesWithProbabilityGreater0.
getNumberOfSetBits();
651 uint_fast64_t currentRow = 0;
652 for (
auto beforeState : result.beforeStates) {
653 if (conditionStates.
get(beforeState)) {
655 ValueType zeroProbability = storm::utility::zero<ValueType>();
656 for (
auto const& successorEntry : transitionMatrix.getRow(beforeState)) {
657 if (statesWithProbabilityGreater0.
get(successorEntry.getColumn())) {
658 builder.
addNextValue(currentRow, normalStatesOffset + numberOfNormalStatesUpToState[successorEntry.getColumn()],
659 successorEntry.getValue());
661 zeroProbability += successorEntry.getValue();
665 builder.
addNextValue(currentRow, deadlockState, zeroProbability);
669 for (
auto const& successorEntry : transitionMatrix.getRow(beforeState)) {
670 if (result.beforeStates.get(successorEntry.getColumn())) {
671 builder.
addNextValue(currentRow, numberOfBeforeStatesUpToState[successorEntry.getColumn()],
672 successorEntry.getValue() *
673 probabilitiesToReachConditionStates[numberOfBeforeStatesUpToState[successorEntry.getColumn()]] /
674 probabilitiesToReachConditionStates[currentRow]);
682 for (
auto state : statesWithProbabilityGreater0) {
683 ValueType zeroProbability = storm::utility::zero<ValueType>();
684 for (
auto const& successorEntry : transitionMatrix.getRow(state)) {
685 if (statesWithProbabilityGreater0.
get(successorEntry.getColumn())) {
686 builder.
addNextValue(currentRow, normalStatesOffset + numberOfNormalStatesUpToState[successorEntry.getColumn()], successorEntry.getValue());
688 zeroProbability += successorEntry.getValue();
692 addDeadlockState =
true;
693 builder.
addNextValue(currentRow, deadlockState, zeroProbability);
697 if (addDeadlockState) {
698 builder.
addNextValue(deadlockState, deadlockState, storm::utility::one<ValueType>());
702 result.transitionMatrix = builder.
build(addDeadlockState ? (deadlockState + 1) : deadlockState);
704 newTargetStates.
resize(result.transitionMatrix.get().getRowCount());
705 for (
auto state : targetStates % statesWithProbabilityGreater0) {
706 newTargetStates.
set(normalStatesOffset + state,
true);
708 result.targetStates = std::move(newTargetStates);
712 std::vector<ValueType> newStateRewards(result.beforeStates.getNumberOfSetBits());
715 newStateRewards.reserve(result.transitionMatrix.get().getRowCount());
716 for (
auto state : statesWithProbabilityGreater0) {
717 newStateRewards.push_back(stateRewards.get()[state]);
720 if (addDeadlockState) {
721 newStateRewards.push_back(storm::utility::zero<ValueType>());
723 result.stateRewards = std::move(newStateRewards);
730template<
typename ValueType,
typename RewardModelType>
731storm::storage::BitVector SparseDtmcPrctlHelper<ValueType, RewardModelType>::BaierTransformedModel::getNewRelevantStates()
const {
733 for (uint64_t i = 0;
i < this->beforeStates.getNumberOfSetBits(); ++
i) {
734 newRelevantStates.set(i);
736 return newRelevantStates;
739template<
typename ValueType,
typename RewardModelType>
747template<
typename ValueType,
typename RewardModelType>
753 std::vector<ValueType> result(transitionMatrix.
getRowCount(), storm::utility::infinity<ValueType>());
755 if (!conditionStates.
empty()) {
756 BaierTransformedModel transformedModel =
757 computeBaierTransformation(env, transitionMatrix, backwardTransitions, targetStates, conditionStates, boost::none);
759 if (transformedModel.noTargetStates) {
769 if (goal.hasRelevantValues()) {
770 newRelevantValues = transformedModel.getNewRelevantStates(goal.relevantValues());
772 newRelevantValues = transformedModel.getNewRelevantStates();
774 goal.setRelevantValues(std::move(newRelevantValues));
775 std::vector<ValueType> conditionalProbabilities =
776 computeUntilProbabilities(env, std::move(goal), newTransitionMatrix, newTransitionMatrix.
transpose(),
786template<
typename ValueType,
typename RewardModelType>
792 std::vector<ValueType> result(transitionMatrix.
getRowCount(), storm::utility::infinity<ValueType>());
794 if (!conditionStates.
empty()) {
795 BaierTransformedModel transformedModel = computeBaierTransformation(env, transitionMatrix, backwardTransitions, targetStates, conditionStates,
796 rewardModel.getTotalRewardVector(transitionMatrix));
798 if (transformedModel.noTargetStates) {
808 if (goal.hasRelevantValues()) {
809 newRelevantValues = transformedModel.getNewRelevantStates(goal.relevantValues());
811 newRelevantValues = transformedModel.getNewRelevantStates();
813 goal.setRelevantValues(std::move(newRelevantValues));
814 std::vector<ValueType> conditionalRewards =
815 computeReachabilityRewards(env, std::move(goal), newTransitionMatrix, newTransitionMatrix.
transpose(), transformedModel.stateRewards.get(),
816 transformedModel.targetStates.get(), qualitative);
826#ifdef STORM_HAVE_CARL
SolverEnvironment & solver()
void setLinearEquationSolverPrecision(boost::optional< storm::RationalNumber > const &newPrecision, boost::optional< bool > const &relativePrecision=boost::none)
bool isForceExact() const
This class contains information that might accelerate the model checking process.
virtual bool isExplicitModelCheckerHint() const
bool solveWithDiscountedValueIteration(Environment const &env, std::optional< OptimizationDirection > dir, std::vector< ValueType > &x, std::vector< ValueType > const &b) const
static std::vector< ValueType > computeNextProbabilities(Environment const &env, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::BitVector const &nextStates)
static std::vector< ValueType > computeReachabilityTimes(Environment const &env, storm::solver::SolveGoal< ValueType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &targetStates, bool qualitative, ModelCheckerHint const &hint=ModelCheckerHint())
static std::vector< ValueType > computeReachabilityRewards(Environment const &env, storm::solver::SolveGoal< ValueType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, RewardModelType const &rewardModel, storm::storage::BitVector const &targetStates, bool qualitative, ModelCheckerHint const &hint=ModelCheckerHint())
static std::vector< ValueType > computeUntilProbabilities(Environment const &env, storm::solver::SolveGoal< ValueType > &&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, ModelCheckerHint const &hint=ModelCheckerHint())
static std::vector< ValueType > computeConditionalProbabilities(Environment const &env, storm::solver::SolveGoal< ValueType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &conditionStates, bool qualitative)
static std::vector< ValueType > computeAllUntilProbabilities(Environment const &env, storm::solver::SolveGoal< ValueType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::BitVector const &initialStates, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
static std::vector< ValueType > computeTotalRewards(Environment const &env, storm::solver::SolveGoal< ValueType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, RewardModelType const &rewardModel, bool qualitative, ModelCheckerHint const &hint=ModelCheckerHint())
static std::map< storm::storage::sparse::state_type, ValueType > computeRewardBoundedValues(Environment const &env, storm::models::sparse::Dtmc< ValueType > const &model, std::shared_ptr< storm::logic::OperatorFormula const > rewardBoundedFormula)
static std::vector< ValueType > computeConditionalRewards(Environment const &env, storm::solver::SolveGoal< ValueType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, RewardModelType const &rewardModel, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &conditionStates, bool qualitative)
static std::vector< ValueType > computeInstantaneousRewards(Environment const &env, storm::solver::SolveGoal< ValueType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, RewardModelType const &rewardModel, uint_fast64_t stepCount)
static std::vector< ValueType > computeDiscountedTotalRewards(Environment const &env, storm::solver::SolveGoal< ValueType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, RewardModelType const &rewardModel, bool qualitative, ValueType discountFactor, ModelCheckerHint const &hint=ModelCheckerHint())
static std::vector< ValueType > computeGloballyProbabilities(Environment const &env, storm::solver::SolveGoal< ValueType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &psiStates, bool qualitative)
static std::vector< ValueType > computeDiscountedCumulativeRewards(Environment const &env, storm::solver::SolveGoal< ValueType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, RewardModelType const &rewardModel, uint_fast64_t stepBound, ValueType discountFactor)
static std::vector< ValueType > computeCumulativeRewards(Environment const &env, storm::solver::SolveGoal< ValueType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, RewardModelType const &rewardModel, uint_fast64_t stepBound)
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...
void setEquationSystemFormatForEpochModel(storm::solver::LinearEquationSolverProblemFormat eqSysFormat)
This class represents a discrete-time Markov chain.
storm::storage::BitVector const & getInitialStates() const
Retrieves the initial states of the model.
LinearEquationSolverRequirements getRequirements(Environment const &env) const
Retrieves the requirements of the solver if it was created with the current settings.
virtual LinearEquationSolverProblemFormat getEquationProblemFormat(Environment const &env) const
Retrieves the problem format that the solver expects if it was created with the current settings.
SolverRequirement const & upperBounds() const
std::string getEnabledRequirementsAsString() const
Checks whether there are no critical requirements left.
bool hasEnabledCriticalRequirement() const
std::unique_ptr< Multiplier< ValueType > > create(Environment const &env, storm::storage::SparseMatrix< ValueType > const &matrix)
A bit vector that is internally represented as a vector of 64-bit values.
void complement()
Negates all bits in the bit vector.
std::vector< uint64_t > getNumberOfSetBitsBeforeIndices() const
Retrieves a vector that holds at position i the number of bits set before index i.
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.
void resize(uint64_t newLength, bool init=false)
Resizes the bit vector to hold the given new number of bits.
bool get(uint64_t index) const
Retrieves the truth value of the bit at the given index and performs a bound check.
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.
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.
void convertToEquationSystem()
Transforms the matrix into an equation system.
void makeRowsAbsorbing(storm::storage::BitVector const &rows, bool dropZeroEntries=false)
This function makes the given rows absorbing.
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...
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.
void deleteDiagonalEntries(bool dropZeroEntries=false)
Sets all diagonal elements to zero.
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.
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_THROW(cond, exception, message)
#define STORM_PRINT_AND_LOG(message)
SFTBDDChecker::ValueType ValueType
std::vector< ValueType > computeUpperRewardBounds(storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< ValueType > const &rewards, std::vector< ValueType > const &oneStepTargetProbabilities)
std::unique_ptr< storm::solver::LinearEquationSolver< ValueType > > configureLinearEquationSolver(Environment const &env, SolveGoal< ValueType, SolutionType > &&goal, storm::solver::LinearEquationSolverFactory< ValueType > const &factory, MatrixType &&matrix)
std::pair< storm::storage::BitVector, storm::storage::BitVector > performProb01(storm::models::sparse::DeterministicModel< T > const &model, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi i...
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 performProbGreater0(storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound, uint_fast64_t maximalSteps)
Performs a backward depth-first search trough the underlying graph structure of the given model to de...
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...
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 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...
storm::storage::BitVector filterZero(std::vector< T > const &values)
Retrieves a bit vector containing all the indices for which the value at this position is equal to ze...
std::vector< Type > filterVector(std::vector< Type > const &in, storm::storage::BitVector const &filter)
bool isOne(ValueType const &a)
bool isZero(ValueType const &a)