diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index b12fb11ce..3b13c8a3f 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -2,6 +2,8 @@ #include "src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h" +#include "src/modelchecker/multiobjective/pcaa.h" + #include "src/models/sparse/StandardRewardModel.h" #include "src/utility/macros.h" @@ -34,7 +36,15 @@ namespace storm { storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::FragmentSpecification fragment = storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setReachabilityRewardFormulasAllowed(true); fragment.setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true); - return formula.isInFragment(fragment); + if(formula.isInFragment(fragment)) { + return true; + } else { + fragment = storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(true); + //In general, each initial state requires an individual scheduler (in contrast to single objective model checking). Let's exclude multiple initial states. + if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; + if(!checkTask.isOnlyInitialStatesRelevantSet()) return false; + return formula.isInFragment(fragment); + } } template @@ -107,7 +117,12 @@ namespace storm { std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeTimes(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } - + + template + std::unique_ptr SparseMarkovAutomatonCslModelChecker::checkMultiObjectiveFormula(CheckTask const& checkTask) { + return multiobjective::performPcaa(this->getModel(), checkTask.getFormula()); + } + template class SparseMarkovAutomatonCslModelChecker>; } } diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 5fbfb85e4..a4b911b33 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -26,6 +26,7 @@ namespace storm { virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr checkMultiObjectiveFormula(CheckTask const& checkTask) override; private: // An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices. diff --git a/src/modelchecker/multiobjective/Pcaa.cpp b/src/modelchecker/multiobjective/Pcaa.cpp index 1937835d4..5d6eacf22 100644 --- a/src/modelchecker/multiobjective/Pcaa.cpp +++ b/src/modelchecker/multiobjective/Pcaa.cpp @@ -9,6 +9,8 @@ #include "src/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h" #include "src/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h" #include "src/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h" +#include "src/settings//SettingsManager.h" +#include "src/settings/modules/MultiObjectiveSettings.h" #include "src/exceptions/InvalidArgumentException.h" @@ -22,6 +24,12 @@ namespace storm { STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "Multi-objective Model checking on model with multiple initial states is not supported."); #ifdef STORM_HAVE_CARL + + // If we consider an MA, ensure that it is closed + if(model.isOfType(storm::models::ModelType::MarkovAutomaton)) { + STORM_LOG_THROW(dynamic_cast const *>(&model)->isClosed(), storm::exceptions::InvalidArgumentException, "Unable to check multi-objective formula on non-closed Markov automaton."); + } + auto preprocessorResult = SparsePcaaPreprocessor::preprocess(model, formula); STORM_LOG_DEBUG("Preprocessing done. Result: " << preprocessorResult); @@ -41,7 +49,12 @@ namespace storm { break; } - return query->check(); + auto result = query->check(); + + if(settings::getModule().isExportPlotSet()) { + query->exportPlotOfCurrentApproximation(storm::settings::getModule().getExportPlotDirectory()); + } + return result; #else STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Multi-objective model checking requires carl."); return nullptr; diff --git a/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp b/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp deleted file mode 100644 index f16b208b5..000000000 --- a/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp +++ /dev/null @@ -1,46 +0,0 @@ -#include "src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.h" - -#include "src/utility/macros.h" -#include "src/logic/Formulas.h" -#include "src/logic/FragmentSpecification.h" - -#include "src/models/sparse/StandardRewardModel.h" - -#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" -#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" - -#include "src/modelchecker/multiobjective/pcaa.h" - -#include "src/exceptions/InvalidArgumentException.h" - -namespace storm { - namespace modelchecker { - template - SparseMaMultiObjectiveModelChecker::SparseMaMultiObjectiveModelChecker(SparseMaModelType const& model) : SparseMarkovAutomatonCslModelChecker(model) { - // Intentionally left empty. - } - - template - bool SparseMaMultiObjectiveModelChecker::canHandle(CheckTask const& checkTask) const { - // A formula without multi objective (sub)formulas can be handled by the base class - if(SparseMarkovAutomatonCslModelChecker::canHandle(checkTask)) return true; - //In general, each initial state requires an individual scheduler (in contrast to single objective model checking). Let's exclude this. - if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; - if(!checkTask.isOnlyInitialStatesRelevantSet()) return false; - return checkTask.getFormula().isInFragment(storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(true)); - } - - template - std::unique_ptr SparseMaMultiObjectiveModelChecker::checkMultiObjectiveFormula(CheckTask const& checkTask) { - STORM_LOG_ASSERT(this->getModel().getInitialStates().getNumberOfSetBits() == 1, "Multi-objective Model checking on model with multiple initial states is not supported."); - STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidArgumentException, "Unable to check multi-objective formula in non-closed Markov automaton."); - - return multiobjective::performPcaa(this->getModel(), checkTask.getFormula()); - } - - - - template class SparseMaMultiObjectiveModelChecker>; - // template class SparseMaMultiObjectiveModelChecker>; - } -} diff --git a/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.h b/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.h deleted file mode 100644 index 4d20e6140..000000000 --- a/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.h +++ /dev/null @@ -1,27 +0,0 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMAMULTIOBJECTIVEMODELCHECKER_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMAMULTIOBJECTIVEMODELCHECKER_H_ - -#include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" - -namespace storm { - namespace modelchecker { - template - class SparseMaMultiObjectiveModelChecker : public SparseMarkovAutomatonCslModelChecker { - public: - typedef typename SparseMaModelType::ValueType ValueType; - typedef typename SparseMaModelType::RewardModelType RewardModelType; - - explicit SparseMaMultiObjectiveModelChecker(SparseMaModelType const& model); - - virtual bool canHandle(CheckTask const& checkTask) const override; - - virtual std::unique_ptr checkMultiObjectiveFormula(CheckTask const& checkTask) override; - - private: - - - }; - } // namespace modelchecker -} // namespace storm - -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMAMULTIOBJECTIVEMODELCHECKER_H_ */ diff --git a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp deleted file mode 100644 index 9f561b06e..000000000 --- a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp +++ /dev/null @@ -1,43 +0,0 @@ -#include "src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h" - -#include "src/utility/macros.h" -#include "src/logic/Formulas.h" -#include "src/logic/FragmentSpecification.h" - -#include "src/models/sparse/StandardRewardModel.h" - -#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" -#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" - -#include "src/modelchecker/multiobjective/pcaa.h" - -namespace storm { - namespace modelchecker { - template - SparseMdpMultiObjectiveModelChecker::SparseMdpMultiObjectiveModelChecker(SparseMdpModelType const& model) : SparseMdpPrctlModelChecker(model) { - // Intentionally left empty. - } - - template - bool SparseMdpMultiObjectiveModelChecker::canHandle(CheckTask const& checkTask) const { - // A formula without multi objective (sub)formulas can be handled by the base class - if(SparseMdpPrctlModelChecker::canHandle(checkTask)) return true; - //In general, each initial state requires an individual scheduler (in contrast to single objective model checking). Let's exclude this. - if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; - if(!checkTask.isOnlyInitialStatesRelevantSet()) return false; - return checkTask.getFormula().isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true)); - } - - template - std::unique_ptr SparseMdpMultiObjectiveModelChecker::checkMultiObjectiveFormula(CheckTask const& checkTask) { - STORM_LOG_ASSERT(this->getModel().getInitialStates().getNumberOfSetBits() == 1, "Multi Objective Model checking on model with multiple initial states is not supported."); - return multiobjective::performPcaa(this->getModel(), checkTask.getFormula()); - } - - - template class SparseMdpMultiObjectiveModelChecker>; -#ifdef STORM_HAVE_CARL - template class SparseMdpMultiObjectiveModelChecker>; -#endif - } -} diff --git a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h deleted file mode 100644 index ad0c2aa2b..000000000 --- a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h +++ /dev/null @@ -1,27 +0,0 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMDPMULTIOBJECTIVEMODELCHECKER_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMDPMULTIOBJECTIVEMODELCHECKER_H_ - -#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" - -namespace storm { - namespace modelchecker { - template - class SparseMdpMultiObjectiveModelChecker : public SparseMdpPrctlModelChecker { - public: - typedef typename SparseMdpModelType::ValueType ValueType; - typedef typename SparseMdpModelType::RewardModelType RewardModelType; - - explicit SparseMdpMultiObjectiveModelChecker(SparseMdpModelType const& model); - - virtual bool canHandle(CheckTask const& checkTask) const override; - - virtual std::unique_ptr checkMultiObjectiveFormula(CheckTask const& checkTask) override; - - private: - - - }; - } // namespace modelchecker -} // namespace storm - -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMDPMULTIOBJECTIVEMODELCHECKER_H_ */ diff --git a/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp deleted file mode 100644 index b81fbba1c..000000000 --- a/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp +++ /dev/null @@ -1,422 +0,0 @@ -#include "src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.h" - -#include - -#include "src/adapters/CarlAdapter.h" -#include "src/models/sparse/MarkovAutomaton.h" -#include "src/models/sparse/StandardRewardModel.h" -#include "src/transformer/EndComponentEliminator.h" -#include "src/utility/macros.h" -#include "src/utility/vector.h" - -#include "src/exceptions/InvalidOperationException.h" - -namespace storm { - namespace modelchecker { - namespace helper { - - template - SparseMaMultiObjectiveWeightVectorChecker::SparseMaMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : SparseMultiObjectiveWeightVectorChecker(data) { - // Set the (discretized) state action rewards. - this->discreteActionRewards.resize(data.objectives.size()); - for(auto objIndex : this->objectivesWithNoUpperTimeBound) { - typename SparseMaModelType::RewardModelType const& rewModel = this->data.preprocessedModel.getRewardModel(this->data.objectives[objIndex].rewardModelName); - STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected."); - this->discreteActionRewards[objIndex] = rewModel.hasStateActionRewards() ? rewModel.getStateActionRewardVector() : std::vector(this->data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero()); - if(rewModel.hasStateRewards()) { - // Note that state rewards are earned over time and thus play no role for probabilistic states - for(auto markovianState : this->data.getMarkovianStatesOfPreprocessedModel()) { - this->discreteActionRewards[objIndex][this->data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[markovianState]] += rewModel.getStateReward(markovianState) / this->data.preprocessedModel.getExitRate(markovianState); - } - } - } - } - - template - void SparseMaMultiObjectiveWeightVectorChecker::boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) { - - // Split the preprocessed model into transitions from/to probabilistic/Markovian states. - SubModel MS = createSubModel(true, weightedRewardVector); - SubModel PS = createSubModel(false, weightedRewardVector); - - // Apply digitization to Markovian transitions - ValueType digitizationConstant = getDigitizationConstant(); - digitize(MS, digitizationConstant); - - // Get for each occurring (digitized) timeBound the indices of the objectives with that bound. - TimeBoundMap lowerTimeBounds; - TimeBoundMap upperTimeBounds; - digitizeTimeBounds(lowerTimeBounds, upperTimeBounds, digitizationConstant); - - // Initialize a minMaxSolver to compute an optimal scheduler (w.r.t. PS) for each epoch - // The end components that stay in PS will be removed. - // Note that the end component elimination could be omitted if we forbid zeno behavior - std::unique_ptr minMax = initMinMaxSolverData(PS); - - // Store the optimal choices of PS as computed by the minMax solver. - std::vector optimalChoicesAtCurrentEpoch(PS.getNumberOfStates(), std::numeric_limits::max()); - - // create a linear equation solver for the model induced by the optimal choice vector. - // the solver will be updated whenever the optimal choice vector has changed. - // We choose Jacobi since we call the solver very frequently on 'easy' inputs (note that jacobi without preconditioning has very little overhead). - LinEqSolverData linEq; - linEq.factory.getSettings().setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings::SolutionMethod::Jacobi); - linEq.factory.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings::Preconditioner::None); - linEq.b.resize(PS.getNumberOfStates()); - - // Stores the objectives for which we need to compute values in the current time epoch. - storm::storage::BitVector consideredObjectives = this->objectivesWithNoUpperTimeBound; - - auto lowerTimeBoundIt = lowerTimeBounds.begin(); - auto upperTimeBoundIt = upperTimeBounds.begin(); - uint_fast64_t currentEpoch = std::max(lowerTimeBounds.empty() ? 0 : lowerTimeBoundIt->first, upperTimeBounds.empty() ? 0 : upperTimeBoundIt->first); - while(true) { - // Update the objectives that are considered at the current time epoch as well as the (weighted) reward vectors. - updateDataToCurrentEpoch(MS, PS, *minMax, consideredObjectives, currentEpoch, weightVector, lowerTimeBoundIt, lowerTimeBounds, upperTimeBoundIt, upperTimeBounds); - - // Compute the values that can be obtained at probabilistic states in the current time epoch - performPSStep(PS, MS, *minMax, linEq, optimalChoicesAtCurrentEpoch, consideredObjectives); - - // Compute values that can be obtained at Markovian states after letting one (digitized) time unit pass. - // Only perform such a step if there is time left. - if(currentEpoch>0) { - performMSStep(MS, PS, consideredObjectives); - --currentEpoch; - } else { - break; - } - } - - // compose the results from MS and PS - storm::utility::vector::setVectorValues(this->weightedResult, MS.states, MS.weightedSolutionVector); - storm::utility::vector::setVectorValues(this->weightedResult, PS.states, PS.weightedSolutionVector); - for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) { - storm::utility::vector::setVectorValues(this->objectiveResults[objIndex], MS.states, MS.objectiveSolutionVectors[objIndex]); - storm::utility::vector::setVectorValues(this->objectiveResults[objIndex], PS.states, PS.objectiveSolutionVectors[objIndex]); - } - } - - - template - typename SparseMaMultiObjectiveWeightVectorChecker::SubModel SparseMaMultiObjectiveWeightVectorChecker::createSubModel(bool createMS, std::vector const& weightedRewardVector) const { - SubModel result; - - storm::storage::BitVector probabilisticStates = ~this->data.getMarkovianStatesOfPreprocessedModel(); - result.states = createMS ? this->data.getMarkovianStatesOfPreprocessedModel() : probabilisticStates; - result.choices = this->data.preprocessedModel.getTransitionMatrix().getRowIndicesOfRowGroups(result.states); - STORM_LOG_ASSERT(!createMS || result.states.getNumberOfSetBits() == result.choices.getNumberOfSetBits(), "row groups for Markovian states should consist of exactly one row"); - - //We need to add diagonal entries for selfloops on Markovian states. - result.toMS = this->data.preprocessedModel.getTransitionMatrix().getSubmatrix(true, result.states, this->data.getMarkovianStatesOfPreprocessedModel(), createMS); - result.toPS = this->data.preprocessedModel.getTransitionMatrix().getSubmatrix(true, result.states, probabilisticStates, false); - STORM_LOG_ASSERT(result.getNumberOfStates() == result.states.getNumberOfSetBits() && result.getNumberOfStates() == result.toMS.getRowGroupCount() && result.getNumberOfStates() == result.toPS.getRowGroupCount(), "Invalid state count for subsystem"); - STORM_LOG_ASSERT(result.getNumberOfChoices() == result.choices.getNumberOfSetBits() && result.getNumberOfChoices() == result.toMS.getRowCount() && result.getNumberOfChoices() == result.toPS.getRowCount(), "Invalid state count for subsystem"); - - result.weightedRewardVector.resize(result.getNumberOfChoices()); - storm::utility::vector::selectVectorValues(result.weightedRewardVector, result.choices, weightedRewardVector); - result.objectiveRewardVectors.resize(this->data.objectives.size()); - for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) { - std::vector& objVector = result.objectiveRewardVectors[objIndex]; - objVector = std::vector(result.weightedRewardVector.size(), storm::utility::zero()); - if(this->objectivesWithNoUpperTimeBound.get(objIndex)) { - storm::utility::vector::selectVectorValues(objVector, result.choices, this->discreteActionRewards[objIndex]); - } else { - typename SparseMaModelType::RewardModelType const& rewModel = this->data.preprocessedModel.getRewardModel(this->data.objectives[objIndex].rewardModelName); - STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected."); - STORM_LOG_ASSERT(!rewModel.hasStateRewards(), "State rewards for bounded objectives for MAs are not expected (bounded rewards are not supported)."); - if(rewModel.hasStateActionRewards()) { - storm::utility::vector::selectVectorValues(objVector, result.choices, rewModel.getStateActionRewardVector()); - } - } - } - - result.weightedSolutionVector.resize(result.getNumberOfStates()); - storm::utility::vector::selectVectorValues(result.weightedSolutionVector, result.states, this->weightedResult); - result.objectiveSolutionVectors.resize(this->data.objectives.size()); - for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) { - result.objectiveSolutionVectors[objIndex].resize(result.weightedSolutionVector.size()); - storm::utility::vector::selectVectorValues(result.objectiveSolutionVectors[objIndex], result.states, this->objectiveResults[objIndex]); - } - - result.auxChoiceValues.resize(result.getNumberOfChoices()); - - return result; - } - - template - template ::SupportsExponential, int>::type> - VT SparseMaMultiObjectiveWeightVectorChecker::getDigitizationConstant() const { - STORM_LOG_DEBUG("Retrieving digitization constant"); - // We need to find a delta such that for each objective it holds that lowerbound/delta , upperbound/delta are natural numbers and - // If there is a lower and an upper bound: - // 1 - e^(-maxRate lowerbound) * (1 + maxRate delta) ^ (lowerbound / delta) + 1-e^(-maxRate upperbound) * (1 + maxRate delta) ^ (upperbound / delta) + (1-e^(-maxRate delta) <= maximumLowerUpperBoundGap - // If there is only an upper bound: - // 1-e^(-maxRate upperbound) * (1 + maxRate delta) ^ (upperbound / delta) <= maximumLowerUpperBoundGap - - // Initialize some data for fast and easy access - VT const maxRate = this->data.preprocessedModel.getMaximalExitRate(); - std::vector> eToPowerOfMinusMaxRateTimesBound; - VT smallestNonZeroBound = storm::utility::zero(); - for(auto const& obj : this->data.objectives) { - eToPowerOfMinusMaxRateTimesBound.emplace_back(); - if(obj.lowerTimeBound){ - STORM_LOG_ASSERT(!storm::utility::isZero(*obj.lowerTimeBound), "Got zero-valued lower bound."); // should have been handled in preprocessing - STORM_LOG_ASSERT(!obj.upperTimeBound || *obj.lowerTimeBound < *obj.upperTimeBound, "Got point intervall or empty intervall on time bounded property which is not supported"); // should also have been handled in preprocessing - eToPowerOfMinusMaxRateTimesBound.back().first = std::exp(-maxRate * (*obj.lowerTimeBound)); - smallestNonZeroBound = storm::utility::isZero(smallestNonZeroBound) ? *obj.lowerTimeBound : std::min(smallestNonZeroBound, *obj.lowerTimeBound); - } - if(obj.upperTimeBound){ - STORM_LOG_ASSERT(!storm::utility::isZero(*obj.upperTimeBound), "Got zero-valued upper bound."); // should have been handled in preprocessing - eToPowerOfMinusMaxRateTimesBound.back().second = std::exp(-maxRate * (*obj.upperTimeBound)); - smallestNonZeroBound = storm::utility::isZero(smallestNonZeroBound) ? *obj.upperTimeBound : std::min(smallestNonZeroBound, *obj.upperTimeBound); - } - } - if(storm::utility::isZero(smallestNonZeroBound)) { - // There are no time bounds. In this case, one is a valid digitization constant. - return storm::utility::one(); - } - - // We brute-force a delta, since a direct computation is apparently not easy. - // Also note that the number of times this loop runs is a lower bound for the number of minMaxSolver invocations. - // Hence, this brute-force approach will most likely not be a bottleneck. - uint_fast64_t smallestStepBound = 1; - VT delta = smallestNonZeroBound / smallestStepBound; - while(true) { - bool deltaValid = true; - for(auto const& obj : this->data.objectives) { - if((obj.lowerTimeBound && *obj.lowerTimeBound/delta != std::floor(*obj.lowerTimeBound/delta)) || - (obj.upperTimeBound && *obj.upperTimeBound/delta != std::floor(*obj.upperTimeBound/delta))) { - deltaValid = false; - break; - } - } - if(deltaValid) { - for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) { - auto const& obj = this->data.objectives[objIndex]; - VT precisionOfObj = storm::utility::zero(); - if(obj.lowerTimeBound) { - precisionOfObj += storm::utility::one() - (eToPowerOfMinusMaxRateTimesBound[objIndex].first * storm::utility::pow(storm::utility::one() + maxRate * delta, *obj.lowerTimeBound / delta) ) - + storm::utility::one() - std::exp(-maxRate * delta); - } - if(obj.upperTimeBound) { - precisionOfObj += storm::utility::one() - (eToPowerOfMinusMaxRateTimesBound[objIndex].second * storm::utility::pow(storm::utility::one() + maxRate * delta, *obj.upperTimeBound / delta) ); - } - if(precisionOfObj > this->maximumLowerUpperBoundGap) { - deltaValid = false; - break; - } - } - } - if(deltaValid) { - break; - } - ++smallestStepBound; - STORM_LOG_ASSERT(delta>smallestNonZeroBound / smallestStepBound, "Digitization constant is expected to become smaller in every iteration"); - delta = smallestNonZeroBound / smallestStepBound; - } - STORM_LOG_DEBUG("Found digitization constant: " << delta << ". At least " << smallestStepBound << " digitization steps will be necessarry"); - return delta; - } - - template - template ::SupportsExponential, int>::type> - VT SparseMaMultiObjectiveWeightVectorChecker::getDigitizationConstant() const { - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded probabilities of MAs is unsupported for this value type."); - } - - template - template ::SupportsExponential, int>::type> - void SparseMaMultiObjectiveWeightVectorChecker::digitize(SubModel& MS, VT const& digitizationConstant) const { - std::vector rateVector(MS.getNumberOfChoices()); - storm::utility::vector::selectVectorValues(rateVector, MS.states, this->data.preprocessedModel.getExitRates()); - for(uint_fast64_t row = 0; row < rateVector.size(); ++row) { - VT const eToMinusRateTimesDelta = std::exp(-rateVector[row] * digitizationConstant); - for(auto& entry : MS.toMS.getRow(row)) { - entry.setValue((storm::utility::one() - eToMinusRateTimesDelta) * entry.getValue()); - if(entry.getColumn() == row) { - entry.setValue(entry.getValue() + eToMinusRateTimesDelta); - } - } - for(auto& entry : MS.toPS.getRow(row)) { - entry.setValue((storm::utility::one() - eToMinusRateTimesDelta) * entry.getValue()); - } - MS.weightedRewardVector[row] *= storm::utility::one() - eToMinusRateTimesDelta; - for(auto& objVector : MS.objectiveRewardVectors) { - objVector[row] *= storm::utility::one() - eToMinusRateTimesDelta; - } - } - } - - template - template ::SupportsExponential, int>::type> - void SparseMaMultiObjectiveWeightVectorChecker::digitize(SubModel& subModel, VT const& digitizationConstant) const { - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded probabilities of MAs is unsupported for this value type."); - } - - template - template ::SupportsExponential, int>::type> - void SparseMaMultiObjectiveWeightVectorChecker::digitizeTimeBounds(TimeBoundMap& lowerTimeBounds, TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) { - - VT const maxRate = this->data.preprocessedModel.getMaximalExitRate(); - for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) { - auto const& obj = this->data.objectives[objIndex]; - VT errorTowardsZero; - VT errorAwayFromZero; - if(obj.lowerTimeBound) { - uint_fast64_t digitizedBound = storm::utility::convertNumber((*obj.lowerTimeBound)/digitizationConstant); - auto timeBoundIt = lowerTimeBounds.insert(std::make_pair(digitizedBound, storm::storage::BitVector(this->data.objectives.size(), false))).first; - timeBoundIt->second.set(objIndex); - VT digitizationError = storm::utility::one(); - digitizationError -= std::exp(-maxRate * (*obj.lowerTimeBound)) * storm::utility::pow(storm::utility::one() + maxRate * digitizationConstant, digitizedBound); - errorTowardsZero = -digitizationError; - errorAwayFromZero = storm::utility::one() - std::exp(-maxRate * digitizationConstant);; - } else { - errorTowardsZero = storm::utility::zero(); - errorAwayFromZero = storm::utility::zero(); - } - if(obj.upperTimeBound) { - uint_fast64_t digitizedBound = storm::utility::convertNumber((*obj.upperTimeBound)/digitizationConstant); - auto timeBoundIt = upperTimeBounds.insert(std::make_pair(digitizedBound, storm::storage::BitVector(this->data.objectives.size(), false))).first; - timeBoundIt->second.set(objIndex); - VT digitizationError = storm::utility::one(); - digitizationError -= std::exp(-maxRate * (*obj.upperTimeBound)) * storm::utility::pow(storm::utility::one() + maxRate * digitizationConstant, digitizedBound); - errorAwayFromZero += digitizationError; - } - STORM_LOG_ASSERT(errorTowardsZero + errorAwayFromZero <= this->maximumLowerUpperBoundGap, "Precision not sufficient."); - if (obj.rewardsArePositive) { - this->offsetsToLowerBound[objIndex] = -errorTowardsZero; - this->offsetsToUpperBound[objIndex] = errorAwayFromZero; - } else { - this->offsetsToLowerBound[objIndex] = -errorAwayFromZero; - this->offsetsToUpperBound[objIndex] = errorTowardsZero; - } - } - } - - template - template ::SupportsExponential, int>::type> - void SparseMaMultiObjectiveWeightVectorChecker::digitizeTimeBounds(TimeBoundMap& lowerTimeBounds, TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) { - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded probabilities of MAs is unsupported for this value type."); - } - - template - std::unique_ptr::MinMaxSolverData> SparseMaMultiObjectiveWeightVectorChecker::initMinMaxSolverData(SubModel const& PS) const { - std::unique_ptr result(new MinMaxSolverData()); - - result->b.resize(result->matrix.getRowCount()); - result->x.resize(result->matrix.getRowGroupCount()); - for(uint_fast64_t state=0; state < result->fromPSStateMapping.size(); ++state) { - if(result->fromPSStateMapping[state] < result->x.size()) { - result->x[result->fromPSStateMapping[state]] = PS.weightedSolutionVector[state]; - } - } - - storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxSolverFactory; - result->solver = minMaxSolverFactory.create(result->matrix); - result->solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); - result->solver->setTrackScheduler(true); - result->solver->allocateAuxMemory(storm::solver::MinMaxLinearEquationSolverOperation::SolveEquations); - - return result; - } - - template - void SparseMaMultiObjectiveWeightVectorChecker::updateDataToCurrentEpoch(SubModel& MS, SubModel& PS, MinMaxSolverData& minMax, storm::storage::BitVector& consideredObjectives, uint_fast64_t const& currentEpoch, std::vector const& weightVector, TimeBoundMap::iterator& lowerTimeBoundIt, TimeBoundMap const& lowerTimeBounds, TimeBoundMap::iterator& upperTimeBoundIt, TimeBoundMap const& upperTimeBounds) { - - //Note that lower time bounds are always strict. Hence, we need to react when the current epoch equals the stored bound. - if(lowerTimeBoundIt != lowerTimeBounds.end() && currentEpoch == lowerTimeBoundIt->first) { - for(auto objIndex : lowerTimeBoundIt->second) { - // No more reward is earned for this objective. - storm::utility::vector::addScaledVector(MS.weightedRewardVector, MS.objectiveRewardVectors[objIndex], -weightVector[objIndex]); - storm::utility::vector::addScaledVector(PS.weightedRewardVector, PS.objectiveRewardVectors[objIndex], -weightVector[objIndex]); - MS.objectiveRewardVectors[objIndex] = std::vector(MS.objectiveRewardVectors[objIndex].size(), storm::utility::zero()); - PS.objectiveRewardVectors[objIndex] = std::vector(PS.objectiveRewardVectors[objIndex].size(), storm::utility::zero()); - } - ++lowerTimeBoundIt; - } - - if(upperTimeBoundIt != upperTimeBounds.end() && currentEpoch == upperTimeBoundIt->first) { - consideredObjectives |= upperTimeBoundIt->second; - for(auto objIndex : upperTimeBoundIt->second) { - // This objective now plays a role in the weighted sum - storm::utility::vector::addScaledVector(MS.weightedRewardVector, MS.objectiveRewardVectors[objIndex], weightVector[objIndex]); - storm::utility::vector::addScaledVector(PS.weightedRewardVector, PS.objectiveRewardVectors[objIndex], weightVector[objIndex]); - } - ++upperTimeBoundIt; - } - - // Update the solver data - PS.toMS.multiplyWithVector(MS.weightedSolutionVector, PS.auxChoiceValues); - storm::utility::vector::addVectors(PS.auxChoiceValues, PS.weightedRewardVector, PS.auxChoiceValues); - storm::utility::vector::selectVectorValues(minMax.b, minMax.toPSChoiceMapping, PS.auxChoiceValues); - } - - template - void SparseMaMultiObjectiveWeightVectorChecker::performPSStep(SubModel& PS, SubModel const& MS, MinMaxSolverData& minMax, LinEqSolverData& linEq, std::vector& optimalChoicesAtCurrentEpoch, storm::storage::BitVector const& consideredObjectives) const { - // compute a choice vector for the probabilistic states that is optimal w.r.t. the weighted reward vector - std::vector newOptimalChoices(PS.getNumberOfStates()); - minMax.solver->solveEquations(minMax.x, minMax.b); - this->transformReducedSolutionToOriginalModel(minMax.matrix, minMax.x, minMax.solver->getScheduler()->getChoices(), minMax.toPSChoiceMapping, minMax.fromPSStateMapping, PS.toPS, PS.weightedSolutionVector, newOptimalChoices); - // check whether the linEqSolver needs to be updated, i.e., whether the scheduler has changed - if(linEq.solver == nullptr || newOptimalChoices != optimalChoicesAtCurrentEpoch) { - optimalChoicesAtCurrentEpoch.swap(newOptimalChoices); - linEq.solver = nullptr; - storm::storage::SparseMatrix linEqMatrix = PS.toPS.selectRowsFromRowGroups(optimalChoicesAtCurrentEpoch, true); - linEqMatrix.convertToEquationSystem(); - linEq.solver = linEq.factory.create(std::move(linEqMatrix)); - linEq.solver->allocateAuxMemory(storm::solver::LinearEquationSolverOperation::SolveEquations); - } - - // Get the results for the individual objectives. - // Note that we do not consider an estimate for each objective (as done in the unbounded phase) since the results from the previous epoch are already pretty close - for(auto objIndex : consideredObjectives) { - auto const& objectiveRewardVectorPS = PS.objectiveRewardVectors[objIndex]; - auto const& objectiveSolutionVectorMS = MS.objectiveSolutionVectors[objIndex]; - // compute rhs of equation system, i.e., PS.toMS * x + Rewards - // To safe some time, only do this for the obtained optimal choices - auto itGroupIndex = PS.toPS.getRowGroupIndices().begin(); - auto itChoiceOffset = optimalChoicesAtCurrentEpoch.begin(); - for(auto& bValue : linEq.b) { - uint_fast64_t row = (*itGroupIndex) + (*itChoiceOffset); - bValue = objectiveRewardVectorPS[row]; - for(auto const& entry : PS.toMS.getRow(row)){ - bValue += entry.getValue() * objectiveSolutionVectorMS[entry.getColumn()]; - } - ++itGroupIndex; - ++itChoiceOffset; - } - linEq.solver->solveEquations(PS.objectiveSolutionVectors[objIndex], linEq.b); - } - } - - template - void SparseMaMultiObjectiveWeightVectorChecker::performMSStep(SubModel& MS, SubModel const& PS, storm::storage::BitVector const& consideredObjectives) const { - - MS.toMS.multiplyWithVector(MS.weightedSolutionVector, MS.auxChoiceValues); - storm::utility::vector::addVectors(MS.weightedRewardVector, MS.auxChoiceValues, MS.weightedSolutionVector); - MS.toPS.multiplyWithVector(PS.weightedSolutionVector, MS.auxChoiceValues); - storm::utility::vector::addVectors(MS.weightedSolutionVector, MS.auxChoiceValues, MS.weightedSolutionVector); - - for(auto objIndex : consideredObjectives) { - MS.toMS.multiplyWithVector(MS.objectiveSolutionVectors[objIndex], MS.auxChoiceValues); - storm::utility::vector::addVectors(MS.objectiveRewardVectors[objIndex], MS.auxChoiceValues, MS.objectiveSolutionVectors[objIndex]); - MS.toPS.multiplyWithVector(PS.objectiveSolutionVectors[objIndex], MS.auxChoiceValues); - storm::utility::vector::addVectors(MS.objectiveSolutionVectors[objIndex], MS.auxChoiceValues, MS.objectiveSolutionVectors[objIndex]); - } - } - - - template class SparseMaMultiObjectiveWeightVectorChecker>; - template double SparseMaMultiObjectiveWeightVectorChecker>::getDigitizationConstant() const; - template void SparseMaMultiObjectiveWeightVectorChecker>::digitize(SparseMaMultiObjectiveWeightVectorChecker>::SubModel& subModel, double const& digitizationConstant) const; - template void SparseMaMultiObjectiveWeightVectorChecker>::digitizeTimeBounds(SparseMaMultiObjectiveWeightVectorChecker>::TimeBoundMap& lowerTimeBounds, SparseMaMultiObjectiveWeightVectorChecker>::TimeBoundMap& upperTimeBounds, double const& digitizationConstant); -#ifdef STORM_HAVE_CARL -// template class SparseMaMultiObjectiveWeightVectorChecker>; - // template storm::RationalNumber SparseMaMultiObjectiveWeightVectorChecker>::getDigitizationConstant() const; - // template void SparseMaMultiObjectiveWeightVectorChecker>::digitize(SparseMaMultiObjectiveWeightVectorChecker>::SubModel& subModel, storm::RationalNumber const& digitizationConstant) const; -// template void SparseMaMultiObjectiveWeightVectorChecker>::digitizeTimeBounds(SparseMaMultiObjectiveWeightVectorChecker>::TimeBoundMap& lowerTimeBounds, SparseMaMultiObjectiveWeightVectorChecker>::TimeBoundMap& upperTimeBounds, storm::RationalNumber const& digitizationConstant); -#endif - - } - } -} diff --git a/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.h b/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.h deleted file mode 100644 index 9710cde28..000000000 --- a/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.h +++ /dev/null @@ -1,157 +0,0 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMAMULTIOBJECTIVEWEIGHTVECTORCHECKER_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMAMULTIOBJECTIVEWEIGHTVECTORCHECKER_H_ - -#include -#include - -#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h" -#include "src/solver/LinearEquationSolver.h" -#include "src/solver/GmmxxLinearEquationSolver.h" -#include "src/solver/MinMaxLinearEquationSolver.h" -#include "src/utility/NumberTraits.h" - -namespace storm { - namespace modelchecker { - namespace helper { - - /*! - * Helper Class that takes preprocessed multi objective data and a weight vector and ... - * - computes the maximal expected reward w.r.t. the weighted sum of the rewards of the individual objectives - * - extracts the scheduler that induces this maximum - * - computes for each objective the value induced by this scheduler - */ - template - class SparseMaMultiObjectiveWeightVectorChecker : public SparseMultiObjectiveWeightVectorChecker { - public: - typedef typename SparseMaModelType::ValueType ValueType; - typedef SparseMultiObjectivePreprocessorData PreprocessorData; - - SparseMaMultiObjectiveWeightVectorChecker(PreprocessorData const& data); - - private: - - /* - * Stores (digitized) time bounds in descending order - */ - typedef std::map> TimeBoundMap; - - /* - * Stores the ingredients of a sub model - */ - struct SubModel { - storm::storage::BitVector states; // The states that are part of this sub model - storm::storage::BitVector choices; // The choices that are part of this sub model - - storm::storage::SparseMatrix toMS; // Transitions to Markovian states - storm::storage::SparseMatrix toPS; // Transitions to probabilistic states - - std::vector weightedRewardVector; - std::vector> objectiveRewardVectors; - - std::vector weightedSolutionVector; - std::vector> objectiveSolutionVectors; - - std::vector auxChoiceValues; //stores auxiliary values for every choice - - uint_fast64_t getNumberOfStates() const { return toMS.getRowGroupCount(); }; - uint_fast64_t getNumberOfChoices() const { return toMS.getRowCount(); }; - }; - - /* - * Stores the data that is relevant to invoke the minMaxSolver and retrieve the result. - */ - struct MinMaxSolverData { - std::unique_ptr> solver; // the solver itself - - storm::storage::SparseMatrix matrix; // the considered matrix - std::vector toPSChoiceMapping; // maps rows of the considered matrix to choices of the PS SubModel - std::vector fromPSStateMapping; // maps states of the PS SubModel to row groups of the considered matrix - - std::vector b; - std::vector x; - }; - - struct LinEqSolverData { - storm::solver::GmmxxLinearEquationSolverFactory factory; - std::unique_ptr> solver; - - std::vector b; - }; - - /*! - * - * @param weightVector the weight vector of the current check - * @param weightedRewardVector the weighted rewards considering the unbounded objectives. Will be invalidated after calling this. - */ - virtual void boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) override; - - /*! - * Retrieves the data for a submodel of the data->preprocessedModel - * @param createMS if true, the submodel containing the Markovian states is created. - * if false, the submodel containing the probabilistic states is created. - */ - SubModel createSubModel(bool createMS, std::vector const& weightedRewardVector) const; - - /*! - * Retrieves the delta used for digitization - */ - template ::SupportsExponential, int>::type = 0> - VT getDigitizationConstant() const; - template ::SupportsExponential, int>::type = 0> - VT getDigitizationConstant() const; - - /*! - * Digitizes the given matrix and vectors w.r.t. the given digitization constant and the given rate vector. - */ - template ::SupportsExponential, int>::type = 0> - void digitize(SubModel& subModel, VT const& digitizationConstant) const; - template ::SupportsExponential, int>::type = 0> - void digitize(SubModel& subModel, VT const& digitizationConstant) const; - - /* - * Fills the given maps with the digitized time bounds. Also sets the offsetsToLowerBound / offsetsToUpperBound values - * according to the digitization error - */ - template ::SupportsExponential, int>::type = 0> - void digitizeTimeBounds(TimeBoundMap& lowerTimeBounds, TimeBoundMap& upperTimeBounds, VT const& digitizationConstant); - template ::SupportsExponential, int>::type = 0> - void digitizeTimeBounds(TimeBoundMap& lowerTimeBounds, TimeBoundMap& upperTimeBounds, VT const& digitizationConstant); - - - /*! - * Computes a reduction of the PStoPS submodel which does not contain end components in which no choice with reward is taken. - * With the reduction, a MinMaxSolver is initialized. - */ - std::unique_ptr initMinMaxSolverData(SubModel const& PS) const; - - /* - * Updates the reward vectors within the split model, - * the reward vector of the reduced PStoPS model, and - * objectives that are considered at the current time epoch. - */ - void updateDataToCurrentEpoch(SubModel& MS, SubModel& PS, MinMaxSolverData& minMax, storm::storage::BitVector& consideredObjectives, uint_fast64_t const& currentEpoch, std::vector const& weightVector, TimeBoundMap::iterator& lowerTimeBoundIt, TimeBoundMap const& lowerTimeBounds, TimeBoundMap::iterator& upperTimeBoundIt, TimeBoundMap const& upperTimeBounds); - - /* - * Performs a step for the probabilistic states, that is - * * Compute an optimal scheduler for the weighted reward sum - * * Compute the values for the individual objectives w.r.t. that scheduler - * - * The resulting values represent the rewards at probabilistic states that are obtained at the current time epoch. - */ - void performPSStep(SubModel& PS, SubModel const& MS, MinMaxSolverData& minMax, LinEqSolverData& linEq, std::vector& optimalChoicesAtCurrentEpoch, storm::storage::BitVector const& consideredObjectives) const; - - /* - * Performs a step for the Markovian states, that is - * * Compute values for the weighted reward sum as well as for the individual objectives - * - * The resulting values represent the rewards at Markovian states that are obtained after one (digitized) time unit has passed. - */ - void performMSStep(SubModel& MS, SubModel const& PS, storm::storage::BitVector const& consideredObjectives) const; - - }; - - } - } -} - -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMAMULTIOBJECTIVEWEIGHTEDVECTORCHECKER_H_ */ diff --git a/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp deleted file mode 100644 index 229535235..000000000 --- a/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp +++ /dev/null @@ -1,117 +0,0 @@ -#include "src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.h" - -#include "src/adapters/CarlAdapter.h" -#include "src/models/sparse/Mdp.h" -#include "src/models/sparse/StandardRewardModel.h" -#include "src/utility/macros.h" -#include "src/utility/vector.h" - - -namespace storm { - namespace modelchecker { - namespace helper { - - template - SparseMdpMultiObjectiveWeightVectorChecker::SparseMdpMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : SparseMultiObjectiveWeightVectorChecker(data) { - // set the state action rewards - for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) { - typename SparseMdpModelType::RewardModelType const& rewModel = this->data.preprocessedModel.getRewardModel(this->data.objectives[objIndex].rewardModelName); - STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Reward model has transition rewards which is not expected."); - this->discreteActionRewards[objIndex] = rewModel.getTotalRewardVector(this->data.preprocessedModel.getTransitionMatrix()); - } - } - - template - void SparseMdpMultiObjectiveWeightVectorChecker::boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) { - // Allocate some memory so this does not need to happen for each time epoch - std::vector optimalChoicesInCurrentEpoch(this->data.preprocessedModel.getNumberOfStates()); - std::vector choiceValues(weightedRewardVector.size()); - std::vector temporaryResult(this->data.preprocessedModel.getNumberOfStates()); - std::vector zeroReward(weightedRewardVector.size(), storm::utility::zero()); - // Get for each occurring timeBound the indices of the objectives with that bound. - std::map> lowerTimeBounds; - std::map> upperTimeBounds; - for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) { - auto const& obj = this->data.objectives[objIndex]; - if(obj.lowerTimeBound) { - auto timeBoundIt = lowerTimeBounds.insert(std::make_pair(storm::utility::convertNumber(*obj.lowerTimeBound), storm::storage::BitVector(this->data.objectives.size(), false))).first; - STORM_LOG_WARN_COND(storm::utility::convertNumber(timeBoundIt->first) == (*obj.lowerTimeBound), "Rounded non-integral bound " << *obj.lowerTimeBound << " to " << timeBoundIt->first << "."); - timeBoundIt->second.set(objIndex); - } - if(obj.upperTimeBound) { - auto timeBoundIt = upperTimeBounds.insert(std::make_pair(storm::utility::convertNumber(*obj.upperTimeBound), storm::storage::BitVector(this->data.objectives.size(), false))).first; - STORM_LOG_WARN_COND(storm::utility::convertNumber(timeBoundIt->first) == (*obj.upperTimeBound), "Rounded non-integral bound " << *obj.upperTimeBound << " to " << timeBoundIt->first << "."); - timeBoundIt->second.set(objIndex); - - // There is no error for the values of these objectives. - this->offsetsToLowerBound[objIndex] = storm::utility::zero(); - this->offsetsToUpperBound[objIndex] = storm::utility::zero(); - } - } - - // Stores the objectives for which we need to compute values in the current time epoch. - storm::storage::BitVector consideredObjectives = this->objectivesWithNoUpperTimeBound; - - // Stores objectives for which the current epoch passed their lower bound - storm::storage::BitVector lowerBoundViolatedObjectives(consideredObjectives.size(), false); - - auto lowerTimeBoundIt = lowerTimeBounds.begin(); - auto upperTimeBoundIt = upperTimeBounds.begin(); - uint_fast64_t currentEpoch = std::max(lowerTimeBounds.empty() ? 0 : lowerTimeBoundIt->first - 1, upperTimeBounds.empty() ? 0 : upperTimeBoundIt->first); // consider lowerBound - 1 since we are interested in the first epoch that passes the bound - - while(currentEpoch > 0) { - //For lower time bounds we need to react when the currentEpoch passed the bound - // Hence, we substract 1 from the lower time bounds. - if(lowerTimeBoundIt != lowerTimeBounds.end() && currentEpoch == lowerTimeBoundIt->first - 1) { - lowerBoundViolatedObjectives |= lowerTimeBoundIt->second; - for(auto objIndex : lowerTimeBoundIt->second) { - // No more reward is earned for this objective. - storm::utility::vector::addScaledVector(weightedRewardVector, this->discreteActionRewards[objIndex], -weightVector[objIndex]); - } - ++lowerTimeBoundIt; - } - - if(upperTimeBoundIt != upperTimeBounds.end() && currentEpoch == upperTimeBoundIt->first) { - consideredObjectives |= upperTimeBoundIt->second; - for(auto objIndex : upperTimeBoundIt->second) { - // This objective now plays a role in the weighted sum - storm::utility::vector::addScaledVector(weightedRewardVector, this->discreteActionRewards[objIndex], weightVector[objIndex]); - } - ++upperTimeBoundIt; - } - - // Get values and scheduler for weighted sum of objectives - this->data.preprocessedModel.getTransitionMatrix().multiplyWithVector(this->weightedResult, choiceValues); - storm::utility::vector::addVectors(choiceValues, weightedRewardVector, choiceValues); - storm::utility::vector::reduceVectorMax(choiceValues, this->weightedResult, this->data.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), &optimalChoicesInCurrentEpoch); - - // get values for individual objectives - // TODO we could compute the result for one of the objectives from the weighted result, the given weight vector, and the remaining objective results. - for(auto objIndex : consideredObjectives) { - std::vector& objectiveResult = this->objectiveResults[objIndex]; - std::vector const& objectiveRewards = lowerBoundViolatedObjectives.get(objIndex) ? zeroReward : this->discreteActionRewards[objIndex]; - auto rowGroupIndexIt = this->data.preprocessedModel.getTransitionMatrix().getRowGroupIndices().begin(); - auto optimalChoiceIt = optimalChoicesInCurrentEpoch.begin(); - for(ValueType& stateValue : temporaryResult){ - uint_fast64_t row = (*rowGroupIndexIt) + (*optimalChoiceIt); - ++rowGroupIndexIt; - ++optimalChoiceIt; - stateValue = objectiveRewards[row]; - for(auto const& entry : this->data.preprocessedModel.getTransitionMatrix().getRow(row)) { - stateValue += entry.getValue() * objectiveResult[entry.getColumn()]; - } - } - objectiveResult.swap(temporaryResult); - } - --currentEpoch; - } - } - - template class SparseMdpMultiObjectiveWeightVectorChecker>; -#ifdef STORM_HAVE_CARL - template class SparseMdpMultiObjectiveWeightVectorChecker>; -#endif - - } - } -} diff --git a/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.h b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.h deleted file mode 100644 index f7b8f6747..000000000 --- a/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.h +++ /dev/null @@ -1,45 +0,0 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMDPMULTIOBJECTIVEWEIGHTVECTORCHECKER_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMDPMULTIOBJECTIVEWEIGHTVECTORCHECKER_H_ - -#include - -#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h" - -namespace storm { - namespace modelchecker { - namespace helper { - - /*! - * Helper Class that takes preprocessed multi objective data and a weight vector and ... - * - computes the maximal expected reward w.r.t. the weighted sum of the rewards of the individual objectives - * - extracts the scheduler that induces this maximum - * - computes for each objective the value induced by this scheduler - */ - template - class SparseMdpMultiObjectiveWeightVectorChecker : public SparseMultiObjectiveWeightVectorChecker { - public: - typedef typename SparseMdpModelType::ValueType ValueType; - typedef SparseMultiObjectivePreprocessorData PreprocessorData; - - SparseMdpMultiObjectiveWeightVectorChecker(PreprocessorData const& data); - - private: - - /*! - * For each time epoch (starting with the maximal stepBound occurring in the objectives), this method - * - determines the objectives that are relevant in the current time epoch - * - determines the maximizing scheduler for the weighted reward vector of these objectives - * - computes the values of these objectives w.r.t. this scheduler - * - * @param weightVector the weight vector of the current check - * @param weightedRewardVector the weighted rewards considering the unbounded objectives. Will be invalidated after calling this. - */ - virtual void boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) override; - - }; - - } - } -} - -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMDPMULTIOBJECTIVEWEIGHTEDVECTORCHECKER_H_ */ diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp deleted file mode 100644 index 7f4442306..000000000 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp +++ /dev/null @@ -1,353 +0,0 @@ -#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h" - -#include "src/adapters/CarlAdapter.h" -#include "src/models/sparse/Mdp.h" -#include "src/models/sparse/MarkovAutomaton.h" -#include "src/models/sparse/StandardRewardModel.h" -#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h" -#include "src/utility/constants.h" -#include "src/utility/vector.h" -#include "src/settings//SettingsManager.h" -#include "src/settings/modules/MultiObjectiveSettings.h" -#include "src/settings/modules/GeneralSettings.h" - -#include "src/exceptions/UnexpectedException.h" - -namespace storm { - namespace modelchecker { - namespace helper { - - - template - typename SparseMultiObjectiveHelper::ResultData SparseMultiObjectiveHelper::check(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker) { - ResultData resultData; - resultData.overApproximation() = storm::storage::geometry::Polytope::createUniversalPolytope(); - resultData.underApproximation() = storm::storage::geometry::Polytope::createEmptyPolytope(); - - // Set the maximum gap between lower and upper bound of the weightVectorChecker result. - // This is the maximal edge length of the box we have to consider around each computed point - // We pick the gap such that the maximal distance between two points within this box is less than the given precision divided by two. - SparseModelValueType gap = storm::utility::convertNumber(storm::settings::getModule().getPrecision()); - gap /= (storm::utility::one() + storm::utility::one()); - gap /= storm::utility::sqrt(static_cast(preprocessorData.objectives.size())); - weightVectorChecker->setMaximumLowerUpperBoundGap(gap); - - if(!checkIfPreprocessingWasConclusive(preprocessorData)) { - switch(preprocessorData.queryType) { - case PreprocessorData::QueryType::Achievability: - achievabilityQuery(preprocessorData, weightVectorChecker, resultData); - break; - case PreprocessorData::QueryType::Numerical: - numericalQuery(preprocessorData, weightVectorChecker, resultData); - break; - case PreprocessorData::QueryType::Pareto: - paretoQuery(preprocessorData, weightVectorChecker, resultData); - break; - default: - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unknown Query Type"); - } - } - return resultData; - } - - template - bool SparseMultiObjectiveHelper::checkIfPreprocessingWasConclusive(PreprocessorData const& preprocessorData) { - if(preprocessorData.objectives.empty()) { - return true; - } - for(auto const& preprocessorResult : preprocessorData.solutionsFromPreprocessing) { - if(preprocessorResult.first == PreprocessorData::PreprocessorObjectiveSolution::False || - preprocessorResult.first == PreprocessorData::PreprocessorObjectiveSolution::Undefined) { - return true; - } - } - return false; - } - - template - void SparseMultiObjectiveHelper::achievabilityQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData) { - // Get a point that represents the thresholds - Point thresholds; - thresholds.reserve(preprocessorData.objectives.size()); - storm::storage::BitVector strictThresholds(preprocessorData.objectives.size()); - for(uint_fast64_t objIndex = 0; objIndex < preprocessorData.objectives.size(); ++objIndex) { - thresholds.push_back(storm::utility::convertNumber(*preprocessorData.objectives[objIndex].threshold)); - strictThresholds.set(objIndex, preprocessorData.objectives[objIndex].thresholdIsStrict); - } - // repeatedly refine the over/ under approximation until the threshold point is either in the under approx. or not in the over approx. - storm::storage::BitVector individualObjectivesToBeChecked(preprocessorData.objectives.size(), true); - do { - WeightVector separatingVector = findSeparatingVector(thresholds, resultData.underApproximation(), individualObjectivesToBeChecked); - performRefinementStep(std::move(separatingVector), preprocessorData.produceSchedulers, weightVectorChecker, resultData); - if(!checkIfThresholdsAreSatisfied(resultData.overApproximation(), thresholds, strictThresholds)){ - resultData.setThresholdsAreAchievable(false); - } - if(checkIfThresholdsAreSatisfied(resultData.underApproximation(), thresholds, strictThresholds)){ - resultData.setThresholdsAreAchievable(true); - } - } while(!resultData.isThresholdsAreAchievableSet() && !maxStepsPerformed(resultData)); - } - - template - void SparseMultiObjectiveHelper::numericalQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData) { - STORM_LOG_ASSERT(preprocessorData.indexOfOptimizingObjective, "Detected numerical query but index of optimizing objective is not set."); - // initialize some data - uint_fast64_t optimizingObjIndex = *preprocessorData.indexOfOptimizingObjective; - Point thresholds; - thresholds.reserve(preprocessorData.objectives.size()); - storm::storage::BitVector strictThresholds(preprocessorData.objectives.size(), false); - std::vector> thresholdConstraints; - thresholdConstraints.reserve(preprocessorData.objectives.size()-1); - for(uint_fast64_t objIndex = 0; objIndex < preprocessorData.objectives.size(); ++objIndex) { - if(preprocessorData.objectives[objIndex].threshold) { - thresholds.push_back(storm::utility::convertNumber(*preprocessorData.objectives[objIndex].threshold)); - WeightVector normalVector(preprocessorData.objectives.size(), storm::utility::zero()); - normalVector[objIndex] = -storm::utility::one(); - thresholdConstraints.emplace_back(std::move(normalVector), -thresholds.back()); - strictThresholds.set(objIndex, preprocessorData.objectives[objIndex].thresholdIsStrict); - } else { - thresholds.push_back(storm::utility::zero()); - } - } - // Note: If we have a single objective (i.e., no objectives with thresholds), thresholdsAsPolytope gets no constraints - auto thresholdsAsPolytope = storm::storage::geometry::Polytope::create(thresholdConstraints); - WeightVector directionOfOptimizingObjective(preprocessorData.objectives.size(), storm::utility::zero()); - directionOfOptimizingObjective[optimizingObjIndex] = storm::utility::one(); - - // Try to find one valid solution - storm::storage::BitVector individualObjectivesToBeChecked(preprocessorData.objectives.size(), true); - individualObjectivesToBeChecked.set(optimizingObjIndex, false); - do { - WeightVector separatingVector = findSeparatingVector(thresholds, resultData.underApproximation(), individualObjectivesToBeChecked); - performRefinementStep(std::move(separatingVector), preprocessorData.produceSchedulers, weightVectorChecker, resultData); - //Pick the threshold for the optimizing objective low enough so valid solutions are not excluded - thresholds[optimizingObjIndex] = std::min(thresholds[optimizingObjIndex], resultData.refinementSteps().back().getLowerBoundPoint()[optimizingObjIndex]); - if(!checkIfThresholdsAreSatisfied(resultData.overApproximation(), thresholds, strictThresholds)){ - resultData.setThresholdsAreAchievable(false); - } - if(checkIfThresholdsAreSatisfied(resultData.underApproximation(), thresholds, strictThresholds)){ - resultData.setThresholdsAreAchievable(true); - } - } while(!resultData.isThresholdsAreAchievableSet() && !maxStepsPerformed(resultData)); - if(resultData.getThresholdsAreAchievable()) { - STORM_LOG_DEBUG("Found a solution that satisfies the objective thresholds."); - individualObjectivesToBeChecked.clear(); - // Improve the found solution. - // Note that we do not have to care whether a threshold is strict anymore, because the resulting optimum should be - // the supremum over all strategies. Hence, one could combine a scheduler inducing the optimum value (but possibly violating strict - // thresholds) and (with very low probability) a scheduler that satisfies all (possibly strict) thresholds. - while(true) { - std::pair optimizationRes = resultData.underApproximation()->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective); - STORM_LOG_THROW(optimizationRes.second, storm::exceptions::UnexpectedException, "The underapproximation is either unbounded or empty."); - thresholds[optimizingObjIndex] = optimizationRes.first[optimizingObjIndex]; - resultData.setNumericalResult(thresholds[optimizingObjIndex]); - STORM_LOG_DEBUG("Best solution found so far is " << resultData.template getNumericalResult() << "."); - //Compute an upper bound for the optimum and check for convergence - optimizationRes = resultData.overApproximation()->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective); - if(optimizationRes.second) { - resultData.setPrecisionOfResult(optimizationRes.first[optimizingObjIndex] - thresholds[optimizingObjIndex]); - STORM_LOG_DEBUG("Solution can be improved by at most " << resultData.template getPrecisionOfResult()); - } - if(targetPrecisionReached(resultData) || maxStepsPerformed(resultData)) { - resultData.setOptimumIsAchievable(checkIfThresholdsAreSatisfied(resultData.underApproximation(), thresholds, strictThresholds)); - break; - } - WeightVector separatingVector = findSeparatingVector(thresholds, resultData.underApproximation(), individualObjectivesToBeChecked); - performRefinementStep(std::move(separatingVector), preprocessorData.produceSchedulers, weightVectorChecker, resultData); - } - } - } - - template - void SparseMultiObjectiveHelper::paretoQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData) { - //First consider the objectives individually - for(uint_fast64_t objIndex = 0; objIndex()); - direction[objIndex] = storm::utility::one(); - performRefinementStep(std::move(direction), preprocessorData.produceSchedulers, weightVectorChecker, resultData); - } - - while(true) { - // Get the halfspace of the underApproximation with maximal distance to a vertex of the overApproximation - std::vector> underApproxHalfspaces = resultData.underApproximation()->getHalfspaces(); - std::vector overApproxVertices = resultData.overApproximation()->getVertices(); - uint_fast64_t farestHalfspaceIndex = underApproxHalfspaces.size(); - RationalNumberType farestDistance = storm::utility::zero(); - for(uint_fast64_t halfspaceIndex = 0; halfspaceIndex < underApproxHalfspaces.size(); ++halfspaceIndex) { - for(auto const& vertex : overApproxVertices) { - RationalNumberType distance = -underApproxHalfspaces[halfspaceIndex].euclideanDistance(vertex); - if(distance > farestDistance) { - farestHalfspaceIndex = halfspaceIndex; - farestDistance = distance; - } - } - } - resultData.setPrecisionOfResult(farestDistance); - STORM_LOG_DEBUG("Current precision of the approximation of the pareto curve is " << resultData.template getPrecisionOfResult()); - if(targetPrecisionReached(resultData) || maxStepsPerformed(resultData)) { - break; - } - WeightVector direction = underApproxHalfspaces[farestHalfspaceIndex].normalVector(); - performRefinementStep(std::move(direction), preprocessorData.produceSchedulers, weightVectorChecker, resultData); - } - } - - template - typename SparseMultiObjectiveHelper::WeightVector SparseMultiObjectiveHelper::findSeparatingVector(Point const& pointToBeSeparated, std::shared_ptr> const& underApproximation, storm::storage::BitVector& individualObjectivesToBeChecked) { - STORM_LOG_DEBUG("Searching a weight vector to seperate the point given by " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(pointToBeSeparated)) << "."); - - if(underApproximation->isEmpty()) { - // In this case, every weight vector is separating - uint_fast64_t objIndex = individualObjectivesToBeChecked.getNextSetIndex(0) % pointToBeSeparated.size(); - WeightVector result(pointToBeSeparated.size(), storm::utility::zero()); - result[objIndex] = storm::utility::one(); - individualObjectivesToBeChecked.set(objIndex, false); - return result; - } - - // Reaching this point means that the underApproximation contains halfspaces. The seperating vector has to be the normal vector of one of these halfspaces. - // We pick one with maximal distance to the given point. However, weight vectors that correspond to checking individual objectives take precedence. - std::vector> halfspaces = underApproximation->getHalfspaces(); - uint_fast64_t farestHalfspaceIndex = halfspaces.size(); - RationalNumberType farestDistance = -storm::utility::one(); - bool foundSeparatingSingleObjectiveVector = false; - for(uint_fast64_t halfspaceIndex = 0; halfspaceIndex < halfspaces.size(); ++halfspaceIndex) { - // Note that we are looking for a halfspace that does not contain the point. Thus, the returned distances are negated. - RationalNumberType distance = -halfspaces[halfspaceIndex].euclideanDistance(pointToBeSeparated); - if(distance >= storm::utility::zero()) { - storm::storage::BitVector nonZeroVectorEntries = ~storm::utility::vector::filterZero(halfspaces[halfspaceIndex].normalVector()); - bool isSingleObjectiveVector = nonZeroVectorEntries.getNumberOfSetBits() == 1 && individualObjectivesToBeChecked.get(nonZeroVectorEntries.getNextSetIndex(0)); - // Check if this halfspace is better than the current one - if((!foundSeparatingSingleObjectiveVector && isSingleObjectiveVector ) || (foundSeparatingSingleObjectiveVector==isSingleObjectiveVector && distance>farestDistance)) { - foundSeparatingSingleObjectiveVector = foundSeparatingSingleObjectiveVector || isSingleObjectiveVector; - farestHalfspaceIndex = halfspaceIndex; - farestDistance = distance; - } - } - } - if(foundSeparatingSingleObjectiveVector) { - storm::storage::BitVector nonZeroVectorEntries = ~storm::utility::vector::filterZero(halfspaces[farestHalfspaceIndex].normalVector()); - individualObjectivesToBeChecked.set(nonZeroVectorEntries.getNextSetIndex(0), false); - } - - STORM_LOG_THROW(farestHalfspaceIndex(halfspaces[farestHalfspaceIndex].normalVector())) << "."); - return halfspaces[farestHalfspaceIndex].normalVector(); - } - - template - void SparseMultiObjectiveHelper::performRefinementStep(WeightVector&& direction, bool saveScheduler, WeightVectorCheckerType weightVectorChecker, ResultData& result) { - // Normalize the direction vector so that the entries sum up to one - storm::utility::vector::scaleVectorInPlace(direction, storm::utility::one() / std::accumulate(direction.begin(), direction.end(), storm::utility::zero())); - // Check if we already did a refinement step with that direction vector. If this is the case, we increase the precision. - // We start with the most recent steps to consider the most recent result for this direction vector - boost::optional oldMaximumLowerUpperBoundGap; - for(auto stepIt = result.refinementSteps().rbegin(); stepIt != result.refinementSteps().rend(); ++stepIt) { - if(stepIt->getWeightVector() == direction) { - STORM_LOG_WARN("Performing multiple refinement steps with the same direction vector."); - oldMaximumLowerUpperBoundGap = weightVectorChecker->getMaximumLowerUpperBoundGap(); - std::vector lowerUpperDistances = stepIt->getUpperBoundPoint(); - storm::utility::vector::subtractVectors(lowerUpperDistances, stepIt->getLowerBoundPoint(), lowerUpperDistances); - // shorten the distance between lower and upper bound for the new result by multiplying the current distance with 0.5 - // TODO: try other values/strategies? - RationalNumberType distance = storm::utility::sqrt(storm::utility::vector::dotProduct(lowerUpperDistances, lowerUpperDistances)); - weightVectorChecker->setMaximumLowerUpperBoundGap(std::min(*oldMaximumLowerUpperBoundGap, storm::utility::convertNumber(distance) * storm::utility::convertNumber(0.5))); - break; - } - } - weightVectorChecker->check(storm::utility::vector::convertNumericVector(direction)); - if(oldMaximumLowerUpperBoundGap) { - // Reset the precision back to the previous values - weightVectorChecker->setMaximumLowerUpperBoundGap(*oldMaximumLowerUpperBoundGap); - } - STORM_LOG_DEBUG("weighted objectives checker result (lower bounds) is " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(weightVectorChecker->getLowerBoundsOfInitialStateResults()))); - - if(saveScheduler) { - result.refinementSteps().emplace_back(direction, - storm::utility::vector::convertNumericVector(weightVectorChecker->getLowerBoundsOfInitialStateResults()), - storm::utility::vector::convertNumericVector(weightVectorChecker->getUpperBoundsOfInitialStateResults()), - weightVectorChecker->getScheduler()); - } else { - result.refinementSteps().emplace_back(direction, - storm::utility::vector::convertNumericVector(weightVectorChecker->getLowerBoundsOfInitialStateResults()), - storm::utility::vector::convertNumericVector(weightVectorChecker->getUpperBoundsOfInitialStateResults())); - } - updateOverApproximation(result.refinementSteps(), result.overApproximation()); - updateUnderApproximation(result.refinementSteps(), result.underApproximation()); - } - - template - void SparseMultiObjectiveHelper::updateOverApproximation(std::vector const& refinementSteps, std::shared_ptr>& overApproximation) { - storm::storage::geometry::Halfspace h(refinementSteps.back().getWeightVector(), storm::utility::vector::dotProduct(refinementSteps.back().getWeightVector(), refinementSteps.back().getUpperBoundPoint())); - - // Due to numerical issues, it might be the case that the updated overapproximation does not contain the underapproximation, - // e.g., when the new point is strictly contained in the underapproximation. Check if this is the case. - RationalNumberType maximumOffset = h.offset(); - for(auto const& step : refinementSteps){ - maximumOffset = std::max(maximumOffset, storm::utility::vector::dotProduct(h.normalVector(), step.getLowerBoundPoint())); - } - if(maximumOffset > h.offset()){ - // We correct the issue by shifting the halfspace such that it contains the underapproximation - h.offset() = maximumOffset; - STORM_LOG_WARN("Numerical issues: The overapproximation would not contain the underapproximation. Hence, a halfspace is shifted by " << storm::utility::convertNumber(h.euclideanDistance(refinementSteps.back().getUpperBoundPoint())) << "."); - } - overApproximation = overApproximation->intersection(h); - STORM_LOG_DEBUG("Updated OverApproximation to " << overApproximation->toString(true)); - } - - template - void SparseMultiObjectiveHelper::updateUnderApproximation(std::vector const& refinementSteps, std::shared_ptr>& underApproximation) { - std::vector paretoPoints; - paretoPoints.reserve(refinementSteps.size()); - for(auto const& step : refinementSteps) { - paretoPoints.push_back(step.getLowerBoundPoint()); - } - underApproximation = storm::storage::geometry::Polytope::createDownwardClosure(paretoPoints); - STORM_LOG_DEBUG("Updated UnderApproximation to " << underApproximation->toString(true)); - } - - template - bool SparseMultiObjectiveHelper::checkIfThresholdsAreSatisfied(std::shared_ptr> const& polytope, Point const& thresholds, storm::storage::BitVector const& strictThresholds) { - std::vector> halfspaces = polytope->getHalfspaces(); - for(auto const& h : halfspaces) { - RationalNumberType distance = h.distance(thresholds); - if(distance < storm::utility::zero()) { - return false; - } - if(distance == storm::utility::zero()) { - // In this case, the thresholds point is on the boundary of the polytope. - // Check if this is problematic for the strict thresholds - for(auto strictThreshold : strictThresholds) { - if(h.normalVector()[strictThreshold] > storm::utility::zero()) { - return false; - } - } - } - } - return true; - } - - template - bool SparseMultiObjectiveHelper::targetPrecisionReached(ResultData& resultData) { - resultData.setTargetPrecisionReached(resultData.isPrecisionOfResultSet() && - resultData.getPrecisionOfResult() < storm::utility::convertNumber(storm::settings::getModule().getPrecision())); - return resultData.getTargetPrecisionReached(); - } - - template - bool SparseMultiObjectiveHelper::maxStepsPerformed(ResultData& resultData) { - resultData.setMaxStepsPerformed(storm::settings::getModule().isMaxStepsSet() && - resultData.refinementSteps().size() >= storm::settings::getModule().getMaxSteps()); - return resultData.getMaxStepsPerformed(); - } - -#ifdef STORM_HAVE_CARL - template class SparseMultiObjectiveHelper, storm::RationalNumber>; - template class SparseMultiObjectiveHelper, storm::RationalNumber>; - - template class SparseMultiObjectiveHelper, storm::RationalNumber>; - template class SparseMultiObjectiveHelper, storm::RationalNumber>; -#endif - } - } -} diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h deleted file mode 100644 index 0afb224b7..000000000 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h +++ /dev/null @@ -1,99 +0,0 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPER_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPER_H_ - -#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h" -#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h" -#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveRefinementStep.h" -#include "src/modelchecker/multiObjective/helper/SparseMultiObjectiveWeightVectorChecker.h" -#include "src/storage/geometry/Polytope.h" -#include "src/storage/TotalScheduler.h" - - -namespace storm { - namespace modelchecker { - namespace helper { - - template - class SparseMultiObjectiveHelper { - public: - typedef typename SparseModelType::ValueType SparseModelValueType; - - typedef SparseMultiObjectivePreprocessorData PreprocessorData; - typedef SparseMultiObjectiveResultData ResultData; - typedef SparseMultiObjectiveRefinementStep RefinementStep; - typedef std::shared_ptr> WeightVectorCheckerType; - - typedef std::vector Point; - typedef std::vector WeightVector; - - static ResultData check(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker); - - private: - - /* - * Checks whether the preprocessing was already conclusive, e.g., the result for one objective is undefined or false - * - * @return true iff preprocessing was conclusive - */ - static bool checkIfPreprocessingWasConclusive(PreprocessorData const& preprocessorData); - - static void achievabilityQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData); - static void numericalQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData); - static void paretoQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData); - - /* - * Returns a weight vector w that separates the under approximation from the given point p, i.e., - * For each x in the under approximation, it holds that w*x <= w*p - * - * @param pointToBeSeparated the point that is to be seperated - * @param underapproximation the current under approximation - * @param objectivesToBeCheckedIndividually stores for each objective whether it still makes sense to check for this objective individually (i.e., with weight vector given by w_{objIndex} = 1 ) - */ - static WeightVector findSeparatingVector(Point const& pointToBeSeparated, std::shared_ptr> const& underApproximation, storm::storage::BitVector& individualObjectivesToBeChecked); - - /* - * Refines the current result w.r.t. the given direction vector. - */ - static void performRefinementStep(WeightVector&& direction, bool saveScheduler, WeightVectorCheckerType weightVectorChecker, ResultData& resultData); - - /* - * Updates the overapproximation after a refinement step has been performed - * - * @param refinementSteps the steps performed so far. The last entry should be the newest step, whose information is not yet included in the approximation. - * @param overApproximation the current overApproximation that will be updated - */ - static void updateOverApproximation(std::vector const& refinementSteps, std::shared_ptr>& overApproximation); - - /* - * Updates the underapproximation after a refinement step has been performed - * - * @param refinementSteps the steps performed so far. The last entry should be the newest step, whose information is not yet included in the approximation. - * @param underApproximation the current underApproximation that will be updated - */ - static void updateUnderApproximation(std::vector const& refinementSteps, std::shared_ptr>& underApproximation); - - /* - * Returns true iff there is a point in the given polytope that satisfies the given thresholds. - * It is assumed that the given polytope contains the downward closure of its vertices. - */ - static bool checkIfThresholdsAreSatisfied(std::shared_ptr> const& polytope, Point const& thresholds, storm::storage::BitVector const& strictThresholds); - - /* - * Returns whether the desired precision (as given in the settings) is reached by the current result. - * If the given resultData does not specify a precisionOfResult, false is returned. - * Also sets the resultData.targetPrecisionReached flag accordingly. - */ - static bool targetPrecisionReached(ResultData& resultData); - - /* - * Returns whether a maximum number of refinement steps is given in the settings and this threshold has been reached. - * Also sets the resultData.maxStepsPerformed flag accordingly. - */ - static bool maxStepsPerformed(ResultData& resultData); - }; - - } - } -} - -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPER_H_ */ diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h deleted file mode 100644 index 8d37a6786..000000000 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h +++ /dev/null @@ -1,73 +0,0 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEOBJECTIVEINFORMATION_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEOBJECTIVEINFORMATION_H_ - -#include -#include - -#include "src/logic/Formulas.h" - -namespace storm { - namespace modelchecker { - namespace helper { - template - struct SparseMultiObjectiveObjectiveInformation { - // the original input formula - std::shared_ptr originalFormula; - - // the name of the considered reward model in the preprocessedModel - std::string rewardModelName; - - // true if all rewards for this objective are positive, false if all rewards are negative. - bool rewardsArePositive; - - // transformation from the values of the preprocessed model to the ones for the actual input model, i.e., - // x is achievable in the preprocessed model iff factor*x + offset is achievable in the original model - ValueType toOriginalValueTransformationFactor; - ValueType toOriginalValueTransformationOffset; - - // The probability/reward threshold for the preprocessed model (if originalFormula specifies one). - // This is always a lower bound. - boost::optional threshold; - // True iff the specified threshold is strict, i.e., > - bool thresholdIsStrict = false; - - // The time bound(s) for the formula (if given by the originalFormula) - boost::optional lowerTimeBound; - boost::optional upperTimeBound; - - // Stores whether reward finiteness has been checked for this objective. - bool rewardFinitenessChecked; - - void printToStream(std::ostream& out) const { - out << std::setw(30) << originalFormula->toString(); - out << " \t(toOrigVal:" << std::setw(3) << toOriginalValueTransformationFactor << "*x +" << std::setw(3) << toOriginalValueTransformationOffset << ", \t"; - out << "intern threshold:"; - if(threshold){ - out << (thresholdIsStrict ? " >" : ">="); - out << std::setw(5) << (*threshold) << ","; - } else { - out << " none,"; - } - out << " \t"; - out << "intern reward model: " << std::setw(10) << rewardModelName; - out << (rewardsArePositive ? " (positive)" : " (negative)") << ", \t"; - out << "time bounds:"; - if(lowerTimeBound) { - if(upperTimeBound) { - out << "[" << *lowerTimeBound << ", " << *upperTimeBound << "]"; - } else { - out << ">=" << std::setw(5) << *lowerTimeBound; - } - } else if (upperTimeBound) { - out << "<=" << std::setw(5) << *upperTimeBound; - } else { - out << " none"; - } - out << ")" << std::endl; - } - }; - } - } -} - -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEOBJECTIVEINFORMATION_H_ */ diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp deleted file mode 100644 index 5c3675fce..000000000 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp +++ /dev/null @@ -1,363 +0,0 @@ - #include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h" - -#include - -#include "src/adapters/CarlAdapter.h" -#include "src/models/sparse/Mdp.h" -#include "src/models/sparse/MarkovAutomaton.h" -#include "src/models/sparse/StandardRewardModel.h" -#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" -#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "src/modelchecker/results/ParetoCurveCheckResult.h" -#include "src/storage/geometry/Polytope.h" -#include "src/storage/geometry/Hyperrectangle.h" -#include "src/settings//SettingsManager.h" -#include "src/settings/modules/MultiObjectiveSettings.h" -#include "src/settings/modules/GeneralSettings.h" -#include "src/settings/modules/IOSettings.h" -#include "src/utility/export.h" -#include "src/utility/macros.h" -#include "src/utility/vector.h" - -#include "src/exceptions/UnexpectedException.h" - -namespace storm { - namespace modelchecker { - namespace helper { - - template - typename std::unique_ptr SparseMultiObjectivePostprocessor::postprocess(PreprocessorData const& preprocessorData, ResultData const& resultData, boost::optional const& preprocessorStopwatch, boost::optional const& helperStopwatch, boost::optional const& postprocessorStopwatch) { - STORM_LOG_WARN_COND(!resultData.getMaxStepsPerformed(), "Multi-objective model checking has been aborted since the maximum number of refinement steps has been performed. The results are most likely incorrect."); - - std::unique_ptr result(new ExplicitQualitativeCheckResult());; - - if(preprocessorData.originalFormula.hasQualitativeResult()) { - result = postprocessAchievabilityQuery(preprocessorData, resultData); - } else if(preprocessorData.originalFormula.hasNumericalResult()){ - result = postprocessNumericalQuery(preprocessorData, resultData); - } else if (preprocessorData.originalFormula.hasParetoCurveResult()) { - result = postprocessParetoQuery(preprocessorData, resultData); - } else { - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unknown Query Type"); - } - - STORM_LOG_INFO(getInfo(result, preprocessorData, resultData, preprocessorStopwatch, helperStopwatch, postprocessorStopwatch)); - - exportPlot(result, preprocessorData, resultData, preprocessorStopwatch, helperStopwatch, postprocessorStopwatch); - - return result; - } - - template - typename std::unique_ptr SparseMultiObjectivePostprocessor::postprocessAchievabilityQuery(PreprocessorData const& preprocessorData, ResultData const& resultData) { - STORM_LOG_ASSERT(preprocessorData.queryType == PreprocessorData::QueryType::Achievability, "Expected an achievability query."); - uint_fast64_t initState = preprocessorData.originalModel.getInitialStates().getNextSetIndex(0); - - //Incorporate the results from prerpocessing - for(uint_fast64_t subformulaIndex = 0; subformulaIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subformulaIndex) { - switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex].first) { - case PreprocessorData::PreprocessorObjectiveSolution::None: - // Nothing to be done - break; - case PreprocessorData::PreprocessorObjectiveSolution::False: - return std::unique_ptr(new ExplicitQualitativeCheckResult(initState, false)); - case PreprocessorData::PreprocessorObjectiveSolution::True: - // Nothing to be done - break; - case PreprocessorData::PreprocessorObjectiveSolution::Undefined: - STORM_LOG_ERROR("The result for the objective " << preprocessorData.originalFormula.getSubformula(subformulaIndex) << " is not defined."); - return std::unique_ptr(new ExplicitQualitativeCheckResult(initState, false)); - default: - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected type of solution obtained in preprocessing."); - } - } - - if(preprocessorData.objectives.empty()) { - return std::unique_ptr(new ExplicitQualitativeCheckResult(initState, true)); - } - - // This might be due to reaching the max. number of refinement steps (so no exception is thrown) - STORM_LOG_ERROR_COND(resultData.isThresholdsAreAchievableSet(), "Could not find out whether the thresholds are achievable."); - - return std::unique_ptr(new ExplicitQualitativeCheckResult(initState, resultData.isThresholdsAreAchievableSet() &&resultData.getThresholdsAreAchievable())); - } - - template - typename std::unique_ptr SparseMultiObjectivePostprocessor::postprocessNumericalQuery(PreprocessorData const& preprocessorData, ResultData const& resultData) { - - //The queryType might be achievability (when the numerical result was obtained in preprocessing) - STORM_LOG_ASSERT(preprocessorData.queryType == PreprocessorData::QueryType::Numerical || - preprocessorData.queryType == PreprocessorData::QueryType::Achievability, "Expected a numerical or an achievability query."); - uint_fast64_t initState = preprocessorData.originalModel.getInitialStates().getNextSetIndex(0); - - //Incorporate the results from prerpocessing - boost::optional preprocessorNumericalResult; - for(uint_fast64_t subformulaIndex = 0; subformulaIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subformulaIndex) { - switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex].first) { - case PreprocessorData::PreprocessorObjectiveSolution::None: - // Nothing to be done - break; - case PreprocessorData::PreprocessorObjectiveSolution::False: - return std::unique_ptr(new ExplicitQualitativeCheckResult(initState, false)); - case PreprocessorData::PreprocessorObjectiveSolution::True: - // Nothing to be done - break; - case PreprocessorData::PreprocessorObjectiveSolution::Numerical: - STORM_LOG_ASSERT(!preprocessorNumericalResult, "There are multiple numerical results obtained in preprocessing"); - preprocessorNumericalResult = preprocessorData.solutionsFromPreprocessing[subformulaIndex].second; - break; - case PreprocessorData::PreprocessorObjectiveSolution::Unbounded: - STORM_LOG_ASSERT(!preprocessorNumericalResult, "There are multiple numerical results obtained in preprocessing"); - preprocessorNumericalResult = storm::utility::infinity(); - break; - case PreprocessorData::PreprocessorObjectiveSolution::Undefined: - STORM_LOG_ERROR("The result for the objective " << preprocessorData.originalFormula.getSubformula(subformulaIndex) << " is not defined."); - return std::unique_ptr(new ExplicitQualitativeCheckResult(initState, false)); - default: - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected solution obtained in preprocessing."); - } - } - - // Check whether the given thresholds are achievable - if(preprocessorData.objectives.empty() || (resultData.isThresholdsAreAchievableSet() && resultData.getThresholdsAreAchievable())) { - // Get the numerical result - if(preprocessorNumericalResult) { - STORM_LOG_ASSERT(!resultData.isNumericalResultSet(), "Result was found in preprocessing but there is also one in the resultData"); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(initState, *preprocessorNumericalResult)); - } else { - STORM_LOG_ASSERT(resultData.isNumericalResultSet(), "Postprocessing for numerical query invoked, but no numerical result is given"); - STORM_LOG_ASSERT(preprocessorData.indexOfOptimizingObjective, "Postprocessing for numerical query invoked, but no index of optimizing objective is specified"); - ObjectiveInformation const& optimizingObjective = preprocessorData.objectives[*preprocessorData.indexOfOptimizingObjective]; - ValueType resultForOriginalModel = resultData.template getNumericalResult() * optimizingObjective.toOriginalValueTransformationFactor + optimizingObjective.toOriginalValueTransformationOffset; - STORM_LOG_WARN_COND(resultData.getTargetPrecisionReached(), "The target precision for numerical queries has not been reached."); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(initState, resultForOriginalModel)); - } - } else { - STORM_LOG_ERROR_COND(resultData.isThresholdsAreAchievableSet(), "Could not find out whether the thresholds are achievable."); // This might be due to reaching the max. number of refinement steps (so no exception is thrown) - - return std::unique_ptr(new ExplicitQualitativeCheckResult(initState, false)); - } - } - - template - typename std::unique_ptr SparseMultiObjectivePostprocessor::postprocessParetoQuery(PreprocessorData const& preprocessorData, ResultData const& resultData) { - uint_fast64_t initState = preprocessorData.originalModel.getInitialStates().getNextSetIndex(0); - - //Issue a warning for objectives that have been solved in preprocessing - for(uint_fast64_t subformulaIndex = 0; subformulaIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subformulaIndex) { - switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex].first) { - case PreprocessorData::PreprocessorObjectiveSolution::None: - // Nothing to be done - break; - case PreprocessorData::PreprocessorObjectiveSolution::False: - return std::unique_ptr(new ExplicitQualitativeCheckResult(initState, false)); - case PreprocessorData::PreprocessorObjectiveSolution::True: - // Nothing to be done - break; - case PreprocessorData::PreprocessorObjectiveSolution::Numerical: - STORM_LOG_WARN("The result of the objective " << preprocessorData.originalFormula.getSubformula(subformulaIndex) << " was obtained in preprocessing and will not be incorporated in the check result. Objective Result is zero."); - break; - case PreprocessorData::PreprocessorObjectiveSolution::Unbounded: - STORM_LOG_WARN("The result of the objective " << preprocessorData.originalFormula.getSubformula(subformulaIndex) << " was obtained in preprocessing and will not be incorporated in the check result. Objective Result is infinity."); - break; - case PreprocessorData::PreprocessorObjectiveSolution::Undefined: - STORM_LOG_ERROR("The result for the objective " << preprocessorData.originalFormula.getSubformula(subformulaIndex) << " is not defined."); - return std::unique_ptr(new ExplicitQualitativeCheckResult(initState, false)); - default: - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected solution obtained in preprocessing."); - } - } - - std::vector> paretoOptimalPoints; - paretoOptimalPoints.reserve(resultData.refinementSteps().size()); - for(auto const& step : resultData.refinementSteps()) { - paretoOptimalPoints.push_back(storm::utility::vector::convertNumericVector(transformToOriginalValues(step.getLowerBoundPoint(), preprocessorData))); - } - return std::unique_ptr(new ParetoCurveCheckResult( - initState, - std::move(paretoOptimalPoints), - transformToOriginalValues(resultData.underApproximation(), preprocessorData)->template convertNumberRepresentation(), - transformToOriginalValues(resultData.overApproximation(), preprocessorData)->template convertNumberRepresentation())); - } - - template - std::vector SparseMultiObjectivePostprocessor::transformToOriginalValues(std::vector const& vector, PreprocessorData const& preprocessorData) { - std::vector result; - result.reserve(vector.size()); - for(uint_fast64_t objIndex = 0; objIndex < preprocessorData.objectives.size(); ++objIndex) { - result.push_back(vector[objIndex] * storm::utility::convertNumber(preprocessorData.objectives[objIndex].toOriginalValueTransformationFactor) + storm::utility::convertNumber(preprocessorData.objectives[objIndex].toOriginalValueTransformationOffset)); - } - return result; - } - - template - std::shared_ptr> SparseMultiObjectivePostprocessor::transformToOriginalValues(std::shared_ptr> const& polytope, PreprocessorData const& preprocessorData) { - if(polytope->isEmpty()) { - return storm::storage::geometry::Polytope::createEmptyPolytope(); - } - if(polytope->isUniversal()) { - return storm::storage::geometry::Polytope::createUniversalPolytope(); - } - uint_fast64_t numObjectives = preprocessorData.objectives.size(); - std::vector> transformationMatrix(numObjectives, std::vector(numObjectives, storm::utility::zero())); - std::vector transformationVector; - transformationVector.reserve(numObjectives); - for(uint_fast64_t objIndex = 0; objIndex < numObjectives; ++objIndex) { - transformationMatrix[objIndex][objIndex] = storm::utility::convertNumber(preprocessorData.objectives[objIndex].toOriginalValueTransformationFactor); - transformationVector.push_back(storm::utility::convertNumber(preprocessorData.objectives[objIndex].toOriginalValueTransformationOffset)); - } - return polytope->affineTransformation(transformationMatrix, transformationVector); - } - - - template - void SparseMultiObjectivePostprocessor::exportPlot(std::unique_ptr const& checkResult, PreprocessorData const& preprocessorData, ResultData const& resultData, boost::optional const& preprocessorStopwatch, boost::optional const& helperStopwatch, boost::optional const& postprocessorStopwatch) { - - if(!settings::getModule().isExportPlotSet()) { - return; - } - STORM_LOG_ERROR_COND(preprocessorData.objectives.size()==2, "Exporting plot requested but this is only implemented for the two-dimensional case."); - - auto transformedUnderApprox = transformToOriginalValues(resultData.underApproximation(), preprocessorData); - auto transformedOverApprox = transformToOriginalValues(resultData.overApproximation(), preprocessorData); - - // Get pareto points as well as a hyperrectangle that is used to guarantee that the resulting polytopes are bounded. - storm::storage::geometry::Hyperrectangle boundaries(std::vector(preprocessorData.objectives.size(), storm::utility::zero()), std::vector(preprocessorData.objectives.size(), storm::utility::zero())); - std::vector> paretoPoints; - paretoPoints.reserve(resultData.refinementSteps().size()); - for(auto const& step : resultData.refinementSteps()) { - paretoPoints.push_back(transformToOriginalValues(step.getLowerBoundPoint(), preprocessorData)); - boundaries.enlarge(paretoPoints.back()); - } - auto underApproxVertices = transformedUnderApprox->getVertices(); - for(auto const& v : underApproxVertices) { - boundaries.enlarge(v); - } - auto overApproxVertices = transformedOverApprox->getVertices(); - for(auto const& v : overApproxVertices) { - boundaries.enlarge(v); - } - - //Further enlarge the boundaries a little - storm::utility::vector::scaleVectorInPlace(boundaries.lowerBounds(), RationalNumberType(11) / RationalNumberType(10)); - storm::utility::vector::scaleVectorInPlace(boundaries.upperBounds(), RationalNumberType(11) / RationalNumberType(10)); - - auto boundariesAsPolytope = boundaries.asPolytope(); - std::vector columnHeaders = {"x", "y"}; - - std::vector> pointsForPlotting; - underApproxVertices = transformedUnderApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder(); - pointsForPlotting.reserve(underApproxVertices.size()); - for(auto const& v : underApproxVertices) { - pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); - } - storm::utility::exportDataToCSVFile(storm::settings::getModule().getExportPlotDirectory() + "underapproximation.csv", pointsForPlotting, columnHeaders); - - pointsForPlotting.clear(); - overApproxVertices = transformedOverApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder(); - pointsForPlotting.reserve(overApproxVertices.size()); - for(auto const& v : overApproxVertices) { - pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); - } - storm::utility::exportDataToCSVFile(storm::settings::getModule().getExportPlotDirectory() + "overapproximation.csv", pointsForPlotting, columnHeaders); - - pointsForPlotting.clear(); - pointsForPlotting.reserve(paretoPoints.size()); - for(auto const& v : paretoPoints) { - pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); - } - storm::utility::exportDataToCSVFile(storm::settings::getModule().getExportPlotDirectory() + "paretopoints.csv", pointsForPlotting, columnHeaders); - - pointsForPlotting.clear(); - auto boundVertices = boundariesAsPolytope->getVerticesInClockwiseOrder(); - pointsForPlotting.reserve(4); - for(auto const& v : boundVertices) { - pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); - } - storm::utility::exportDataToCSVFile(storm::settings::getModule().getExportPlotDirectory() + "boundaries.csv", pointsForPlotting, columnHeaders); - } - - template - std::string SparseMultiObjectivePostprocessor::getInfo(std::unique_ptr const& checkResult, PreprocessorData const& preprocessorData, ResultData const& resultData, boost::optional const& preprocessorStopwatch, boost::optional const& helperStopwatch, boost::optional const& postprocessorStopwatch) { - - std::stringstream statistics; - statistics << preprocessorData; - statistics << std::endl; - statistics << std::endl; - statistics << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; - statistics << " Multi-objective Model Checking Result " << std::endl; - statistics << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; - statistics << std::endl; - statistics << *checkResult; - statistics << std::endl; - statistics << std::endl; - statistics << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; - statistics << " Multi-objective Model Checking Statistics " << std::endl; - statistics << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; - statistics << std::endl; - statistics << "Recorded Runtimes (in seconds):" << std::endl; - storm::utility::Stopwatch combinedTime; - combinedTime.pause(); - if(preprocessorStopwatch) { - statistics << "\t Preprocessing: " << std::setw(8) << *preprocessorStopwatch << std::endl; - combinedTime.addToAccumulatedSeconds(preprocessorStopwatch->getAccumulatedSeconds()); - } - if(helperStopwatch) { - statistics << "\t Iterations: " << std::setw(8) << *helperStopwatch << std::endl; - combinedTime.addToAccumulatedSeconds(helperStopwatch->getAccumulatedSeconds()); - } - if(postprocessorStopwatch) { - statistics << "\t Postprocessing: " << std::setw(8) << *postprocessorStopwatch << std::endl; - combinedTime.addToAccumulatedSeconds(postprocessorStopwatch->getAccumulatedSeconds()); - } - statistics << "\t Combined: " << std::setw(8) << combinedTime << std::endl; - statistics << std::endl; - statistics << "Performed Refinement Steps: " << resultData.refinementSteps().size() << (resultData.getMaxStepsPerformed() ? " (computation aborted) " : "" ) << std::endl; - statistics << "Precision (Approximation): " << "Goal precision: " << settings::getModule().getPrecision(); - if(resultData.isPrecisionOfResultSet()) { - statistics << " Achieved precision: " << storm::utility::convertNumber(resultData.getPrecisionOfResult()) << ( resultData.getTargetPrecisionReached() ? "" : " (goal not achieved)"); - } - statistics << std::endl; - statistics << "Convergence precision for iterative solvers: " << settings::getModule().getPrecision() << std::endl; - statistics << std::endl; - statistics << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; - statistics << " Data in CSV format " << std::endl; - statistics << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; - statistics << "model_Header;Constants;States;Choices;Transitions;Properties;" << std::endl; - statistics << "model_data;" - << storm::settings::modules::IOSettings().getConstantDefinitionString() << ";" - << preprocessorData.originalModel.getNumberOfStates() << ";" - << preprocessorData.originalModel.getNumberOfChoices() << ";" - << preprocessorData.originalModel.getNumberOfTransitions() << ";" - << preprocessorData.originalFormula << ";" - << std::endl; - statistics << "result_Header;Iterations;Time Combined;Accuracy;Time Iterations;" << std::endl; - statistics << "result_data;" - << resultData.refinementSteps().size() << ";" - << combinedTime << ";"; - if(resultData.isPrecisionOfResultSet()) { - statistics << storm::utility::convertNumber(resultData.getPrecisionOfResult()) << ";"; - } else { - statistics << ";"; - } - if(helperStopwatch) { - statistics << *helperStopwatch << ";"; - } else { - statistics << ";"; - } - statistics << std::endl; - return statistics.str(); - } - - -#ifdef STORM_HAVE_CARL - template class SparseMultiObjectivePostprocessor, storm::RationalNumber>; - template class SparseMultiObjectivePostprocessor, storm::RationalNumber>; - - template class SparseMultiObjectivePostprocessor, storm::RationalNumber>; - template class SparseMultiObjectivePostprocessor, storm::RationalNumber>; -#endif - - } - } -} diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h deleted file mode 100644 index 8ca4274f0..000000000 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h +++ /dev/null @@ -1,55 +0,0 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPOSTPROCESSOR_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPOSTPROCESSOR_H_ - - -#include -#include - -#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h" -#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h" -#include "src/modelchecker/results/CheckResult.h" -#include "src/utility/Stopwatch.h" - -namespace storm { - namespace modelchecker { - namespace helper { - - /* - * Helper Class to invoke the necessary preprocessing for multi objective model checking - */ - template - class SparseMultiObjectivePostprocessor { - public: - typedef typename SparseModelType::ValueType ValueType; - typedef typename SparseModelType::RewardModelType RewardModelType; - - typedef SparseMultiObjectiveObjectiveInformation ObjectiveInformation; - typedef SparseMultiObjectivePreprocessorData PreprocessorData; - typedef SparseMultiObjectiveResultData ResultData; - - /*! - * Postprocesses the multi objective model checking result. - * - * @param preprocessorData the data of the preprocessing - * @param resultData the data of the model checking - */ - static std::unique_ptr postprocess(PreprocessorData const& preprocessorData, ResultData const& resultData, boost::optional const& preprocessorStopwatch = boost::none, boost::optional const& helperStopwatch = boost::none, boost::optional const& postprocessorStopwatch = boost::none); - - private: - static std::unique_ptr postprocessAchievabilityQuery(PreprocessorData const& preprocessorData, ResultData const& resultData); - static std::unique_ptr postprocessNumericalQuery(PreprocessorData const& preprocessorData, ResultData const& resultData); - static std::unique_ptr postprocessParetoQuery(PreprocessorData const& preprocessorData, ResultData const& resultData); - - static std::vector transformToOriginalValues(std::vector const& vector, PreprocessorData const& preprocessorData); - static std::shared_ptr> transformToOriginalValues(std::shared_ptr> const& polytope, PreprocessorData const& preprocessorData); - - static void exportPlot(std::unique_ptr const& checkResult, PreprocessorData const& preprocessorData, ResultData const& resultData, boost::optional const& preprocessorStopwatch, boost::optional const& helperStopwatch, boost::optional const& postprocessorStopwatch); - - static std::string getInfo(std::unique_ptr const& checkResult, PreprocessorData const& preprocessorData, ResultData const& resultData, boost::optional const& preprocessorStopwatch, boost::optional const& helperStopwatch, boost::optional const& postprocessorStopwatch); - }; - - } - } -} - -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPOSTPROCESSOR_H_ */ diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp deleted file mode 100644 index 6279079ec..000000000 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp +++ /dev/null @@ -1,546 +0,0 @@ - #include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h" - -#include "src/models/sparse/Mdp.h" -#include "src/models/sparse/MarkovAutomaton.h" -#include "src/models/sparse/StandardRewardModel.h" -#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" -#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" -#include "src/storage/MaximalEndComponentDecomposition.h" -#include "src/transformer/StateDuplicator.h" -#include "src/transformer/SubsystemBuilder.h" -#include "src/utility/macros.h" -#include "src/utility/vector.h" -#include "src/utility/graph.h" -#include "src/utility/Stopwatch.h" - -#include "src/exceptions/InvalidPropertyException.h" -#include "src/exceptions/UnexpectedException.h" - -namespace storm { - namespace modelchecker { - namespace helper { - - template - typename SparseMultiObjectivePreprocessor::PreprocessorData SparseMultiObjectivePreprocessor::preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel) { - - PreprocessorData data(originalFormula, originalModel, SparseModelType(originalModel), storm::utility::vector::buildVectorForRange(0, originalModel.getNumberOfStates())); - - //Invoke preprocessing on the individual objectives - for(auto const& subFormula : originalFormula.getSubformulas()){ - STORM_LOG_DEBUG("Preprocessing objective " << *subFormula<< "."); - data.objectives.emplace_back(); - ObjectiveInformation& currentObjective = data.objectives.back(); - currentObjective.originalFormula = subFormula; - if(currentObjective.originalFormula->isOperatorFormula()) { - preprocessFormula(currentObjective.originalFormula->asOperatorFormula(), data, currentObjective); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the subformula " << *subFormula << " of " << originalFormula << " because it is not supported"); - } - } - - //We can now remove all original reward models to save some memory - std::set origRewardModels = originalFormula.getReferencedRewardModels(); - for (auto const& rewModel : origRewardModels){ - data.preprocessedModel.removeRewardModel(rewModel); - } - - ensureRewardFiniteness(data); - handleObjectivesWithSolutionFromPreprocessing(data); - - // Set the query type. In case of a numerical query, also set the index of the objective to be optimized. - // Note: If there are only zero (or one) objectives left, we should not consider a pareto query! - storm::storage::BitVector objectivesWithoutThreshold(data.objectives.size()); - for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) { - objectivesWithoutThreshold.set(objIndex, !data.objectives[objIndex].threshold); - } - uint_fast64_t numOfObjectivesWithoutThreshold = objectivesWithoutThreshold.getNumberOfSetBits(); - if(numOfObjectivesWithoutThreshold == 0) { - data.queryType = PreprocessorData::QueryType::Achievability; - } else if (numOfObjectivesWithoutThreshold == 1) { - data.queryType = PreprocessorData::QueryType::Numerical; - data.indexOfOptimizingObjective = objectivesWithoutThreshold.getNextSetIndex(0); - } else if (numOfObjectivesWithoutThreshold == data.objectives.size()) { - data.queryType = PreprocessorData::QueryType::Pareto; - } else { - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The number of objectives without threshold is not valid. It should be either 0 (achievabilityQuery), 1 (numericalQuery), or " << data.objectives.size() << " (paretoQuery). Got " << numOfObjectivesWithoutThreshold << " instead."); - } - return data; - } - - template - void SparseMultiObjectivePreprocessor::updatePreprocessedModel(PreprocessorData& data, SparseModelType& newPreprocessedModel, std::vector& newToOldStateIndexMapping) { - data.preprocessedModel = std::move(newPreprocessedModel); - // the given newToOldStateIndexMapping reffers to the indices of the former preprocessedModel as 'old indices' - for(auto & preprocessedModelStateIndex : newToOldStateIndexMapping){ - preprocessedModelStateIndex = data.newToOldStateIndexMapping[preprocessedModelStateIndex]; - } - data.newToOldStateIndexMapping = std::move(newToOldStateIndexMapping); - } - - template - void SparseMultiObjectivePreprocessor::preprocessFormula(storm::logic::OperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) { - - // Get a unique name for the new reward model. - currentObjective.rewardModelName = "objective" + std::to_string(data.objectives.size()); - while(data.preprocessedModel.hasRewardModel(currentObjective.rewardModelName)){ - currentObjective.rewardModelName = "_" + currentObjective.rewardModelName; - } - - currentObjective.toOriginalValueTransformationFactor = storm::utility::one(); - currentObjective.toOriginalValueTransformationOffset = storm::utility::zero(); - currentObjective.rewardsArePositive = true; - - bool formulaMinimizes = false; - if(formula.hasBound()) { - currentObjective.threshold = storm::utility::convertNumber(formula.getBound().threshold); - currentObjective.thresholdIsStrict = storm::logic::isStrict(formula.getBound().comparisonType); - //Note that we minimize for upper bounds since we are looking for the EXISTENCE of a satisfying scheduler - formulaMinimizes = !storm::logic::isLowerBound(formula.getBound().comparisonType); - } else if (formula.hasOptimalityType()){ - formulaMinimizes = storm::solver::minimize(formula.getOptimalityType()); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Current objective " << formula << " does not specify whether to minimize or maximize"); - } - if(formulaMinimizes) { - // We negate all the values so we can consider the maximum for this objective - // Thus, all objectives will be maximized. - currentObjective.rewardsArePositive = false; - currentObjective.toOriginalValueTransformationFactor = -storm::utility::one(); - } - - if(formula.isProbabilityOperatorFormula()){ - preprocessFormula(formula.asProbabilityOperatorFormula(), data, currentObjective); - } else if(formula.isRewardOperatorFormula()){ - preprocessFormula(formula.asRewardOperatorFormula(), data, currentObjective); - } else if(formula.isTimeOperatorFormula()){ - preprocessFormula(formula.asTimeOperatorFormula(), data, currentObjective); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the objective " << formula << " because it is not supported"); - } - - if(currentObjective.threshold) { - currentObjective.threshold = (currentObjective.threshold.get() - currentObjective.toOriginalValueTransformationOffset) / currentObjective.toOriginalValueTransformationFactor; - } - } - - template - void SparseMultiObjectivePreprocessor::preprocessFormula(storm::logic::ProbabilityOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) { - currentObjective.rewardFinitenessChecked = true; - bool isProb0Formula = false; - bool isProb1Formula = false; - if(currentObjective.threshold && !currentObjective.thresholdIsStrict) { - isProb0Formula = !currentObjective.rewardsArePositive && storm::utility::isZero(*currentObjective.threshold); - isProb1Formula = currentObjective.rewardsArePositive && storm::utility::isOne(*currentObjective.threshold); - } - - if(formula.getSubformula().isUntilFormula()){ - preprocessFormula(formula.getSubformula().asUntilFormula(), data, currentObjective, isProb0Formula, isProb1Formula); - } else if(formula.getSubformula().isBoundedUntilFormula()){ - preprocessFormula(formula.getSubformula().asBoundedUntilFormula(), data, currentObjective); - } else if(formula.getSubformula().isGloballyFormula()){ - preprocessFormula(formula.getSubformula().asGloballyFormula(), data, currentObjective, isProb0Formula, isProb1Formula); - } else if(formula.getSubformula().isEventuallyFormula()){ - preprocessFormula(formula.getSubformula().asEventuallyFormula(), data, currentObjective, isProb0Formula, isProb1Formula); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); - } - } - - template - void SparseMultiObjectivePreprocessor::preprocessFormula(storm::logic::RewardOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) { - // Check if the reward model is uniquely specified - STORM_LOG_THROW((formula.hasRewardModelName() && data.preprocessedModel.hasRewardModel(formula.getRewardModelName())) - || data.preprocessedModel.hasUniqueRewardModel(), storm::exceptions::InvalidPropertyException, "The reward model is not unique and the formula " << formula << " does not specify a reward model."); - - // reward finiteness has to be checked later iff infinite reward is possible for the subformula - currentObjective.rewardFinitenessChecked = formula.getSubformula().isCumulativeRewardFormula() || (formula.getSubformula().isEventuallyFormula() && !currentObjective.rewardsArePositive); - - if(formula.getSubformula().isEventuallyFormula()){ - preprocessFormula(formula.getSubformula().asEventuallyFormula(), data, currentObjective, false, false, formula.getOptionalRewardModelName()); - } else if(formula.getSubformula().isCumulativeRewardFormula()) { - preprocessFormula(formula.getSubformula().asCumulativeRewardFormula(), data, currentObjective, formula.getOptionalRewardModelName()); - } else if(formula.getSubformula().isTotalRewardFormula()) { - preprocessFormula(formula.getSubformula().asTotalRewardFormula(), data, currentObjective, formula.getOptionalRewardModelName()); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); - } - } - - template - void SparseMultiObjectivePreprocessor::preprocessFormula(storm::logic::TimeOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) { - // Time formulas are only supported for Markov automata - STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Time operator formulas are only supported for Markov automata."); - - // reward finiteness does not need to be checked if we want to minimize time - currentObjective.rewardFinitenessChecked = !currentObjective.rewardsArePositive; - - if(formula.getSubformula().isEventuallyFormula()){ - preprocessFormula(formula.getSubformula().asEventuallyFormula(), data, currentObjective, false, false); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); - } - } - - template - void SparseMultiObjectivePreprocessor::preprocessFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, bool isProb0Formula, bool isProb1Formula) { - CheckTask phiTask(formula.getLeftSubformula()); - CheckTask psiTask(formula.getRightSubformula()); - storm::modelchecker::SparsePropositionalModelChecker mc(data.preprocessedModel); - STORM_LOG_THROW(mc.canHandle(phiTask) && mc.canHandle(psiTask), storm::exceptions::InvalidPropertyException, "The subformulas of " << formula << " should be propositional."); - storm::storage::BitVector phiStates = mc.check(phiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector(); - storm::storage::BitVector psiStates = mc.check(psiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector(); - - if(!(psiStates & data.preprocessedModel.getInitialStates()).empty() && !currentObjective.lowerTimeBound) { - // The probability is always one - data.solutionsFromPreprocessing[data.objectives.size()-1].first = PreprocessorData::PreprocessorObjectiveSolution::Numerical; - data.solutionsFromPreprocessing[data.objectives.size()-1].second = currentObjective.rewardsArePositive ? storm::utility::one() : -storm::utility::one(); - return; - } - - auto duplicatorResult = storm::transformer::StateDuplicator::transform(data.preprocessedModel, ~phiStates | psiStates); - updatePreprocessedModel(data, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping); - - storm::storage::BitVector newPsiStates(data.preprocessedModel.getNumberOfStates(), false); - for(auto const& oldPsiState : psiStates){ - //note that psiStates are always located in the second copy - newPsiStates.set(duplicatorResult.secondCopyOldToNewStateIndexMapping[oldPsiState], true); - } - - if(isProb0Formula || isProb1Formula) { - storm::storage::BitVector subsystemStates; - storm::storage::BitVector noIncomingTransitionFromFirstCopyStates; - if(isProb0Formula) { - storm::storage::BitVector statesReachableInSecondCopy = storm::utility::graph::getReachableStates(data.preprocessedModel.getTransitionMatrix(), duplicatorResult.gateStates & (~newPsiStates), duplicatorResult.secondCopy, storm::storage::BitVector(data.preprocessedModel.getNumberOfStates(), false)); - subsystemStates = statesReachableInSecondCopy | (duplicatorResult.firstCopy & storm::utility::graph::performProb0E(data.preprocessedModel, data.preprocessedModel.getBackwardTransitions(), duplicatorResult.firstCopy, newPsiStates)); - noIncomingTransitionFromFirstCopyStates = newPsiStates; - } else { - storm::storage::BitVector statesReachableInSecondCopy = storm::utility::graph::getReachableStates(data.preprocessedModel.getTransitionMatrix(), newPsiStates, duplicatorResult.secondCopy, storm::storage::BitVector(data.preprocessedModel.getNumberOfStates(), false)); - data.preprocessedModel.getStateLabeling().setStates(data.prob1StatesLabel, data.preprocessedModel.getStateLabeling().getStates(data.prob1StatesLabel) & statesReachableInSecondCopy); - subsystemStates = statesReachableInSecondCopy | storm::utility::graph::performProb1E(data.preprocessedModel, data.preprocessedModel.getBackwardTransitions(), duplicatorResult.firstCopy, newPsiStates); - noIncomingTransitionFromFirstCopyStates = duplicatorResult.gateStates & (~newPsiStates); - } - if((subsystemStates & data.preprocessedModel.getInitialStates()).empty()) { - data.solutionsFromPreprocessing[data.objectives.size()-1].first = PreprocessorData::PreprocessorObjectiveSolution::False; - } else { - data.solutionsFromPreprocessing[data.objectives.size()-1].first = PreprocessorData::PreprocessorObjectiveSolution::True; - // Get a subsystem that deletes actions for which the property would be violated - storm::storage::BitVector consideredActions(data.preprocessedModel.getTransitionMatrix().getRowCount(), true); - for(auto state : duplicatorResult.firstCopy) { - for(uint_fast64_t action = data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; action < data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state +1]; ++action) { - for(auto const& entry : data.preprocessedModel.getTransitionMatrix().getRow(action)) { - if(noIncomingTransitionFromFirstCopyStates.get(entry.getColumn())) { - consideredActions.set(action, false); - break; - } - } - } - } - if(!subsystemStates.full() || !consideredActions.full()) { - auto subsystemBuilderResult = storm::transformer::SubsystemBuilder::transform(data.preprocessedModel, subsystemStates, consideredActions); - updatePreprocessedModel(data, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping); - } - } - } else { - // build stateAction reward vector that gives (one*transitionProbability) reward whenever a transition leads from the firstCopy to a psiState - std::vector objectiveRewards(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero()); - for (auto const& firstCopyState : duplicatorResult.firstCopy) { - for (uint_fast64_t row = data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[firstCopyState]; row < data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[firstCopyState + 1]; ++row) { - objectiveRewards[row] = data.preprocessedModel.getTransitionMatrix().getConstrainedRowSum(row, newPsiStates); - } - } - if(!currentObjective.rewardsArePositive) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards, -storm::utility::one()); - } - data.preprocessedModel.addRewardModel(currentObjective.rewardModelName, RewardModelType(boost::none, objectiveRewards)); - } - } - - template - void SparseMultiObjectivePreprocessor::preprocessFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) { - - if(formula.hasDiscreteTimeBound()) { - currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getDiscreteTimeBound()); - } else { - if(data.originalModel.isOfType(storm::models::ModelType::Mdp)) { - STORM_LOG_THROW(formula.getIntervalBounds().first == std::round(formula.getIntervalBounds().first), storm::exceptions::InvalidPropertyException, "Expected a boundedUntilFormula with discrete lower time bound but got " << formula << "."); - STORM_LOG_THROW(formula.getIntervalBounds().second == std::round(formula.getIntervalBounds().second), storm::exceptions::InvalidPropertyException, "Expected a boundedUntilFormula with discrete upper time bound but got " << formula << "."); - } else { - STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Got a boundedUntilFormula which can not be checked for the current model type."); - STORM_LOG_THROW(formula.getIntervalBounds().second > formula.getIntervalBounds().first, storm::exceptions::InvalidPropertyException, "Neither empty nor point intervalls are allowed but got " << formula << "."); - } - if(!storm::utility::isZero(formula.getIntervalBounds().first)) { - currentObjective.lowerTimeBound = storm::utility::convertNumber(formula.getIntervalBounds().first); - } - currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getIntervalBounds().second); - } - preprocessFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data, currentObjective, false, false); - } - - template - void SparseMultiObjectivePreprocessor::preprocessFormula(storm::logic::GloballyFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, bool isProb0Formula, bool isProb1Formula) { - // The formula will be transformed to an until formula for the complementary event. - // If the original formula minimizes, the complementary one will maximize and vice versa. - // Hence, the decision whether to consider positive or negative rewards flips. - currentObjective.rewardsArePositive = !currentObjective.rewardsArePositive; - // To transform from the value of the preprocessed model back to the value of the original model, we have to add 1 to the result. - // The transformation factor has already been set correctly. - currentObjective.toOriginalValueTransformationOffset = storm::utility::one(); - - auto negatedSubformula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer()); - - // We need to swap the two flags isProb0Formula and isProb1Formula - preprocessFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), negatedSubformula), data, currentObjective, isProb1Formula, isProb0Formula); - } - - template - void SparseMultiObjectivePreprocessor::preprocessFormula(storm::logic::EventuallyFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, bool isProb0Formula, bool isProb1Formula, boost::optional const& optionalRewardModelName) { - if(formula.isReachabilityProbabilityFormula()){ - preprocessFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), data, currentObjective, isProb0Formula, isProb1Formula); - return; - } - - CheckTask targetTask(formula.getSubformula()); - storm::modelchecker::SparsePropositionalModelChecker mc(data.preprocessedModel); - STORM_LOG_THROW(mc.canHandle(targetTask), storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " should be propositional."); - storm::storage::BitVector targetStates = mc.check(targetTask)->asExplicitQualitativeCheckResult().getTruthValuesVector(); - - if(!(targetStates & data.preprocessedModel.getInitialStates()).empty()) { - // The value is always zero - data.solutionsFromPreprocessing[data.objectives.size()-1].first = PreprocessorData::PreprocessorObjectiveSolution::Numerical; - data.solutionsFromPreprocessing[data.objectives.size()-1].second = storm::utility::zero(); - return; - } - - auto duplicatorResult = storm::transformer::StateDuplicator::transform(data.preprocessedModel, targetStates); - updatePreprocessedModel(data, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping); - - // Add a reward model that gives zero reward to the actions of states of the second copy. - RewardModelType objectiveRewards(boost::none); - if(formula.isReachabilityRewardFormula()) { - objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); - objectiveRewards.reduceToStateBasedRewards(data.preprocessedModel.getTransitionMatrix(), false); - if(objectiveRewards.hasStateRewards()) { - storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), duplicatorResult.secondCopy, storm::utility::zero()); - } - if(objectiveRewards.hasStateActionRewards()) { - for(auto secondCopyState : duplicatorResult.secondCopy) { - std::fill_n(objectiveRewards.getStateActionRewardVector().begin() + data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[secondCopyState], data.preprocessedModel.getTransitionMatrix().getRowGroupSize(secondCopyState), storm::utility::zero()); - } - } - } else if(formula.isReachabilityTimeFormula() && data.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton)) { - objectiveRewards = RewardModelType(std::vector(data.preprocessedModel.getNumberOfStates(), storm::utility::zero())); - storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), data.getMarkovianStatesOfPreprocessedModel() & duplicatorResult.firstCopy, storm::utility::one()); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The formula " << formula << " neither considers reachability probabilities nor reachability rewards " << (data.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton) ? "nor reachability time" : "") << ". This is not supported."); - } - if(!currentObjective.rewardsArePositive){ - if(objectiveRewards.hasStateRewards()) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one()); - } - if(objectiveRewards.hasStateActionRewards()) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one()); - } - } - data.preprocessedModel.addRewardModel(currentObjective.rewardModelName, std::move(objectiveRewards)); - - // States of the first copy from which the second copy is not reachable with prob 1 under any scheduler can - // be removed as the expected reward/time is not defined for these states. - // We also need to enforce that the second copy will be reached eventually with prob 1. - data.preprocessedModel.getStateLabeling().setStates(data.prob1StatesLabel, data.preprocessedModel.getStateLabeling().getStates(data.prob1StatesLabel) & duplicatorResult.secondCopy); - storm::storage::BitVector subsystemStates = duplicatorResult.secondCopy | storm::utility::graph::performProb1E(data.preprocessedModel, data.preprocessedModel.getBackwardTransitions(), duplicatorResult.firstCopy, duplicatorResult.gateStates); - if((subsystemStates & data.preprocessedModel.getInitialStates()).empty()) { - data.solutionsFromPreprocessing[data.objectives.size()-1].first = PreprocessorData::PreprocessorObjectiveSolution::Undefined; - } else if(!subsystemStates.full()) { - auto subsystemBuilderResult = storm::transformer::SubsystemBuilder::transform(data.preprocessedModel, subsystemStates, storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), true)); - updatePreprocessedModel(data, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping); - } - } - - template - void SparseMultiObjectivePreprocessor::preprocessFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional const& optionalRewardModelName) { - STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type."); - STORM_LOG_THROW(formula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Expected a cumulativeRewardFormula with a discrete time bound but got " << formula << "."); - if(formula.getDiscreteTimeBound()==0) { - data.solutionsFromPreprocessing[data.objectives.size()-1].first = PreprocessorData::PreprocessorObjectiveSolution::Numerical; - data.solutionsFromPreprocessing[data.objectives.size()-1].second = storm::utility::zero(); - return; - } - currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getDiscreteTimeBound()); - - RewardModelType objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); - objectiveRewards.reduceToStateBasedRewards(data.preprocessedModel.getTransitionMatrix(), false); - if(!currentObjective.rewardsArePositive){ - if(objectiveRewards.hasStateRewards()) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one()); - } - if(objectiveRewards.hasStateActionRewards()) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one()); - } - } - data.preprocessedModel.addRewardModel(currentObjective.rewardModelName, std::move(objectiveRewards)); - } - - template - void SparseMultiObjectivePreprocessor::preprocessFormula(storm::logic::TotalRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional const& optionalRewardModelName) { - RewardModelType objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); - objectiveRewards.reduceToStateBasedRewards(data.preprocessedModel.getTransitionMatrix(), false); - if(!currentObjective.rewardsArePositive){ - if(objectiveRewards.hasStateRewards()) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one()); - } - if(objectiveRewards.hasStateActionRewards()) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one()); - } - } - data.preprocessedModel.addRewardModel(currentObjective.rewardModelName, std::move(objectiveRewards)); - } - - - template - void SparseMultiObjectivePreprocessor::ensureRewardFiniteness(PreprocessorData& data) { - bool negativeRewardsOccur = false; - bool positiveRewardsOccur = false; - for(auto& obj : data.objectives) { - if (!obj.rewardFinitenessChecked) { - negativeRewardsOccur |= !obj.rewardsArePositive; - positiveRewardsOccur |= obj.rewardsArePositive; - } - } - storm::storage::BitVector actionsWithNegativeReward; - if(negativeRewardsOccur) { - actionsWithNegativeReward = ensureNegativeRewardFiniteness(data); - } else { - actionsWithNegativeReward = storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), false); - } - if(positiveRewardsOccur) { - ensurePositiveRewardFiniteness(data, actionsWithNegativeReward); - } - } - - template - storm::storage::BitVector SparseMultiObjectivePreprocessor::ensureNegativeRewardFiniteness(PreprocessorData& data) { - - storm::storage::BitVector actionsWithNonNegativeReward(data.preprocessedModel.getTransitionMatrix().getRowCount(), true); - storm::storage::BitVector objectivesWithNegativeReward(data.objectives.size(), false); - for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) { - if (!data.objectives[objIndex].rewardFinitenessChecked && !data.objectives[objIndex].rewardsArePositive) { - data.objectives[objIndex].rewardFinitenessChecked = true; - actionsWithNonNegativeReward &= storm::utility::vector::filterZero(data.preprocessedModel.getRewardModel(data.objectives[objIndex].rewardModelName).getTotalRewardVector(data.preprocessedModel.getTransitionMatrix())); - objectivesWithNegativeReward.set(objIndex, true); - } - } - - storm::storage::BitVector statesWithNegativeRewardForAllChoices(data.preprocessedModel.getNumberOfStates(), false); - storm::storage::BitVector submatrixRows = actionsWithNonNegativeReward; - for(uint_fast64_t state = 0; state < data.preprocessedModel.getNumberOfStates(); ++state) { - // state has negative reward for all choices iff there is no bit set in actionsWithNonNegativeReward for all actions of state - if(actionsWithNonNegativeReward.getNextSetIndex(data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]) >= data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state+1]) { - statesWithNegativeRewardForAllChoices.set(state, true); - // enable one row for the current state to avoid deleting the row group - submatrixRows.set(data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state], true); - } - } - storm::storage::SparseMatrix transitionsWithNonNegativeReward = data.preprocessedModel.getTransitionMatrix().restrictRows(submatrixRows); - - storm::storage::BitVector allStates(data.preprocessedModel.getNumberOfStates(), true); - storm::storage::BitVector statesNeverReachingNegativeRewardForSomeScheduler = storm::utility::graph::performProb0E(transitionsWithNonNegativeReward, transitionsWithNonNegativeReward.getRowGroupIndices(), transitionsWithNonNegativeReward.transpose(true), allStates, statesWithNegativeRewardForAllChoices); - storm::storage::BitVector statesReachingNegativeRewardsFinitelyOftenForSomeScheduler = storm::utility::graph::performProb1E(data.preprocessedModel.getTransitionMatrix(), data.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), data.preprocessedModel.getBackwardTransitions(), allStates, statesNeverReachingNegativeRewardForSomeScheduler); - if((statesReachingNegativeRewardsFinitelyOftenForSomeScheduler & data.preprocessedModel.getInitialStates()).empty()) { - STORM_LOG_WARN("For every scheduler, the induced reward for one or more of the objectives that minimize rewards is infinity."); - for(auto objIndex : objectivesWithNegativeReward) { - if(data.objectives[objIndex].threshold) { - data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::False; - } else { - data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::Unbounded; - } - } - } else if(!statesReachingNegativeRewardsFinitelyOftenForSomeScheduler.full()) { - auto subsystemBuilderResult = storm::transformer::SubsystemBuilder::transform(data.preprocessedModel, statesReachingNegativeRewardsFinitelyOftenForSomeScheduler, storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), true)); - updatePreprocessedModel(data, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping); - return (~actionsWithNonNegativeReward) % subsystemBuilderResult.subsystemActions; - } - return ~actionsWithNonNegativeReward; - } - - template - void SparseMultiObjectivePreprocessor::ensurePositiveRewardFiniteness(PreprocessorData& data, storm::storage::BitVector const& actionsWithNegativeReward) { - storm::utility::Stopwatch sw; - auto mecDecomposition = storm::storage::MaximalEndComponentDecomposition(data.preprocessedModel.getTransitionMatrix(), data.preprocessedModel.getBackwardTransitions()); - STORM_LOG_DEBUG("Maximal end component decomposition for ensuring positive reward finiteness took " << sw << " seconds."); - if(mecDecomposition.empty()) { - return; - } - for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) { - auto& obj = data.objectives[objIndex]; - if (!obj.rewardFinitenessChecked && obj.rewardsArePositive) { - obj.rewardFinitenessChecked = true; - // Find maximal end components that contain a state with positive reward - storm::storage::BitVector actionsWithPositiveRewards = storm::utility::vector::filterGreaterZero(data.preprocessedModel.getRewardModel(obj.rewardModelName).getTotalRewardVector(data.preprocessedModel.getTransitionMatrix())); - for(auto const& mec : mecDecomposition) { - bool ecHasActionWithPositiveReward = false; - for(auto const& stateActionsPair : mec) { - for(auto const& action : stateActionsPair.second) { - STORM_LOG_THROW(!actionsWithNegativeReward.get(action), storm::exceptions::InvalidPropertyException, "Found an end componet that contains rewards for a maximizing and a minimizing objective. This is not supported"); - // Note: we could also check whether some sub EC exists that does not contain negative rewards. - ecHasActionWithPositiveReward |= (actionsWithPositiveRewards.get(action)); - } - } - if(ecHasActionWithPositiveReward) { - if(obj.threshold) { - data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::True; - } else { - data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::Unbounded; - } - break; - } - } - } - } - } - - template - void SparseMultiObjectivePreprocessor::handleObjectivesWithSolutionFromPreprocessing(PreprocessorData& data) { - // Set solution for objectives for which there are no rewards left - for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) { - if(data.solutionsFromPreprocessing[objIndex].first == PreprocessorData::PreprocessorObjectiveSolution::None && - data.preprocessedModel.getRewardModel(data.objectives[objIndex].rewardModelName).isAllZero()) { - data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::Numerical; - data.solutionsFromPreprocessing[objIndex].second = storm::utility::zero(); - } - } - - // Translate numerical solutions from preprocessing to Truth values (if the objective specifies a threshold) or to values for the original model (otherwise). - for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) { - if(data.solutionsFromPreprocessing[objIndex].first == PreprocessorData::PreprocessorObjectiveSolution::Numerical) { - ValueType& value = data.solutionsFromPreprocessing[objIndex].second; - ObjectiveInformation const& obj = data.objectives[objIndex]; - if(obj.threshold) { - if((obj.thresholdIsStrict && value > (*obj.threshold)) || (!obj.thresholdIsStrict && value >= (*obj.threshold))) { - data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::True; - } else { - data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::False; - } - } else { - value = value * obj.toOriginalValueTransformationFactor + obj.toOriginalValueTransformationOffset; - } - } - } - - // Only keep the objectives for which we have no solution yet - storm::storage::BitVector objWithNoSolution = storm::utility::vector::filter>(data.solutionsFromPreprocessing, [&] (std::pair const& value) -> bool { return value.first == PreprocessorData::PreprocessorObjectiveSolution::None; }); - data.objectives = storm::utility::vector::filterVector(data.objectives, objWithNoSolution); - } - - - template class SparseMultiObjectivePreprocessor>; - template class SparseMultiObjectivePreprocessor>; - -#ifdef STORM_HAVE_CARL - template class SparseMultiObjectivePreprocessor>; - template class SparseMultiObjectivePreprocessor>; -#endif - - - } - } -} diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h deleted file mode 100644 index 133501dd4..000000000 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h +++ /dev/null @@ -1,102 +0,0 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSOR_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSOR_H_ - -#include - -#include "src/logic/Formulas.h" -#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h" -#include "src/storage/BitVector.h" - -namespace storm { - namespace modelchecker { - namespace helper { - - /* - * Helper Class to invoke the necessary preprocessing for multi objective model checking - */ - template - class SparseMultiObjectivePreprocessor { - public: - typedef typename SparseModelType::ValueType ValueType; - typedef typename SparseModelType::RewardModelType RewardModelType; - typedef SparseMultiObjectivePreprocessorData PreprocessorData; - typedef SparseMultiObjectiveObjectiveInformation ObjectiveInformation; - - /*! - * Preprocesses the given model w.r.t. the given formulas. - * @param originalModel The considered model - * @param originalFormula the considered formula. The subformulas should only contain one OperatorFormula at top level, i.e., the formula is simple. - */ - static PreprocessorData preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel); - - private: - - /*! - * Updates the preprocessed model stored in the given data to the given model. - * The given newToOldStateIndexMapping should give for each state in the newPreprocessedModel - * the index of the state in the current data.preprocessedModel. - */ - static void updatePreprocessedModel(PreprocessorData& data, SparseModelType& newPreprocessedModel, std::vector& newToOldStateIndexMapping); - - /*! - * Apply the neccessary preprocessing for the given formula. - * @param formula the current (sub)formula - * @param data the information collected so far - * @param isProb0Formula true iff the considered objective is of the form P<=0 [..] - * @param isProb1Formula true iff the considered objective is of the form P>=1 [..] - * @param currentObjective the currently considered objective. The given formula should be a a (sub)formula of this objective - * @param optionalRewardModelName the reward model name that is considered for the formula (if available) - */ - static void preprocessFormula(storm::logic::OperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective); - static void preprocessFormula(storm::logic::ProbabilityOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective); - static void preprocessFormula(storm::logic::RewardOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective); - static void preprocessFormula(storm::logic::TimeOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective); - static void preprocessFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, bool isProb0Formula, bool isProb1Formula); - static void preprocessFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective); - static void preprocessFormula(storm::logic::GloballyFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, bool isProb0Formula, bool isProb1Formula); - static void preprocessFormula(storm::logic::EventuallyFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, bool isProb0Formula, bool isProb1Formula, boost::optional const& optionalRewardModelName = boost::none); - static void preprocessFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional const& optionalRewardModelName = boost::none); - static void preprocessFormula(storm::logic::TotalRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional const& optionalRewardModelName = boost::none); - - /*! - * Checks whether the occurring reward properties are guaranteed to be finite for all states. - * if not, further preprocessing is applied. - * - * For reward properties that maximize, it is checked whether the reward is unbounded for some scheduler - * (i.e., an EC with (only positive) rewards is reachable). - * If yes, the objective is removed as we can combine any scheduler with the scheduler above - * to obtain arbitrary high values. Note that in case of achievability or numerical queries, this combination might - * (theoretically) violate thresholds by some small epsilon. This is ignored as we are working with numerical methods anyway... - * - * For reward properties that minimize, all states from which only infinite reward is possible are removed. - * Note that this excludes solutions of numerical queries where the minimum is infinity... - */ - static void ensureRewardFiniteness(PreprocessorData& data); - - /*! - * Checks reward finiteness for the negative rewards and returns the set of actions in the - * preprocessedModel that give negative rewards for some objective - */ - static storm::storage::BitVector ensureNegativeRewardFiniteness(PreprocessorData& data); - - /*! - * Checks reward finiteness for the positive rewards - */ - static void ensurePositiveRewardFiniteness(PreprocessorData& data, storm::storage::BitVector const& actionsWithNegativeReward); - - /*! - * Handles the objectives for which a solution has been found in preprocessing, that is: - * * Set the solution for objectives for which no reward is left to zero - * * Translate numerical solutions for objectives with a threshold to either True or False - * * Translate numerical solutions for objectives without a threshold to a value for the original model - * * Only keep the objectives for which there is no solution yet - */ - static void handleObjectivesWithSolutionFromPreprocessing(PreprocessorData& data); - - }; - - } - } -} - -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSOR_H_ */ diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h deleted file mode 100644 index be42f58af..000000000 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h +++ /dev/null @@ -1,135 +0,0 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSORDATA_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSORDATA_H_ - -#include -#include -#include -#include -#include - -#include "src/logic/Formulas.h" -#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h" -#include "src/models/sparse/MarkovAutomaton.h" -#include "src/storage/BitVector.h" -#include "src/utility/macros.h" -#include "src/utility/constants.h" - -#include "src/exceptions/UnexpectedException.h" - -namespace storm { - namespace modelchecker { - namespace helper { - - template - struct SparseMultiObjectivePreprocessorData { - - enum class QueryType { Achievability, Numerical, Pareto }; - enum class PreprocessorObjectiveSolution { None, False, True, Numerical, Unbounded, Undefined }; - - storm::logic::MultiObjectiveFormula const& originalFormula; - - // Stores the result for this objective obtained from preprocessing. - // In case of a numerical result, the value is stored in the second entry of the pair. Otherwise, the second entry can be ignored. - std::vector> solutionsFromPreprocessing; - - SparseModelType const& originalModel; - SparseModelType preprocessedModel; - std::vector newToOldStateIndexMapping; - std::string prob1StatesLabel; - - QueryType queryType; - std::vector> objectives; - boost::optional indexOfOptimizingObjective; - - bool produceSchedulers; - - SparseMultiObjectivePreprocessorData(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel, SparseModelType&& preprocessedModel, std::vector&& newToOldStateIndexMapping) : originalFormula(originalFormula), solutionsFromPreprocessing(originalFormula.getNumberOfSubformulas(), std::make_pair(PreprocessorObjectiveSolution::None, storm::utility::zero())), originalModel(originalModel), preprocessedModel(preprocessedModel), newToOldStateIndexMapping(newToOldStateIndexMapping), produceSchedulers(false) { - - // get a unique name for the labels of states that have to be reached with probability 1 and add the label - this->prob1StatesLabel = "prob1"; - while(this->preprocessedModel.hasLabel(this->prob1StatesLabel)) { - this->prob1StatesLabel = "_" + this->prob1StatesLabel; - } - this->preprocessedModel.getStateLabeling().addLabel(this->prob1StatesLabel, storm::storage::BitVector(this->preprocessedModel.getNumberOfStates(), true)); - } - - template - typename std::enable_if>::value, storm::storage::BitVector const&>::type - getMarkovianStatesOfPreprocessedModel() const { - return preprocessedModel.getMarkovianStates(); - } - - template - typename std::enable_if>::value, storm::storage::BitVector const&>::type - getMarkovianStatesOfPreprocessedModel() const { - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Tried to retrieve Markovian states but the considered model is not an MA."); - } - - void printToStream(std::ostream& out) const { - out << std::endl; - out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; - out << " Multi-objective Preprocessor Data " << std::endl; - out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; - out << std::endl; - out << "Original Formula: " << std::endl; - out << "--------------------------------------------------------------" << std::endl; - out << "\t" << originalFormula << std::endl; - bool hasOneObjectiveSolvedInPreprocessing = false; - for(uint_fast64_t subformulaIndex = 0; subformulaIndex < originalFormula.getNumberOfSubformulas(); ++subformulaIndex) { - if(!hasOneObjectiveSolvedInPreprocessing && solutionsFromPreprocessing[subformulaIndex].first != PreprocessorObjectiveSolution::None) { - hasOneObjectiveSolvedInPreprocessing = true; - out << std::endl; - out << "Solutions of objectives obtained from Preprocessing: " << std::endl; - out << "--------------------------------------------------------------" << std::endl; - } - switch(solutionsFromPreprocessing[subformulaIndex].first) { - case PreprocessorObjectiveSolution::None: - break; - case PreprocessorObjectiveSolution::False: - out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= false" << std::endl; - break; - case PreprocessorObjectiveSolution::True: - out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= true" << std::endl; - break; - case PreprocessorObjectiveSolution::Numerical: - out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= " << solutionsFromPreprocessing[subformulaIndex].second << std::endl; - break; - case PreprocessorObjectiveSolution::Unbounded: - out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= unbounded" << std::endl; - break; - case PreprocessorObjectiveSolution::Undefined: - out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= undefined" << std::endl; - break; - default: - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "no case for PreprocessorObjectiveSolution."); - } - } - out << std::endl; - out << "Objectives:" << std::endl; - out << "--------------------------------------------------------------" << std::endl; - for (auto const& obj : objectives) { - obj.printToStream(out); - } - out << "--------------------------------------------------------------" << std::endl; - out << std::endl; - out << "Original Model Information:" << std::endl; - originalModel.printModelInformationToStream(out); - out << std::endl; - out << "Preprocessed Model Information:" << std::endl; - preprocessedModel.printModelInformationToStream(out); - out << std::endl; - out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; - } - - - friend std::ostream& operator<<(std::ostream& out, SparseMultiObjectivePreprocessorData const& data) { - data.printToStream(out); - return out; - } - - }; - } - } -} - -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSORDATA_H_ */ diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveRefinementStep.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveRefinementStep.h deleted file mode 100644 index cdc66c884..000000000 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveRefinementStep.h +++ /dev/null @@ -1,63 +0,0 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEREFINEMENTSTEP_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEREFINEMENTSTEP_H_ - -#include -#include - -#include "src/storage/TotalScheduler.h" - -namespace storm { - namespace modelchecker { - namespace helper { - - template - class SparseMultiObjectiveRefinementStep { - - public: - SparseMultiObjectiveRefinementStep(std::vector const& weightVector, std::vector const& lowerBoundPoint, std::vector const& upperBoundPoint, storm::storage::TotalScheduler const& scheduler) : weightVector(weightVector), lowerBoundPoint(lowerBoundPoint), upperBoundPoint(upperBoundPoint), scheduler(scheduler) { - //Intentionally left empty - } - - SparseMultiObjectiveRefinementStep(std::vector&& weightVector, std::vector&& lowerBoundPoint, std::vector&& upperBoundPoint, storm::storage::TotalScheduler&& scheduler) : weightVector(weightVector), lowerBoundPoint(lowerBoundPoint), upperBoundPoint(upperBoundPoint), scheduler(scheduler) { - //Intentionally left empty - } - - SparseMultiObjectiveRefinementStep(std::vector const& weightVector, std::vector const& lowerBoundPoint, std::vector const& upperBoundPoint) : weightVector(weightVector), lowerBoundPoint(lowerBoundPoint), upperBoundPoint(upperBoundPoint) { - //Intentionally left empty - } - - SparseMultiObjectiveRefinementStep(std::vector&& weightVector, std::vector&& lowerBoundPoint, std::vector&& upperBoundPoint) : weightVector(weightVector), lowerBoundPoint(lowerBoundPoint), upperBoundPoint(upperBoundPoint) { - //Intentionally left empty - } - - std::vector const& getWeightVector() const { - return weightVector; - } - - std::vector const& getLowerBoundPoint() const { - return lowerBoundPoint; - } - - std::vector const& getUpperBoundPoint() const { - return upperBoundPoint; - } - - bool hasScheduler() const { - return static_cast(scheduler); - } - - storm::storage::TotalScheduler const& getScheduler() const { - return scheduler.get(); - } - - private: - std::vector const weightVector; - std::vector const lowerBoundPoint; - std::vector const upperBoundPoint; - boost::optional const scheduler; - }; - } - } -} - -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEREFINEMENTSTEP_H_ */ diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h deleted file mode 100644 index 5bb1f0f77..000000000 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h +++ /dev/null @@ -1,135 +0,0 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVERESULTDATA_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVERESULTDATA_H_ - -#include -#include -#include - -#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveRefinementStep.h" -#include "src/storage/geometry/Polytope.h" -#include "src/utility/macros.h" - -#include "src/exceptions/InvalidStateException.h" - -namespace storm { - namespace modelchecker { - namespace helper { - - template - class SparseMultiObjectiveResultData { - - public: - std::vector>& refinementSteps() { - return steps; - } - std::vector> const& refinementSteps() const { - return steps; - } - - std::shared_ptr>& overApproximation() { - return overApprox; - } - std::shared_ptr> const& overApproximation() const { - return overApprox; - } - - std::shared_ptr>& underApproximation() { - return underApprox; - } - std::shared_ptr> const& underApproximation() const { - return underApprox; - } - - void setThresholdsAreAchievable(bool value) { - thresholdsAreAchievable = value ? Tribool::True : Tribool::False; - } - bool isThresholdsAreAchievableSet() const { - return thresholdsAreAchievable != Tribool::Indeterminate; - } - bool getThresholdsAreAchievable() const { - STORM_LOG_THROW(isThresholdsAreAchievableSet(), storm::exceptions::InvalidStateException, "Could not retrieve whether thresholds are acheivable: value not set."); - return thresholdsAreAchievable == Tribool::True; - } - - void setNumericalResult(RationalNumberType value) { - numericalResult = value; - } - bool isNumericalResultSet() const { - return static_cast(numericalResult); - } - template - TargetValueType getNumericalResult() const { - return storm::utility::convertNumber(numericalResult.get()); - } - - void setOptimumIsAchievable(bool value) { - optimumIsAchievable = value ? Tribool::True : Tribool::False; - } - bool isOptimumIsAchievableSet() const { - return optimumIsAchievable != Tribool::Indeterminate; - } - bool getOptimumIsAchievableAchievable() const { - STORM_LOG_THROW(isOptimumIsAchievableSet(), storm::exceptions::InvalidStateException, "Could not retrieve whether the computed optimum is acheivable: value not set."); - return optimumIsAchievable == Tribool::True; - } - - void setPrecisionOfResult(RationalNumberType value) { - precisionOfResult = value; - } - bool isPrecisionOfResultSet() const { - return static_cast(precisionOfResult); - } - template - TargetValueType getPrecisionOfResult() const { - return storm::utility::convertNumber(precisionOfResult.get()); - } - - void setTargetPrecisionReached(bool value) { - targetPrecisionReached = value; - } - bool getTargetPrecisionReached() const { - return targetPrecisionReached; - } - - void setMaxStepsPerformed(bool value) { - maxStepsPerformed = value; - } - bool getMaxStepsPerformed() const { - return maxStepsPerformed; - } - - private: - - enum class Tribool { False, True, Indeterminate }; - - //Stores the results for the individual iterations - std::vector> steps; - //Stores an overapproximation of the set of achievable values - std::shared_ptr> overApprox; - //Stores an underapproximation of the set of achievable values - std::shared_ptr> underApprox; - - // Stores the result of an achievability query (if applicable). - // For a numerical query, stores whether there is one feasible solution. - Tribool thresholdsAreAchievable = Tribool::Indeterminate; - - //Stores the result of a numerical query (if applicable). - boost::optional numericalResult; - //For numerical queries, this is true iff there is an actual scheduler that induces the computed supremum (i.e., supremum == maximum) - Tribool optimumIsAchievable = Tribool::Indeterminate; - - //Stores the achieved precision for numerical and pareto queries - boost::optional precisionOfResult; - - //Stores whether the precision of the result is sufficient (only applicable to numerical and pareto queries) - bool targetPrecisionReached = true; - - //Stores whether the computation was aborted due to performing too many refinement steps - bool maxStepsPerformed = false; - - }; - } - } -} - -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVERESULTDATA_H_ */ diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp deleted file mode 100644 index e7d3fddf3..000000000 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp +++ /dev/null @@ -1,242 +0,0 @@ -#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h" - -#include - -#include "src/adapters/CarlAdapter.h" -#include "src/models/sparse/Mdp.h" -#include "src/models/sparse/MarkovAutomaton.h" -#include "src/models/sparse/StandardRewardModel.h" -#include "src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" -#include "src/solver/MinMaxLinearEquationSolver.h" -#include "src/transformer/EndComponentEliminator.h" -#include "src/utility/graph.h" -#include "src/utility/macros.h" -#include "src/utility/vector.h" - -#include "src/exceptions/IllegalFunctionCallException.h" -#include "src/exceptions/NotImplementedException.h" - -namespace storm { - namespace modelchecker { - namespace helper { - - - template - SparseMultiObjectiveWeightVectorChecker::SparseMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : data(data), objectivesWithNoUpperTimeBound(data.objectives.size()), discreteActionRewards(data.objectives.size()), checkHasBeenCalled(false), objectiveResults(data.objectives.size()), offsetsToLowerBound(data.objectives.size()), offsetsToUpperBound(data.objectives.size()) { - - // set the unbounded objectives - for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) { - objectivesWithNoUpperTimeBound.set(objIndex, !data.objectives[objIndex].upperTimeBound); - } - // Enlarge the set of prob1 states to the states that are only reachable via prob1 states - statesThatAreAllowedToBeVisitedInfinitelyOften = ~storm::utility::graph::getReachableStates(data.preprocessedModel.getTransitionMatrix(), data.preprocessedModel.getInitialStates(), ~data.preprocessedModel.getStates(data.prob1StatesLabel), storm::storage::BitVector(data.preprocessedModel.getNumberOfStates(), false)); - } - - - template - void SparseMultiObjectiveWeightVectorChecker::check(std::vector const& weightVector) { - checkHasBeenCalled=true; - STORM_LOG_DEBUG("Invoked WeightVectorChecker with weights " << std::endl << "\t" << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(weightVector))); - std::vector weightedRewardVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero()); - for(auto objIndex : objectivesWithNoUpperTimeBound) { - storm::utility::vector::addScaledVector(weightedRewardVector, discreteActionRewards[objIndex], weightVector[objIndex]); - } - unboundedWeightedPhase(weightedRewardVector); - unboundedIndividualPhase(weightVector); - // Only invoke boundedPhase if necessarry, i.e., if there is at least one objective with a time bound - for(auto const& obj : this->data.objectives) { - if(obj.lowerTimeBound || obj.upperTimeBound) { - boundedPhase(weightVector, weightedRewardVector); - break; - } - } - STORM_LOG_DEBUG("Weight vector check done. Lower bounds for results in initial state: " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(getLowerBoundsOfInitialStateResults()))); - } - - template - void SparseMultiObjectiveWeightVectorChecker::setMaximumLowerUpperBoundGap(ValueType const& value) { - this->maximumLowerUpperBoundGap = value; - } - - template - typename SparseMultiObjectiveWeightVectorChecker::ValueType const& SparseMultiObjectiveWeightVectorChecker::getMaximumLowerUpperBoundGap() const { - return this->maximumLowerUpperBoundGap; - } - - template - std::vector::ValueType> SparseMultiObjectiveWeightVectorChecker::getLowerBoundsOfInitialStateResults() const { - STORM_LOG_THROW(checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before."); - uint_fast64_t initstate = *this->data.preprocessedModel.getInitialStates().begin(); - std::vector res; - res.reserve(this->data.objectives.size()); - for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) { - res.push_back(this->objectiveResults[objIndex][initstate] + this->offsetsToLowerBound[objIndex]); - } - return res; - } - - template - std::vector::ValueType> SparseMultiObjectiveWeightVectorChecker::getUpperBoundsOfInitialStateResults() const { - STORM_LOG_THROW(checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before."); - uint_fast64_t initstate = *this->data.preprocessedModel.getInitialStates().begin(); - std::vector res; - res.reserve(this->data.objectives.size()); - for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) { - res.push_back(this->objectiveResults[objIndex][initstate] + this->offsetsToUpperBound[objIndex]); - } - return res; - } - - template - storm::storage::TotalScheduler const& SparseMultiObjectiveWeightVectorChecker::getScheduler() const { - STORM_LOG_THROW(this->checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before."); - for(auto const& obj : this->data.objectives) { - STORM_LOG_THROW(!obj.lowerTimeBound && !obj.upperTimeBound, storm::exceptions::NotImplementedException, "Scheduler retrival is not implemented for timeBounded objectives."); - } - return scheduler; - } - - template - void SparseMultiObjectiveWeightVectorChecker::unboundedWeightedPhase(std::vector const& weightedRewardVector) { - if(this->objectivesWithNoUpperTimeBound.empty()) { - this->weightedResult = std::vector(data.preprocessedModel.getNumberOfStates(), storm::utility::zero()); - this->scheduler = storm::storage::TotalScheduler(data.preprocessedModel.getNumberOfStates()); - return; - } - // Remove end components in which no reward is earned - - auto ecEliminatorResult = storm::transformer::EndComponentEliminator::transform(data.preprocessedModel.getTransitionMatrix(), storm::utility::vector::filterZero(weightedRewardVector), storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowGroupCount(), true), storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowGroupCount(), true)); - - std::vector subRewardVector(ecEliminatorResult.newToOldRowMapping.size()); - storm::utility::vector::selectVectorValues(subRewardVector, ecEliminatorResult.newToOldRowMapping, weightedRewardVector); - std::vector subResult(ecEliminatorResult.matrix.getRowGroupCount()); - - storm::solver::GeneralMinMaxLinearEquationSolverFactory solverFactory; - std::unique_ptr> solver = solverFactory.create(ecEliminatorResult.matrix); - solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); - solver->setTrackScheduler(true); - solver->solveEquations(subResult, subRewardVector); - - this->weightedResult = std::vector(data.preprocessedModel.getNumberOfStates()); - std::vector optimalChoices(data.preprocessedModel.getNumberOfStates()); - - transformReducedSolutionToOriginalModel(ecEliminatorResult.matrix, subResult, solver->getScheduler()->getChoices(), ecEliminatorResult.newToOldRowMapping, ecEliminatorResult.oldToNewStateMapping, this->data.preprocessedModel.getTransitionMatrix(), this->weightedResult, optimalChoices); - - this->scheduler = storm::storage::TotalScheduler(std::move(optimalChoices)); - } - - template - void SparseMultiObjectiveWeightVectorChecker::unboundedIndividualPhase(std::vector const& weightVector) { - - storm::storage::SparseMatrix deterministicMatrix = data.preprocessedModel.getTransitionMatrix().selectRowsFromRowGroups(this->scheduler.getChoices(), true); - storm::storage::SparseMatrix deterministicBackwardTransitions = deterministicMatrix.transpose(); - std::vector deterministicStateRewards(deterministicMatrix.getRowCount()); - storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; - - // We compute an estimate for the results of the individual objectives which is obtained from the weighted result and the result of the objectives computed so far. - // Note that weightedResult = Sum_{i=1}^{n} w_i * objectiveResult_i. - std::vector weightedSumOfUncheckedObjectives = weightedResult; - ValueType sumOfWeightsOfUncheckedObjectives = storm::utility::vector::sum_if(weightVector, objectivesWithNoUpperTimeBound); - - for(uint_fast64_t const& objIndex : storm::utility::vector::getSortedIndices(weightVector)) { - if(objectivesWithNoUpperTimeBound.get(objIndex)){ - offsetsToLowerBound[objIndex] = storm::utility::zero(); - offsetsToUpperBound[objIndex] = storm::utility::zero(); - storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), data.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), discreteActionRewards[objIndex]); - storm::storage::BitVector statesWithRewards = ~storm::utility::vector::filterZero(deterministicStateRewards); - // As target states, we pick the states from which no reward is reachable. - storm::storage::BitVector targetStates = ~storm::utility::graph::performProbGreater0(deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards); - - // Compute the estimate for this objective - if(!storm::utility::isZero(weightVector[objIndex])) { - objectiveResults[objIndex] = weightedSumOfUncheckedObjectives; - storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], storm::utility::one() / sumOfWeightsOfUncheckedObjectives); - } - - // Make sure that the objectiveResult is initialized in some way - objectiveResults[objIndex].resize(data.preprocessedModel.getNumberOfStates(), storm::utility::zero()); - - // Invoke the linear equation solver - objectiveResults[objIndex] = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(deterministicMatrix, - deterministicBackwardTransitions, - deterministicStateRewards, - targetStates, - false, //no qualitative checking, - linearEquationSolverFactory, - objectiveResults[objIndex]); - // Update the estimate for the next objectives. - if(!storm::utility::isZero(weightVector[objIndex])) { - storm::utility::vector::addScaledVector(weightedSumOfUncheckedObjectives, objectiveResults[objIndex], -weightVector[objIndex]); - sumOfWeightsOfUncheckedObjectives -= weightVector[objIndex]; - } - } else { - objectiveResults[objIndex] = std::vector(data.preprocessedModel.getNumberOfStates(), storm::utility::zero()); - } - } - } - - template - void SparseMultiObjectiveWeightVectorChecker::transformReducedSolutionToOriginalModel(storm::storage::SparseMatrix const& reducedMatrix, - std::vector const& reducedSolution, - std::vector const& reducedOptimalChoices, - std::vector const& reducedToOriginalChoiceMapping, - std::vector const& originalToReducedStateMapping, - storm::storage::SparseMatrix const& originalMatrix, - std::vector& originalSolution, - std::vector& originalOptimalChoices) const { - - storm::storage::BitVector statesWithUndefinedScheduler(originalMatrix.getRowGroupCount(), false); - for(uint_fast64_t state = 0; state < originalMatrix.getRowGroupCount(); ++state) { - uint_fast64_t stateInReducedModel = originalToReducedStateMapping[state]; - // Check if the state exists in the reduced model - if(stateInReducedModel < reducedMatrix.getRowGroupCount()) { - originalSolution[state] = reducedSolution[stateInReducedModel]; - // Check if the chosen row originaly belonged to the current state - uint_fast64_t chosenRowInReducedModel = reducedMatrix.getRowGroupIndices()[stateInReducedModel] + reducedOptimalChoices[stateInReducedModel]; - uint_fast64_t chosenRowInOriginalModel = reducedToOriginalChoiceMapping[chosenRowInReducedModel]; - if(chosenRowInOriginalModel >= originalMatrix.getRowGroupIndices()[state] && - chosenRowInOriginalModel < originalMatrix.getRowGroupIndices()[state+1]) { - originalOptimalChoices[state] = chosenRowInOriginalModel - originalMatrix.getRowGroupIndices()[state]; - } else { - statesWithUndefinedScheduler.set(state); - } - } else { - // if the state does not exist in the reduced model, it means that the result is always zero, independent of the scheduler. - // Hence, we don't have to set the scheduler explicitly - originalSolution[state] = storm::utility::zero(); - } - } - while(!statesWithUndefinedScheduler.empty()) { - for(auto state : statesWithUndefinedScheduler) { - // Try to find a choice that stays inside the EC (i.e., for which all successors are represented by the same state in the reduced model) - // And at least one successor has a defined scheduler. - // This way, a scheduler is chosen that leads (with probability one) to the state of the EC for which the scheduler is defined - uint_fast64_t stateInReducedModel = originalToReducedStateMapping[state]; - for(uint_fast64_t row = originalMatrix.getRowGroupIndices()[state]; row < originalMatrix.getRowGroupIndices()[state+1]; ++row) { - bool rowStaysInEC = true; - bool rowLeadsToDefinedScheduler = false; - for(auto const& entry : originalMatrix.getRow(row)) { - rowStaysInEC &= ( stateInReducedModel == originalToReducedStateMapping[entry.getColumn()]); - rowLeadsToDefinedScheduler |= !statesWithUndefinedScheduler.get(entry.getColumn()); - } - if(rowStaysInEC && rowLeadsToDefinedScheduler) { - originalOptimalChoices[state] = row - originalMatrix.getRowGroupIndices()[state]; - statesWithUndefinedScheduler.set(state, false); - } - } - } - } - } - - - - template class SparseMultiObjectiveWeightVectorChecker>; - template class SparseMultiObjectiveWeightVectorChecker>; -#ifdef STORM_HAVE_CARL - template class SparseMultiObjectiveWeightVectorChecker>; - template class SparseMultiObjectiveWeightVectorChecker>; -#endif - - } - } -} diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h deleted file mode 100644 index 3022769d7..000000000 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h +++ /dev/null @@ -1,138 +0,0 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEWEIGHTVECTORCHECKER_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEWEIGHTVECTORCHECKER_H_ - -#include - -#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h" -#include "src/storage/TotalScheduler.h" - -namespace storm { - namespace modelchecker { - namespace helper { - - /*! - * Helper Class that takes preprocessed multi objective data and a weight vector and ... - * - computes the maximal expected reward w.r.t. the weighted sum of the rewards of the individual objectives - * - extracts the scheduler that induces this maximum - * - computes for each objective the value induced by this scheduler - */ - template - class SparseMultiObjectiveWeightVectorChecker { - public: - typedef typename SparseModelType::ValueType ValueType; - typedef typename SparseModelType::RewardModelType RewardModelType; - typedef SparseMultiObjectivePreprocessorData PreprocessorData; - - SparseMultiObjectiveWeightVectorChecker(PreprocessorData const& data); - - /*! - * - computes the maximal expected reward w.r.t. the weighted sum of the rewards of the individual objectives - * - extracts the scheduler that induces this maximum - * - computes for each objective the value induced by this scheduler - */ - void check(std::vector const& weightVector); - - /*! - * Sets the maximum gap that is allowed between the lower and upper bound of the result of some objective. - */ - void setMaximumLowerUpperBoundGap(ValueType const& value); - - /*! - * Retrieves the maximum gap that is allowed between the lower and upper bound of the result of some objective. - */ - ValueType const& getMaximumLowerUpperBoundGap() const; - - /*! - * Retrieves the results of the individual objectives at the initial state of the given model. - * Note that check(..) has to be called before retrieving results. Otherwise, an exception is thrown. - * Also note that there is no guarantee that the lower/upper bounds are sound - * as long as the underlying solution methods are unsound (e.g., standard value iteration). - */ - std::vector getLowerBoundsOfInitialStateResults() const; - std::vector getUpperBoundsOfInitialStateResults() const; - - /*! - * Retrieves a scheduler that induces the current values - * Note that check(..) has to be called before retrieving the scheduler. Otherwise, an exception is thrown. - */ - storm::storage::TotalScheduler const& getScheduler() const; - - - protected: - - /*! - * Determines the scheduler that maximizes the weighted reward vector of the unbounded objectives - * - * @param weightedRewardVector the weighted rewards (only considering the unbounded objectives) - */ - void unboundedWeightedPhase(std::vector const& weightedRewardVector); - - /*! - * Computes the values of the objectives that do not have a stepBound w.r.t. the scheduler computed in the unboundedWeightedPhase - * - * @param weightVector the weight vector of the current check - */ - void unboundedIndividualPhase(std::vector const& weightVector); - - /*! - * For each time epoch (starting with the maximal stepBound occurring in the objectives), this method - * - determines the objectives that are relevant in the current time epoch - * - determines the maximizing scheduler for the weighted reward vector of these objectives - * - computes the values of these objectives w.r.t. this scheduler - * - * @param weightVector the weight vector of the current check - * @param weightedRewardVector the weighted rewards considering the unbounded objectives. Will be invalidated after calling this. - */ - virtual void boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) = 0; - - /*! - * Transforms the results of a min-max-solver that considers a reduced model (without end components) to a result for the original (unreduced) model - */ - void transformReducedSolutionToOriginalModel(storm::storage::SparseMatrix const& reducedMatrix, - std::vector const& reducedSolution, - std::vector const& reducedOptimalChoices, - std::vector const& reducedToOriginalChoiceMapping, - std::vector const& originalToReducedStateMapping, - storm::storage::SparseMatrix const& originalMatrix, - std::vector& originalSolution, - std::vector& originalOptimalChoices) const; - - - // stores the considered information of the multi-objective model checking problem - PreprocessorData const& data; - // stores the indices of the objectives for which there is no upper time bound - storm::storage::BitVector objectivesWithNoUpperTimeBound; - // stores the (discretized) state action rewards for each objective. - std::vector>discreteActionRewards; - - // stores the set of states for which it is allowed to visit them infinitely often - // This means that, if one of the states is part of a neutral EC, it is allowed to - // stay in this EC forever. - storm::storage::BitVector statesThatAreAllowedToBeVisitedInfinitelyOften; - - // becomes true after the first call of check(..) - bool checkHasBeenCalled; - - // stores the maximum gap that is allowed between the lower and upper bound of the result of some objective. - ValueType maximumLowerUpperBoundGap; - - // The result for the weighted reward vector (for all states of the model) - std::vector weightedResult; - // The lower bounds of the results for the individual objectives (w.r.t. all states of the model) - std::vector> objectiveResults; - // Stores for each objective the distance between the computed result (w.r.t. the initial state) and a lower/upper bound for the actual result. - // The distances are stored as a (possibly negative) offset that has to be added to to the objectiveResults. - // Note that there is no guarantee that the lower/upper bounds are sound as long as the underlying solution method is not sound (e.g. standard value iteration). - std::vector offsetsToLowerBound; - std::vector offsetsToUpperBound; - - // The scheduler that maximizes the weighted rewards - storm::storage::TotalScheduler scheduler; - - }; - - } - } -} - -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEWEIGHTEDVECTORCHECKER_H_ */ diff --git a/src/modelchecker/multiobjective/pcaa/SparsePCAAPreprocessor.cpp b/src/modelchecker/multiobjective/pcaa/SparsePCAAPreprocessor.cpp index 3201de777..c49038492 100644 --- a/src/modelchecker/multiobjective/pcaa/SparsePCAAPreprocessor.cpp +++ b/src/modelchecker/multiobjective/pcaa/SparsePCAAPreprocessor.cpp @@ -66,10 +66,12 @@ namespace storm { result.actionsWithPositiveReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false); result.actionsWithNegativeReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false); for(uint_fast64_t objIndex = 0; objIndex < result.objectives.size(); ++objIndex) { - if(result.objectives[objIndex].rewardsArePositive) { - result.actionsWithPositiveReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix())); - } else { - result.actionsWithNegativeReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix())); + if(!result.objectives[objIndex].upperTimeBound) { + if(result.objectives[objIndex].rewardsArePositive) { + result.actionsWithPositiveReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix())); + } else { + result.actionsWithNegativeReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix())); + } } } @@ -371,6 +373,8 @@ namespace storm { result.possiblyRecurrentStates |= statesInCurrentECWithNeutralAction; }else{ // Check if the ec contains neutral sub ecs. This is done by adding the subECs to our list of ECs + // A neutral subEC only consist of states that can stay in statesInCurrentECWithNeutralAction + statesInCurrentECWithNeutralAction = storm::utility::graph::performProb0E(result.preprocessedModel.getTransitionMatrix(), result.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), backwardTransitions,statesInCurrentECWithNeutralAction, ~statesInCurrentECWithNeutralAction); auto subECs = storm::storage::MaximalEndComponentDecomposition(result.preprocessedModel.getTransitionMatrix(), backwardTransitions, statesInCurrentECWithNeutralAction); ecs.reserve(ecs.size() + subECs.size()); for(auto& ec : subECs){ diff --git a/src/modelchecker/multiobjective/pcaa/SparsePCAAPreprocessorReturnType.h b/src/modelchecker/multiobjective/pcaa/SparsePCAAPreprocessorReturnType.h index 271c85ebc..add8d7830 100644 --- a/src/modelchecker/multiobjective/pcaa/SparsePCAAPreprocessorReturnType.h +++ b/src/modelchecker/multiobjective/pcaa/SparsePCAAPreprocessorReturnType.h @@ -39,9 +39,9 @@ namespace storm { // Maps any state of the preprocessed model to the corresponding state of the original Model std::vector newToOldStateIndexMapping; - // The actions of the preprocessed model that have positive reward assigned for at least one objective + // The actions of the preprocessed model that have positive reward assigned for at least one objective (objectives with an upper time-bound are ignored!) storm::storage::BitVector actionsWithPositiveReward; - // The actions of the preprocessed model that have negative reward assigned for at least one objective + // The actions of the preprocessed model that have negative reward assigned for at least one objective (objectives with an upper time-bound are ignored!) storm::storage::BitVector actionsWithNegativeReward; // The actions of the preprocessed model that are part of an EC storm::storage::BitVector ecActions; diff --git a/src/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp b/src/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp index 0d4d879f3..d16fd9eb7 100644 --- a/src/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp +++ b/src/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp @@ -115,7 +115,6 @@ namespace storm { STORM_LOG_THROW(optimizationRes.second, storm::exceptions::UnexpectedException, "The underapproximation is either unbounded or empty."); result = optimizationRes.first[indexOfOptimizingObjective]; STORM_LOG_DEBUG("Best solution found so far is ~" << storm::utility::convertNumber(result) << "."); - thresholds[indexOfOptimizingObjective] = result; //Compute an upper bound for the optimum and check for convergence optimizationRes = this->overApproximation->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective); if(optimizationRes.second) { @@ -125,7 +124,10 @@ namespace storm { return result; } else { STORM_LOG_DEBUG("Solution can be improved by at most " << storm::utility::convertNumber(precisionOfResult)); + thresholds[indexOfOptimizingObjective] = optimizationRes.first[indexOfOptimizingObjective]; } + } else { + thresholds[indexOfOptimizingObjective] = result + storm::utility::one(); } WeightVector separatingVector = this->findSeparatingVector(thresholds); this->performRefinementStep(std::move(separatingVector)); diff --git a/src/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp b/src/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp index 45390e711..93b17c126 100644 --- a/src/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp +++ b/src/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp @@ -7,10 +7,12 @@ #include "src/modelchecker/multiobjective/pcaa/PcaaObjective.h" #include "src/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h" #include "src/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h" -#include "src/utility/constants.h" -#include "src/utility/vector.h" #include "src/settings//SettingsManager.h" #include "src/settings/modules/MultiObjectiveSettings.h" +#include "src/storage/geometry/Hyperrectangle.h" +#include "src/utility/constants.h" +#include "src/utility/vector.h" +#include "src/utility/export.h" #include "src/exceptions/UnexpectedException.h" @@ -44,12 +46,6 @@ namespace storm { this->weightVectorChecker = std::unique_ptr>>(new SparseMaPcaaWeightVectorChecker>(model, objectives, actionsWithNegativeReward, ecActions, possiblyRecurrentStates)); } - // template<> - // void SparsePcaaQuery, storm::RationalNumber>::initializeWeightVectorChecker(storm::models::sparse::MarkovAutomaton const& model, std::vector> const& objectives, storm::storage::BitVector const& actionsWithNegativeReward, storm::storage::BitVector const& ecActions, storm::storage::BitVector const& possiblyRecurrentStates) { - // this->weightVectorChecker = std::unique_ptr>>(new SparseMaPcaaWeightVectorChecker>(model, objectives, actionsWithNegativeReward, ecActions, possiblyRecurrentStates)); - // } - - template typename SparsePcaaQuery::WeightVector SparsePcaaQuery::findSeparatingVector(Point const& pointToBeSeparated) { STORM_LOG_DEBUG("Searching a weight vector to seperate the point given by " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(pointToBeSeparated)) << "."); @@ -193,12 +189,75 @@ namespace storm { return polytope->affineTransformation(transformationMatrix, transformationVector); } + template + void SparsePcaaQuery::exportPlotOfCurrentApproximation(std::string const& destinationDir) const { + + STORM_LOG_ERROR_COND(objectives.size()==2, "Exporting plot requested but this is only implemented for the two-dimensional case."); + + auto transformedUnderApprox = transformPolytopeToOriginalModel(underApproximation); + auto transformedOverApprox = transformPolytopeToOriginalModel(overApproximation); + + // Get pareto points as well as a hyperrectangle that is used to guarantee that the resulting polytopes are bounded. + storm::storage::geometry::Hyperrectangle boundaries(std::vector(objectives.size(), storm::utility::zero()), std::vector(objectives.size(), storm::utility::zero())); + std::vector> paretoPoints; + paretoPoints.reserve(refinementSteps.size()); + for(auto const& step : refinementSteps) { + paretoPoints.push_back(transformPointToOriginalModel(step.lowerBoundPoint)); + boundaries.enlarge(paretoPoints.back()); + } + auto underApproxVertices = transformedUnderApprox->getVertices(); + for(auto const& v : underApproxVertices) { + boundaries.enlarge(v); + } + auto overApproxVertices = transformedOverApprox->getVertices(); + for(auto const& v : overApproxVertices) { + boundaries.enlarge(v); + } + + //Further enlarge the boundaries a little + storm::utility::vector::scaleVectorInPlace(boundaries.lowerBounds(), GeometryValueType(15) / GeometryValueType(10)); + storm::utility::vector::scaleVectorInPlace(boundaries.upperBounds(), GeometryValueType(15) / GeometryValueType(10)); + + auto boundariesAsPolytope = boundaries.asPolytope(); + std::vector columnHeaders = {"x", "y"}; + + std::vector> pointsForPlotting; + underApproxVertices = transformedUnderApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder(); + pointsForPlotting.reserve(underApproxVertices.size()); + for(auto const& v : underApproxVertices) { + pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); + } + storm::utility::exportDataToCSVFile(destinationDir + "underapproximation.csv", pointsForPlotting, columnHeaders); + + pointsForPlotting.clear(); + overApproxVertices = transformedOverApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder(); + pointsForPlotting.reserve(overApproxVertices.size()); + for(auto const& v : overApproxVertices) { + pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); + } + storm::utility::exportDataToCSVFile(destinationDir + "overapproximation.csv", pointsForPlotting, columnHeaders); + + pointsForPlotting.clear(); + pointsForPlotting.reserve(paretoPoints.size()); + for(auto const& v : paretoPoints) { + pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); + } + storm::utility::exportDataToCSVFile(destinationDir + "paretopoints.csv", pointsForPlotting, columnHeaders); + + pointsForPlotting.clear(); + auto boundVertices = boundariesAsPolytope->getVerticesInClockwiseOrder(); + pointsForPlotting.reserve(4); + for(auto const& v : boundVertices) { + pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); + } + storm::utility::exportDataToCSVFile(destinationDir + "boundaries.csv", pointsForPlotting, columnHeaders); + } + #ifdef STORM_HAVE_CARL template class SparsePcaaQuery, storm::RationalNumber>; template class SparsePcaaQuery, storm::RationalNumber>; template class SparsePcaaQuery, storm::RationalNumber>; - // template class SparsePcaaQuery, storm::RationalNumber>; #endif } } diff --git a/src/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h b/src/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h index 4aba85b3b..962686d71 100644 --- a/src/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h +++ b/src/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h @@ -27,6 +27,14 @@ namespace storm { */ virtual std::unique_ptr check() = 0; + /* + * Exports the current approximations and the currently processed points into respective .csv files located at the given directory. + * The polytopes are represented as the set of vertices. + * Note that the approximations will be intersected with a (sufficiently large) hyperrectangle in order to ensure that the polytopes are bounded + * This only works for 2 dimensional queries. + */ + void exportPlotOfCurrentApproximation(std::string const& destinationDir) const; + protected: /* diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index c0bbe6efa..2253efef1 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -14,6 +14,8 @@ #include "src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" +#include "src/modelchecker/multiobjective/pcaa.h" + #include "src/solver/LpSolver.h" #include "src/settings/modules/GeneralSettings.h" @@ -41,7 +43,15 @@ namespace storm { template bool SparseMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true)); + if(formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true))) { + return true; + } else { + // Check whether we consider a multi-objective formula + // For multi-objective model checking, each initial state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude multiple initial states. + if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; + if(!checkTask.isOnlyInitialStatesRelevantSet()) return false; + return checkTask.getFormula().isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true)); + } } template @@ -145,7 +155,12 @@ namespace storm { std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeLongRunAverageProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } - + + template + std::unique_ptr SparseMdpPrctlModelChecker::checkMultiObjectiveFormula(CheckTask const& checkTask) { + return multiobjective::performPcaa(this->getModel(), checkTask.getFormula()); + } + template class SparseMdpPrctlModelChecker>; #ifdef STORM_HAVE_CARL diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 4ff9f153d..bd819541c 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -27,6 +27,7 @@ namespace storm { virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr checkMultiObjectiveFormula(CheckTask const& checkTask) override; private: // An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices. diff --git a/src/utility/export.h b/src/utility/export.h index 980f53409..bc8e7c156 100644 --- a/src/utility/export.h +++ b/src/utility/export.h @@ -41,7 +41,7 @@ namespace storm { } */ - void exportStringToFile(std::string const& str, std::string filepath) { + inline void exportStringToFile(std::string const& str, std::string filepath) { std::ofstream filestream; filestream.open(filepath); STORM_LOG_THROW(filestream.is_open(), storm::exceptions::FileIoException , "Could not open file " << filepath << "."); @@ -49,7 +49,7 @@ namespace storm { } template - void exportDataToCSVFile(std::string filepath, std::vector> const& data, boost::optional> const& columnHeaders) { + inline void exportDataToCSVFile(std::string filepath, std::vector> const& data, boost::optional> const& columnHeaders) { std::ofstream filestream; filestream.open(filepath); STORM_LOG_THROW(filestream.is_open(), storm::exceptions::FileIoException , "Could not open file " << filepath << "."); diff --git a/src/utility/storm.h b/src/utility/storm.h index c78906434..20f9b5771 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -71,8 +71,6 @@ #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h" #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" -#include "src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h" -#include "src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -306,20 +304,11 @@ namespace storm { template std::unique_ptr verifySparseMdp(std::shared_ptr> mdp, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; - if(task.getFormula().isMultiObjectiveFormula()) { - storm::modelchecker::SparseMdpMultiObjectiveModelChecker> modelchecker(*mdp); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); - } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported."); - } + storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); } else { - storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); - } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported."); - } + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported."); } return result; } @@ -331,20 +320,11 @@ namespace storm { if (!ma->isClosed()) { ma->close(); } - if(task.getFormula().isMultiObjectiveFormula()) { - storm::modelchecker::SparseMaMultiObjectiveModelChecker> modelchecker(*ma); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); - } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported."); - } + storm::modelchecker::SparseMarkovAutomatonCslModelChecker> modelchecker(*ma); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); } else { - storm::modelchecker::SparseMarkovAutomatonCslModelChecker> modelchecker(*ma); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); - } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported."); - } + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported."); } return result; } diff --git a/test/functional/modelchecker/SparseMaMultiObjectiveModelCheckerTest.cpp b/test/functional/modelchecker/SparseMaPcaaModelCheckerTest.cpp similarity index 88% rename from test/functional/modelchecker/SparseMaMultiObjectiveModelCheckerTest.cpp rename to test/functional/modelchecker/SparseMaPcaaModelCheckerTest.cpp index 6841588a0..5ed3e1a92 100644 --- a/test/functional/modelchecker/SparseMaMultiObjectiveModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMaPcaaModelCheckerTest.cpp @@ -3,7 +3,7 @@ #ifdef STORM_HAVE_HYPRO -#include "src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.h" +#include "src/modelchecker/multiobjective/pcaa.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ParetoCurveCheckResult.h" @@ -16,7 +16,7 @@ /* Rationals for MAs not supported at this point -TEST(SparseMaMultiObjectiveModelCheckerTest, serverRationalNumbers) { +TEST(SparseMaPcaaModelCheckerTest, serverRationalNumbers) { std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/ma/server/server.ma"; std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto @@ -29,7 +29,7 @@ TEST(SparseMaMultiObjectiveModelCheckerTest, serverRationalNumbers) { storm::generator::NextStateGeneratorOptions options(formulas); std::shared_ptr> ma = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); - storm::modelchecker::SparseMaMultiObjectiveModelChecker> checker(*ma); + storm::modelchecker::SparseMarkovAutomatonCslModelChecker> checker(*ma); std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); ASSERT_TRUE(result->isParetoCurveCheckResult()); @@ -47,7 +47,7 @@ TEST(SparseMaMultiObjectiveModelCheckerTest, serverRationalNumbers) { }*/ -TEST(SparseMaMultiObjectiveModelCheckerTest, server) { +TEST(SparseMaPcaaModelCheckerTest, server) { std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/ma/server/server.ma"; std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto @@ -59,9 +59,9 @@ TEST(SparseMaMultiObjectiveModelCheckerTest, server) { program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); std::shared_ptr> ma = storm::buildSparseModel(program, formulas, true)->as>(); - storm::modelchecker::SparseMaMultiObjectiveModelChecker> checker(*ma); + storm::modelchecker::SparseMarkovAutomatonCslModelChecker> checker(*ma); - std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); + std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isParetoCurveCheckResult()); std::vector p = {11.0/6.0, 1.0/2.0}; diff --git a/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp deleted file mode 100644 index f99939612..000000000 --- a/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp +++ /dev/null @@ -1,395 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#ifdef STORM_HAVE_HYPRO - -#include "src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h" -#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" -#include "src/models/sparse/Mdp.h" -#include "src/settings/modules/GeneralSettings.h" -#include "src/settings/SettingsManager.h" -#include "src/utility/storm.h" - - - -TEST(SparseMdpMultiObjectiveModelCheckerTest, probEqual1Objective) { - - std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/multiobjective1.nm"; - std::string formulasAsString = "multi(Rmax=? [ F s=2 ], P>=1 [ s=0 U s=1 ]) "; - formulasAsString += "; \n multi(Rmax=? [ F s=2 ], P>=1 [ F s=1 ]) "; - - // programm, model, formula - storm::prism::Program program = storm::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas, true)->as>(); - uint_fast64_t const initState = *mdp->getInitialStates().begin(); - - storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); - - std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(7.647057, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[1], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(7.647057, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); - -} - -TEST(SparseMdpMultiObjectiveModelCheckerTest, probEqual0Objective) { - - std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/multiobjective1.nm"; - std::string formulasAsString = "multi(Rmax=? [ F s=2 ], P<=0 [ s=0 U s=1 ]) "; - formulasAsString += "; \n multi(Rmax=? [ F s=2 ], P<=0 [ F s=1 ]) "; - - // programm, model, formula - storm::prism::Program program = storm::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas, true)->as>(); - uint_fast64_t const initState = *mdp->getInitialStates().begin(); - - storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); - - std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[1], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); - -} - -TEST(SparseMdpMultiObjectiveModelCheckerTest, preprocessorResultsTest) { - - std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/multiobjective2.nm"; - std::string formulasAsString = "multi(Rmin=? [ F s=2 ], P>=1 [ s!=1 U s=2 ]) "; - formulasAsString += "; \n multi(Rmax=? [ F s=2 ], P>=1 [ s!=1 U s=2 ]) "; - formulasAsString += "; \n multi(R<=0 [ F s=2 ], P>=1 [ s!=1 U s=2 ]) "; - formulasAsString += "; \n multi(R>0 [ F s=2 ], P>=1 [ s!=1 U s=2 ]) "; - formulasAsString += "; \n multi(Rmin=? [ F s=2 ], P>=1 [ F s=1 ], P>=1 [F s=2]) "; - formulasAsString += "; \n multi(Rmax=? [ F s=2 ], P>=1 [ F s=1 ], P>=1 [F s=2]) "; - formulasAsString += "; \n multi(R>=300 [ F s=2 ], P>=1 [ F s=1 ], P>=1 [F s=2]) "; - formulasAsString += "; \n multi(R<10 [ F s=2 ], P>=1 [ F s=1 ], P>=1 [F s=2]) "; - formulasAsString += "; \n multi(Rmin=? [ C ]) "; - formulasAsString += "; \n multi(Rmax=? [ C ]) "; - formulasAsString += "; \n multi(R>1 [ C ]) "; - formulasAsString += "; \n multi(R<1 [ C ]) "; - formulasAsString += "; \n multi(Pmax=? [ G true ]) "; - formulasAsString += "; \n multi(Pmin=? [ G true ]) "; - formulasAsString += "; \n multi(P>0.9 [ G true ]) "; - formulasAsString += "; \n multi(P>1 [ G true ]) "; - formulasAsString += "; \n multi(Pmax=? [ G false ]) "; - formulasAsString += "; \n multi(P>0 [ G false ]) "; - formulasAsString += "; \n multi(Pmin=? [ F \"init\" ]) "; - formulasAsString += "; \n multi(P>0.5 [ F \"init\" ]) "; - - // programm, model, formula - storm::prism::Program program = storm::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas, true)->as>(); - uint_fast64_t const initState = *mdp->getInitialStates().begin(); - - storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); - - std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[1], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[2], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[3], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[4], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(10.0, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[5], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_EQ(storm::utility::infinity(), result->asExplicitQuantitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[6], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[7], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[8], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_EQ(storm::utility::infinity(), result->asExplicitQuantitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[9], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_EQ(storm::utility::infinity(), result->asExplicitQuantitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[10], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[11], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[12], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_EQ(storm::utility::one(), result->asExplicitQuantitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[13], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_EQ(storm::utility::one(), result->asExplicitQuantitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[14], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[15], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[16], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_EQ(storm::utility::zero(), result->asExplicitQuantitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[17], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[18], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_EQ(storm::utility::one(), result->asExplicitQuantitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[19], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); - - -} - -TEST(SparseMdpMultiObjectiveModelCheckerTest, consensus) { - - std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/consensus/consensus2_3_2.nm"; - std::string formulasAsString = "multi(Pmax=? [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ]) "; // numerical - formulasAsString += "; \n multi(P>=0.1 [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ])"; // achievability (true) - formulasAsString += "; \n multi(P>=0.11 [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ])"; // achievability (false) - - // programm, model, formula - storm::prism::Program program = storm::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas, true)->as>(); - uint_fast64_t const initState = *mdp->getInitialStates().begin();; - - storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); - - std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(0.10833260970000025, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[1], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[2], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); - -} - -TEST(SparseMdpMultiObjectiveModelCheckerTest, zeroconf) { - - std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/zeroconf/zeroconf4.nm"; - std::string formulasAsString = "multi(Pmax=? [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ]) "; // numerical - formulasAsString += "; \n multi(P>=0.0003 [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ])"; // achievability (true) - formulasAsString += "; \n multi(P>=0.00031 [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ])"; // achievability (false) - - // programm, model, formula - storm::prism::Program program = storm::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas, true)->as>(); - uint_fast64_t const initState = *mdp->getInitialStates().begin(); - - storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); - - std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(0.0003075787401574803, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[1], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[2], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); - -} - -TEST(SparseMdpMultiObjectiveModelCheckerTest, zeroconfTb) { - - std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/zeroconf-tb/zeroconf-tb2_14.nm"; - std::string formulasAsString = " multi(Pmax=? [ F time_error=1 ] , P>=0.81[ G (error=0) ])"; // numerical - formulasAsString += "; \n multi(P>=0.00000008 [ F time_error=1 ] , P>=0.81[ G (error=0) ])"; // achievability (true) - formulasAsString += "; \n multi(P>=0.000000081 [ F time_error=1 ] , P>=0.81[ G (error=0) ])"; // achievability (false) - - // programm, model, formula - storm::prism::Program program = storm::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas, true)->as>(); - uint_fast64_t const initState = *mdp->getInitialStates().begin(); - - storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); - - std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(8.059348391417451e-8, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[1], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[2], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); - -} - -TEST(SparseMdpMultiObjectiveModelCheckerTest, team3with2objectives) { - - std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/team/team2obj_3.nm"; - std::string formulasAsString = " multi(Pmax=? [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ])"; // numerical - formulasAsString += "; \n multi(P>=0.871 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ])"; // achievability (true) - formulasAsString += "; \n multi(P>=0.872 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ])"; // achievability (false) - - // programm, model, formula - storm::prism::Program program = storm::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas, true)->as>(); - uint_fast64_t const initState = *mdp->getInitialStates().begin(); - - storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); - - std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(0.8714285710612256, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[1], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[2], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); - -} - -TEST(SparseMdpMultiObjectiveModelCheckerTest, team3with3objectives) { - - std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/team/team3obj_3.nm"; - std::string formulasAsString = "multi(Pmax=? [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F task2_completed ])"; // numerical - formulasAsString += "; \n multi(P>=0.744 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F task2_completed ])"; // achievability (true) - formulasAsString += "; \n multi(P>=0.745 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F task2_completed ])"; // achievability (false) - - // programm, model, formula - storm::prism::Program program = storm::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas, true)->as>(); - uint_fast64_t const initState = *mdp->getInitialStates().begin(); - - storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); - - std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(0.7448979591841851, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[1], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[2], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); - -} - -TEST(SparseMdpMultiObjectiveModelCheckerTest, scheduler) { - - std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/scheduler/scheduler05.nm"; - std::string formulasAsString = "multi(R{\"time\"}min=?[ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [ F \"tasks_complete\" ]) "; // numerical - formulasAsString += "; \n multi(R{\"time\"}<= 11.778[ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [ F \"tasks_complete\" ]) "; // achievability (true) - formulasAsString += "; \n multi(R{\"time\"}<= 11.777 [ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [ F \"tasks_complete\" ]) "; // achievability (false) - - // programm, model, formula - storm::prism::Program program = storm::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas, true)->as>(); - uint_fast64_t const initState = *mdp->getInitialStates().begin(); - - storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); - - std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(11.77777778, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[1], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[2], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); - -} - -TEST(SparseMdpMultiObjectiveModelCheckerTest, dpm) { - - std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/dpm/dpm100.nm"; - std::string formulasAsString = "multi(R{\"power\"}min=? [ C<=100 ], R{\"queue\"}<=70 [ C<=100 ])"; // numerical - formulasAsString += "; \n multi(R{\"power\"}<=121.613 [ C<=100 ], R{\"queue\"}<=70 [ C<=100 ])"; // achievability (true) - formulasAsString += "; \n multi(R{\"power\"}<=121.612 [ C<=100 ], R{\"queue\"}<=70 [ C<=100 ])"; // achievability (false) - - // programm, model, formula - storm::prism::Program program = storm::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas, true)->as>(); - uint_fast64_t const initState = *mdp->getInitialStates().begin(); - - storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); - - std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(121.61288420945114, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[1], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); - - result = checker.check(storm::modelchecker::CheckTask(*formulas[2], true)); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); - -} - - - - -#endif /* STORM_HAVE_HYPRO */ diff --git a/test/functional/modelchecker/SparseMdpPcaaModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpPcaaModelCheckerTest.cpp new file mode 100644 index 000000000..c5c08051f --- /dev/null +++ b/test/functional/modelchecker/SparseMdpPcaaModelCheckerTest.cpp @@ -0,0 +1,228 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#ifdef STORM_HAVE_HYPRO + +#include "src/modelchecker/multiobjective/pcaa.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "src/models/sparse/Mdp.h" +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/SettingsManager.h" +#include "src/utility/storm.h" + + +TEST(SparseMdpPcaaModelCheckerTest, consensus) { + + std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/consensus/consensus2_3_2.nm"; + std::string formulasAsString = "multi(Pmax=? [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ]) "; // numerical + formulasAsString += "; \n multi(P>=0.1 [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ])"; // achievability (true) + formulasAsString += "; \n multi(P>=0.11 [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ])"; // achievability (false) + + // programm, model, formula + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas, true)->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin();; + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(0.10833260970000025, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); + + result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[1]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + + result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[2]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); + +} + +TEST(SparseMdpPcaaModelCheckerTest, zeroconf) { + + std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/zeroconf/zeroconf4.nm"; + std::string formulasAsString = "multi(Pmax=? [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ]) "; // numerical + formulasAsString += "; \n multi(P>=0.0003 [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ])"; // achievability (true) + formulasAsString += "; \n multi(P>=0.00031 [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ])"; // achievability (false) + + // programm, model, formula + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas, true)->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin(); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(0.0003075787401574803, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); + + result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[1]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + + result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[2]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); + +} + +TEST(SparseMdpPcaaModelCheckerTest, zeroconfTb) { + + std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/zeroconf-tb/zeroconf-tb2_14.nm"; + std::string formulasAsString = " multi(Pmax=? [ F time_error=1 ] , P>=0.81[ G (error=0) ])"; // numerical + formulasAsString += "; \n multi(P>=0.00000008 [ F time_error=1 ] , P>=0.81[ G (error=0) ])"; // achievability (true) + formulasAsString += "; \n multi(P>=0.000000081 [ F time_error=1 ] , P>=0.81[ G (error=0) ])"; // achievability (false) + + // programm, model, formula + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas, true)->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin(); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(8.059348391417451e-8, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); + + result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[1]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + + result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[2]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); + +} + +TEST(SparseMdpPcaaModelCheckerTest, team3with2objectives) { + + std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/team/team2obj_3.nm"; + std::string formulasAsString = " multi(Pmax=? [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ])"; // numerical + formulasAsString += "; \n multi(P>=0.871 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ])"; // achievability (true) + formulasAsString += "; \n multi(P>=0.872 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ])"; // achievability (false) + + // programm, model, formula + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas, true)->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin(); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(0.8714285710612256, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); + + result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[1]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + + result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[2]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); + +} + +TEST(SparseMdpPcaaModelCheckerTest, team3with3objectives) { + + std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/team/team3obj_3.nm"; + std::string formulasAsString = "multi(Pmax=? [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F task2_completed ])"; // numerical + formulasAsString += "; \n multi(P>=0.744 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F task2_completed ])"; // achievability (true) + formulasAsString += "; \n multi(P>=0.745 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F task2_completed ])"; // achievability (false) + + // programm, model, formula + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas, true)->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin(); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(0.7448979591841851, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); + + result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[1]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + + result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[2]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); + +} + +TEST(SparseMdpPcaaModelCheckerTest, scheduler) { + + std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/scheduler/scheduler05.nm"; + std::string formulasAsString = "multi(R{\"time\"}min=?[ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [ F \"tasks_complete\" ]) "; // numerical + formulasAsString += "; \n multi(R{\"time\"}<= 11.778[ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [ F \"tasks_complete\" ]) "; // achievability (true) + formulasAsString += "; \n multi(R{\"time\"}<= 11.777 [ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [ F \"tasks_complete\" ]) "; // achievability (false) + + // programm, model, formula + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas, true)->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin(); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(11.77777778, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); + + result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[1]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + + result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[2]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); + +} + +TEST(SparseMdpPcaaModelCheckerTest, dpm) { + + std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/dpm/dpm100.nm"; + std::string formulasAsString = "multi(R{\"power\"}min=? [ C<=100 ], R{\"queue\"}<=70 [ C<=100 ])"; // numerical + formulasAsString += "; \n multi(R{\"power\"}<=121.613 [ C<=100 ], R{\"queue\"}<=70 [ C<=100 ])"; // achievability (true) + formulasAsString += "; \n multi(R{\"power\"}<=121.612 [ C<=100 ], R{\"queue\"}<=70 [ C<=100 ])"; // achievability (false) + + // programm, model, formula + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas, true)->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin(); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(121.61288420945114, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); + + result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[1]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + + result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[2]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); + +} + + + + +#endif /* STORM_HAVE_HYPRO */ diff --git a/test/functional/transformer/EndComponentEliminatorTest.cpp b/test/functional/transformer/EndComponentEliminatorTest.cpp index 2210eafc8..9a990f409 100644 --- a/test/functional/transformer/EndComponentEliminatorTest.cpp +++ b/test/functional/transformer/EndComponentEliminatorTest.cpp @@ -34,6 +34,9 @@ TEST(NeutralECRemover, SimpleModelTest) { storm::storage::SparseMatrix matrix; ASSERT_NO_THROW(matrix = builder.build()); + storm::storage::BitVector subsystem(5, true); + subsystem.set(2, false); + storm::storage::BitVector possibleEcRows(12, true); possibleEcRows.set(3, false); possibleEcRows.set(6, false); @@ -44,8 +47,7 @@ TEST(NeutralECRemover, SimpleModelTest) { storm::storage::BitVector allowEmptyRows(5, true); allowEmptyRows.set(1, false); allowEmptyRows.set(4, false); - storm::storage::BitVector subsystem(5, true); - allowEmptyRows.set(2, false); + auto res = storm::transformer::EndComponentEliminator::transform(matrix, subsystem, possibleEcRows, allowEmptyRows);