diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
index 79cc6fc87..cb110be26 100644
--- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
+++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
@@ -141,8 +141,7 @@ namespace storm {
ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
-
- auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper<ValueType>::computeUntilProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint());
+ auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper<ValueType>::computeUntilProbabilitiesSound(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint());
std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
if(checkTask.isShieldingTask()) {
storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true);
diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
index 31ddac9da..784fc27d5 100644
--- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
+++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
@@ -9,6 +9,7 @@
#include "storm/utility/vector.h"
#include "storm/utility/graph.h"
#include "storm/modelchecker/rpatl/helper/internal/GameViHelper.h"
+#include "storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h"
namespace storm {
namespace modelchecker {
@@ -59,6 +60,43 @@ namespace storm {
return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
}
+ template<typename ValueType>
+ SMGSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeUntilProbabilitiesSound(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, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) {
+
+ storm::modelchecker::helper::internal::SoundGameViHelper<ValueType> viHelper(transitionMatrix, statesOfCoalition);
+
+ // Initialize the x vector and solution vector result.
+ // TODO Fabian: maybe relevant states (later)
+ std::vector<ValueType> xL = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+ // std::transform(xL.begin(), xL.end(), psiStates.begin(), xL, [](double& a) { a *= 3; }) // TODO Fabian
+ // assigning 1s to the xL vector for all Goal states
+ assert(xL.size() == psiStates.size());
+ for (size_t i = 0; i < xL.size(); i++)
+ {
+ if (psiStates[xL.size() - i])
+ xL[i] = 1;
+ }
+ STORM_LOG_DEBUG("xL " << xL);
+ std::vector<ValueType> xU = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+ storm::storage::BitVector probGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates);
+ // assigning 1s to the xU vector for all states except the states s where Prob(sEf) = 0 for all goal states f
+ assert(xU.size() == probGreater0.size());
+ for (size_t i = 0; i < xL.size(); i++)
+ {
+ if (probGreater0[i])
+ xU[i] = 1;
+ }
+ STORM_LOG_DEBUG("xU " << xU);
+
+ std::vector<ValueType> result = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+ // std::vector<ValueType> constrainedChoiceValues = std::vector<ValueType>(b.size(), storm::utility::zero<ValueType>()); // TODO Fabian: do I need this?
+ std::vector<ValueType> constrainedChoiceValues;
+
+ viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues);
+
+ assert(false);
+ }
+
template<typename ValueType>
storm::storage::Scheduler<ValueType> SparseSmgRpatlHelper<ValueType>::expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates) {
storm::storage::Scheduler<ValueType> completeScheduler(psiStates.size());
diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h
index 0592c929b..741d5961d 100644
--- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h
+++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h
@@ -35,6 +35,7 @@ namespace storm {
class SparseSmgRpatlHelper {
public:
static SMGSparseModelCheckingHelperReturnType<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, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint());
+ static SMGSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilitiesSound(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, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint);
static SMGSparseModelCheckingHelperReturnType<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, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint());
static SMGSparseModelCheckingHelperReturnType<ValueType> computeNextProbabilities(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, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint);
static SMGSparseModelCheckingHelperReturnType<ValueType> computeBoundedGloballyProbabilities(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, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint, uint64_t lowerBound, uint64_t upperBound);
diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
new file mode 100644
index 000000000..239a89d31
--- /dev/null
+++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
@@ -0,0 +1,255 @@
+#include "SoundGameViHelper.h"
+
+#include "storm/environment/Environment.h"
+#include "storm/environment/solver/SolverEnvironment.h"
+#include "storm/environment/solver/GameSolverEnvironment.h"
+
+
+#include "storm/utility/SignalHandler.h"
+#include "storm/utility/vector.h"
+
+namespace storm {
+ namespace modelchecker {
+ namespace helper {
+ namespace internal {
+
+ template <typename ValueType>
+ SoundGameViHelper<ValueType>::SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) {
+ // Intentionally left empty.
+ }
+
+ template <typename ValueType>
+ void SoundGameViHelper<ValueType>::prepareSolversAndMultipliers(const Environment& env) {
+ STORM_LOG_DEBUG("\n" << _transitionMatrix);
+ _multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix);
+ _x1IsCurrent = false;
+ }
+
+ template <typename ValueType>
+ void SoundGameViHelper<ValueType>::performValueIteration(Environment const& env, std::vector<ValueType>& xL, std::vector<ValueType>& xU, storm::solver::OptimizationDirection const dir, std::vector<ValueType>& constrainedChoiceValues) {
+ // new pair (x_old, x_new) for over_approximation()
+
+ prepareSolversAndMultipliers(env);
+ // Get precision for convergence check.
+ ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().game().getPrecision());
+
+ STORM_LOG_DEBUG("hello" << "world");
+ uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations();
+ //_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+ _x1L = xL;
+ _x2L = _x1L;
+
+ _x1U = xU;
+ _x2U = _x1U;
+
+ if (this->isProduceSchedulerSet()) {
+ if (!this->_producedOptimalChoices.is_initialized()) {
+ this->_producedOptimalChoices.emplace();
+ }
+ this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount());
+ }
+
+ uint64_t iter = 0;
+ constrainedChoiceValues = std::vector<ValueType>(xL.size(), storm::utility::zero<ValueType>()); // ??
+
+ while (iter < maxIter) {
+ performIterationStep(env, dir);
+ if (checkConvergence(precision)) {
+ //_multiplier->multiply(env, xNewL(), nullptr, constrainedChoiceValues); // TODO Fabian: ???
+ break;
+ }
+ if (storm::utility::resources::isTerminate()) {
+ break;
+ }
+ ++iter;
+ }
+ xL = xNewL();
+ xU = xNewU();
+
+ STORM_LOG_DEBUG("result xL: " << xL);
+ STORM_LOG_DEBUG("result xU: " << xU);
+
+ if (isProduceSchedulerSet()) {
+ // We will be doing one more iteration step and track scheduler choices this time.
+ performIterationStep(env, dir, &_producedOptimalChoices.get());
+ }
+ }
+
+ template <typename ValueType>
+ void SoundGameViHelper<ValueType>::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices) {
+ // under approximation
+ if (!_multiplier) {
+ prepareSolversAndMultipliers(env);
+ }
+ _x1IsCurrent = !_x1IsCurrent;
+
+ if (choices == nullptr) {
+ _multiplier->multiplyAndReduce(env, dir, xOldL(), nullptr, xNewL(), nullptr, &_statesOfCoalition);
+ } else {
+ _multiplier->multiplyAndReduce(env, dir, xOldL(), nullptr, xNewL(), choices, &_statesOfCoalition);
+ }
+
+ // over_approximation
+
+ if (choices == nullptr) {
+ _multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), nullptr, &_statesOfCoalition);
+ } else {
+ _multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), choices, &_statesOfCoalition);
+ }
+
+ // TODO Fabian: find_MSECs() & deflate()
+
+ }
+
+ template <typename ValueType>
+ bool SoundGameViHelper<ValueType>::checkConvergence(ValueType threshold) const {
+ STORM_LOG_ASSERT(_multiplier, "tried to check for convergence without doing an iteration first.");
+ // Now check whether the currently produced results are precise enough
+ STORM_LOG_ASSERT(threshold > storm::utility::zero<ValueType>(), "Did not expect a non-positive threshold.");
+ auto x1It = xOldL().begin();
+ auto x1Ite = xOldL().end();
+ auto x2It = xNewL().begin();
+ ValueType maxDiff = (*x2It - *x1It);
+ ValueType minDiff = maxDiff;
+ // The difference between maxDiff and minDiff is zero at this point. Thus, it doesn't make sense to check the threshold now.
+ for (++x1It, ++x2It; x1It != x1Ite; ++x1It, ++x2It) {
+ ValueType diff = (*x2It - *x1It);
+ // Potentially update maxDiff or minDiff
+ bool skipCheck = false;
+ if (maxDiff < diff) {
+ maxDiff = diff;
+ } else if (minDiff > diff) {
+ minDiff = diff;
+ } else {
+ skipCheck = true;
+ }
+ // Check convergence
+ if (!skipCheck && (maxDiff - minDiff) > threshold) {
+ return false;
+ }
+ }
+ return true;
+ }
+
+ template <typename ValueType>
+ void SoundGameViHelper<ValueType>::setProduceScheduler(bool value) {
+ _produceScheduler = value;
+ }
+
+ template <typename ValueType>
+ bool SoundGameViHelper<ValueType>::isProduceSchedulerSet() const {
+ return _produceScheduler;
+ }
+
+ template <typename ValueType>
+ void SoundGameViHelper<ValueType>::setShieldingTask(bool value) {
+ _shieldingTask = value;
+ }
+
+ template <typename ValueType>
+ bool SoundGameViHelper<ValueType>::isShieldingTask() const {
+ return _shieldingTask;
+ }
+
+ template <typename ValueType>
+ void SoundGameViHelper<ValueType>::updateTransitionMatrix(storm::storage::SparseMatrix<ValueType> newTransitionMatrix) {
+ _transitionMatrix = newTransitionMatrix;
+ }
+
+ template <typename ValueType>
+ void SoundGameViHelper<ValueType>::updateStatesOfCoalition(storm::storage::BitVector newStatesOfCoalition) {
+ _statesOfCoalition = newStatesOfCoalition;
+ }
+
+ template <typename ValueType>
+ std::vector<uint64_t> const& SoundGameViHelper<ValueType>::getProducedOptimalChoices() const {
+ STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested.");
+ STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?");
+ return this->_producedOptimalChoices.get();
+ }
+
+ template <typename ValueType>
+ std::vector<uint64_t>& SoundGameViHelper<ValueType>::getProducedOptimalChoices() {
+ STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested.");
+ STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?");
+ return this->_producedOptimalChoices.get();
+ }
+
+ template <typename ValueType>
+ storm::storage::Scheduler<ValueType> SoundGameViHelper<ValueType>::extractScheduler() const{
+ auto const& optimalChoices = getProducedOptimalChoices();
+ storm::storage::Scheduler<ValueType> scheduler(optimalChoices.size());
+ for (uint64_t state = 0; state < optimalChoices.size(); ++state) {
+ scheduler.setChoice(optimalChoices[state], state);
+ }
+ return scheduler;
+ }
+
+ template <typename ValueType>
+ void SoundGameViHelper<ValueType>::getChoiceValues(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType>& choiceValues) {
+ _multiplier->multiply(env, x, nullptr, choiceValues);
+ }
+
+ template <typename ValueType>
+ void SoundGameViHelper<ValueType>::fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices) {
+ std::vector<ValueType> allChoices = std::vector<ValueType>(rowGroupIndices.at(rowGroupIndices.size() - 1), storm::utility::zero<ValueType>());
+ auto choice_it = choiceValues.begin();
+ for(uint state = 0; state < rowGroupIndices.size() - 1; state++) {
+ uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state];
+ if (psiStates.get(state)) {
+ for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) {
+ allChoices.at(rowGroupIndices.at(state) + choice) = *choice_it;
+ }
+ }
+ }
+ choiceValues = allChoices;
+ }
+
+ template <typename ValueType>
+ std::vector<ValueType>& SoundGameViHelper<ValueType>::xNewL() {
+ return _x1IsCurrent ? _x1L : _x2L;
+ }
+
+ template <typename ValueType>
+ std::vector<ValueType> const& SoundGameViHelper<ValueType>::xNewL() const {
+ return _x1IsCurrent ? _x1L : _x2L;
+ }
+
+ template <typename ValueType>
+ std::vector<ValueType>& SoundGameViHelper<ValueType>::xOldL() {
+ return _x1IsCurrent ? _x2L : _x1L;
+ }
+
+ template <typename ValueType>
+ std::vector<ValueType> const& SoundGameViHelper<ValueType>::xOldL() const {
+ return _x1IsCurrent ? _x2L : _x1L;
+ }
+
+ template <typename ValueType>
+ std::vector<ValueType>& SoundGameViHelper<ValueType>::xNewU() {
+ return _x1IsCurrent ? _x1U : _x2U;
+ }
+
+ template <typename ValueType>
+ std::vector<ValueType> const& SoundGameViHelper<ValueType>::xNewU() const {
+ return _x1IsCurrent ? _x1U : _x2U;
+ }
+
+ template <typename ValueType>
+ std::vector<ValueType>& SoundGameViHelper<ValueType>::xOldU() {
+ return _x1IsCurrent ? _x2U : _x1U;
+ }
+
+ template <typename ValueType>
+ std::vector<ValueType> const& SoundGameViHelper<ValueType>::xOldU() const {
+ return _x1IsCurrent ? _x2U : _x1U;
+ }
+
+ template class SoundGameViHelper<double>;
+#ifdef STORM_HAVE_CARL
+ template class SoundGameViHelper<storm::RationalNumber>;
+#endif
+ }
+ }
+ }
+}
diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h
new file mode 100644
index 000000000..f4e3d5b35
--- /dev/null
+++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h
@@ -0,0 +1,119 @@
+#pragma once
+
+#include "storm/storage/SparseMatrix.h"
+#include "storm/solver/LinearEquationSolver.h"
+#include "storm/solver/MinMaxLinearEquationSolver.h"
+#include "storm/solver/Multiplier.h"
+
+namespace storm {
+ class Environment;
+
+ namespace storage {
+ template <typename VT> class Scheduler;
+ }
+
+ namespace modelchecker {
+ namespace helper {
+ namespace internal {
+
+ template <typename ValueType>
+ class SoundGameViHelper {
+ public:
+ SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition);
+
+ void prepareSolversAndMultipliers(const Environment& env);
+
+ /*!
+ * Perform value iteration until convergence
+ */
+ void performValueIteration(Environment const& env, std::vector<ValueType>& xL, std::vector<ValueType>& xU, storm::solver::OptimizationDirection const dir, std::vector<ValueType>& constrainedChoiceValues);
+
+ /*!
+ * Sets whether an optimal scheduler shall be constructed during the computation
+ */
+ void setProduceScheduler(bool value);
+
+ /*!
+ * @return whether an optimal scheduler shall be constructed during the computation
+ */
+ bool isProduceSchedulerSet() const;
+
+ /*!
+ * Sets whether an optimal scheduler shall be constructed during the computation
+ */
+ void setShieldingTask(bool value);
+
+ /*!
+ * @return whether an optimal scheduler shall be constructed during the computation
+ */
+ bool isShieldingTask() const;
+
+ /*!
+ * Changes the transitionMatrix to the given one.
+ */
+ void updateTransitionMatrix(storm::storage::SparseMatrix<ValueType> newTransitionMatrix);
+
+ /*!
+ * Changes the statesOfCoalition to the given one.
+ */
+ void updateStatesOfCoalition(storm::storage::BitVector newStatesOfCoalition);
+
+ storm::storage::Scheduler<ValueType> extractScheduler() const;
+
+ void getChoiceValues(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType>& choiceValues);
+
+ /*!
+ * Fills the choice values vector to the original size with zeros for ~psiState choices.
+ */
+ void fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices);
+
+ private:
+ /*!
+ * Performs one iteration step for value iteration
+ */
+ void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);
+
+ /*!
+ * Checks whether the curently computed value achieves the desired precision
+ */
+ bool checkConvergence(ValueType precision) const;
+
+ std::vector<ValueType>& xNewL();
+ std::vector<ValueType> const& xNewL() const;
+
+ std::vector<ValueType>& xOldL();
+ std::vector<ValueType> const& xOldL() const;
+
+ std::vector<ValueType>& xNewU();
+ std::vector<ValueType> const& xNewU() const;
+
+ std::vector<ValueType>& xOldU();
+ std::vector<ValueType> const& xOldU() const;
+
+ bool _x1IsCurrent;
+
+ /*!
+ * @pre before calling this, a computation call should have been performed during which scheduler production was enabled.
+ * @return the produced scheduler of the most recent call.
+ */
+ std::vector<uint64_t> const& getProducedOptimalChoices() const;
+
+ /*!
+ * @pre before calling this, a computation call should have been performed during which scheduler production was enabled.
+ * @return the produced scheduler of the most recent call.
+ */
+ std::vector<uint64_t>& getProducedOptimalChoices();
+
+ storm::storage::SparseMatrix<ValueType> _transitionMatrix;
+ storm::storage::BitVector _statesOfCoalition;
+ std::vector<ValueType> _x, _x1L, _x2L, _x1U, _x2U;
+ std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier;
+
+ bool _produceScheduler = false;
+ bool _shieldingTask = false;
+ boost::optional<std::vector<uint64_t>> _producedOptimalChoices;
+ };
+ }
+ }
+ }
+}