Skip to content

Commit

Permalink
format
Browse files Browse the repository at this point in the history
  • Loading branch information
@sjunges
sjunges committed Aug 25, 2023
1 parent 722ca95 commit 1e606bd
Show file tree
Hide file tree
Showing 14 changed files with 47 additions and 43 deletions.
1 change: 0 additions & 1 deletion src/storm/adapters/RationalFunctionForward.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@

namespace carl {


template<typename P>
class FactorizedPolynomial;

Expand Down
12 changes: 8 additions & 4 deletions src/storm/modelchecker/AbstractModelChecker.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -135,7 +135,8 @@ std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeUntilProbab
}

template<typename ModelType>
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeHOAPathProbabilities(Environment const& env, CheckTask<storm::logic::HOAPathFormula, SolutionType> const& checkTask) {
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeHOAPathProbabilities(
Environment const& env, CheckTask<storm::logic::HOAPathFormula, SolutionType> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
}

Expand All @@ -146,7 +147,8 @@ std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeLTLProbabil
}

template<typename ModelType>
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeStateFormulaProbabilities(Environment const& env, CheckTask<storm::logic::Formula, SolutionType> const& checkTask) {
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeStateFormulaProbabilities(
Environment const& env, CheckTask<storm::logic::Formula, SolutionType> const& checkTask) {
// recurse
std::unique_ptr<CheckResult> resultPointer = this->check(env, checkTask.getFormula());
if (resultPointer->isExplicitQualitativeCheckResult()) {
Expand Down Expand Up @@ -241,7 +243,8 @@ std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeTimes(Envir
}

template<typename ModelType>
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType, CheckTask<storm::logic::EventuallyFormula, SolutionType> const& checkTask) {
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeReachabilityTimes(
Environment const& env, storm::logic::RewardMeasureType, CheckTask<storm::logic::EventuallyFormula, SolutionType> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
"This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
}
Expand Down Expand Up @@ -294,7 +297,8 @@ std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::checkAtomicExpress
}

template<typename ModelType>
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::checkAtomicLabelFormula(Environment const& env, CheckTask<storm::logic::AtomicLabelFormula, SolutionType> const& checkTask) {
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::checkAtomicLabelFormula(
Environment const& env, CheckTask<storm::logic::AtomicLabelFormula, SolutionType> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
"This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
}
Expand Down
3 changes: 2 additions & 1 deletion src/storm/modelchecker/AbstractModelChecker.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -113,7 +113,8 @@ class AbstractModelChecker {
CheckTask<storm::logic::RewardOperatorFormula, SolutionType> const& checkTask);
virtual std::unique_ptr<CheckResult> checkTimeOperatorFormula(Environment const& env,
CheckTask<storm::logic::TimeOperatorFormula, SolutionType> const& checkTask);
virtual std::unique_ptr<CheckResult> checkLongRunAverageOperatorFormula(Environment const& env, CheckTask<storm::logic::LongRunAverageOperatorFormula, SolutionType> const& checkTask);
virtual std::unique_ptr<CheckResult> checkLongRunAverageOperatorFormula(
Environment const& env, CheckTask<storm::logic::LongRunAverageOperatorFormula, SolutionType> const& checkTask);
virtual std::unique_ptr<CheckResult> checkUnaryBooleanStateFormula(Environment const& env,
CheckTask<storm::logic::UnaryBooleanStateFormula, SolutionType> const& checkTask);

Expand Down
3 changes: 2 additions & 1 deletion src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,8 @@ class SparseMdpPrctlModelChecker : public SparsePropositionalModelChecker<Sparse
CheckTask<storm::logic::ConditionalFormula, SolutionType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType,
CheckTask<storm::logic::CumulativeRewardFormula, SolutionType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType,
virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(
Environment const& env, storm::logic::RewardMeasureType rewardMeasureType,
CheckTask<storm::logic::InstantaneousRewardFormula, SolutionType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType,
CheckTask<storm::logic::TotalRewardFormula, SolutionType> const& checkTask) override;
Expand Down
18 changes: 9 additions & 9 deletions src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -147,7 +147,7 @@ std::map<storm::storage::sparse::state_type, SolutionType> SparseMdpPrctlHelper<
template<typename ValueType, typename SolutionType>
std::vector<SolutionType> SparseMdpPrctlHelper<ValueType, SolutionType>::computeNextProbabilities(
Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
storm::storage::BitVector const& nextStates) {
storm::storage::BitVector const& nextStates) {
if constexpr (std::is_same_v<ValueType, storm::Interval>) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support next probabilities with reward models.");
} else {
Expand Down Expand Up @@ -330,9 +330,9 @@ void extractValueAndSchedulerHint(SparseMdpHintType<SolutionType>& hintStorage,
template<typename ValueType, typename SolutionType>
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) {
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) {
SparseMdpHintType<SolutionType> result;

// There are no end components if we minimize until probabilities or
Expand Down Expand Up @@ -442,8 +442,7 @@ MaybeStateResult<SolutionType> computeValuesForMaybeStates(Environment const& en
bool produceScheduler, SparseMdpHintType<SolutionType>& hint) {
// Initialize the solution vector.
std::vector<SolutionType> x =
hint.hasValueHint()
? std::move(hint.getValueHint())
hint.hasValueHint() ? std::move(hint.getValueHint())
: std::vector<SolutionType>(submatrix.getRowGroupCount(),
hint.hasLowerResultBound() ? hint.getLowerResultBound() : storm::utility::zero<SolutionType>());

Expand Down Expand Up @@ -718,7 +717,8 @@ MDPSparseModelCheckingHelperReturnType<SolutionType> SparseMdpPrctlHelper<ValueT

// Obtain proper hint information either from the provided hint or from requirements of the solver.
SparseMdpHintType<SolutionType> hintInformation = computeHints<ValueType, SolutionType>(
env, SemanticSolutionType::UntilProbabilities, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, phiStates, qualitativeStateSets.statesWithProbability1, produceScheduler);
env, SemanticSolutionType::UntilProbabilities, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates,
phiStates, qualitativeStateSets.statesWithProbability1, produceScheduler);

// Declare the components of the equation system we will solve.
storm::storage::SparseMatrix<ValueType> submatrix;
Expand Down Expand Up @@ -820,7 +820,7 @@ template<typename ValueType, typename SolutionType>
template<typename RewardModelType>
std::vector<SolutionType> SparseMdpPrctlHelper<ValueType, SolutionType>::computeInstantaneousRewards(
Environment const& env, storm::solver::SolveGoal<ValueType, SolutionType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
RewardModelType const& rewardModel, uint_fast64_t stepCount) {
RewardModelType const& rewardModel, uint_fast64_t stepCount) {
if constexpr (std::is_same_v<ValueType, storm::Interval>) {
throw storm::exceptions::NotImplementedException() << "We do not support this function with interval models.";
} else {
Expand All @@ -841,7 +841,7 @@ template<typename ValueType, typename SolutionType>
template<typename RewardModelType>
std::vector<SolutionType> SparseMdpPrctlHelper<ValueType, SolutionType>::computeCumulativeRewards(
Environment const& env, storm::solver::SolveGoal<ValueType, SolutionType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
RewardModelType const& rewardModel, uint_fast64_t stepBound) {
RewardModelType const& rewardModel, uint_fast64_t stepBound) {
if constexpr (std::is_same_v<ValueType, storm::Interval>) {
throw storm::exceptions::NotImplementedException() << "We do not support this function with interval models.";
} else {
Expand Down
31 changes: 15 additions & 16 deletions src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ class SparseMdpPrctlHelper {

static std::vector<SolutionType> computeNextProbabilities(Environment const& env, OptimizationDirection dir,
storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
storm::storage::BitVector const& nextStates);
storm::storage::BitVector const& nextStates);

static MDPSparseModelCheckingHelperReturnType<SolutionType> computeUntilProbabilities(
Environment const& env, storm::solver::SolveGoal<ValueType, SolutionType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
Expand All @@ -53,27 +53,27 @@ class SparseMdpPrctlHelper {
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);
storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
storm::storage::BitVector const& psiStates, bool qualitative,
bool produceScheduler, bool useMecBasedTechnique = false);

template<typename RewardModelType>
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);
RewardModelType const& rewardModel, uint_fast64_t stepCount);

template<typename RewardModelType>
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);
storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
RewardModelType const& rewardModel, uint_fast64_t stepBound);

template<typename RewardModelType>
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());
storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
RewardModelType const& rewardModel, bool qualitative, bool produceScheduler,
ModelCheckerHint const& hint = ModelCheckerHint());

template<typename RewardModelType>
static MDPSparseModelCheckingHelperReturnType<SolutionType> computeReachabilityRewards(
Expand All @@ -83,15 +83,14 @@ class SparseMdpPrctlHelper {

static MDPSparseModelCheckingHelperReturnType<SolutionType> computeReachabilityTimes(
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& targetStates, bool qualitative,
bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint());
storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, bool qualitative,
bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint());

static std::vector<SolutionType> computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal<ValueType, SolutionType>&& goal,
storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
storm::models::sparse::StandardRewardModel<storm::Interval> const& intervalRewardModel,
bool lowerBoundOfIntervals, storm::storage::BitVector const& targetStates, bool qualitative);
storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
storm::models::sparse::StandardRewardModel<storm::Interval> const& intervalRewardModel,
bool lowerBoundOfIntervals, storm::storage::BitVector const& targetStates, bool qualitative);

static std::unique_ptr<CheckResult> computeConditionalProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType, SolutionType>&& goal,
storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
Expand Down
2 changes: 1 addition & 1 deletion src/storm/models/sparse/Model.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -439,6 +439,7 @@ class Model : public storm::models::Model<CValueType> {
* @return
*/
virtual std::string additionalDotStateInfo(uint64_t state) const;

private:
// Upon construction of a model, this function asserts that the specified components are valid
void assertValidityOfComponents(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const& components) const;
Expand Down Expand Up @@ -494,4 +495,3 @@ std::set<storm::RationalFunctionVariable> getAllParameters(Model<storm::Rational
} // namespace sparse
} // namespace models
} // namespace storm

2 changes: 1 addition & 1 deletion src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -209,7 +209,7 @@ bool IterativeMinMaxLinearEquationSolver<ValueType, SolutionType>::solveEquation
template<typename ValueType, typename SolutionType>
bool IterativeMinMaxLinearEquationSolver<ValueType, SolutionType>::performPolicyIteration(
Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x, std::vector<ValueType> const& b,
std::vector<storm::storage::sparse::state_type>&& initialPolicy) const {
std::vector<storm::storage::sparse::state_type>&& initialPolicy) const {
if constexpr (std::is_same_v<ValueType, storm::Interval>) {
throw storm::exceptions::NotImplementedException() << "We did not implement policy iteration for interval-based models.";
return false;
Expand Down
4 changes: 2 additions & 2 deletions src/storm/solver/MinMaxLinearEquationSolver.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -175,6 +175,7 @@ class MinMaxLinearEquationSolver : public AbstractEquationSolver<SolutionType> {
* Retrieves whether the solver is aware that the requirements were checked.
*/
bool isRequirementsCheckedSet() const;

protected:
virtual bool internalSolveEquations(Environment const& env, OptimizationDirection d, std::vector<SolutionType>& x,
std::vector<ValueType> const& b) const = 0;
Expand Down Expand Up @@ -208,7 +209,7 @@ class MinMaxLinearEquationSolver : public AbstractEquationSolver<SolutionType> {
bool requirementsChecked;

/// For uncertain models, if this flag is set to true, the uncertainty is resolved adverserially and angelically otherwise.
bool robust; // TODO use.
bool robust; // TODO use.
};

template<typename ValueType, typename SolutionType = ValueType>
Expand Down Expand Up @@ -249,4 +250,3 @@ class GeneralMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolv

} // namespace solver
} // namespace storm

Loading

0 comments on commit 1e606bd

Please sign in to comment.