diff --git a/README.md b/README.md index aeb2fa0f5..9220d2dfd 100644 --- a/README.md +++ b/README.md @@ -1,68 +1,3 @@ -Storm - A Modern Probabilistic Model Checker +Tempest - A Shield Synthesis Tool ============================================ -[![Build Status](https://github.com/moves-rwth/storm/workflows/Build%20Test/badge.svg)](https://github.com/moves-rwth/storm/actions) -[![GitHub release](https://img.shields.io/github/release/moves-rwth/storm.svg)](https://github.com/moves-rwth/storm/releases/) -[![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.1181896.svg)](https://doi.org/10.5281/zenodo.1181896) - - -For more instructions, check out the documentation found in [Getting Started](http://www.stormchecker.org/getting-started.html). - - -Benchmarks ----------------------------- - -Example input files for Storm can be obtained from -https://github.com/moves-rwth/storm-examples. - -Various Benchmarks together with example invocations of Storm can be found at the [Quantitative Verification Benchmark Set (QVBS)](http://qcomp.org/benchmarks). - -Further examples and benchmarks can be found in the following repositories: - -* **Prism files** (DTMC, MDP, CTMC): -http://www.prismmodelchecker.org/benchmarks -* **Jani files** (DTMC, MDP, CTMC, MA): -http://jani-spec.org -* **GSPN**s: -(private, contact: sebastian.junges@cs.rwth-aachen.de) -* **DFT**s: -https://github.com/moves-rwth/dft-examples -* **PGCL**: -(private, contact: sebastian.junges@cs.rwth-aachen.de) - - -Authors ------------------------------ -Storm has been developed at RWTH Aachen University. - -###### Principal developers -* Christian Hensel -* Sebastian Junges -* Joost-Pieter Katoen -* Tim Quatmann -* Matthias Volk - -###### Developers (lexicographical order) -* Jana Berger -* Alexander Bork -* David Korzeniewski -* Jip Spel - -###### Contributors (lexicographical order) -* Daniel Basgöze -* Dimitri Bohlender -* Harold Bruintjes -* Michael Deutschen -* Linus Heck -* Thomas Heinemann -* Thomas Henn -* Tom Janson -* Jan Karuc -* Joachim Klein -* Gereon Kremer -* Sascha Vincent Kurowski -* Hannah Mertens -* Stefan Pranger -* Svenja Stein -* Manuel Sascha Weiand -* Lukas Westhofen diff --git a/resources/3rdparty/cudd-3.0.0/config.h.in b/resources/3rdparty/cudd-3.0.0/config.h.in index 1bea1dd11..8d78585dd 100644 --- a/resources/3rdparty/cudd-3.0.0/config.h.in +++ b/resources/3rdparty/cudd-3.0.0/config.h.in @@ -33,9 +33,6 @@ /* Define to 1 if you have the header file. */ #undef HAVE_MATH_H -/* Define to 1 if you have the header file. */ -#undef HAVE_MEMORY_H - /* Define to 1 if your compiler supports enough C++11 */ #undef HAVE_MODERN_CXX @@ -57,6 +54,9 @@ /* Define to 1 if you have the header file. */ #undef HAVE_STDINT_H +/* Define to 1 if you have the header file. */ +#undef HAVE_STDIO_H + /* Define to 1 if you have the header file. */ #undef HAVE_STDLIB_H @@ -139,7 +139,9 @@ /* The size of `void *', as computed by sizeof. */ #undef SIZEOF_VOID_P -/* Define to 1 if you have the ANSI C header files. */ +/* Define to 1 if all of the C90 standard headers exist (not just the ones + required in a freestanding environment). This macro is provided for + backward compatibility; new code need not use it. */ #undef STDC_HEADERS /* Define to 1 to use system qsort */ diff --git a/resources/examples/testfiles/smg/example_smg.nm b/resources/examples/testfiles/smg/example_smg.nm new file mode 100644 index 000000000..875070051 --- /dev/null +++ b/resources/examples/testfiles/smg/example_smg.nm @@ -0,0 +1,32 @@ +// taken from Julia Eisentraut "Value iteration for simple stochastic games: Stopping criterion +// and learning algorithm" - Fig. 1 + + +smg + +const double p = 2/3; + +player maxP + [q_action1], [q_action2] +endplayer + +player minP + [p_action1] +endplayer + +player sinkstates + state_space +endplayer + + +module state_space + s : [0..3]; + + [p_action1] s=0 -> (s'=1); + + [q_action1] s=1 -> (s'=0); + [q_action2] s=1 -> (1-p) : (s'=1) + (p/2) : (s'=2) + (p/2) : (s'=3); + + [] s=2 -> true; + [] s=3 -> true; +endmodule diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index e41bdf47f..cb915a005 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -49,6 +49,11 @@ #include "storm/settings/modules/HintSettings.h" #include "storm/storage/Qvbs.h" +#include "storm/shields/AbstractShield.h" +#include "storm/shields/PreShield.h" +#include "storm/shields/PostShield.h" +#include "storm/shields/OptimalShield.h" + #include "storm/utility/Stopwatch.h" namespace storm { @@ -1043,6 +1048,27 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export not supported for this property."); } } + if (ioSettings.isExportShieldSet()) { + if (result->isExplicitQuantitativeCheckResult()) { + if (result-> template asExplicitQuantitativeCheckResult().hasShield()) { + auto shield = result->template asExplicitQuantitativeCheckResult().getShield(); + if(shield->isPreShield()) { + shield->asPreShield().construct(); + } else if(shield->isPostShield()) { + shield->asPostShield().construct(); + } else if(shield->isOptimalShield()) { + shield->asOptimalShield().construct(); + } + + STORM_PRINT_AND_LOG("Exporting shield ... "); + + STORM_LOG_WARN_COND(exportCount == 0, "Prepending " << exportCount << " to file name for this property because there are multiple properties."); + storm::api::exportShield(sparseModel, shield, (exportCount == 0 ? std::string("") : std::to_string(exportCount)) + ioSettings.getExportShieldFilename()); + } + } + } + + if (ioSettings.isExportCheckResultSet()) { STORM_LOG_WARN_COND(sparseModel->hasStateValuations(), "No information of state valuations available. The result output will use internal state ids. You might be interested in building the model with state valuations using --buildstateval."); STORM_LOG_WARN_COND(exportCount == 0, "Prepending " << exportCount << " to file name for this property because there are multiple properties."); diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 53f3ba6c8..afb21561b 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -180,7 +180,7 @@ namespace storm { constantDefinition.name("constant definition"); // Shielding properties - shieldExpression = (qi::lit("<") > label > qi::lit(",") > shieldingType > -(qi::lit(",") > shieldComparison) > qi::lit(">"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3)]; + shieldExpression = (qi::lit("<") > shieldingType > -(qi::lit(",") > shieldComparison) > qi::lit(">"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldExpression, phoenix::ref(*this), qi::_1, qi::_2)]; shieldExpression.name("shield expression"); @@ -645,12 +645,12 @@ namespace storm { return std::make_pair(comparisonType, value); } - std::shared_ptr FormulaParserGrammar::createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional> comparisonStruct) { + std::shared_ptr FormulaParserGrammar::createShieldExpression(storm::logic::ShieldingType type, boost::optional> comparisonStruct) { if(comparisonStruct.is_initialized()) { - return std::shared_ptr(new storm::logic::ShieldExpression(type, name, comparisonStruct.get().first, comparisonStruct.get().second)); + return std::shared_ptr(new storm::logic::ShieldExpression(type, comparisonStruct.get().first, comparisonStruct.get().second)); } else { STORM_LOG_INFO("Construction of shield without a comparison parameter (lambda or gamma) will default to 'lambda=0'"); - return std::shared_ptr(new storm::logic::ShieldExpression(type, name)); + return std::shared_ptr(new storm::logic::ShieldExpression(type)); } } diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index 97089658e..c4916ffbb 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -249,7 +249,7 @@ namespace storm { std::shared_ptr createGameFormula(storm::logic::PlayerCoalition const& coalition, std::shared_ptr const& subformula) const; std::pair createShieldComparisonStruct(storm::logic::ShieldComparison comparisonType, double value); - std::shared_ptr createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional> comparisonStruct); + std::shared_ptr createShieldExpression(storm::logic::ShieldingType type, boost::optional> comparisonStruct); bool areConstantDefinitionsAllowed() const; void addConstant(std::string const& name, ConstantDataType type, boost::optional const& expression); diff --git a/src/storm/api/export.h b/src/storm/api/export.h index 6f4b82f77..452e957d2 100644 --- a/src/storm/api/export.h +++ b/src/storm/api/export.h @@ -11,6 +11,7 @@ #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/exceptions/NotSupportedException.h" +#include "storm/shields/AbstractShield.h" namespace storm { @@ -62,6 +63,19 @@ namespace storm { } storm::utility::closeFile(stream); } + + template + void exportShield(std::shared_ptr> const& model, std::shared_ptr> const& shield, std::string const& filename) { + std::ofstream stream; + storm::utility::openFile(filename, stream); + std::string jsonFileExtension = ".json"; + if (filename.size() > 4 && std::equal(jsonFileExtension.rbegin(), jsonFileExtension.rend(), filename.rbegin())) { + shield->printJsonToStream(stream, model); + } else { + shield->printToStream(stream, model); + } + storm::utility::closeFile(stream); + } template inline void exportCheckResultToJson(std::shared_ptr> const& model, std::unique_ptr const& checkResult, std::string const& filename) { diff --git a/src/storm/api/verification.h b/src/storm/api/verification.h index 868c00be3..3abb50803 100644 --- a/src/storm/api/verification.h +++ b/src/storm/api/verification.h @@ -458,7 +458,7 @@ namespace storm { template typename std::enable_if::value, std::unique_ptr>::type verifyWithDdEngine(storm::Environment const&, std::shared_ptr> const&, storm::modelchecker::CheckTask const&) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Dd engine cannot verify MDPs with this data type."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, ""); } template diff --git a/src/storm/logic/ShieldExpression.cpp b/src/storm/logic/ShieldExpression.cpp index 841d1a400..9902f625a 100644 --- a/src/storm/logic/ShieldExpression.cpp +++ b/src/storm/logic/ShieldExpression.cpp @@ -6,11 +6,11 @@ namespace storm { namespace logic { ShieldExpression::ShieldExpression() {} - ShieldExpression::ShieldExpression(ShieldingType type, std::string filename) : type(type), filename(filename) { + ShieldExpression::ShieldExpression(ShieldingType type) : type(type) { //Intentionally left empty } - ShieldExpression::ShieldExpression(ShieldingType type, std::string filename, ShieldComparison comparison, double value) : type(type), filename(filename), comparison(comparison), value(value) { + ShieldExpression::ShieldExpression(ShieldingType type, ShieldComparison comparison, double value) : type(type), comparison(comparison), value(value) { //Intentionally left empty } @@ -74,11 +74,7 @@ namespace storm { prettyString += "-Shield "; prettyString += "with " + comparisonType + " comparison (" + comparisonToString() + " = " + std::to_string(value) + "):"; return prettyString; - } - - std::string ShieldExpression::getFilename() const { - return filename; - } + } std::ostream& operator<<(std::ostream& out, ShieldExpression const& shieldExpression) { out << shieldExpression.toString(); diff --git a/src/storm/logic/ShieldExpression.h b/src/storm/logic/ShieldExpression.h index 808ebddf9..eddf0becb 100644 --- a/src/storm/logic/ShieldExpression.h +++ b/src/storm/logic/ShieldExpression.h @@ -18,8 +18,8 @@ namespace storm { class ShieldExpression { public: ShieldExpression(); - ShieldExpression(ShieldingType type, std::string filename); - ShieldExpression(ShieldingType type, std::string filename, ShieldComparison comparison, double value); + ShieldExpression(ShieldingType type); + ShieldExpression(ShieldingType type, ShieldComparison comparison, double value); bool isRelative() const; bool isPreSafetyShield() const; @@ -34,15 +34,12 @@ namespace storm { std::string comparisonToString() const; std::string toString() const; std::string prettify() const; - std::string getFilename() const; friend std::ostream& operator<<(std::ostream& stream, ShieldExpression const& shieldExpression); private: ShieldingType type; ShieldComparison comparison = ShieldComparison::Relative; double value = 0; - - std::string filename; }; } } diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp new file mode 100644 index 000000000..6b8f63739 --- /dev/null +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp @@ -0,0 +1,311 @@ +#include "SparseSmgLraHelper.h" + +#include "storm/storage/MaximalEndComponent.h" +#include "storm/storage/StronglyConnectedComponent.h" + +#include "storm/utility/graph.h" +#include "storm/utility/vector.h" +#include "storm/utility/macros.h" +#include "storm/utility/SignalHandler.h" + +#include "storm/environment/solver/SolverEnvironment.h" +#include "storm/environment/solver/LongRunAverageSolverEnvironment.h" +#include "storm/environment/solver/MinMaxSolverEnvironment.h" +#include "storm/environment/solver/MultiplierEnvironment.h" +#include "storm/environment/solver/GameSolverEnvironment.h" + +#include "modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h" +#include "storm/exceptions/UnmetRequirementException.h" + +#define SOLVE_MDP 50 + +namespace storm { + namespace modelchecker { + namespace helper { + namespace internal { + + template + SparseSmgLraHelper::SparseSmgLraHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) { + + } + + template + std::vector SparseSmgLraHelper::computeLongRunAverageRewardsSound(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel) { + std::vector result; + std::vector stateRewardsGetter = std::vector(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); + if (rewardModel.hasStateRewards()) { + stateRewardsGetter = rewardModel.getStateRewardVector(); + } + ValueGetter actionRewardsGetter; + if (rewardModel.hasStateActionRewards() || rewardModel.hasTransitionRewards()) { + if (rewardModel.hasTransitionRewards()) { + actionRewardsGetter = [&] (uint64_t globalChoiceIndex) { return rewardModel.getStateActionAndTransitionReward(globalChoiceIndex, this->_transitionMatrix); }; + } else { + actionRewardsGetter = [&] (uint64_t globalChoiceIndex) { return rewardModel.getStateActionReward(globalChoiceIndex); }; + } + } else { + actionRewardsGetter = [] (uint64_t) { return storm::utility::zero(); }; + } + _b = getBVector(stateRewardsGetter, actionRewardsGetter); + + // If requested, allocate memory for the choices made + if (this->_produceScheduler) { + if (!this->_producedOptimalChoices.is_initialized()) { + _producedOptimalChoices.emplace(); + } + _producedOptimalChoices->resize(_transitionMatrix.getRowGroupCount()); + } + + prepareMultiplier(env, rewardModel); + performValueIteration(env, rewardModel, _b, result); + + return result; + } + + template + std::vector SparseSmgLraHelper::getBVector(std::vector const& stateRewardsGetter, ValueGetter const& actionRewardsGetter) { + std::vector b = std::vector(_transitionMatrix.getRowCount()); + size_t globalChoiceCount = 0; + auto rowGroupIndices = _transitionMatrix.getRowGroupIndices(); + for (size_t state = 0; state < _transitionMatrix.getRowGroupCount(); state++) { + size_t rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; + for (size_t choice = 0; choice < rowGroupSize; choice++, globalChoiceCount++) + { + b[globalChoiceCount] = stateRewardsGetter[state] + actionRewardsGetter(globalChoiceCount); + } + } + return b; + } + + template + void SparseSmgLraHelper::performValueIteration(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const& b, std::vector& result) + { + std::vector choicesForStrategies = std::vector(_transitionMatrix.getRowGroupCount(), 0); + auto precision = storm::utility::convertNumber(env.solver().lra().getPrecision()); + + Environment envMinMax = env; + envMinMax.solver().lra().setPrecision(precision / storm::utility::convertNumber(2)); + do + { + size_t iteration_count = 0; + // Convergent recommender procedure + + _multiplier->multiplyAndReduce(env, _optimizationDirection, xNew(), &b, xNew(), &choicesForStrategies, &_statesOfCoalition); + + if (iteration_count % SOLVE_MDP == 0) { // only every 50th iteration + storm::storage::BitVector fixedMaxStrat = getStrategyFixedBitVec(choicesForStrategies, MinMaxStrategy::MaxStrategy); + storm::storage::BitVector fixedMinStrat = getStrategyFixedBitVec(choicesForStrategies, MinMaxStrategy::MinStrategy); + + // compute bounds + if (fixedMaxStrat != _fixedMaxStrat) { + storm::storage::SparseMatrix restrictedMaxMatrix = _transitionMatrix.restrictRows(fixedMaxStrat); + + storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper MaxSolver(restrictedMaxMatrix); + + MaxSolver.setOptimizationDirection(OptimizationDirection::Minimize); + MaxSolver.setProduceChoiceValues(false); + _resultForMax = MaxSolver.computeLongRunAverageRewards(envMinMax, rewardModel); + _fixedMaxStrat = fixedMaxStrat; + + for (size_t i = 0; i < xNewL().size(); i++) { + xNewL()[i] = std::max(xNewL()[i], _resultForMax[i]); + } + } + + if (fixedMinStrat != _fixedMinStrat) { + storm::storage::SparseMatrix restrictedMinMatrix = _transitionMatrix.restrictRows(fixedMinStrat); + + storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper MinSolver(restrictedMinMatrix); + MinSolver.setOptimizationDirection(OptimizationDirection::Maximize); + MinSolver.setProduceChoiceValues(false); + _resultForMin = MinSolver.computeLongRunAverageRewards(envMinMax, rewardModel); + _fixedMinStrat = fixedMinStrat; + + for (size_t i = 0; i < xNewU().size(); i++) { + xNewU()[i] = std::min(xNewU()[i], _resultForMin[i]); + } + } + } + + } while (!checkConvergence(precision)); + + if (_produceScheduler) { + _multiplier->multiplyAndReduce(env, _optimizationDirection, xNew(), &b, xNew(), &_producedOptimalChoices.get(), &_statesOfCoalition); + } + + if (_produceChoiceValues) { + if (!this->_choiceValues.is_initialized()) { + this->_choiceValues.emplace(); + } + this->_choiceValues->resize(this->_transitionMatrix.getRowCount()); + _choiceValues = calcChoiceValues(env, rewardModel); + } + result = xNewL(); + } + + + template + storm::storage::BitVector SparseSmgLraHelper::getStrategyFixedBitVec(std::vector const& choices, MinMaxStrategy strategy) { + storm::storage::BitVector restrictBy(_transitionMatrix.getRowCount(), true); + auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices(); + + for(uint state = 0; state < _transitionMatrix.getRowGroupCount(); state++) { + if ((_minimizerStates[state] && strategy == MinMaxStrategy::MaxStrategy) || (!_minimizerStates[state] && strategy == MinMaxStrategy::MinStrategy)) + continue; + + uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; + for(uint rowGroupIndex = 0; rowGroupIndex < rowGroupSize; rowGroupIndex++) { + if ((rowGroupIndex) != choices[state]) { + restrictBy.set(rowGroupIndex + rowGroupIndices[state], false); + } + } + } + return restrictBy; + } + + template + std::vector SparseSmgLraHelper::calcChoiceValues(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel) { + std::vector choiceValues(_transitionMatrix.getRowCount()); + _multiplier->multiply(env, xNewL(), nullptr, choiceValues); + + return choiceValues; + } + + template + std::vector SparseSmgLraHelper::getChoiceValues() const { + STORM_LOG_ASSERT(_produceChoiceValues, "Trying to get the computed choice values although this was not requested."); + STORM_LOG_ASSERT(this->_choiceValues.is_initialized(), "Trying to get the computed choice values but none were available. Was there a computation call before?"); + return this->_choiceValues.get(); + } + + template + storm::storage::Scheduler SparseSmgLraHelper::extractScheduler() const{ + auto const& optimalChoices = getProducedOptimalChoices(); + storm::storage::Scheduler scheduler(optimalChoices.size()); + + for (uint64_t state = 0; state < optimalChoices.size(); ++state) { + scheduler.setChoice(optimalChoices[state], state); + } + + return scheduler; + } + + template + std::vector const& SparseSmgLraHelper::getProducedOptimalChoices() const { + STORM_LOG_ASSERT(_produceScheduler, "Trying to get the produced optimal choices although no scheduler was requested."); + STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?"); + + return this->_producedOptimalChoices.get(); + } + + template + void SparseSmgLraHelper::prepareMultiplier(const Environment& env, storm::models::sparse::StandardRewardModel const& rewardModel) + { + _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); + if (_statesOfCoalition.size()) { + _minimizerStates = _optimizationDirection == OptimizationDirection::Maximize ? _statesOfCoalition : ~_statesOfCoalition; + } + else { + _minimizerStates = storm::storage::BitVector(_transitionMatrix.getRowGroupCount(), _optimizationDirection == OptimizationDirection::Minimize); + } + + _xL = std::vector(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); + _x = _xL; + + _fixedMaxStrat = storm::storage::BitVector(_transitionMatrix.getRowCount(), false); + _fixedMinStrat = storm::storage::BitVector(_transitionMatrix.getRowCount(), false); + + _resultForMin = std::vector(_transitionMatrix.getRowGroupCount()); + _resultForMax = std::vector(_transitionMatrix.getRowGroupCount()); + + _xU = std::vector(_transitionMatrix.getRowGroupCount(), std::numeric_limits::infinity()); + } + + template + bool SparseSmgLraHelper::checkConvergence(ValueType threshold) const { + STORM_LOG_ASSERT(_multiplier, "tried to check for convergence without doing an iteration first."); + // Now check whether the currently produced results are precise enough + STORM_LOG_ASSERT(threshold > storm::utility::zero(), "Did not expect a non-positive threshold."); + auto x1It = xNewL().begin(); + auto x1Ite = xNewL().end(); + auto x2It = xNewU().begin(); + for (; x1It != x1Ite; x1It++, x2It++) { + ValueType diff = (*x2It - *x1It); + if (diff > threshold) { + return false; + } + } + return true; + } + + template + std::vector& SparseSmgLraHelper::xNewL() { + return _xL; + } + + template + std::vector const& SparseSmgLraHelper::xNewL() const { + return _xL; + } + + template + std::vector& SparseSmgLraHelper::xNewU() { + return _xU; + } + + template + std::vector const& SparseSmgLraHelper::xNewU() const { + return _xU; + } + + template + std::vector& SparseSmgLraHelper::xNew() { + return _x; + } + + template + std::vector const& SparseSmgLraHelper::xNew() const { + return _x; + } + + + template + void SparseSmgLraHelper::setRelevantStates(storm::storage::BitVector relevantStates){ + _relevantStates = relevantStates; + } + + template + void SparseSmgLraHelper::setValueThreshold(storm::logic::ComparisonType const& comparisonType, const ValueType &thresholdValue) { + _valueThreshold = std::make_pair(comparisonType, thresholdValue); + } + + template + void SparseSmgLraHelper::setOptimizationDirection(storm::solver::OptimizationDirection const& direction) { + _optimizationDirection = direction; + } + + template + void SparseSmgLraHelper::setProduceScheduler(bool value) { + _produceScheduler = value; + } + + template + void SparseSmgLraHelper::setProduceChoiceValues(bool value) { + _produceChoiceValues = value; + } + + template + void SparseSmgLraHelper::setQualitative(bool value) { + _isQualitativeSet = value; + } + + template class SparseSmgLraHelper; +#ifdef STORM_HAVE_CARL + template class SparseSmgLraHelper; +#endif + + } + } + } +} + diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h new file mode 100644 index 000000000..4a6537945 --- /dev/null +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h @@ -0,0 +1,108 @@ +#pragma once + +#include "storm/storage/SparseMatrix.h" +#include "storm/storage/BitVector.h" +#include "storm/solver/LinearEquationSolver.h" +#include "storm/solver/MinMaxLinearEquationSolver.h" +#include "storm/solver/Multiplier.h" +#include "storm/logic/ComparisonType.h" + + +namespace storm { + class Environment; + + + namespace modelchecker { + namespace helper { + namespace internal { + + enum class MinMaxStrategy { + MaxStrategy, + MinStrategy + }; + + template + class SparseSmgLraHelper { + public: + // Function mapping from indices to values + typedef std::function ValueGetter; + + SparseSmgLraHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const statesOfCoalition); + + void performValueIteration(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const& b, std::vector& result); + + std::vector getChoiceValues() const; + + storm::storage::Scheduler extractScheduler() const; + + std::vector const& getProducedOptimalChoices() const; + + void prepareMultiplier(const Environment& env, storm::models::sparse::StandardRewardModel const& rewardModel); + + std::vector computeLongRunAverageRewardsSound(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel); + + void setRelevantStates(storm::storage::BitVector relevantStates); + + void setValueThreshold(storm::logic::ComparisonType const& comparisonType, ValueType const& thresholdValue); + + void setOptimizationDirection(storm::solver::OptimizationDirection const& direction); + + void setProduceScheduler(bool value); + + void setProduceChoiceValues(bool value); + + void setQualitative(bool value); + + private: + + bool checkConvergence(ValueType threshold) const; + + storm::storage::BitVector getStrategyFixedBitVec(std::vector const& choices, MinMaxStrategy strategy); + + std::vector getBVector(std::vector const& stateRewardsGetter, ValueGetter const& actionRewardsGetter); + + std::vector calcChoiceValues(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel); + + std::vector& xNew(); + std::vector const& xNew() const; + + std::vector& xNewL(); + std::vector const& xNewL() const; + + std::vector& xNewU(); + std::vector const& xNewU() const; + + storm::storage::SparseMatrix const& _transitionMatrix; + storm::storage::BitVector const _statesOfCoalition; + + storm::storage::BitVector _relevantStates; + storm::storage::BitVector _minimizerStates; + + storm::storage::BitVector _fixedMinStrat; + storm::storage::BitVector _fixedMaxStrat; + std::vector _resultForMax; + std::vector _resultForMin; + + std::vector _b; + + boost::optional> _valueThreshold; + storm::solver::OptimizationDirection _optimizationDirection; + bool _produceScheduler; + bool _produceChoiceValues; + bool _isQualitativeSet; + + std::vector _x, _xL, _xU; + std::vector _Tsx1, _Tsx2, _TsChoiceValues; + std::vector _Isx, _Isb, _IsChoiceValues; + std::unique_ptr> _multiplier; + std::unique_ptr> _Solver; + std::unique_ptr> _DetIsSolver; + std::unique_ptr _IsSolverEnv; + + boost::optional> _producedOptimalChoices; + boost::optional> _choiceValues; + }; + } + } + } +} diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 5a96c23ef..a4001036f 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -45,7 +45,7 @@ namespace storm { template bool SparseMdpPrctlModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isInFragment(storm::logic::prctlstar().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true))) { + if (formula.isInFragment(storm::logic::prctlstar().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setBoundedGloballyFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true))) { return true; } else if (checkTask.isOnlyInitialStatesRelevantSet()) { auto multiObjectiveFragment = storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true).setTimeBoundedCumulativeRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setRewardAccumulationAllowed(true); @@ -69,6 +69,34 @@ namespace storm { } } + template + std::unique_ptr SparseMdpPrctlModelChecker::computeBoundedGloballyProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::BoundedGloballyFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound."); + STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula lower step bound must be discrete/integral."); + STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); + std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + storm::modelchecker::helper::SparseNondeterministicStepBoundedHorizonHelper helper; + std::vector numericResult; + + //This works only with empty vectors, no nullptr + storm::storage::BitVector resultMaybeStates; + std::vector choiceValues; + + storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); + numericResult = helper.compute(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), allStatesBv, ~subResult.getTruthValuesVector(), pathFormula.getNonStrictLowerBound(), pathFormula.getNonStrictUpperBound(), resultMaybeStates, choiceValues, checkTask.getHint()); + // flip directions TODO + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + if(checkTask.isShieldingTask()) { + auto shield = tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(resultMaybeStates), storm::storage::BitVector(resultMaybeStates.size(), true)); + result->asExplicitQuantitativeCheckResult().setShield(std::move(shield)); + } + + return result; + } + template std::unique_ptr SparseMdpPrctlModelChecker::computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); @@ -100,10 +128,13 @@ namespace storm { std::vector choiceValues; numericResult = helper.compute(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictLowerBound(), pathFormula.getNonStrictUpperBound(), resultMaybeStates, choiceValues, checkTask.getHint()); + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(numericResult))); if(checkTask.isShieldingTask()) { - tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(resultMaybeStates), storm::storage::BitVector(resultMaybeStates.size(), true)); + auto shield = tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(resultMaybeStates), storm::storage::BitVector(resultMaybeStates.size(), true)); + result->asExplicitQuantitativeCheckResult().setShield(std::move(shield)); } - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + + return result; } } @@ -116,8 +147,10 @@ namespace storm { auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNextProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { - tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.maybeStates), storm::storage::BitVector(ret.maybeStates.size(), true)); - } else if (checkTask.isProduceSchedulersSet() && ret.scheduler) { + auto shield = tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.maybeStates), storm::storage::BitVector(ret.maybeStates.size(), true)); + result->asExplicitQuantitativeCheckResult().setShield(std::move(shield)); + } + if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); } return result; @@ -134,8 +167,11 @@ namespace storm { auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), checkTask.getHint()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { - tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.maybeStates), storm::storage::BitVector(ret.maybeStates.size(), true)); - } else if (checkTask.isProduceSchedulersSet() && ret.scheduler) { + + auto shield = tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true), storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true)); + result->asExplicitQuantitativeCheckResult().setShield(std::move(shield)); + } + if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); } return result; @@ -148,10 +184,14 @@ namespace storm { std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeGloballyProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet()); + STORM_LOG_DEBUG(ret.values); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { - tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(),subResult.getTruthValuesVector(), storm::storage::BitVector(ret.maybeStates.size(), true)); - } else if (checkTask.isProduceSchedulersSet() && ret.scheduler) { + auto shield = tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(),subResult.getTruthValuesVector(), storm::storage::BitVector(ret.maybeStates.size(), true)); + result->asExplicitQuantitativeCheckResult().setShield(std::move(shield)); + + } + if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); } return result; @@ -300,7 +340,8 @@ namespace storm { std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values))); if(checkTask.isShieldingTask()) { storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); - tempest::shields::createQuantitativeShield(std::make_shared>(this->getModel()), helper.getChoiceValues(), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, allStatesBv); + auto shield = tempest::shields::createQuantitativeShield(std::make_shared>(this->getModel()), helper.getChoiceValues(), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, allStatesBv); + result->asExplicitQuantitativeCheckResult().setShield(std::move(shield)); } else if (checkTask.isProduceSchedulersSet()) { result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); } @@ -313,7 +354,7 @@ namespace storm { auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix()); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); - auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); + auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values))); if (checkTask.isProduceSchedulersSet()) { result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 3feb0802d..8e364d520 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -4,29 +4,30 @@ #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/models/sparse/Mdp.h" #include "storm/solver/MinMaxLinearEquationSolver.h" - +#include "storm/shields/AbstractShield.h" namespace storm { - + class Environment; - + namespace modelchecker { template class SparseMdpPrctlModelChecker : public SparsePropositionalModelChecker { public: typedef typename SparseMdpModelType::ValueType ValueType; typedef typename SparseMdpModelType::RewardModelType RewardModelType; - + explicit SparseMdpPrctlModelChecker(SparseMdpModelType const& model); - + /*! * Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model). * @param requiresSingleInitialState if not nullptr, this flag is set to true iff checking this formula requires a model with a single initial state */ static bool canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState = nullptr); - + // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; + std::unique_ptr computeBoundedGloballyProbabilities(Environment const& env, CheckTask const& checkTask); virtual std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeNextProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; @@ -43,7 +44,7 @@ namespace storm { virtual std::unique_ptr computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr checkMultiObjectiveFormula(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr checkQuantileFormula(Environment const& env, CheckTask const& checkTask) override; - + }; } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 68951bf1b..760cdce42 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -676,40 +676,15 @@ namespace storm { extractSchedulerChoices(*scheduler, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates); } } - if (goal.isShieldingTask()) { - std::vector subResult; - uint sizeChoiceValues = 0; - for(uint counter = 0; counter < qualitativeStateSets.maybeStates.size(); counter++) { - if(qualitativeStateSets.maybeStates.get(counter)) { - subResult.push_back(result.at(counter)); - } - } - - submatrix = transitionMatrix.getSubmatrix(true, qualitativeStateSets.maybeStates, qualitativeStateSets.maybeStates, false); - auto sub_multiplier = storm::solver::MultiplierFactory().create(env, submatrix); - sub_multiplier->multiply(env, subResult, &b, maybeStateChoiceValues); - - } } } - std::vector choiceValues = std::vector(transitionMatrix.getRowGroupIndices().at(transitionMatrix.getRowGroupIndices().size() - 1), storm::utility::zero()); - auto choice_it = maybeStateChoiceValues.begin(); - for(uint state = 0; state < transitionMatrix.getRowGroupIndices().size() - 1; state++) { - uint rowGroupSize = transitionMatrix.getRowGroupIndices().at(state + 1) - transitionMatrix.getRowGroupIndices().at(state); - if (qualitativeStateSets.maybeStates.get(state)) { - for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { - choiceValues.at(transitionMatrix.getRowGroupIndices().at(state) + choice) = *choice_it; - } - } else if (qualitativeStateSets.statesWithProbability0.get(state)) { - for(uint choice = 0; choice < rowGroupSize; choice++) { - choiceValues.at(transitionMatrix.getRowGroupIndices().at(state) + choice) = 0; - } - } else if (qualitativeStateSets.statesWithProbability1.get(state)) { - for(uint choice = 0; choice < rowGroupSize; choice++) { - choiceValues.at(transitionMatrix.getRowGroupIndices().at(state) + choice) = 1; - } - } + std::vector choiceValues; + if(goal.isShieldingTask()) { + choiceValues = std::vector(transitionMatrix.getRowGroupIndices().at(transitionMatrix.getRowGroupIndices().size() - 1), storm::utility::zero()); + std::vector b = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); + auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); + multiplier->multiply(env, result, &b, choiceValues); } // Extend scheduler with choices for the states in the qualitative state sets. diff --git a/src/storm/modelchecker/results/CheckResult.cpp b/src/storm/modelchecker/results/CheckResult.cpp index 26eb24946..28be6339f 100644 --- a/src/storm/modelchecker/results/CheckResult.cpp +++ b/src/storm/modelchecker/results/CheckResult.cpp @@ -166,6 +166,10 @@ namespace storm { bool CheckResult::hasScheduler() const { return false; } + + bool CheckResult::hasShield() const { + return false; + } // Explicitly instantiate the template functions. template QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult(); diff --git a/src/storm/modelchecker/results/CheckResult.h b/src/storm/modelchecker/results/CheckResult.h index 740a8269d..bfb462949 100644 --- a/src/storm/modelchecker/results/CheckResult.h +++ b/src/storm/modelchecker/results/CheckResult.h @@ -113,6 +113,7 @@ namespace storm { SymbolicParetoCurveCheckResult const& asSymbolicParetoCurveCheckResult() const; virtual bool hasScheduler() const; + virtual bool hasShield() const; virtual std::ostream& writeToStream(std::ostream& out) const = 0; }; diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index ee7c2d91d..b3c83efb6 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -204,6 +204,11 @@ namespace storm { bool ExplicitQuantitativeCheckResult::hasScheduler() const { return static_cast(scheduler); } + + template + bool ExplicitQuantitativeCheckResult::hasShield() const { + return static_cast(shield); + } template void ExplicitQuantitativeCheckResult::setScheduler(std::unique_ptr>&& scheduler) { @@ -222,6 +227,23 @@ namespace storm { return *scheduler.get(); } + template + void ExplicitQuantitativeCheckResult::setShield(std::unique_ptr> shield) { + this->shield = std::move(shield); + } + + template + std::shared_ptr::IndexType>> const& ExplicitQuantitativeCheckResult::getShield() const { + STORM_LOG_THROW(this->hasShield(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing shield."); + return shield.get(); + } + + template + std::shared_ptr::IndexType>>& ExplicitQuantitativeCheckResult::getShield() { + STORM_LOG_THROW(this->hasShield(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing shield."); + return shield.get(); + } + template void print(std::ostream& out, ValueType const& value) { if (value == storm::utility::infinity()) { diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h index 4fe38b0f0..d434e10b1 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h @@ -14,6 +14,8 @@ #include "storm/utility/OsDetection.h" #include "storm/adapters/JsonAdapter.h" +#include "storm/shields/AbstractShield.h" + namespace storm { namespace modelchecker { // fwd @@ -24,7 +26,8 @@ namespace storm { public: typedef std::vector vector_type; typedef std::map map_type; - + typedef typename storm::storage::SparseMatrix::index_type IndexType; + ExplicitQuantitativeCheckResult(); ExplicitQuantitativeCheckResult(map_type const& values); ExplicitQuantitativeCheckResult(map_type&& values); @@ -74,10 +77,16 @@ namespace storm { virtual ValueType sum() const override; virtual bool hasScheduler() const override; + virtual bool hasShield() const override; + void setScheduler(std::unique_ptr>&& scheduler); storm::storage::Scheduler const& getScheduler() const; storm::storage::Scheduler& getScheduler(); + void setShield(std::unique_ptr> shield); + std::shared_ptr> const& getShield() const; + std::shared_ptr>& getShield(); + storm::json toJson(boost::optional const& stateValuations = boost::none) const; private: @@ -86,6 +95,8 @@ namespace storm { // An optional scheduler that accompanies the values. boost::optional>> scheduler; + boost::optional>> shield; + }; } } diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index ca7271aa9..754ca74b2 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -14,6 +14,8 @@ #include "storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h" #include "storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h" +#include "storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h" + #include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" #include "storm/logic/FragmentSpecification.h" @@ -141,12 +143,36 @@ namespace storm { ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); + if (env.solver().isForceSoundness()) { + auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeUntilProbabilitiesSound( + env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), + this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), + checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); + + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); + if(checkTask.isShieldingTask()) { + storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); + auto shield = tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, ~statesOfCoalition); + result->asExplicitQuantitativeCheckResult().setShield(std::move(shield)); + } + if (checkTask.isProduceSchedulersSet() && ret.scheduler) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); + } + return result; + } + + auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeUntilProbabilities( + env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), + this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), + checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); + STORM_LOG_DEBUG(ret.values); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); - tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, ~statesOfCoalition); - } else if (checkTask.isProduceSchedulersSet() && ret.scheduler) { + auto shield = tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, ~statesOfCoalition); + result->asExplicitQuantitativeCheckResult().setShield(std::move(shield)); + } + if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); } return result; @@ -162,8 +188,10 @@ namespace storm { std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); - tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, ~statesOfCoalition); - } else if (checkTask.isProduceSchedulersSet() && ret.scheduler) { + auto shield = tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, ~statesOfCoalition); + result->asExplicitQuantitativeCheckResult().setShield(std::move(shield)); + } + if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); } return result; @@ -197,7 +225,8 @@ namespace storm { std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); - tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, ~statesOfCoalition); + auto shield = tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, ~statesOfCoalition); + result->asExplicitQuantitativeCheckResult().setShield(std::move(shield)); } return result; } @@ -219,7 +248,8 @@ namespace storm { auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeBoundedUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint(), pathFormula.getNonStrictLowerBound(), pathFormula.getNonStrictUpperBound()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { - tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), ~statesOfCoalition); + auto shield = tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), ~statesOfCoalition); + result->asExplicitQuantitativeCheckResult().setShield(std::move(shield)); } return result; } @@ -232,15 +262,34 @@ namespace storm { template std::unique_ptr SparseSmgRpatlModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + + if (env.solver().isForceSoundness()) { + storm::modelchecker::helper::internal::SparseSmgLraHelper helper(this->getModel().getTransitionMatrix(), statesOfCoalition); + storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); + auto values = helper.computeLongRunAverageRewardsSound(env, rewardModel.get()); + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values))); + + if(checkTask.isShieldingTask()) { + storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); + auto shield = tempest::shields::createQuantitativeShield(std::make_shared>(this->getModel()), helper.getChoiceValues(), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, statesOfCoalition); + result->asExplicitQuantitativeCheckResult().setShield(std::move(shield)); + } + if (checkTask.isProduceSchedulersSet()) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); + } + return result; + } + storm::modelchecker::helper::SparseNondeterministicGameInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix(), statesOfCoalition); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); - std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values))); if(checkTask.isShieldingTask()) { storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); - tempest::shields::createQuantitativeShield(std::make_shared>(this->getModel()), helper.getChoiceValues(), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, statesOfCoalition); - } else if (checkTask.isProduceSchedulersSet()) { + auto shield = tempest::shields::createQuantitativeShield(std::make_shared>(this->getModel()), helper.getChoiceValues(), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, statesOfCoalition); + result->asExplicitQuantitativeCheckResult().setShield(std::move(shield)); + } + if (checkTask.isProduceSchedulersSet()) { result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); } return result; diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 31ddac9da..e2a349a50 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -9,6 +9,7 @@ #include "storm/utility/vector.h" #include "storm/utility/graph.h" #include "storm/modelchecker/rpatl/helper/internal/GameViHelper.h" +#include "storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h" namespace storm { namespace modelchecker { @@ -21,8 +22,7 @@ namespace storm { // Relevant states are those states which are phiStates and not PsiStates. storm::storage::BitVector relevantStates = phiStates & ~psiStates; - - // Initialize the x vector and solution vector result. + // Initialize the x vector and solution vector result. std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::zero()); std::vector result = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates); @@ -60,7 +60,80 @@ namespace storm { } template - storm::storage::Scheduler SparseSmgRpatlHelper::expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates) { + SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeUntilProbabilitiesSound(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { + storm::storage::BitVector probGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates); + std::unique_ptr> scheduler; + storm::storage::BitVector relevantStates = phiStates; + + // Initialize the x vector and solution vector result. + std::vector xL = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + // assigning 1s to the xL vector for all Goal states + auto xL_begin = xL.begin(); + std::for_each(xL.begin(), xL.end(), [&psiStates, &xL_begin](ValueType &it) + { + if (psiStates[&it - &(*xL_begin)]) + it = 1; + }); + size_t i = 0; + auto new_end = std::remove_if(xL.begin(), xL.end(), [&relevantStates, &i](const auto& item) { + bool ret = !(relevantStates[i]); + i++; + return ret; + }); + xL.erase(new_end, xL.end()); + xL.resize(relevantStates.getNumberOfSetBits()); + std::vector xU = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + // assigning 1s to the xU vector for all states except the states s where Prob(sEf) = 0 for all goal states f + auto xU_begin = xU.begin(); + std::for_each(xU.begin(), xU.end(), [&probGreater0, &xU_begin](ValueType &it) + { + if (probGreater0[&it - &(*xU_begin)]) + it = 1; + }); + i = 0; + auto new_end_U = std::remove_if(xU.begin(), xU.end(), [&relevantStates, &i](const auto& item) { + bool ret = !(relevantStates[i]); + i++; + return ret; + }); + xU.erase(new_end_U, xU.end()); + xU.resize(relevantStates.getNumberOfSetBits()); + + storm::storage::BitVector clippedPsiStates(relevantStates.getNumberOfSetBits()); + clippedPsiStates.setClippedStatesOfCoalition(relevantStates, psiStates); + + std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates); + std::vector result = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + + storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); + clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); + std::vector constrainedChoiceValues = std::vector(b.size(), storm::utility::zero()); + + if (!relevantStates.empty()) { + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); + storm::modelchecker::helper::internal::SoundGameViHelper viHelper(submatrix, submatrix.transpose(), b, clippedStatesOfCoalition, + clippedPsiStates, goal.direction()); + + if (produceScheduler) { + viHelper.setProduceScheduler(true); + } + + viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues); + + viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); + storm::utility::vector::setVectorValues(result, relevantStates, xL); + + if (produceScheduler) { + scheduler = + std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates, true)); + } + } + + return SMGSparseModelCheckingHelperReturnType(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); + } + + template + storm::storage::Scheduler SparseSmgRpatlHelper::expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates, bool sound) { storm::storage::Scheduler completeScheduler(psiStates.size()); uint_fast64_t maybeStatesCounter = 0; uint schedulerSize = psiStates.size(); @@ -68,6 +141,9 @@ namespace storm { // psiStates already fulfill formulae so we can set an arbitrary action if(psiStates.get(stateCounter)) { completeScheduler.setChoice(0, stateCounter); + if (sound) { + maybeStatesCounter++; + } // ~phiStates do not fulfill formulae so we can set an arbitrary action } else if(notPhiStates.get(stateCounter)) { completeScheduler.setChoice(0, stateCounter); @@ -86,7 +162,22 @@ namespace storm { storm::storage::BitVector notPsiStates = ~psiStates; statesOfCoalition.complement(); - auto result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, qualitative, statesOfCoalition, produceScheduler, hint); + if (env.solver().isForceSoundness()) { + auto result = computeUntilProbabilitiesSound(env, std::move(goal), transitionMatrix, backwardTransitions, + storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, + qualitative, statesOfCoalition, produceScheduler, hint); + for (auto& element : result.values) { + element = storm::utility::one() - element; + } + for (auto& element : result.choiceValues) { + element = storm::utility::one() - element; + } + return result; + } + + auto result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, + storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, + qualitative, statesOfCoalition, produceScheduler, hint); for (auto& element : result.values) { element = storm::utility::one() - element; } diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h index 0592c929b..c0216d23f 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h @@ -35,12 +35,13 @@ namespace storm { class SparseSmgRpatlHelper { public: static SMGSparseModelCheckingHelperReturnType computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); + static SMGSparseModelCheckingHelperReturnType computeUntilProbabilitiesSound(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint); static SMGSparseModelCheckingHelperReturnType computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); static SMGSparseModelCheckingHelperReturnType computeNextProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint); static SMGSparseModelCheckingHelperReturnType computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint, uint64_t lowerBound, uint64_t upperBound); static SMGSparseModelCheckingHelperReturnType computeBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint, uint64_t lowerBound, uint64_t upperBound, bool computeBoundedGlobally = false); private: - static storm::storage::Scheduler expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates); + static storm::storage::Scheduler expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates, bool sound = false); static void expandChoiceValues(std::vector const& rowGroupIndices, storm::storage::BitVector const& relevantStates, std::vector const& constrainedChoiceValues, std::vector& choiceValues); }; } diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp new file mode 100644 index 000000000..aab2935d6 --- /dev/null +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -0,0 +1,371 @@ +#include "SoundGameViHelper.h" + +#include "storm/environment/Environment.h" +#include "storm/environment/solver/SolverEnvironment.h" +#include "storm/environment/solver/GameSolverEnvironment.h" + + +#include "storm/utility/SignalHandler.h" +#include "storm/utility/vector.h" + +namespace storm { + namespace modelchecker { + namespace helper { + namespace internal { + + template + SoundGameViHelper::SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector b, storm::storage::BitVector statesOfCoalition, storm::storage::BitVector psiStates, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _backwardTransitions(backwardTransitions), _statesOfCoalition(statesOfCoalition), _psiStates(psiStates), _optimizationDirection(optimizationDirection), _b(b) { + // Intentionally left empty. + } + + template + void SoundGameViHelper::prepareSolversAndMultipliers(const Environment& env) { + _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); + _x1IsCurrent = false; + if (_statesOfCoalition.size()) { + _minimizerStates = _optimizationDirection == OptimizationDirection::Maximize ? _statesOfCoalition : ~_statesOfCoalition; + } + else { + _minimizerStates = storm::storage::BitVector(_transitionMatrix.getRowGroupCount(), _optimizationDirection == OptimizationDirection::Minimize); + } + _oldPolicy = storm::storage::BitVector(_transitionMatrix.getRowCount(), false); + _timing = std::vector(5, 0); + } + + template + void SoundGameViHelper::performValueIteration(Environment const& env, std::vector& xL, std::vector& xU, storm::solver::OptimizationDirection const dir, std::vector& constrainedChoiceValues) { + + prepareSolversAndMultipliers(env); + // Get precision for convergence check. + ValueType precision = storm::utility::convertNumber(env.solver().game().getPrecision()); + + uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations(); + _x1L = xL; + _x2L = _x1L; + + _x1U = xU; + _x2U = _x1U; + + if (this->isProduceSchedulerSet()) { + if (!this->_producedOptimalChoices.is_initialized()) { + this->_producedOptimalChoices.emplace(); + } + this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount()); + } + + uint64_t iter = 0; + constrainedChoiceValues = std::vector(_transitionMatrix.getRowCount(), storm::utility::zero()); + + while (iter < maxIter) { + performIterationStep(env, dir); + if (checkConvergence(precision)) { + // one last iteration for shield + _multiplier->multiply(env, xNewL(), nullptr, constrainedChoiceValues); + storm::storage::BitVector psiStates = _psiStates; + auto xL_begin = xNewL().begin(); + std::for_each(xNewL().begin(), xNewL().end(), [&psiStates, &xL_begin](ValueType &it){ + if (psiStates[&it - &(*xL_begin)]) + it = 1; + }); + break; + } + if (storm::utility::resources::isTerminate()) { + break; + } + ++iter; + } + xL = xNewL(); + xU = xNewU(); + + if (isProduceSchedulerSet()) { + // We will be doing one more iteration step and track scheduler choices this time. + _x1IsCurrent = !_x1IsCurrent; + _multiplier->multiplyAndReduce(env, dir, xOldL(), nullptr, xNewL(), &_producedOptimalChoices.get(), &_statesOfCoalition); + storm::storage::BitVector psiStates = _psiStates; + auto xL_begin = xNewL().begin(); + std::for_each(xNewL().begin(), xNewL().end(), [&psiStates, &xL_begin](ValueType &it) + { + if (psiStates[&it - &(*xL_begin)]) + it = 1; + }); + } + } + + template + void SoundGameViHelper::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices) { + storm::storage::BitVector reducedMinimizerActions = {storm::storage::BitVector(this->_transitionMatrix.getRowCount(), true)}; + + // under approximation + if (!_multiplier) { + prepareSolversAndMultipliers(env); + } + _x1IsCurrent = !_x1IsCurrent; + std::vector choiceValuesL = std::vector(this->_transitionMatrix.getRowCount(), storm::utility::zero()); + + _multiplier->multiply(env, xOldL(), nullptr, choiceValuesL); + reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, xNewL()); + storm::storage::BitVector psiStates = _psiStates; + auto xL_begin = xNewL().begin(); + std::for_each(xNewL().begin(), xNewL().end(), [&psiStates, &xL_begin](ValueType &it) + { + if (psiStates[&it - &(*xL_begin)]) + it = 1; + }); + + // over_approximation + std::vector choiceValuesU = std::vector(this->_transitionMatrix.getRowCount(), storm::utility::zero()); + + _multiplier->multiply(env, xOldU(), nullptr, choiceValuesU); + reduceChoiceValues(choiceValuesU, nullptr, xNewU()); + auto xU_begin = xNewU().begin(); + std::for_each(xNewU().begin(), xNewU().end(), [&psiStates, &xU_begin](ValueType &it) + { + if (psiStates[&it - &(*xU_begin)]) + it = 1; + }); + + if (reducedMinimizerActions != _oldPolicy) { // new MECs only if Policy changed + // restricting the none optimal minimizer choices + _restrictedTransitions = this->_transitionMatrix.restrictRows(reducedMinimizerActions); + + // find_MSECs() + _MSECs = storm::storage::MaximalEndComponentDecomposition(_restrictedTransitions, _restrictedTransitions.transpose(true)); + } + + // reducing the choiceValuesU + size_t i = 0; + auto new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) { + bool ret = !(reducedMinimizerActions[i]); + i++; + return ret; + }); + choiceValuesU.erase(new_end, choiceValuesU.end()); + + _oldPolicy = reducedMinimizerActions; + + // deflating the MSECs + deflate(_MSECs, _restrictedTransitions, xNewU(), choiceValuesU); + } + + template + void SoundGameViHelper::deflate(storm::storage::MaximalEndComponentDecomposition const MSEC, storage::SparseMatrix const restrictedMatrix, std::vector& xU, std::vector choiceValues) { + + auto rowGroupIndices = restrictedMatrix.getRowGroupIndices(); + auto choice_begin = choiceValues.begin(); + // iterating over all MSECs + for (auto smec_it : MSEC) { + ValueType bestExit = 0; + auto stateSet = smec_it.getStateSet(); + for (uint state : stateSet) { + if (_psiStates[state]) { + bestExit = 1; + break; + } + if (_minimizerStates[state]) continue; + uint rowGroupIndex = rowGroupIndices[state]; + auto exitingCompare = [&state, &smec_it, &choice_begin](const ValueType &lhs, const ValueType &rhs) + { + bool lhsExiting = !smec_it.containsChoice(state, (&lhs - &(*choice_begin))); + bool rhsExiting = !smec_it.containsChoice(state, (&rhs - &(*choice_begin))); + if( lhsExiting && !rhsExiting) return false; + if(!lhsExiting && rhsExiting) return true; + if(!lhsExiting && !rhsExiting) return false; + return lhs < rhs; + }; + uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndex; + + auto choice_it = choice_begin + rowGroupIndex; + auto it = std::max_element(choice_it, choice_it + rowGroupSize, exitingCompare); + ValueType newBestExit = 0; + if (!smec_it.containsChoice(state, it - choice_begin)) { + newBestExit = *it; + } + if (newBestExit > bestExit) + bestExit = newBestExit; + } + // deflating the states of the current MSEC + for (uint state : stateSet) { + xU[state] = std::min(xU[state], bestExit); + } + } + } + + template + void SoundGameViHelper::reduceChoiceValues(std::vector& choiceValues, storm::storage::BitVector* result, std::vector& x) + { + // result BitVec should be initialized with 1s outside the method + + auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices(); + auto choice_it = choiceValues.begin(); + + for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { + uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; + ValueType optChoice; + if (_minimizerStates[state]) { // check if current state is minimizer state + // getting the optimal minimizer choice for the given state + optChoice = *std::min_element(choice_it, choice_it + rowGroupSize); + + if (result != nullptr) { + for (uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { + if (*choice_it > optChoice) { + result->set(rowGroupIndices[state] + choice, 0); + } + } + } + else { + choice_it += rowGroupSize; + } + // reducing the xNew() vector for minimizer states + x[state] = optChoice; + } + else + { + optChoice = *std::max_element(choice_it, choice_it + rowGroupSize); + // reducing the xNew() vector for maximizer states + x[state] = optChoice; + choice_it += rowGroupSize; + } + } + } + + + template + bool SoundGameViHelper::checkConvergence(ValueType threshold) const { + STORM_LOG_ASSERT(_multiplier, "tried to check for convergence without doing an iteration first."); + // Now check whether the currently produced results are precise enough + STORM_LOG_ASSERT(threshold > storm::utility::zero(), "Did not expect a non-positive threshold."); + auto x1It = xNewL().begin(); + auto x1Ite = xNewL().end(); + auto x2It = xNewU().begin(); + for (; x1It != x1Ite; x1It++, x2It++) { + ValueType diff = (*x2It - *x1It); + if (diff > threshold) { + return false; + } + } + return true; + } + + template + void SoundGameViHelper::setProduceScheduler(bool value) { + _produceScheduler = value; + } + + + template + bool SoundGameViHelper::isProduceSchedulerSet() const { + return _produceScheduler; + } + + template + void SoundGameViHelper::setShieldingTask(bool value) { + _shieldingTask = value; + } + + template + bool SoundGameViHelper::isShieldingTask() const { + return _shieldingTask; + } + + template + void SoundGameViHelper::updateTransitionMatrix(storm::storage::SparseMatrix newTransitionMatrix) { + _transitionMatrix = newTransitionMatrix; + } + + template + void SoundGameViHelper::updateStatesOfCoalition(storm::storage::BitVector newStatesOfCoalition) { + _statesOfCoalition = newStatesOfCoalition; + } + + template + std::vector const& SoundGameViHelper::getProducedOptimalChoices() const { + STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); + STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?"); + return this->_producedOptimalChoices.get(); + } + + template + std::vector& SoundGameViHelper::getProducedOptimalChoices() { + STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); + STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?"); + return this->_producedOptimalChoices.get(); + } + + template + storm::storage::Scheduler SoundGameViHelper::extractScheduler() const{ + auto const& optimalChoices = getProducedOptimalChoices(); + storm::storage::Scheduler scheduler(optimalChoices.size()); + for (uint64_t state = 0; state < optimalChoices.size(); ++state) { + scheduler.setChoice(optimalChoices[state], state); + } + return scheduler; + } + + template + void SoundGameViHelper::getChoiceValues(Environment const& env, std::vector const& x, std::vector& choiceValues) { + _multiplier->multiply(env, x, nullptr, choiceValues); + } + + template + void SoundGameViHelper::fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices) { + std::vector allChoices = std::vector(rowGroupIndices.at(rowGroupIndices.size() - 1), storm::utility::zero()); + auto choice_it = choiceValues.begin(); + for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { + uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; + if (psiStates.get(state)) { + for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { + allChoices.at(rowGroupIndices.at(state) + choice) = *choice_it; + } + } + } + choiceValues = allChoices; + } + + template + std::vector& SoundGameViHelper::xNewL() { + return _x1IsCurrent ? _x1L : _x2L; + } + + template + std::vector const& SoundGameViHelper::xNewL() const { + return _x1IsCurrent ? _x1L : _x2L; + } + + template + std::vector& SoundGameViHelper::xOldL() { + return _x1IsCurrent ? _x2L : _x1L; + } + + template + std::vector const& SoundGameViHelper::xOldL() const { + return _x1IsCurrent ? _x2L : _x1L; + } + + template + std::vector& SoundGameViHelper::xNewU() { + return _x1IsCurrent ? _x1U : _x2U; + } + + template + std::vector const& SoundGameViHelper::xNewU() const { + return _x1IsCurrent ? _x1U : _x2U; + } + + template + std::vector& SoundGameViHelper::xOldU() { + return _x1IsCurrent ? _x2U : _x1U; + } + + template + std::vector const& SoundGameViHelper::xOldU() const { + return _x1IsCurrent ? _x2U : _x1U; + } + + template class SoundGameViHelper; +#ifdef STORM_HAVE_CARL + template class SoundGameViHelper; +#endif + } + } + } +} diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h new file mode 100644 index 000000000..e90099fde --- /dev/null +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h @@ -0,0 +1,136 @@ +#pragma once + +#include "storm/storage/SparseMatrix.h" +#include "storm/solver/LinearEquationSolver.h" +#include "storm/solver/MinMaxLinearEquationSolver.h" +#include "storm/solver/Multiplier.h" +#include "storm/storage/MaximalEndComponentDecomposition.h" + +namespace storm { + class Environment; + + namespace storage { + template class Scheduler; + } + + namespace modelchecker { + namespace helper { + namespace internal { + + template + class SoundGameViHelper { + public: + SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector b, storm::storage::BitVector statesOfCoalition, storm::storage::BitVector psiStates, OptimizationDirection const& optimizationDirection); + + void prepareSolversAndMultipliers(const Environment& env); + + /*! + * Perform value iteration until convergence + */ + void performValueIteration(Environment const& env, std::vector& xL, std::vector& xU, storm::solver::OptimizationDirection const dir, std::vector& constrainedChoiceValues); + + /*! + * Sets whether an optimal scheduler shall be constructed during the computation + */ + void setProduceScheduler(bool value); + + /*! + * @return whether an optimal scheduler shall be constructed during the computation + */ + bool isProduceSchedulerSet() const; + + /*! + * Sets whether an optimal scheduler shall be constructed during the computation + */ + void setShieldingTask(bool value); + + /*! + * @return whether an optimal scheduler shall be constructed during the computation + */ + bool isShieldingTask() const; + + /*! + * Changes the transitionMatrix to the given one. + */ + void updateTransitionMatrix(storm::storage::SparseMatrix newTransitionMatrix); + + /*! + * Changes the statesOfCoalition to the given one. + */ + void updateStatesOfCoalition(storm::storage::BitVector newStatesOfCoalition); + + storm::storage::Scheduler extractScheduler() const; + + void getChoiceValues(Environment const& env, std::vector const& x, std::vector& choiceValues); + + /*! + * Fills the choice values vector to the original size with zeros for ~psiState choices. + */ + void fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices); + + void deflate(storm::storage::MaximalEndComponentDecomposition const MECD, storage::SparseMatrix const restrictedMatrix, std::vector& xU, std::vector choiceValues); + + void reduceChoiceValues(std::vector& choiceValues, storm::storage::BitVector* result, std::vector& x); + + private: + /*! + * Performs one iteration step for value iteration + */ + void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); + + /*! + * Checks whether the curently computed value achieves the desired precision + */ + bool checkConvergence(ValueType precision) const; + + std::vector& xNewL(); + std::vector const& xNewL() const; + + std::vector& xOldL(); + std::vector const& xOldL() const; + + std::vector& xNewU(); + std::vector const& xNewU() const; + + std::vector& xOldU(); + std::vector const& xOldU() const; + + bool _x1IsCurrent; + + storm::storage::BitVector _minimizerStates; + + /*! + * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. + * @return the produced scheduler of the most recent call. + */ + std::vector const& getProducedOptimalChoices() const; + + /*! + * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. + * @return the produced scheduler of the most recent call. + */ + std::vector& getProducedOptimalChoices(); + + std::unique_ptr> _multiplier; + + storm::storage::SparseMatrix _transitionMatrix; + storm::storage::SparseMatrix _backwardTransitions; + storm::storage::SparseMatrix _restrictedTransitions; + storm::storage::BitVector _oldPolicy; + storm::storage::BitVector _statesOfCoalition; + storm::storage::BitVector _psiStates; + std::vector _x, _x1L, _x2L, _x1U, _x2U, _b; + OptimizationDirection _optimizationDirection; + + storm::storage::MaximalEndComponentDecomposition _MSECs; + + bool _produceScheduler = false; + bool _shieldingTask = false; + boost::optional> _producedOptimalChoices; + + std::vector _timing; + }; + } + } + } +} diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index f0af3f4ad..d94c67a8e 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -25,6 +25,7 @@ namespace storm { const std::string IOSettings::exportCdfOptionName = "exportcdf"; const std::string IOSettings::exportCdfOptionShortName = "cdf"; const std::string IOSettings::exportSchedulerOptionName = "exportscheduler"; + const std::string IOSettings::exportShieldOptionName = "exportshield"; const std::string IOSettings::exportCheckResultOptionName = "exportresult"; const std::string IOSettings::explicitOptionName = "explicit"; const std::string IOSettings::explicitOptionShortName = "exp"; @@ -64,6 +65,7 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportCdfOptionName, false, "Exports the cumulative density function for reward bounded properties into a .csv file.").setIsAdvanced().setShortName(exportCdfOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to an existing directory where the cdf files will be stored.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportSchedulerOptionName, false, "Exports the choices of an optimal scheduler to the given file (if supported by engine).").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file. Use file extension '.json' to export in json.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportShieldOptionName, false, "Exports the the generated shield to the given file (if supported by engine).").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file. Use file extension '.json' to export in json.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportCheckResultOptionName, false, "Exports the result to a given file (if supported by engine). The export will be in json.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportExplicitOptionName, "", "If given, the loaded model will be written to the specified file in the drn format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build()); @@ -178,6 +180,14 @@ namespace storm { return this->getOption(exportSchedulerOptionName).getArgumentByName("filename").getValueAsString(); } + bool IOSettings::isExportShieldSet() const { + return this->getOption(exportShieldOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getExportShieldFilename() const { + return this->getOption(exportShieldOptionName).getArgumentByName("filename").getValueAsString(); + } + bool IOSettings::isExportCheckResultSet() const { return this->getOption(exportCheckResultOptionName).getHasOptionBeenSet(); } diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 3be8c646d..a03ea372e 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -106,6 +106,16 @@ namespace storm { */ std::string getExportSchedulerFilename() const; + /*! + * Retrieves whether a shield is to be exported. + */ + bool isExportShieldSet() const; + + /*! + * Retrieves a filename to which a shield will be exported. + */ + std::string getExportShieldFilename() const; + /*! * Retrieves whether the check result should be exported. */ @@ -365,6 +375,7 @@ namespace storm { static const std::string exportCdfOptionName; static const std::string exportCdfOptionShortName; static const std::string exportSchedulerOptionName; + static const std::string exportShieldOptionName; static const std::string exportCheckResultOptionName; static const std::string explicitOptionName; static const std::string explicitOptionShortName; diff --git a/src/storm/shields/AbstractShield.cpp b/src/storm/shields/AbstractShield.cpp index 779f3b894..ca446726c 100644 --- a/src/storm/shields/AbstractShield.cpp +++ b/src/storm/shields/AbstractShield.cpp @@ -1,4 +1,7 @@ #include "storm/shields/AbstractShield.h" +#include "storm/shields/PreShield.h" +#include "storm/shields/PostShield.h" +#include "storm/shields/OptimalShield.h" #include @@ -29,6 +32,57 @@ namespace tempest { return optimizationDirection; } + template + void AbstractShield::setShieldingExpression(std::shared_ptr const& shieldingExpression) { + this->shieldingExpression = shieldingExpression; + } + + template + bool AbstractShield::isPreShield() const { + return false; + } + + template + bool AbstractShield::isPostShield() const { + return false; + } + + template + bool AbstractShield::isOptimalShield() const { + return false; + } + + template + PreShield& AbstractShield::asPreShield() { + return dynamic_cast&>(*this); + } + + template + PreShield const& AbstractShield::asPreShield() const { + return dynamic_cast const&>(*this); + } + + template + PostShield& AbstractShield::asPostShield() { + return dynamic_cast&>(*this); + } + + template + PostShield const& AbstractShield::asPostShield() const { + return dynamic_cast const&>(*this); + } + + template + OptimalShield& AbstractShield::asOptimalShield() { + return dynamic_cast&>(*this); + } + + template + OptimalShield const& AbstractShield::asOptimalShield() const { + return dynamic_cast const&>(*this); + } + + template std::string AbstractShield::getClassName() const { return std::string(boost::core::demangled_name(BOOST_CORE_TYPEID(*this))); @@ -38,6 +92,7 @@ namespace tempest { template class AbstractShield::index_type>; #ifdef STORM_HAVE_CARL template class AbstractShield::index_type>; + template class AbstractShield::index_type>; #endif } } diff --git a/src/storm/shields/AbstractShield.h b/src/storm/shields/AbstractShield.h index b479efe71..04401cd6b 100644 --- a/src/storm/shields/AbstractShield.h +++ b/src/storm/shields/AbstractShield.h @@ -16,19 +16,33 @@ #include "storm/logic/ShieldExpression.h" +#include "storm/exceptions/NotSupportedException.h" + + namespace tempest { namespace shields { + template + class PreShield; + template + class PostShield; + template + class OptimalShield; + namespace utility { template struct ChoiceFilter { bool operator()(ValueType v, ValueType opt, double shieldValue) { - Compare compare; - if(relative && std::is_same>::value) { - return compare(v, opt + opt * shieldValue); - } else if(relative && std::is_same>::value) { - return compare(v, opt * shieldValue); + if constexpr (std::is_same_v || std::is_same_v) { + Compare compare; + if(relative && std::is_same>::value) { + return compare(v, opt + opt * shieldValue); + } else if(relative && std::is_same>::value) { + return compare(v, opt * shieldValue); + } + else return compare(v, shieldValue); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot create shields for parametric models"); } - else return compare(v, shieldValue); } }; } @@ -47,9 +61,28 @@ namespace tempest { std::vector computeRowGroupSizes(); storm::OptimizationDirection getOptimizationDirection(); + void setShieldingExpression(std::shared_ptr const& shieldingExpression); std::string getClassName() const; + virtual bool isPreShield() const; + virtual bool isPostShield() const; + virtual bool isOptimalShield() const; + + PreShield& asPreShield(); + PreShield const& asPreShield() const; + + PostShield& asPostShield(); + PostShield const& asPostShield() const; + + OptimalShield& asOptimalShield(); + OptimalShield const& asOptimalShield() const; + + + virtual void printToStream(std::ostream& out, std::shared_ptr> const& model) = 0; + virtual void printJsonToStream(std::ostream& out, std::shared_ptr> const& model) = 0; + + protected: AbstractShield(std::vector const& rowGroupIndices, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); diff --git a/src/storm/shields/OptimalShield.cpp b/src/storm/shields/OptimalShield.cpp index 8be4b1fef..0d8fc0c63 100644 --- a/src/storm/shields/OptimalShield.cpp +++ b/src/storm/shields/OptimalShield.cpp @@ -64,10 +64,41 @@ namespace tempest { return shield; } + + template + std::shared_ptr> OptimalShield::getScheduler() const { + return optimalScheduler; + } + + template + bool OptimalShield::isOptimalShield() const { + return true; + } + + template + void OptimalShield::printJsonToStream(std::ostream& out, std::shared_ptr> const& model) { + optimalScheduler->printJsonToStream(out, model); + } + + template + void OptimalShield::printToStream(std::ostream& out, std::shared_ptr> const& model) { + optimalScheduler->printToStream(out, this->shieldingExpression, model); + } + + //template + //template + //std::enable_if_t::value, storm::storage::PostScheduler> OptimalShield::construct() { + // STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "todo"); + //} + + + // Explicitly instantiate appropriate classes template class OptimalShield::index_type>; #ifdef STORM_HAVE_CARL template class OptimalShield::index_type>; + template class OptimalShield::index_type>; + #endif } } diff --git a/src/storm/shields/OptimalShield.h b/src/storm/shields/OptimalShield.h index b7c55712e..3c2d9a2ff 100644 --- a/src/storm/shields/OptimalShield.h +++ b/src/storm/shields/OptimalShield.h @@ -14,8 +14,16 @@ namespace tempest { storm::storage::PostScheduler construct(); template storm::storage::PostScheduler constructWithCompareType(); + std::shared_ptr> getScheduler() const; + + virtual bool isOptimalShield() const override; + + virtual void printToStream(std::ostream& out, std::shared_ptr> const& model) override; + virtual void printJsonToStream(std::ostream& out, std::shared_ptr> const& model) override; private: std::vector choiceValues; + + std::shared_ptr> optimalScheduler; }; } } diff --git a/src/storm/shields/PostShield.cpp b/src/storm/shields/PostShield.cpp index 5ef487ad0..a3e86b7f2 100644 --- a/src/storm/shields/PostShield.cpp +++ b/src/storm/shields/PostShield.cpp @@ -45,7 +45,7 @@ namespace tempest { } ValueType optProbability = *(choice_it + optProbabilityIndex); if(!relative && !choiceFilter(optProbability, optProbability, this->shieldingExpression->getValue())) { - STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state); + //STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state); shield.setChoice(storm::storage::PostSchedulerChoice(), state, 0); choice_it += rowGroupSize; continue; @@ -67,10 +67,40 @@ namespace tempest { return shield; } + + template + std::shared_ptr> PostShield::getScheduler() const { + return postScheduler; + } + + template + bool PostShield::isPostShield() const { + return true; + } + + template + void PostShield::printJsonToStream(std::ostream& out, std::shared_ptr> const& model) { + postScheduler->printJsonToStream(out, model); + } + + template + void PostShield::printToStream(std::ostream& out, std::shared_ptr> const& model) { + postScheduler->printToStream(out, this->shieldingExpression, model); + } + + //template + //template + //std::enable_if_t::value, storm::storage::PostScheduler> PostShield::construct() { + // STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "todo"); + //} + + // Explicitly instantiate appropriate classes template class PostShield::index_type>; #ifdef STORM_HAVE_CARL template class PostShield::index_type>; + template class PostShield::index_type>; + #endif } } diff --git a/src/storm/shields/PostShield.h b/src/storm/shields/PostShield.h index f2a43905f..2116cf7bb 100644 --- a/src/storm/shields/PostShield.h +++ b/src/storm/shields/PostShield.h @@ -14,8 +14,16 @@ namespace tempest { storm::storage::PostScheduler construct(); template storm::storage::PostScheduler constructWithCompareType(); + std::shared_ptr> getScheduler() const; + + virtual bool isPostShield() const override; + + virtual void printToStream(std::ostream& out, std::shared_ptr> const& model) override; + virtual void printJsonToStream(std::ostream& out, std::shared_ptr> const& model) override; private: std::vector choiceValues; + + std::shared_ptr> postScheduler; }; } } diff --git a/src/storm/shields/PreShield.cpp b/src/storm/shields/PreShield.cpp index a16b777c7..7c62d5788 100644 --- a/src/storm/shields/PreShield.cpp +++ b/src/storm/shields/PreShield.cpp @@ -10,8 +10,12 @@ namespace tempest { // Intentionally left empty. } + template storm::storage::PreScheduler PreShield::construct() { + if constexpr (std::is_same_v) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "todo"); + } if (this->getOptimizationDirection() == storm::OptimizationDirection::Minimize) { if(this->shieldingExpression->isRelative()) { return constructWithCompareType, true>(); @@ -38,7 +42,7 @@ namespace tempest { } for(uint state = 0; state < this->rowGroupIndices.size() - 1; state++) { uint rowGroupSize = this->rowGroupIndices[state + 1] - this->rowGroupIndices[state]; - if(this->relevantStates.get(state)) { + if(true){ //if(this->relevantStates.get(state)) { storm::storage::PreSchedulerChoice enabledChoices; ValueType optProbability; if(std::is_same>::value) { @@ -47,7 +51,7 @@ namespace tempest { optProbability = *std::min_element(choice_it, choice_it + rowGroupSize); } if(!relative && !choiceFilter(optProbability, optProbability, this->shieldingExpression->getValue())) { - STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state); + //STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state); shield.setChoice(storm::storage::PreSchedulerChoice(), state, 0); choice_it += rowGroupSize; continue; @@ -65,12 +69,38 @@ namespace tempest { } } + preScheduler = std::make_shared>(shield); return shield; } + + + template + std::shared_ptr> PreShield::getScheduler() const { + return preScheduler; + } + + template + bool PreShield::isPreShield() const { + return true; + } + + template + void PreShield::printJsonToStream(std::ostream& out, std::shared_ptr> const& model) { + preScheduler->printJsonToStream(out, model); + } + + template + void PreShield::printToStream(std::ostream& out, std::shared_ptr> const& model) { + preScheduler->printToStream(out, this->shieldingExpression, model); + } + + + // Explicitly instantiate appropriate classes template class PreShield::index_type>; #ifdef STORM_HAVE_CARL template class PreShield::index_type>; + template class PreShield::index_type>; #endif } } diff --git a/src/storm/shields/PreShield.h b/src/storm/shields/PreShield.h index 6e98dd7e8..3bf80017c 100644 --- a/src/storm/shields/PreShield.h +++ b/src/storm/shields/PreShield.h @@ -11,11 +11,22 @@ namespace tempest { public: PreShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + storm::storage::PreScheduler construct(); + template storm::storage::PreScheduler constructWithCompareType(); + void setShieldingExpression(std::shared_ptr const& shieldingExpression); + std::shared_ptr> getScheduler() const; + + virtual bool isPreShield() const override; + + virtual void printToStream(std::ostream& out, std::shared_ptr> const& model) override; + virtual void printJsonToStream(std::ostream& out, std::shared_ptr> const& model) override; private: std::vector choiceValues; + + std::shared_ptr> preScheduler; }; } } diff --git a/src/storm/shields/ShieldHandling.cpp b/src/storm/shields/ShieldHandling.cpp index 007959d5d..bcef9332c 100644 --- a/src/storm/shields/ShieldHandling.cpp +++ b/src/storm/shields/ShieldHandling.cpp @@ -2,51 +2,41 @@ namespace tempest { namespace shields { - std::string shieldFilename(std::shared_ptr const& shieldingExpression) { - return shieldingExpression->getFilename() + ".shield"; - } - template - void createShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) { - std::ofstream stream; - storm::utility::openFile(shieldFilename(shieldingExpression), stream); + std::unique_ptr> createShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) { if(coalitionStates.is_initialized()) coalitionStates.get().complement(); if(shieldingExpression->isPreSafetyShield()) { PreShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); - shield.construct().printToStream(stream, shieldingExpression, model); + return std::make_unique>(shield); } else if(shieldingExpression->isPostSafetyShield()) { PostShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); - shield.construct().printToStream(stream, shieldingExpression, model); + return std::make_unique>(shield); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unknown Shielding Type: " + shieldingExpression->typeToString()); - storm::utility::closeFile(stream); } - storm::utility::closeFile(stream); - } + } template - void createQuantitativeShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) { - std::ofstream stream; - storm::utility::openFile(shieldFilename(shieldingExpression), stream); + std::unique_ptr> createQuantitativeShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) { if(coalitionStates.is_initialized()) coalitionStates.get().complement(); // TODO CHECK THIS!!! if(shieldingExpression->isOptimalPreShield()) { PreShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); - shield.construct().printToStream(stream, shieldingExpression, model); + return std::make_unique>(shield); } else if(shieldingExpression->isOptimalPostShield()) { - PostShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); - shield.construct().printToStream(stream, shieldingExpression, model); + PostShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); + return std::make_unique>(shield); + } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unknown Shielding Type: " + shieldingExpression->typeToString()); - storm::utility::closeFile(stream); } - storm::utility::closeFile(stream); } + // Explicitly instantiate appropriate - template void createShield::index_type>(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); - template void createQuantitativeShield::index_type>(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + template std::unique_ptr::index_type>> createShield::index_type>(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + template std::unique_ptr::index_type>> createQuantitativeShield::index_type>(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); #ifdef STORM_HAVE_CARL - template void createShield::index_type>(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); - template void createQuantitativeShield::index_type>(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + template std::unique_ptr::index_type>> createShield::index_type>(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + template std::unique_ptr::index_type>> createQuantitativeShield::index_type>(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); #endif } } diff --git a/src/storm/shields/ShieldHandling.h b/src/storm/shields/ShieldHandling.h index 768888a7d..1fff9a6a0 100644 --- a/src/storm/shields/ShieldHandling.h +++ b/src/storm/shields/ShieldHandling.h @@ -20,13 +20,12 @@ #include "storm/exceptions/InvalidArgumentException.h" namespace tempest { - namespace shields { - std::string shieldFilename(std::shared_ptr const& shieldingExpression); - + namespace shields { template - void createShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + std::unique_ptr> createShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); template - void createQuantitativeShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + std::unique_ptr> createQuantitativeShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + } } diff --git a/src/storm/storage/MaximalEndComponent.cpp b/src/storm/storage/MaximalEndComponent.cpp index aa7453277..d4f51e089 100644 --- a/src/storm/storage/MaximalEndComponent.cpp +++ b/src/storm/storage/MaximalEndComponent.cpp @@ -4,7 +4,6 @@ namespace storm { namespace storage { - std::ostream& operator<<(std::ostream& out, storm::storage::FlatSet const& block); MaximalEndComponent::MaximalEndComponent() : stateToChoicesMapping() { @@ -100,6 +99,18 @@ namespace storm { return stateChoicePair->second.find(choice) != stateChoicePair->second.end(); } + template + bool MaximalEndComponent::isErgodic(storm::storage::SparseMatrix transitionMatrix) const { + auto rowGroupIndices = transitionMatrix.getRowGroupIndices(); + for (auto state : this->getStateSet()) + { + if (getChoicesForState(state).size() == (rowGroupIndices[state + 1] - rowGroupIndices[state])) continue; + return false; + } + return true; + } + + MaximalEndComponent::set_type MaximalEndComponent::getStateSet() const { set_type states; states.reserve(stateToChoicesMapping.size()); @@ -136,5 +147,8 @@ namespace storm { MaximalEndComponent::const_iterator MaximalEndComponent::end() const { return stateToChoicesMapping.end(); } + + template bool MaximalEndComponent::isErgodic(storm::storage::SparseMatrix transitionMatrix) const; + template bool MaximalEndComponent::isErgodic(storm::storage::SparseMatrix transitionMatrix) const; } } diff --git a/src/storm/storage/MaximalEndComponent.h b/src/storm/storage/MaximalEndComponent.h index a1d5b37c2..448159804 100644 --- a/src/storm/storage/MaximalEndComponent.h +++ b/src/storm/storage/MaximalEndComponent.h @@ -5,6 +5,7 @@ #include "storm/storage/sparse/StateType.h" #include "storm/storage/BoostTypes.h" +#include "storm/storage/SparseMatrix.h" namespace storm { namespace storage { @@ -20,6 +21,7 @@ namespace storm { typedef std::unordered_map map_type; typedef map_type::iterator iterator; typedef map_type::const_iterator const_iterator; + /*! * Creates an empty MEC. @@ -124,6 +126,15 @@ namespace storm { * @return True if the given choice is contained in the MEC. */ bool containsChoice(uint_fast64_t state, uint_fast64_t choice) const; + + /*! + * Retrieves whether the MEC is ergodic or not i.e. wether the MEC is exitable or not + * + * @param transitionMatrix the given transition matrix + * @return True if the MEC is ergodic + */ + template + bool isErgodic(storm::storage::SparseMatrix transitionMatrix) const; /*! * Retrieves the set of states contained in the MEC. diff --git a/src/storm/storage/PostScheduler.cpp b/src/storm/storage/PostScheduler.cpp index 11d0a7aed..d8f5a7993 100644 --- a/src/storm/storage/PostScheduler.cpp +++ b/src/storm/storage/PostScheduler.cpp @@ -40,6 +40,12 @@ namespace storm { schedulerChoiceMapping[memoryState][modelState] = choice; } + template + PostSchedulerChoice const& PostScheduler::getChoice(uint_fast64_t modelState, uint_fast64_t memoryState) const { + STORM_LOG_ASSERT(modelState < schedulerChoiceMapping[memoryState].size(), "Illegal model state index"); + return schedulerChoiceMapping[memoryState][modelState]; + } + template bool PostScheduler::isDeterministicScheduler() const { return true; @@ -122,9 +128,71 @@ namespace storm { out << "___________________________________________________________________" << std::endl; } + template + void PostScheduler::printJsonToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices) const { + STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoiceMapping.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler."); + STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given."); + storm::json output; + for (uint64_t state = 0; state < schedulerChoiceMapping.front().size(); ++state) { + // Check whether the state is skipped + if (skipUniqueChoices && model != nullptr && model->getTransitionMatrix().getRowGroupSize(state) == 1) { + continue; + } + + storm::json stateChoicesJson; + if (model && model->hasStateValuations()) { + stateChoicesJson["s"] = model->getStateValuations().template toJson(state); + } else { + stateChoicesJson["s"] = state; + } + + auto const &choice = schedulerChoiceMapping[0][state]; + storm::json choicesJson; + if (!choice.getChoiceMap().empty()) { + for (auto const &choiceProbPair : choice.getChoiceMap()) { + uint64_t globalChoiceIndex = model->getTransitionMatrix().getRowGroupIndices()[state] + std::get<0>(choiceProbPair); + uint64_t globalChoiceCorrectionIndex = model->getTransitionMatrix().getRowGroupIndices()[state] + std::get<1>(choiceProbPair); + storm::json choiceJson; + if (model && model->hasChoiceOrigins() && + model->getChoiceOrigins()->getIdentifier(globalChoiceIndex) != + model->getChoiceOrigins()->getIdentifierForChoicesWithNoOrigin()) { + auto choiceOriginJson = model->getChoiceOrigins()->getChoiceAsJson(globalChoiceIndex); + auto choiceOriginCorrectionJson = model->getChoiceOrigins()->getChoiceAsJson(globalChoiceCorrectionIndex); + std::string choiceActionLabel = choiceOriginJson["action-label"]; + std::string choiceCorrectionActionLabel = choiceOriginCorrectionJson["action-label"]; + choiceOriginJson["action-label"] = choiceActionLabel.append(": ").append(choiceCorrectionActionLabel).append("\n"); + choiceJson["origin"] = choiceOriginJson; + } + if (model && model->hasChoiceLabeling()) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(globalChoiceIndex); + + choiceJson["labels"] = std::vector(choiceLabels.begin(), + choiceLabels.end()); + } + choiceJson["index"] = globalChoiceIndex; + choiceJson["prob"] = storm::utility::convertNumber( + std::get<1>(choiceProbPair)); + + + choicesJson.push_back(std::move(choiceJson)); + } + } else { + choicesJson = "undefined"; + } + + stateChoicesJson["c"] = std::move(choicesJson); + output.push_back(std::move(stateChoicesJson)); + + } + + out << output.dump(4); + } + + template class PostScheduler; #ifdef STORM_HAVE_CARL template class PostScheduler; + template class PostScheduler; #endif } } diff --git a/src/storm/storage/PostScheduler.h b/src/storm/storage/PostScheduler.h index 99fc3c1b8..c2eaebde2 100644 --- a/src/storm/storage/PostScheduler.h +++ b/src/storm/storage/PostScheduler.h @@ -37,6 +37,15 @@ namespace storm { */ void setChoice(PostSchedulerChoice const& newChoice, uint_fast64_t modelState, uint_fast64_t memoryState = 0); + /*! + * Gets the choice defined by the scheduler for the given model and memory state. + * + * @param state The state for which to get the choice. + * @param memoryState the memory state which we consider. + */ + PostSchedulerChoice const& getChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0) const; + + /*! * Is the scheduler defined on the states indicated by the selected-states bitvector? */ @@ -83,6 +92,14 @@ namespace storm { * Requires a model to be given. */ void printToStream(std::ostream& out, std::shared_ptr shieldingExpression, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; + + /*! + * Prints the pre scheduler in json format to the given output stream. + */ + void printJsonToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; + + + private: boost::optional memoryStructure; std::vector>> schedulerChoiceMapping; @@ -97,3 +114,4 @@ namespace storm { }; } } + \ No newline at end of file diff --git a/src/storm/storage/PreScheduler.cpp b/src/storm/storage/PreScheduler.cpp index bb09a81f1..f6f78c41d 100644 --- a/src/storm/storage/PreScheduler.cpp +++ b/src/storm/storage/PreScheduler.cpp @@ -40,6 +40,14 @@ namespace storm { schedulerChoice = choice; } + template + PreSchedulerChoice const& PreScheduler::getChoice(uint_fast64_t modelState, uint_fast64_t memoryState) const { + STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index"); + STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index"); + return schedulerChoices[memoryState][modelState]; + } + + template void PreScheduler::printToStream(std::ostream& out, std::shared_ptr shieldingExpression, std::shared_ptr> model, bool skipUniqueChoices) const { STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == this->schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler."); @@ -129,9 +137,93 @@ namespace storm { out << "___________________________________________________________________" << std::endl; } + + + + template + void PreScheduler::printJsonToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices) const { + STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler."); + STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given."); + storm::json output; + for (uint64_t state = 0; state < schedulerChoices.front().size(); ++state) { + // Check whether the state is skipped + if (skipUniqueChoices && model != nullptr && model->getTransitionMatrix().getRowGroupSize(state) == 1) { + continue; + } + + for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) { + storm::json stateChoicesJson; + if (model && model->hasStateValuations()) { + stateChoicesJson["s"] = model->getStateValuations().template toJson(state); + } else { + stateChoicesJson["s"] = state; + } + + if (!isMemorylessScheduler()) { + stateChoicesJson["m"] = memoryState; + } + + auto const &choice = schedulerChoices[memoryState][state]; + storm::json choicesJson; + if (!choice.getChoiceMap().empty()) { + for (auto const &choiceProbPair : choice.getChoiceMap()) { + uint64_t globalChoiceIndex = model->getTransitionMatrix().getRowGroupIndices()[state] + std::get(choiceProbPair); + storm::json choiceJson; + if (model && model->hasChoiceOrigins() && + model->getChoiceOrigins()->getIdentifier(globalChoiceIndex) != + model->getChoiceOrigins()->getIdentifierForChoicesWithNoOrigin()) { + auto choiceOriginJson = model->getChoiceOrigins()->getChoiceAsJson(globalChoiceIndex); + std::string choiceActionLabel = choiceOriginJson["action-label"]; + choiceOriginJson["action-label"] = choiceActionLabel.append("\n"); + choiceJson["origin"] = choiceOriginJson; + } + if (model && model->hasChoiceLabeling()) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(globalChoiceIndex); + choiceJson["labels"] = std::vector(choiceLabels.begin(), + choiceLabels.end()); + } + choiceJson["index"] = globalChoiceIndex; + choiceJson["prob"] = storm::utility::convertNumber( + std::get(choiceProbPair)); + + // Memory updates + if(!isMemorylessScheduler()) { + choiceJson["memory-updates"] = std::vector>(); + uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + std::get(choiceProbPair); + for (auto entryIt = model->getTransitionMatrix().getRow(row).begin(); entryIt < model->getTransitionMatrix().getRow(row).end(); ++entryIt) { + storm::json updateJson; + // next model state + if (model && model->hasStateValuations()) { + updateJson["s'"] = model->getStateValuations().template toJson(entryIt->getColumn()); + } else { + updateJson["s'"] = entryIt->getColumn(); + } + // next memory state + updateJson["m'"] = this->memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()); + choiceJson["memory-updates"].push_back(std::move(updateJson)); + } + } + + choicesJson.push_back(std::move(choiceJson)); + } + } else { + choicesJson = "undefined"; + } + + stateChoicesJson["c"] = std::move(choicesJson); + output.push_back(std::move(stateChoicesJson)); + } + } + out << output.dump(4); + } + + + + template class PreScheduler; #ifdef STORM_HAVE_CARL template class PreScheduler; + template class PreScheduler; #endif } } diff --git a/src/storm/storage/PreScheduler.h b/src/storm/storage/PreScheduler.h index 5cfa2e8cb..294e7ecc1 100644 --- a/src/storm/storage/PreScheduler.h +++ b/src/storm/storage/PreScheduler.h @@ -13,6 +13,7 @@ namespace storm { /* * TODO needs obvious changes in all comment blocks */ + // TODO inherit from Scheduler? template class PreScheduler { public: @@ -32,10 +33,24 @@ namespace storm { void setChoice(PreSchedulerChoice const& choice, uint_fast64_t modelState, uint_fast64_t memoryState); /*! - * Prints the scheduler to the given output stream. + * Gets the choice defined by the scheduler for the given model and memory state. + * + * @param state The state for which to get the choice. + * @param memoryState the memory state which we consider. + */ + PreSchedulerChoice const& getChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0) const; + + /*! + * Prints the pre scheduler to the given output stream. */ void printToStream(std::ostream& out, std::shared_ptr shieldingExpression, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; + /*! + * Prints the pre scheduler in json format to the given output stream. + */ + void printJsonToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; + + private: boost::optional memoryStructure; std::vector>> schedulerChoices; diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index 3583ac019..f4c039f27 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -85,13 +85,13 @@ TEST(FragmentCheckerTest, Prctl) { ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmax=? [\"label1\" U [5,7] \"label2\"]")); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmax=? [\"label1\" U [5,7] \"label2\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmax=? [G \"label\"]")); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmax=? [G \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmin=? [F <5 \"label\"]")); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmin=? [F <5 \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); } @@ -202,13 +202,13 @@ TEST(FragmentCheckerTest, Rpatl) { ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1,2,3>> Pmin=? [F [2,5] \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <<1,2,3,4,5>> Pmax=? [\"label1\" U [0,7] \"label2\"]")); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <<1,2,3,4,5>> Pmax=? [\"label1\" U [0,7] \"label2\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmax=? [G \"label\"]")); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmax=? [G \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmin=? [G \"label\"]")); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmin=? [G \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); } diff --git a/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp index 7fda8f70c..91f677fc7 100644 --- a/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp @@ -6,6 +6,7 @@ #include "storm-parsers/api/model_descriptions.h" #include "storm/api/properties.h" #include "storm-parsers/api/properties.h" +#include "storm/api/export.h" #include "storm/models/sparse/Smg.h" #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" @@ -99,15 +100,15 @@ namespace { fileNames.push_back("dieSelectionPostSafetygamma07Pmin"); // testing create shielding expressions - std::string formulasString = "<" + fileNames[0] + ", PreSafety, lambda=0.8> Pmax=? [ F <5 \"done\" ]"; - formulasString += "; <" + fileNames[1] + ", PreSafety, gamma=0.8> Pmax=? [ F <5 \"done\" ]"; - formulasString += "; <" + fileNames[2] + ", PreSafety, lambda=0.8> Pmin=? [ F <5 \"done\" ]"; - formulasString += "; <" + fileNames[3] + ", PreSafety, gamma=0.8> Pmin=? [ F <5 \"done\" ]"; + std::string formulasString = " Pmax=? [ F <5 \"done\" ]"; + formulasString += "; Pmax=? [ F <5 \"done\" ]"; + formulasString += "; Pmin=? [ F <5 \"done\" ]"; + formulasString += "; Pmin=? [ F <5 \"done\" ]"; - formulasString += "; <" + fileNames[4] + ", PostSafety, lambda=0.7> Pmax=? [ F <6 \"two\" ]"; - formulasString += "; <" + fileNames[5] + ", PostSafety, gamma=0.7> Pmax=? [ F <6 \"two\" ]"; - formulasString += "; <" + fileNames[6] + ", PostSafety, lambda=0.7> Pmin=? [ F <6 \"two\" ]"; - formulasString += "; <" + fileNames[7] + ", PostSafety, gamma=0.7> Pmin=? [ F <6 \"two\" ]"; + formulasString += "; Pmax=? [ F <6 \"two\" ]"; + formulasString += "; Pmax=? [ F <6 \"two\" ]"; + formulasString += "; Pmin=? [ F <6 \"two\" ]"; + formulasString += "; Pmin=? [ F <6 \"two\" ]"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/die_selection.nm", formulasString); auto mdp = std::move(modelFormulas.first); @@ -130,66 +131,90 @@ namespace { // shielding results filename = fileNames[0]; - auto preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value08)); + auto preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonRelative, value08)); tasks[0].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[0].isShieldingTask()); auto result = checker.check(this->env(), tasks[0]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(mdp, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[1]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value08)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonAbsolute, value08)); tasks[1].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[1].isShieldingTask()); result = checker.check(this->env(), tasks[1]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(mdp, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[2]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value08)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonRelative, value08)); tasks[2].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[2].isShieldingTask()); result = checker.check(this->env(), tasks[2]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(mdp, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[3]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value08)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonAbsolute, value08)); tasks[3].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[3].isShieldingTask()); result = checker.check(this->env(), tasks[3]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(mdp, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[4]; - auto postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value07)); + auto postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonRelative, value07)); tasks[4].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[4].isShieldingTask()); result = checker.check(this->env(), tasks[4]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(mdp, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[5]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value07)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonAbsolute, value07)); tasks[5].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[5].isShieldingTask()); result = checker.check(this->env(), tasks[5]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(mdp, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[6]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value07)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonRelative, value07)); tasks[6].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[6].isShieldingTask()); result = checker.check(this->env(), tasks[6]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(mdp, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[7]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value07)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonAbsolute, value07)); tasks[7].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[7].isShieldingTask()); result = checker.check(this->env(), tasks[7]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(mdp, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); } diff --git a/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp index 096766c29..9009df76f 100644 --- a/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp @@ -5,6 +5,7 @@ #include "storm/api/builder.h" #include "storm-parsers/api/model_descriptions.h" #include "storm/api/properties.h" +#include "storm/api/export.h" #include "storm-parsers/api/properties.h" #include "storm/models/sparse/Smg.h" @@ -107,23 +108,23 @@ namespace { fileNames.push_back("rightDecisionPostSafetyGamma05PminF5"); // testing create shielding expressions - std::string formulasString = "<" + fileNames[0] + ", PreSafety, lambda=0.9> <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <" + fileNames[1] + ", PreSafety, lambda=0.9> <> Pmin=? [ F <=3 \"target\" ]"; - formulasString += "; <" + fileNames[2] + ", PreSafety, gamma=0.9> <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <" + fileNames[3] + ", PreSafety, gamma=0.9> <> Pmin=? [ F <=3 \"target\" ]"; - formulasString += "; <" + fileNames[4] + ", PostSafety, lambda=0.9> <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <" + fileNames[5] + ", PostSafety, lambda=0.9> <> Pmin=? [ F <=3 \"target\" ]"; - formulasString += "; <" + fileNames[6] + ", PostSafety, gamma=0.9> <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <" + fileNames[7] + ", PostSafety, gamma=0.9> <> Pmin=? [ F <=3 \"target\" ]"; - - formulasString += "; <" + fileNames[8] + ", PreSafety, lambda=0.5> <> Pmax=? [ F <=5 \"target\" ]"; - formulasString += "; <" + fileNames[9] + ", PreSafety, lambda=0.5> <> Pmin=? [ F <=5 \"target\" ]"; - formulasString += "; <" + fileNames[10] + ", PreSafety, gamma=0.5> <> Pmax=? [ F <=5 \"target\" ]"; - formulasString += "; <" + fileNames[11] + ", PreSafety, gamma=0.5> <> Pmin=? [ F <=5 \"target\" ]"; - formulasString += "; <" + fileNames[12] + ", PostSafety, lambda=0.5> <> Pmax=? [ F <=5 \"target\" ]"; - formulasString += "; <" + fileNames[13] + ", PostSafety, lambda=0.5> <> Pmin=? [ F <=5 \"target\" ]"; - formulasString += "; <" + fileNames[14] + ", PostSafety, gamma=0.5> <> Pmax=? [ F <=5 \"target\" ]"; - formulasString += "; <" + fileNames[15] + ", PostSafety, gamma=0.5> <> Pmin=? [ F <=5 \"target\" ]"; + std::string formulasString = " <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmin=? [ F <=3 \"target\" ]"; + + formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmin=? [ F <=5 \"target\" ]"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/rightDecision.nm", formulasString); auto smg = std::move(modelFormulas.first); @@ -147,131 +148,179 @@ namespace { // shielding results filename = fileNames[0]; - auto preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value09)); + auto preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonRelative, value09)); tasks[0].setShieldingExpression(preSafetyShieldingExpression); - EXPECT_TRUE(tasks[0].isShieldingTask()); + EXPECT_TRUE(tasks[0].isShieldingTask()); auto result = checker.check(this->env(), tasks[0]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[1]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value09)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonRelative, value09)); tasks[1].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[1].isShieldingTask()); result = checker.check(this->env(), tasks[1]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[2]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value09)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonAbsolute, value09)); tasks[2].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[2].isShieldingTask()); result = checker.check(this->env(), tasks[2]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[3]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value09)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonAbsolute, value09)); tasks[3].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[3].isShieldingTask()); result = checker.check(this->env(), tasks[3]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[4]; - auto postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value09)); + auto postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonRelative, value09)); tasks[4].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[4].isShieldingTask()); result = checker.check(this->env(), tasks[4]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[5]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value09)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonRelative, value09)); tasks[5].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[5].isShieldingTask()); result = checker.check(this->env(), tasks[5]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[6]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value09)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonAbsolute, value09)); tasks[6].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[6].isShieldingTask()); result = checker.check(this->env(), tasks[6]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[7]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value09)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonAbsolute, value09)); tasks[7].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[7].isShieldingTask()); result = checker.check(this->env(), tasks[7]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[8]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value05)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonRelative, value05)); tasks[8].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[8].isShieldingTask()); result = checker.check(this->env(), tasks[8]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[9]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value05)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonRelative, value05)); tasks[9].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[9].isShieldingTask()); result = checker.check(this->env(), tasks[9]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[10]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value05)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonAbsolute, value05)); tasks[10].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[10].isShieldingTask()); result = checker.check(this->env(), tasks[10]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[11]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value05)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonAbsolute, value05)); tasks[11].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[11].isShieldingTask()); result = checker.check(this->env(), tasks[11]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[12]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value05)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonRelative, value05)); tasks[12].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[12].isShieldingTask()); result = checker.check(this->env(), tasks[12]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[13]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value05)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonRelative, value05)); tasks[13].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[13].isShieldingTask()); result = checker.check(this->env(), tasks[13]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[14]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value05)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonAbsolute, value05)); tasks[14].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[14].isShieldingTask()); result = checker.check(this->env(), tasks[14]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[15]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value05)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonAbsolute, value05)); tasks[15].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[15].isShieldingTask()); result = checker.check(this->env(), tasks[15]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); } diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index 79217c614..765d08135 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -17,6 +17,11 @@ #include "storm/settings/modules/CoreSettings.h" #include "storm/logic/Formulas.h" #include "storm/exceptions/UncheckedRequirementException.h" +#include "storm/solver/Multiplier.h" +#include "storm/storage/SparseMatrix.h" +#include "storm/utility/graph.h" +#include "storm/storage/MaximalEndComponentDecomposition.h" +#include "storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h" namespace { @@ -345,5 +350,286 @@ namespace { EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } + TYPED_TEST(SmgRpatlModelCheckerTest, Deflate) { + typedef double ValueType; + std::string formulasString = " <> Pmax=? [F (s=2)]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/example_smg.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + auto transitionMatrix = model->getTransitionMatrix(); + + auto formulas = std::move(modelFormulas.second); + storm::logic::GameFormula const& gameFormula = formulas[0]->asGameFormula(); + + storm::modelchecker::CheckTask checkTask(gameFormula); + + storm::storage::BitVector statesOfCoalition = model->computeStatesOfCoalition(gameFormula.getCoalition()); + statesOfCoalition.complement(); + + + storm::storage::BitVector psiStates = checker->check(this->env(), gameFormula.getSubformula().asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().asStateFormula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector phiStates(model->getNumberOfStates(), true); + + storm::storage::SparseMatrix backwardTransitions = model->getBackwardTransitions(); + storm::OptimizationDirection optimizationDirection = gameFormula.getSubformula().asOperatorFormula().getOptimalityType(); + auto minimizerStates = optimizationDirection == storm::OptimizationDirection::Maximize ? statesOfCoalition : ~statesOfCoalition; + + storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, backwardTransitions, statesOfCoalition, psiStates, optimizationDirection); + viHelper.prepareSolversAndMultipliers(this->env()); + + std::vector xL = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + for (size_t i = 0; i < xL.size(); i++) + { + if (psiStates[i]) + xL[i] = 1; + } + + std::vector xU = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + storm::storage::BitVector probGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates); + auto xU_begin = xU.begin(); + std::for_each(xU.begin(), xU.end(), [&probGreater0, &xU_begin](ValueType &it) + { + if (probGreater0[&it - &(*xU_begin)]) + it = 1; + }); + + // performValueIteration + std::vector _x1L = xL; + std::vector _x2L = _x1L; + + std::vector _x1U = xU; + std::vector _x2U = _x1U; + + // perform first iteration step + storm::storage::BitVector reducedMinimizerActions = {storm::storage::BitVector(transitionMatrix.getRowCount(), true)}; + std::vector choiceValuesL = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); + + viHelper._multiplier->multiply(this->env(), _x2L, nullptr, choiceValuesL); + viHelper.reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, _x1L); + + + // over approximation + std::vector choiceValuesU = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); + + viHelper._multiplier->multiply(this->env(), _x2U, nullptr, choiceValuesU); + viHelper.reduceChoiceValues(choiceValuesU, nullptr, _x1U); + + storm::storage::SparseMatrix restrictedTransMatrix = transitionMatrix.restrictRows(reducedMinimizerActions); + + storm::storage::MaximalEndComponentDecomposition MSEC = storm::storage::MaximalEndComponentDecomposition(restrictedTransMatrix, backwardTransitions); + + // testing MSEC + // ===================================================== + ASSERT_TRUE(MSEC.size() == 3); + storm::storage::MaximalEndComponent const& mec1 = MSEC[0]; + if (mec1.containsState(0)) { + ASSERT_TRUE(mec1.containsState(1)); + ASSERT_FALSE(mec1.containsState(2)); + ASSERT_FALSE(mec1.containsState(3)); + } + else if (mec1.containsState(2)) { + ASSERT_FALSE(mec1.containsState(0)); + ASSERT_FALSE(mec1.containsState(1)); + ASSERT_FALSE(mec1.containsState(3)); + } + else if (mec1.containsState(3)) { + ASSERT_FALSE(mec1.containsState(0)); + ASSERT_FALSE(mec1.containsState(1)); + ASSERT_FALSE(mec1.containsState(2)); + } + else { + // This case must never happen + ASSERT_TRUE(false); + } + + storm::storage::MaximalEndComponent const& mec2 = MSEC[1]; + if (mec2.containsState(0)) { + ASSERT_TRUE(mec2.containsState(1)); + ASSERT_FALSE(mec2.containsState(2)); + ASSERT_FALSE(mec2.containsState(3)); + } + else if (mec2.containsState(2)) { + ASSERT_FALSE(mec2.containsState(0)); + ASSERT_FALSE(mec2.containsState(1)); + ASSERT_FALSE(mec2.containsState(3)); + } + else if (mec2.containsState(3)) { + ASSERT_FALSE(mec2.containsState(0)); + ASSERT_FALSE(mec2.containsState(1)); + ASSERT_FALSE(mec2.containsState(2)); + } + else { + // This case must never happen + ASSERT_TRUE(false); + } + + storm::storage::MaximalEndComponent const& mec3 = MSEC[2]; + if (mec3.containsState(0)) { + ASSERT_TRUE(mec3.containsState(1)); + ASSERT_FALSE(mec3.containsState(2)); + ASSERT_FALSE(mec3.containsState(3)); + } + else if (mec3.containsState(2)) { + ASSERT_FALSE(mec3.containsState(0)); + ASSERT_FALSE(mec3.containsState(1)); + ASSERT_FALSE(mec3.containsState(3)); + } + else if (mec3.containsState(3)) { + ASSERT_FALSE(mec3.containsState(0)); + ASSERT_FALSE(mec3.containsState(1)); + ASSERT_FALSE(mec3.containsState(2)); + } + else { + // This case must never happen + ASSERT_TRUE(false); + } + // ===================================================== + + // reducing the choiceValuesU + size_t i = 0; + auto new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) { + bool ret = !(reducedMinimizerActions[i]); + i++; + return ret; + }); + choiceValuesU.erase(new_end, choiceValuesU.end()); + + // deflating the MSECs + viHelper.deflate(MSEC, restrictedTransMatrix, _x1U, choiceValuesU); + + xL = _x1L; + xU = _x1U; + + // testing x vectors + // ===================================================== + EXPECT_NEAR(this->parseNumber("0"), xL[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0.333333"), xL[1], this->precision()); + EXPECT_NEAR(this->parseNumber("1"), xL[2], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), xL[3], this->precision()); + + EXPECT_NEAR(this->parseNumber("0.666666"), xU[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0.666666"), xU[1], this->precision()); + EXPECT_NEAR(this->parseNumber("1"), xU[2], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), xU[3], this->precision()); + // ===================================================== + + // perform second iteration step + reducedMinimizerActions = {storm::storage::BitVector(transitionMatrix.getRowCount(), true)}; + choiceValuesL = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); + + viHelper._multiplier->multiply(this->env(), _x1L, nullptr, choiceValuesL); + viHelper.reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, _x2L); + + + // over approximation + choiceValuesU = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); + + viHelper._multiplier->multiply(this->env(), _x1U, nullptr, choiceValuesU); + viHelper.reduceChoiceValues(choiceValuesU, nullptr, _x2U); + + restrictedTransMatrix = transitionMatrix.restrictRows(reducedMinimizerActions); + + MSEC = storm::storage::MaximalEndComponentDecomposition(restrictedTransMatrix, backwardTransitions); + + // testing MSEC + // ===================================================== + ASSERT_TRUE(MSEC.size() == 3); + storm::storage::MaximalEndComponent const& mec4 = MSEC[0]; + if (mec4.containsState(0)) { + ASSERT_TRUE(mec4.containsState(1)); + ASSERT_FALSE(mec4.containsState(2)); + ASSERT_FALSE(mec4.containsState(3)); + } + else if (mec4.containsState(2)) { + ASSERT_FALSE(mec4.containsState(0)); + ASSERT_FALSE(mec4.containsState(1)); + ASSERT_FALSE(mec4.containsState(3)); + } + else if (mec4.containsState(3)) { + ASSERT_FALSE(mec4.containsState(0)); + ASSERT_FALSE(mec4.containsState(1)); + ASSERT_FALSE(mec4.containsState(2)); + } + else { + // This case must never happen + ASSERT_TRUE(false); + } + + storm::storage::MaximalEndComponent const& mec5 = MSEC[1]; + if (mec5.containsState(0)) { + ASSERT_TRUE(mec5.containsState(1)); + ASSERT_FALSE(mec5.containsState(2)); + ASSERT_FALSE(mec5.containsState(3)); + } + else if (mec5.containsState(2)) { + ASSERT_FALSE(mec5.containsState(0)); + ASSERT_FALSE(mec5.containsState(1)); + ASSERT_FALSE(mec5.containsState(3)); + } + else if (mec5.containsState(3)) { + ASSERT_FALSE(mec5.containsState(0)); + ASSERT_FALSE(mec5.containsState(1)); + ASSERT_FALSE(mec5.containsState(2)); + } + else { + // This case must never happen + ASSERT_TRUE(false); + } + + storm::storage::MaximalEndComponent const& mec6 = MSEC[2]; + if (mec6.containsState(0)) { + ASSERT_TRUE(mec6.containsState(1)); + ASSERT_FALSE(mec6.containsState(2)); + ASSERT_FALSE(mec6.containsState(3)); + } + else if (mec6.containsState(2)) { + ASSERT_FALSE(mec6.containsState(0)); + ASSERT_FALSE(mec6.containsState(1)); + ASSERT_FALSE(mec6.containsState(3)); + } + else if (mec6.containsState(3)) { + ASSERT_FALSE(mec6.containsState(0)); + ASSERT_FALSE(mec6.containsState(1)); + ASSERT_FALSE(mec6.containsState(2)); + } + else { + // This case must never happen + ASSERT_TRUE(false); + } + // ===================================================== + + // reducing the choiceValuesU + i = 0; + new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) { + bool ret = !(reducedMinimizerActions[i]); + i++; + return ret; + }); + choiceValuesU.erase(new_end, choiceValuesU.end()); + + // deflating the MSECs + viHelper.deflate(MSEC, restrictedTransMatrix, _x2U, choiceValuesU); + + xL = _x2L; + xU = _x2U; + + // testing x vectors + // ===================================================== + EXPECT_NEAR(this->parseNumber("0.333333"), xL[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0.444444"), xL[1], this->precision()); + EXPECT_NEAR(this->parseNumber("1"), xL[2], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), xL[3], this->precision()); + + EXPECT_NEAR(this->parseNumber("0.555555"), xU[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0.555555"), xU[1], this->precision()); + EXPECT_NEAR(this->parseNumber("1"), xU[2], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), xU[3], this->precision()); + // ===================================================== + + } + // TODO: create more test cases (files) } diff --git a/src/test/storm/parser/GameShieldingParserTest.cpp b/src/test/storm/parser/GameShieldingParserTest.cpp index a6ed3cb88..f19cb757b 100644 --- a/src/test/storm/parser/GameShieldingParserTest.cpp +++ b/src/test/storm/parser/GameShieldingParserTest.cpp @@ -6,9 +6,8 @@ TEST(GameShieldingParserTest, PreSafetyShieldTest) { storm::parser::FormulaParser formulaParser; - std::string filename = "preSafetyShieldFileName"; std::string value = "0.9"; - std::string input = "<" + filename + ", PreSafety, lambda=" + value + "> <> Pmax=? [F \"label\"]"; + std::string input = " <> Pmax=? [F \"label\"]"; std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); @@ -25,15 +24,13 @@ TEST(GameShieldingParserTest, PreSafetyShieldTest) { EXPECT_FALSE(shieldExpression->isOptimalShield()); EXPECT_TRUE(shieldExpression->isRelative()); EXPECT_EQ(std::stod(value), shieldExpression->getValue()); - EXPECT_EQ(filename, shieldExpression->getFilename()); } TEST(GameShieldingParserTest, PostShieldTest) { storm::parser::FormulaParser formulaParser; - std::string filename = "postSafetyShieldFileName"; std::string value = "0.7569"; - std::string input = "<" + filename + ", PostSafety, gamma=" + value + "> <> Pmin=? [X !\"label\"]"; + std::string input = " <> Pmin=? [X !\"label\"]"; std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); @@ -50,7 +47,6 @@ TEST(GameShieldingParserTest, PostShieldTest) { EXPECT_FALSE(shieldExpression->isOptimalShield()); EXPECT_FALSE(shieldExpression->isRelative()); EXPECT_EQ(std::stod(value), shieldExpression->getValue()); - EXPECT_EQ(filename, shieldExpression->getFilename()); } TEST(GameShieldingParserTest, OptimalShieldTest) { @@ -60,8 +56,7 @@ TEST(GameShieldingParserTest, OptimalShieldTest) { storm::parser::FormulaParser formulaParser(manager); - std::string filename = "optimalShieldFileName"; - std::string input = "<" + filename + ", Optimal> <> Pmax=? [G x>y]"; + std::string input = " <> Pmax=? [G x>y]"; std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); @@ -76,5 +71,4 @@ TEST(GameShieldingParserTest, OptimalShieldTest) { EXPECT_FALSE(shieldExpression->isPreSafetyShield()); EXPECT_FALSE(shieldExpression->isPostSafetyShield()); EXPECT_TRUE(shieldExpression->isOptimalShield()); - EXPECT_EQ(filename, shieldExpression->getFilename()); } diff --git a/src/test/storm/parser/MdpShieldingParserTest.cpp b/src/test/storm/parser/MdpShieldingParserTest.cpp index 84b69d6db..5efa3e40d 100644 --- a/src/test/storm/parser/MdpShieldingParserTest.cpp +++ b/src/test/storm/parser/MdpShieldingParserTest.cpp @@ -6,9 +6,8 @@ TEST(MdpShieldingParserTest, PreSafetyShieldTest) { storm::parser::FormulaParser formulaParser; - std::string filename = "preSafetyShieldFileName"; std::string value = "0.6667"; - std::string input = "<" + filename + ", PreSafety, gamma=" + value + "> Pmax=? [F \"label\"]"; + std::string input = " Pmax=? [F \"label\"]"; std::shared_ptr formula(nullptr); std::vector property; @@ -22,7 +21,6 @@ TEST(MdpShieldingParserTest, PreSafetyShieldTest) { EXPECT_FALSE(shieldExpression->isOptimalShield()); EXPECT_FALSE(shieldExpression->isRelative()); EXPECT_EQ(std::stod(value), shieldExpression->getValue()); - EXPECT_EQ(filename, shieldExpression->getFilename()); } TEST(MdpShieldingParserTest, PostShieldTest) { @@ -30,7 +28,7 @@ TEST(MdpShieldingParserTest, PostShieldTest) { std::string filename = "postSafetyShieldFileName"; std::string value = "0.95"; - std::string input = "<" + filename + ", PostSafety, lambda=" + value + "> Pmin=? [X !\"label\"]"; + std::string input = " Pmin=? [X !\"label\"]"; std::shared_ptr formula(nullptr); std::vector property; @@ -44,7 +42,6 @@ TEST(MdpShieldingParserTest, PostShieldTest) { EXPECT_FALSE(shieldExpression->isOptimalShield()); EXPECT_TRUE(shieldExpression->isRelative()); EXPECT_EQ(std::stod(value), shieldExpression->getValue()); - EXPECT_EQ(filename, shieldExpression->getFilename()); } TEST(MdpShieldingParserTest, OptimalShieldTest) { @@ -55,7 +52,7 @@ TEST(MdpShieldingParserTest, OptimalShieldTest) { storm::parser::FormulaParser formulaParser(manager); std::string filename = "optimalShieldFileName"; - std::string input = "<" + filename + ", Optimal> Pmax=? [G (a|x>3)]"; + std::string input = " Pmax=? [G (a|x>3)]"; std::shared_ptr formula(nullptr); std::vector property; @@ -67,5 +64,4 @@ TEST(MdpShieldingParserTest, OptimalShieldTest) { EXPECT_FALSE(shieldExpression->isPreSafetyShield()); EXPECT_FALSE(shieldExpression->isPostSafetyShield()); EXPECT_TRUE(shieldExpression->isOptimalShield()); - EXPECT_EQ(filename, shieldExpression->getFilename()); }