From 2d8cc1681cf40fb6b45e3fb5c7beb03e26e78551 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 12 Dec 2017 14:37:22 +0100 Subject: [PATCH 01/18] Fixed indentation --- doc/checklist_new_release.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/checklist_new_release.md b/doc/checklist_new_release.md index a0462b5d8..5fda82ab5 100644 --- a/doc/checklist_new_release.md +++ b/doc/checklist_new_release.md @@ -8,8 +8,8 @@ Note that in most case a simultaneous release of [carl](https://github.com/smtra ``` 2. Update used carl version: - * Update `GIT_TAG` in `resources/3rdparty/carl/CMakeLists.txt` - * Maybe update `CARL_MINVERSION` in `resources/3rdparty/CMakeLists.txt` + * Update `GIT_TAG` in `resources/3rdparty/carl/CMakeLists.txt` + * Maybe update `CARL_MINVERSION` in `resources/3rdparty/CMakeLists.txt` 3. Check that storm builds without errors and all tests are successful * [Travis](https://travis-ci.org/moves-rwth/storm) should run successfully From d8e166094f449369a1024a471b4037f7bd90a9d0 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 12 Dec 2017 14:37:50 +0100 Subject: [PATCH 02/18] Message in cmake if ccache is disabled --- CMakeLists.txt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index c0d958476..0edec97d7 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -105,6 +105,8 @@ if(STORM_COMPILE_WITH_CCACHE) else() message(STATUS "Storm - Could not find ccache.") endif() +else() + message(STATUS "Storm - Disabled use of ccache.") endif() # Directory for test resources. From 91a9f5622f96301e4a7569f4102299773bb69bc5 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 12 Dec 2017 14:43:45 +0100 Subject: [PATCH 03/18] Push successful builds in travis to dockerhub --- .travis.yml | 8 ++++++++ travis/generate_travis.py | 12 ++++++++++++ 2 files changed, 20 insertions(+) diff --git a/.travis.yml b/.travis.yml index fcc0a9a2f..2e0566f2f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -291,6 +291,10 @@ jobs: - docker cp storm:/storm/. . after_failure: - find build -iname '*err*.log' -type f -print -exec cat {} \; + after_success: + - docker login -u '$DOCKER_USERNAME' -p '$DOCKER_PASSWORD'; + - docker tag storm mvolk/storm-debug:travis; + - docker push mvolk/storm-debug:travis; - stage: Test all os: linux compiler: gcc @@ -303,4 +307,8 @@ jobs: - docker cp storm:/storm/. . after_failure: - find build -iname '*err*.log' -type f -print -exec cat {} \; + after_success: + - docker login -u '$DOCKER_USERNAME' -p '$DOCKER_PASSWORD'; + - docker tag storm mvolk/storm:travis; + - docker push mvolk/storm:travis; diff --git a/travis/generate_travis.py b/travis/generate_travis.py index f3ae09641..c50201563 100644 --- a/travis/generate_travis.py +++ b/travis/generate_travis.py @@ -119,6 +119,18 @@ if __name__ == "__main__": buildConfig += " - docker cp storm:/storm/. .\n" buildConfig += " after_failure:\n" buildConfig += " - find build -iname '*err*.log' -type f -print -exec cat {} \;\n" + # Upload to dockerhub + if stage[1] == "TestAll": + buildConfig += " after_success:\n" + buildConfig += " - docker login -u '$DOCKER_USERNAME' -p '$DOCKER_PASSWORD';\n" + if "Debug" in build: + buildConfig += " - docker tag storm mvolk/storm-debug:travis;\n" + buildConfig += " - docker push mvolk/storm-debug:travis;\n" + elif "Release" in build: + buildConfig += " - docker tag storm mvolk/storm:travis;\n" + buildConfig += " - docker push mvolk/storm:travis;\n" + else: + assert False s += buildConfig print(s) From 49a6c5f4edcd647e85184c88e6d336ad918e2750 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 13 Dec 2017 17:51:35 +0100 Subject: [PATCH 04/18] Fixed docker upload in travis --- .travis.yml | 8 ++++---- travis/generate_travis.py | 6 +++--- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/.travis.yml b/.travis.yml index 2e0566f2f..4995abe2d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -292,8 +292,8 @@ jobs: after_failure: - find build -iname '*err*.log' -type f -print -exec cat {} \; after_success: - - docker login -u '$DOCKER_USERNAME' -p '$DOCKER_PASSWORD'; - - docker tag storm mvolk/storm-debug:travis; + - docker login -u "$DOCKER_USERNAME" -p "$DOCKER_PASSWORD"; + - docker commit storm mvolk/storm-debug:travis; - docker push mvolk/storm-debug:travis; - stage: Test all os: linux @@ -308,7 +308,7 @@ jobs: after_failure: - find build -iname '*err*.log' -type f -print -exec cat {} \; after_success: - - docker login -u '$DOCKER_USERNAME' -p '$DOCKER_PASSWORD'; - - docker tag storm mvolk/storm:travis; + - docker login -u "$DOCKER_USERNAME" -p "$DOCKER_PASSWORD"; + - docker commit storm mvolk/storm:travis; - docker push mvolk/storm:travis; diff --git a/travis/generate_travis.py b/travis/generate_travis.py index c50201563..b104661f1 100644 --- a/travis/generate_travis.py +++ b/travis/generate_travis.py @@ -122,12 +122,12 @@ if __name__ == "__main__": # Upload to dockerhub if stage[1] == "TestAll": buildConfig += " after_success:\n" - buildConfig += " - docker login -u '$DOCKER_USERNAME' -p '$DOCKER_PASSWORD';\n" + buildConfig += ' - docker login -u "$DOCKER_USERNAME" -p "$DOCKER_PASSWORD";\n' if "Debug" in build: - buildConfig += " - docker tag storm mvolk/storm-debug:travis;\n" + buildConfig += " - docker commit storm mvolk/storm-debug:travis;\n" buildConfig += " - docker push mvolk/storm-debug:travis;\n" elif "Release" in build: - buildConfig += " - docker tag storm mvolk/storm:travis;\n" + buildConfig += " - docker commit storm mvolk/storm:travis;\n" buildConfig += " - docker push mvolk/storm:travis;\n" else: assert False From dd864c05e07d51a1fb222a48d1df00a11515c41c Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 14 Dec 2017 11:43:04 +0100 Subject: [PATCH 05/18] properly resizing weights vector in Fox-Glynn if the right bound is moved further due to the desired accuracy --- src/storm/utility/numerical.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storm/utility/numerical.cpp b/src/storm/utility/numerical.cpp index cec474ff7..2f2b64355 100644 --- a/src/storm/utility/numerical.cpp +++ b/src/storm/utility/numerical.cpp @@ -229,6 +229,7 @@ namespace storm { } else { t = j; result.right = j + result.left; + result.weights.resize(result.right - result.left + 1); // It's time to compute W. break; From 109b738258d94d13571e2e0ba4142f399733fc21 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 14 Dec 2017 17:31:52 +0100 Subject: [PATCH 06/18] adding some more output to Fox-Glynn --- src/storm/utility/numerical.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/utility/numerical.cpp b/src/storm/utility/numerical.cpp index 2f2b64355..38b793fa5 100644 --- a/src/storm/utility/numerical.cpp +++ b/src/storm/utility/numerical.cpp @@ -258,8 +258,8 @@ namespace storm { } result.totalWeight += result.weights[j]; - STORM_LOG_TRACE("Fox-Glynn: ltp = " << result.left << ", rtp = " << result.right << ", w = " << result.totalWeight << "."); - + STORM_LOG_TRACE("Fox-Glynn(lambda=" << lambda << ", eps=" << epsilon << "): ltp = " << result.left << ", rtp = " << result.right << ", w = " << result.totalWeight << "."); + return result; } From 37e0385e6939a7c637163abc6539c4f9a1f7ae7d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 15 Dec 2017 11:05:14 +0100 Subject: [PATCH 07/18] Remove hack in travis tests --- travis/build-helper.sh | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/travis/build-helper.sh b/travis/build-helper.sh index 04c2dc52e..7d722dc99 100755 --- a/travis/build-helper.sh +++ b/travis/build-helper.sh @@ -50,13 +50,7 @@ run() { # Test all travis_fold start test_all cd build - # Hack to avoid memout problem with jit and sylvan - # 1. Run other tests without builder tests - ctest test --output-on-failure -E run-test-builder - # 2. Run builder tests without sylvan tests - ./bin/test-builder --gtest_filter=-"DdJaniModelBuilderTest_Sylvan.*" - # 3. Just run sylvan tests - ./bin/test-builder --gtest_filter="DdJaniModelBuilderTest_Sylvan.*" + ctest test --output-on-failure travis_fold end test_all ;; From 88851f0105a72be35ca85c33087455a7fc724945 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 18 Dec 2017 23:34:58 +0100 Subject: [PATCH 08/18] install headers to include/storm --- src/storm/CMakeLists.txt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt index 0ed4b0d1c..0cf8d3183 100644 --- a/src/storm/CMakeLists.txt +++ b/src/storm/CMakeLists.txt @@ -74,3 +74,5 @@ add_dependencies(binaries storm-main) # installation install(TARGETS storm RUNTIME DESTINATION bin LIBRARY DESTINATION lib) install(TARGETS storm-main RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) +install(DIRECTORY ${CMAKE_BINARY_DIR}/include/ DESTINATION include/storm + FILES_MATCHING PATTERN "*.h") From 8e7d3107ca95d0f73e686f556c48fcb9fbca9cb2 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 20 Dec 2017 10:45:39 +0100 Subject: [PATCH 09/18] added function to check whether a matrix is the identity matrix --- src/storm/storage/SparseMatrix.cpp | 29 +++++++++++++++++++++++++++++ src/storm/storage/SparseMatrix.h | 3 +++ 2 files changed, 32 insertions(+) diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 9d92d5e35..83ff4f3af 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -2015,6 +2015,35 @@ namespace storm { return true; } + template + bool SparseMatrix::isIdentityMatrix() const { + if (this->getRowCount() != this->getColumnCount()) { + return false; + } + if (this->getNonzeroEntryCount() != this->getRowCount()) { + return false; + } + for (uint64_t row = 0; row < this->getRowCount(); ++row) { + bool rowHasEntry = false; + for (auto const& entry : this->getRow(row)) { + if (entry.getColumn() == row) { + if (!storm::utility::isOne(entry.getValue())) { + return false; + } + rowHasEntry = true; + } else { + if (!storm::utility::isZero(entry.getValue())) { + return false; + } + } + } + if (!rowHasEntry) { + return false; + } + } + return true; + } + template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix) { // Print column numbers in header. diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index 92cb31b00..08a23ab2e 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -929,6 +929,9 @@ namespace storm { template bool isSubmatrixOf(SparseMatrix const& matrix) const; + // Returns true if the matrix is the identity matrix + bool isIdentityMatrix() const; + template friend std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); From c59d2160ee69e252a39b969c013d9c09b0ea78bc Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 20 Dec 2017 10:46:38 +0100 Subject: [PATCH 10/18] Implemented (multi-dimensional) cost bounded properties for DTMCs (sparse engine only) --- .../prctl/SparseDtmcPrctlModelChecker.cpp | 48 +++-- .../prctl/helper/SparseDtmcPrctlHelper.cpp | 176 +++++++++++++++++- .../prctl/helper/SparseDtmcPrctlHelper.h | 6 +- .../prctl/helper/SparseMdpPrctlHelper.cpp | 8 +- .../MultiDimensionalRewardUnfolding.cpp | 95 ++++++++-- .../MultiDimensionalRewardUnfolding.h | 14 +- .../helper/rewardbounded/ProductModel.cpp | 18 +- .../prctl/helper/rewardbounded/ProductModel.h | 10 +- 8 files changed, 321 insertions(+), 54 deletions(-) diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 922adc4de..36e6eb9a2 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -36,21 +36,32 @@ namespace storm { template bool SparseDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true)); + return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true)); } template std::unique_ptr SparseDtmcPrctlModelChecker::computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); - STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound."); - STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); - std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); - std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *linearEquationSolverFactory, checkTask.getHint()); - std::unique_ptr result = std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); - return result; + if (pathFormula.isMultiDimensional() || pathFormula.getTimeBoundReference().isRewardBound()) { + STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Checking non-trivial bounded until probabilities can only be computed for the initial states of the model."); + storm::logic::OperatorInformation opInfo; + if (checkTask.isBoundSet()) { + opInfo.bound = checkTask.getBound(); + } + auto formula = std::make_shared(checkTask.getFormula().asSharedPointer(), opInfo); + auto numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeRewardBoundedValues(env, this->getModel(), formula, *linearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } else { + STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound."); + STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); + std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); + std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeStepBoundedUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *linearEquationSolverFactory, checkTask.getHint()); + std::unique_ptr result = std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + return result; + } } template @@ -85,9 +96,20 @@ namespace storm { template std::unique_ptr SparseDtmcPrctlModelChecker::computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); - STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *linearEquationSolverFactory); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + if (rewardPathFormula.isMultiDimensional() || rewardPathFormula.getTimeBoundReference().isRewardBound()) { + STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Checking non-trivial bounded until probabilities can only be computed for the initial states of the model."); + storm::logic::OperatorInformation opInfo; + if (checkTask.isBoundSet()) { + opInfo.bound = checkTask.getBound(); + } + auto formula = std::make_shared(checkTask.getFormula().asSharedPointer(), checkTask.getRewardModel(), opInfo); + auto numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeRewardBoundedValues(env, this->getModel(), formula, *linearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } else { + STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *linearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } } template diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 8d3f0f68d..fd52e4437 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -15,6 +15,18 @@ #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" #include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h" +#include "storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h" + +#include "storm/environment/solver/SolverEnvironment.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/IOSettings.h" + +#include "storm/utility/Stopwatch.h" +#include "storm/utility/ProgressMeasurement.h" +#include "storm/utility/export.h" #include "storm/utility/macros.h" #include "storm/utility/ConstantsComparator.h" @@ -29,12 +41,12 @@ namespace storm { namespace modelchecker { namespace helper { template - std::vector SparseDtmcPrctlHelper::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, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint) { + std::vector SparseDtmcPrctlHelper::computeStepBoundedUntilProbabilities(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, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint) { std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); // If we identify the states that have probability 0 of reaching the target states, we can exclude them in the further analysis. storm::storage::BitVector maybeStates; - + if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { maybeStates = hint.template asExplicitModelCheckerHint().getMaybeStates(); } else { @@ -68,8 +80,168 @@ namespace storm { return result; } + template + std::vector analyzeTrivialDtmcEpochModel(typename rewardbounded::MultiDimensionalRewardUnfolding::EpochModel& epochModel) { + + std::vector epochResult; + epochResult.reserve(epochModel.epochInStates.getNumberOfSetBits()); + auto stepSolutionIt = epochModel.stepSolutions.begin(); + auto stepChoiceIt = epochModel.stepChoices.begin(); + for (auto const& state : epochModel.epochInStates) { + while (*stepChoiceIt < state) { + ++stepChoiceIt; + ++stepSolutionIt; + } + if (epochModel.objectiveRewardFilter.front().get(state)) { + if (*stepChoiceIt == state) { + epochResult.push_back(epochModel.objectiveRewards.front()[state] + *stepSolutionIt); + } else { + epochResult.push_back(epochModel.objectiveRewards.front()[state]); + } + } else { + if (*stepChoiceIt == state) { + epochResult.push_back(*stepSolutionIt); + } else { + epochResult.push_back(storm::utility::zero()); + } + } + } + return epochResult; + } + + template + std::vector analyzeNonTrivialDtmcEpochModel(Environment const& env, typename rewardbounded::MultiDimensionalRewardUnfolding::EpochModel& epochModel, std::vector& x, std::vector& b, std::unique_ptr>& linEqSolver, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional const& lowerBound, boost::optional const& upperBound) { + + // Update some data for the case that the Matrix has changed + if (epochModel.epochMatrixChanged) { + x.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero()); + linEqSolver = linearEquationSolverFactory.create(env, epochModel.epochMatrix, storm::solver::LinearEquationSolverTask::SolveEquations); + linEqSolver->setCachingEnabled(true); + auto req = linEqSolver->getRequirements(env, storm::solver::LinearEquationSolverTask::SolveEquations); + if (lowerBound) { + linEqSolver->setLowerBound(lowerBound.get()); + req.clearLowerBounds(); + } + if (upperBound) { + linEqSolver->setUpperBound(upperBound.get()); + req.clearUpperBounds(); + } + STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked."); + } + + // Prepare the right hand side of the equation system + b.assign(epochModel.epochMatrix.getRowCount(), storm::utility::zero()); + std::vector const& objectiveValues = epochModel.objectiveRewards.front(); + for (auto const& choice : epochModel.objectiveRewardFilter.front()) { + b[choice] = objectiveValues[choice]; + } + auto stepSolutionIt = epochModel.stepSolutions.begin(); + for (auto const& choice : epochModel.stepChoices) { + b[choice] += *stepSolutionIt; + ++stepSolutionIt; + } + assert(stepSolutionIt == epochModel.stepSolutions.end()); + + // Solve the minMax equation system + linEqSolver->solveEquations(env, x, b); + + return storm::utility::vector::filterVector(x, epochModel.epochInStates); + } + + template<> + std::map SparseDtmcPrctlHelper::computeRewardBoundedValues(Environment const& env, storm::models::sparse::Dtmc const& model, std::shared_ptr rewardBoundedFormula, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The specified property is not supported by this value type."); + return std::map(); + } + template + std::map SparseDtmcPrctlHelper::computeRewardBoundedValues(Environment const& env, storm::models::sparse::Dtmc const& model, std::shared_ptr rewardBoundedFormula, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + storm::utility::Stopwatch swAll(true), swBuild, swCheck; + + storm::modelchecker::helper::rewardbounded::MultiDimensionalRewardUnfolding rewardUnfolding(model, rewardBoundedFormula); + + // Get lower and upper bounds for the solution. + auto lowerBound = rewardUnfolding.getLowerObjectiveBound(); + auto upperBound = rewardUnfolding.getUpperObjectiveBound(); + + // Initialize epoch models + auto initEpoch = rewardUnfolding.getStartEpoch(); + auto epochOrder = rewardUnfolding.getEpochComputationOrder(initEpoch); + + // initialize data that will be needed for each epoch + std::vector x, b; + std::unique_ptr> linEqSolver; + Environment preciseEnv = env; + ValueType precision = rewardUnfolding.getRequiredEpochModelPrecision(initEpoch, storm::utility::convertNumber(storm::settings::getModule().getPrecision())); + preciseEnv.solver().setLinearEquationSolverPrecision(storm::utility::convertNumber(precision)); + + // In case of cdf export we store the necessary data. + std::vector> cdfData; + + // Set the correct equation problem format + rewardUnfolding.setEquationSystemFormatForEpochModel(linearEquationSolverFactory.getEquationProblemFormat(preciseEnv)); + bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat(preciseEnv) == solver::LinearEquationSolverProblemFormat::EquationSystem; + + storm::utility::ProgressMeasurement progress("epochs"); + progress.setMaxCount(epochOrder.size()); + progress.startNewMeasurement(0); + uint64_t numCheckedEpochs = 0; + for (auto const& epoch : epochOrder) { + swBuild.start(); + auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch); + swBuild.stop(); swCheck.start(); + // If the epoch matrix is empty we do not need to solve a linear equation system + if ((convertToEquationSystem && epochModel.epochMatrix.isIdentityMatrix()) || (!convertToEquationSystem && epochModel.epochMatrix.getEntryCount() == 0)) { + rewardUnfolding.setSolutionForCurrentEpoch(analyzeTrivialDtmcEpochModel(epochModel)); + } else { + rewardUnfolding.setSolutionForCurrentEpoch(analyzeNonTrivialDtmcEpochModel(preciseEnv, epochModel, x, b, linEqSolver, linearEquationSolverFactory, lowerBound, upperBound)); + } + swCheck.stop(); + if (storm::settings::getModule().isExportCdfSet() && !rewardUnfolding.getEpochManager().hasBottomDimension(epoch)) { + std::vector cdfEntry; + for (uint64_t i = 0; i < rewardUnfolding.getEpochManager().getDimensionCount(); ++i) { + uint64_t offset = rewardUnfolding.getDimension(i).isUpperBounded ? 0 : 1; + cdfEntry.push_back(storm::utility::convertNumber(rewardUnfolding.getEpochManager().getDimensionOfEpoch(epoch, i) + offset) * rewardUnfolding.getDimension(i).scalingFactor); + } + cdfEntry.push_back(rewardUnfolding.getInitialStateResult(epoch)); + cdfData.push_back(std::move(cdfEntry)); + } + ++numCheckedEpochs; + progress.updateProgress(numCheckedEpochs); + } + + std::map result; + for (auto const& initState : model.getInitialStates()) { + result[initState] = rewardUnfolding.getInitialStateResult(initEpoch, initState); + } + + swAll.stop(); + + if (storm::settings::getModule().isExportCdfSet()) { + std::vector headers; + for (uint64_t i = 0; i < rewardUnfolding.getEpochManager().getDimensionCount(); ++i) { + headers.push_back(rewardUnfolding.getDimension(i).formula->toString()); + } + headers.push_back("Result"); + storm::utility::exportDataToCSVFile(storm::settings::getModule().getExportCdfDirectory() + "cdf.csv", cdfData, headers); + } + + if (storm::settings::getModule().isShowStatisticsSet()) { + STORM_PRINT_AND_LOG("---------------------------------" << std::endl); + STORM_PRINT_AND_LOG("Statistics:" << std::endl); + STORM_PRINT_AND_LOG("---------------------------------" << std::endl); + STORM_PRINT_AND_LOG(" #checked epochs: " << epochOrder.size() << "." << std::endl); + STORM_PRINT_AND_LOG(" overall Time: " << swAll << "." << std::endl); + STORM_PRINT_AND_LOG("Epoch Model building Time: " << swBuild << "." << std::endl); + STORM_PRINT_AND_LOG("Epoch Model checking Time: " << swCheck << "." << std::endl); + STORM_PRINT_AND_LOG("---------------------------------" << std::endl); + } + + return result; + } + + template std::vector SparseDtmcPrctlHelper::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::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint) { std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index 0c0712723..ead15de74 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -5,6 +5,7 @@ #include +#include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/hints/ModelCheckerHint.h" @@ -26,7 +27,10 @@ namespace storm { template > class SparseDtmcPrctlHelper { public: - static std::vector 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, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); + + static std::vector computeStepBoundedUntilProbabilities(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, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); + + static std::map computeRewardBoundedValues(Environment const& env, storm::models::sparse::Dtmc const& model, std::shared_ptr rewardBoundedFormula, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); static std::vector computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 8c7b0dc7e..10311c2a2 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -87,7 +87,7 @@ namespace storm { } template - std::vector analyzeTrivialEpochModel(OptimizationDirection dir, typename rewardbounded::MultiDimensionalRewardUnfolding::EpochModel& epochModel) { + std::vector analyzeTrivialMdpEpochModel(OptimizationDirection dir, typename rewardbounded::MultiDimensionalRewardUnfolding::EpochModel& epochModel) { // Assert that the epoch model is indeed trivial assert(epochModel.epochMatrix.getEntryCount() == 0); @@ -137,7 +137,7 @@ namespace storm { } template - std::vector analyzeNonTrivialEpochModel(Environment const& env, OptimizationDirection dir, typename rewardbounded::MultiDimensionalRewardUnfolding::EpochModel& epochModel, std::vector& x, std::vector& b, std::unique_ptr>& minMaxSolver, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional const& lowerBound, boost::optional const& upperBound) { + std::vector analyzeNonTrivialMdpEpochModel(Environment const& env, OptimizationDirection dir, typename rewardbounded::MultiDimensionalRewardUnfolding::EpochModel& epochModel, std::vector& x, std::vector& b, std::unique_ptr>& minMaxSolver, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional const& lowerBound, boost::optional const& upperBound) { // Update some data for the case that the Matrix has changed if (epochModel.epochMatrixChanged) { @@ -215,9 +215,9 @@ namespace storm { swBuild.stop(); swCheck.start(); // If the epoch matrix is empty we do not need to solve a linear equation system if (epochModel.epochMatrix.getEntryCount() == 0) { - rewardUnfolding.setSolutionForCurrentEpoch(analyzeTrivialEpochModel(dir, epochModel)); + rewardUnfolding.setSolutionForCurrentEpoch(analyzeTrivialMdpEpochModel(dir, epochModel)); } else { - rewardUnfolding.setSolutionForCurrentEpoch(analyzeNonTrivialEpochModel(preciseEnv, dir, epochModel, x, b, minMaxSolver, minMaxLinearEquationSolverFactory, lowerBound, upperBound)); + rewardUnfolding.setSolutionForCurrentEpoch(analyzeNonTrivialMdpEpochModel(preciseEnv, dir, epochModel, x, b, minMaxSolver, minMaxLinearEquationSolverFactory, lowerBound, upperBound)); } swCheck.stop(); if (storm::settings::getModule().isExportCdfSet() && !rewardUnfolding.getEpochManager().hasBottomDimension(epoch)) { diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp index ec599fd37..efc3c81f7 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -10,6 +10,8 @@ #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/Dtmc.h" #include "storm/transformer/EndComponentEliminator.h" @@ -24,14 +26,13 @@ namespace storm { namespace rewardbounded { template - MultiDimensionalRewardUnfolding::MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::vector> const& objectives) : model(model), objectives(objectives) { + MultiDimensionalRewardUnfolding::MultiDimensionalRewardUnfolding(storm::models::sparse::Model const& model, std::vector> const& objectives) : model(model), objectives(objectives) { initialize(); } template - MultiDimensionalRewardUnfolding::MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::shared_ptr objectiveFormula) : model(model) { + MultiDimensionalRewardUnfolding::MultiDimensionalRewardUnfolding(storm::models::sparse::Model const& model, std::shared_ptr objectiveFormula) : model(model) { - STORM_LOG_THROW(objectiveFormula->hasOptimalityType(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); if (objectiveFormula->isProbabilityOperatorFormula()) { if (objectiveFormula->getSubformula().isMultiObjectiveFormula()) { for (auto const& subFormula : objectiveFormula->getSubformula().asMultiObjectiveFormula().getSubformulas()) { @@ -91,7 +92,7 @@ namespace storm { // lower bounded until formulas with non-trivial left hand side are excluded as this would require some additional effort (in particular the ProductModel::transformMemoryState method). STORM_LOG_THROW(dimension.isUpperBounded || subformula.getLeftSubformula(dim).isTrueFormula(), storm::exceptions::NotSupportedException, "Lower bounded until formulas are only supported by this method if the left subformula is 'true'. Got " << subformula << " instead."); if (subformula.getTimeBoundReference(dim).isTimeBound() || subformula.getTimeBoundReference(dim).isStepBound()) { - dimensionWiseEpochSteps.push_back(std::vector(model.getNumberOfChoices(), 1)); + dimensionWiseEpochSteps.push_back(std::vector(model.getTransitionMatrix().getRowCount(), 1)); dimension.scalingFactor = storm::utility::one(); } else { STORM_LOG_ASSERT(subformula.getTimeBoundReference(dim).isRewardBound(), "Unexpected type of time bound."); @@ -114,7 +115,7 @@ namespace storm { dimension.objectiveIndex = objIndex; dimension.isUpperBounded = true; if (subformula.getTimeBoundReference(dim).isTimeBound() || subformula.getTimeBoundReference(dim).isStepBound()) { - dimensionWiseEpochSteps.push_back(std::vector(model.getNumberOfChoices(), 1)); + dimensionWiseEpochSteps.push_back(std::vector(model.getTransitionMatrix().getRowCount(), 1)); dimension.scalingFactor = storm::utility::one(); } else { STORM_LOG_ASSERT(subformula.getTimeBoundReference(dim).isRewardBound(), "Unexpected type of time bound."); @@ -166,8 +167,8 @@ namespace storm { epochManager = EpochManager(dimensions.size()); // Convert the epoch steps to a choice-wise representation - epochSteps.reserve(model.getNumberOfChoices()); - for (uint64_t choice = 0; choice < model.getNumberOfChoices(); ++choice) { + epochSteps.reserve(model.getTransitionMatrix().getRowCount()); + for (uint64_t choice = 0; choice < model.getTransitionMatrix().getRowCount(); ++choice) { Epoch step; uint64_t dim = 0; for (auto const& dimensionSteps : dimensionWiseEpochSteps) { @@ -396,7 +397,7 @@ namespace storm { // std::cout << "Setting epoch class for epoch " << epochManager.toString(epoch) << std::endl; auto productObjectiveRewards = productModel->computeObjectiveRewards(epochClass, objectives); - storm::storage::BitVector stepChoices(productModel->getProduct().getNumberOfChoices(), false); + storm::storage::BitVector stepChoices(productModel->getProduct().getTransitionMatrix().getRowCount(), false); uint64_t choice = 0; for (auto const& step : productModel->getSteps()) { if (!epochManager.isZeroEpoch(step) && epochManager.getSuccessorEpoch(epoch, step) != epoch) { @@ -421,7 +422,7 @@ namespace storm { } } - storm::storage::BitVector zeroObjRewardChoices(productModel->getProduct().getNumberOfChoices(), true); + storm::storage::BitVector zeroObjRewardChoices(productModel->getProduct().getTransitionMatrix().getRowCount(), true); for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { if (violatedLowerBoundedDimensions.isDisjointFrom(objectiveDimensions[objIndex])) { zeroObjRewardChoices &= storm::utility::vector::filterZero(productObjectiveRewards[objIndex]); @@ -433,15 +434,68 @@ namespace storm { storm::storage::BitVector productInStates = productModel->getInStates(epochClass); // The epoch model only needs to consider the states that are reachable from a relevant state storm::storage::BitVector consideredStates = storm::utility::graph::getReachableStates(epochModel.epochMatrix, productInStates, allProductStates, ~allProductStates); - // std::cout << "numInStates = " << productInStates.getNumberOfSetBits() << std::endl; - // std::cout << "numConsideredStates = " << consideredStates.getNumberOfSetBits() << std::endl; // We assume that there is no end component in which objective reward is earned STORM_LOG_ASSERT(!storm::utility::graph::checkIfECWithChoiceExists(epochModel.epochMatrix, epochModel.epochMatrix.transpose(true), allProductStates, ~zeroObjRewardChoices & ~stepChoices), "There is a scheduler that yields infinite reward for one objective. This case should be excluded"); - auto ecElimResult = storm::transformer::EndComponentEliminator::transform(epochModel.epochMatrix, consideredStates, zeroObjRewardChoices & ~stepChoices, consideredStates); - epochModel.epochMatrix = std::move(ecElimResult.matrix); - epochModelToProductChoiceMap = std::move(ecElimResult.newToOldRowMapping); + // Create the epoch model matrix + std::vector productToEpochModelStateMapping; + if (model.isOfType(storm::models::ModelType::Dtmc)) { + assert(zeroObjRewardChoices.size() == productModel->getProduct().getNumberOfStates()); + assert(stepChoices.size() == productModel->getProduct().getNumberOfStates()); + STORM_LOG_ASSERT(equationSolverProblemFormatForEpochModel.is_initialized(), "Linear equation problem format was not set."); + bool convertToEquationSystem = equationSolverProblemFormatForEpochModel.get() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; + // For DTMCs we consider the subsystem induced by the considered states. + // The transitions for states with zero reward are filtered out to guarantee a unique solution of the eq-system. + auto backwardTransitions = epochModel.epochMatrix.transpose(true); + storm::storage::BitVector nonZeroRewardStates = storm::utility::graph::performProbGreater0(backwardTransitions, consideredStates, consideredStates & (~zeroObjRewardChoices | stepChoices)); + // If there is at least one considered state with reward zero, we have to add a 'zero-reward-state' to the epoch model. + bool requiresZeroRewardState = nonZeroRewardStates != consideredStates; + uint64_t numEpochModelStates = nonZeroRewardStates.getNumberOfSetBits(); + uint64_t zeroRewardInState = numEpochModelStates; + if (requiresZeroRewardState) { + ++numEpochModelStates; + } + storm::storage::SparseMatrixBuilder builder; + if (!nonZeroRewardStates.empty()) { + builder = storm::storage::SparseMatrixBuilder(epochModel.epochMatrix.getSubmatrix(true, nonZeroRewardStates, nonZeroRewardStates, convertToEquationSystem)); + } + if (requiresZeroRewardState) { + if (convertToEquationSystem) { + // add a diagonal entry + builder.addNextValue(zeroRewardInState, zeroRewardInState, storm::utility::zero()); + } + epochModel.epochMatrix = builder.build(numEpochModelStates, numEpochModelStates); + } else { + assert (!nonZeroRewardStates.empty()); + epochModel.epochMatrix = builder.build(); + } + if (convertToEquationSystem) { + epochModel.epochMatrix.convertToEquationSystem(); + } + + epochModelToProductChoiceMap.clear(); + epochModelToProductChoiceMap.reserve(numEpochModelStates); + productToEpochModelStateMapping.assign(nonZeroRewardStates.size(), zeroRewardInState); + for (auto const& productState : nonZeroRewardStates) { + productToEpochModelStateMapping[productState] = epochModelToProductChoiceMap.size(); + epochModelToProductChoiceMap.push_back(productState); + } + if (requiresZeroRewardState) { + uint64_t zeroRewardProductState = (consideredStates & ~nonZeroRewardStates).getNextSetIndex(0); + assert(zeroRewardProductState < consideredStates.size()); + epochModelToProductChoiceMap.push_back(zeroRewardProductState); + } + } else if (model.isOfType(storm::models::ModelType::Mdp)) { + // Eliminate zero-reward end components + auto ecElimResult = storm::transformer::EndComponentEliminator::transform(epochModel.epochMatrix, consideredStates, zeroObjRewardChoices & ~stepChoices, consideredStates); + epochModel.epochMatrix = std::move(ecElimResult.matrix); + epochModelToProductChoiceMap = std::move(ecElimResult.newToOldRowMapping); + productToEpochModelStateMapping = std::move(ecElimResult.oldToNewStateMapping); + } else { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unsupported model type."); + } + epochModel.stepChoices = storm::storage::BitVector(epochModel.epochMatrix.getRowCount(), false); for (uint64_t choice = 0; choice < epochModel.epochMatrix.getRowCount(); ++choice) { if (stepChoices.get(epochModelToProductChoiceMap[choice])) { @@ -466,14 +520,14 @@ namespace storm { epochModel.epochInStates = storm::storage::BitVector(epochModel.epochMatrix.getRowGroupCount(), false); for (auto const& productState : productInStates) { - STORM_LOG_ASSERT(ecElimResult.oldToNewStateMapping[productState] < epochModel.epochMatrix.getRowGroupCount(), "Selected product state does not exist in the epoch model."); - epochModel.epochInStates.set(ecElimResult.oldToNewStateMapping[productState], true); + STORM_LOG_ASSERT(productToEpochModelStateMapping[productState] < epochModel.epochMatrix.getRowGroupCount(), "Selected product state does not exist in the epoch model."); + epochModel.epochInStates.set(productToEpochModelStateMapping[productState], true); } std::vector toEpochModelInStatesMap(productModel->getProduct().getNumberOfStates(), std::numeric_limits::max()); std::vector epochModelStateToInStateMap = epochModel.epochInStates.getNumberOfSetBitsBeforeIndices(); for (auto const& productState : productInStates) { - toEpochModelInStatesMap[productState] = epochModelStateToInStateMap[ecElimResult.oldToNewStateMapping[productState]]; + toEpochModelInStatesMap[productState] = epochModelStateToInStateMap[productToEpochModelStateMapping[productState]]; } productStateToEpochModelInStateMap = std::make_shared const>(std::move(toEpochModelInStatesMap)); @@ -487,6 +541,13 @@ namespace storm { } + template + void MultiDimensionalRewardUnfolding::setEquationSystemFormatForEpochModel(storm::solver::LinearEquationSolverProblemFormat eqSysFormat) { + STORM_LOG_ASSERT(model.isOfType(storm::models::ModelType::Dtmc), "Trying to set the equation problem format although the model is not deterministic."); + equationSolverProblemFormatForEpochModel = eqSysFormat; + } + + template template::type> typename MultiDimensionalRewardUnfolding::SolutionType MultiDimensionalRewardUnfolding::getScaledSolution(SolutionType const& solution, ValueType const& scalingFactor) const { diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h index 11a15a82a..e1b96c64c 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -8,7 +8,8 @@ #include "storm/modelchecker/prctl/helper/rewardbounded/EpochManager.h" #include "storm/modelchecker/prctl/helper/rewardbounded/ProductModel.h" #include "storm/modelchecker/prctl/helper/rewardbounded/Dimension.h" -#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/Model.h" +#include "storm/solver/LinearEquationSolverProblemFormat.h" #include "storm/utility/vector.h" #include "storm/storage/memorystructure/MemoryStructure.h" #include "storm/utility/Stopwatch.h" @@ -43,8 +44,8 @@ namespace storm { * @param objectives The (preprocessed) objectives * */ - MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::vector> const& objectives); - MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::shared_ptr objectiveFormula); + MultiDimensionalRewardUnfolding(storm::models::sparse::Model const& model, std::vector> const& objectives); + MultiDimensionalRewardUnfolding(storm::models::sparse::Model const& model, std::shared_ptr objectiveFormula); ~MultiDimensionalRewardUnfolding() = default; @@ -53,6 +54,8 @@ namespace storm { EpochModel& setCurrentEpoch(Epoch const& epoch); + void setEquationSystemFormatForEpochModel(storm::solver::LinearEquationSolverProblemFormat eqSysFormat); + /*! * Returns the precision required for the analyzis of each epoch model in order to achieve the given overall precision */ @@ -106,7 +109,7 @@ namespace storm { EpochSolution const& getEpochSolution(std::map const& solutions, Epoch const& epoch); SolutionType const& getStateSolution(EpochSolution const& epochSolution, uint64_t const& productState); - storm::models::sparse::Mdp const& model; + storm::models::sparse::Model const& model; std::vector> objectives; std::unique_ptr> productModel; @@ -118,6 +121,9 @@ namespace storm { EpochModel epochModel; boost::optional currentEpoch; + // In case of DTMCs we have different options for the equation problem format the epoch model will have. + boost::optional equationSolverProblemFormatForEpochModel; + EpochManager epochManager; std::vector> dimensions; diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp index fa327d34e..af41c8a4f 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp @@ -9,6 +9,8 @@ #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/Dtmc.h" #include "storm/exceptions/UnexpectedException.h" #include "storm/exceptions/NotSupportedException.h" @@ -19,7 +21,7 @@ namespace storm { namespace rewardbounded { template - ProductModel::ProductModel(storm::models::sparse::Mdp const& model, std::vector> const& objectives, std::vector> const& dimensions, std::vector const& objectiveDimensions, EpochManager const& epochManager, std::vector const& originalModelSteps) : dimensions(dimensions), objectiveDimensions(objectiveDimensions), epochManager(epochManager), memoryStateManager(dimensions.size()) { + ProductModel::ProductModel(storm::models::sparse::Model const& model, std::vector> const& objectives, std::vector> const& dimensions, std::vector const& objectiveDimensions, EpochManager const& epochManager, std::vector const& originalModelSteps) : dimensions(dimensions), objectiveDimensions(objectiveDimensions), epochManager(epochManager), memoryStateManager(dimensions.size()) { for (uint64_t dim = 0; dim < dimensions.size(); ++dim) { if (!dimensions[dim].memoryLabel) { @@ -34,7 +36,7 @@ namespace storm { storm::storage::SparseModelMemoryProduct productBuilder(memory.product(model)); setReachableProductStates(productBuilder, originalModelSteps, memoryStateMap); - product = productBuilder.build()->template as>(); + product = productBuilder.build(); uint64_t numModelStates = productBuilder.getOriginalModel().getNumberOfStates(); MemoryState upperMemStateBound = memoryStateManager.getUpperMemoryStateBound(); @@ -57,7 +59,7 @@ namespace storm { } // Map choice indices of the product to the state where it origins - choiceToStateMap.reserve(getProduct().getNumberOfChoices()); + choiceToStateMap.reserve(getProduct().getTransitionMatrix().getRowCount()); for (uint64_t productState = 0; productState < numProductStates; ++productState) { uint64_t groupSize = getProduct().getTransitionMatrix().getRowGroupSize(productState); for (uint64_t i = 0; i < groupSize; ++i) { @@ -66,7 +68,7 @@ namespace storm { } // Compute the epoch steps for the product - steps.resize(getProduct().getNumberOfChoices(), 0); + steps.resize(getProduct().getTransitionMatrix().getRowCount(), 0); for (uint64_t modelState = 0; modelState < numModelStates; ++modelState) { uint64_t numChoices = productBuilder.getOriginalModel().getTransitionMatrix().getRowGroupSize(modelState); uint64_t firstChoice = productBuilder.getOriginalModel().getTransitionMatrix().getRowGroupIndices()[modelState]; @@ -92,9 +94,9 @@ namespace storm { template - storm::storage::MemoryStructure ProductModel::computeMemoryStructure(storm::models::sparse::Mdp const& model, std::vector> const& objectives) const { + storm::storage::MemoryStructure ProductModel::computeMemoryStructure(storm::models::sparse::Model const& model, std::vector> const& objectives) const { - storm::modelchecker::SparsePropositionalModelChecker> mc(model); + storm::modelchecker::SparsePropositionalModelChecker> mc(model); // Create a memory structure that remembers whether (sub)objectives are satisfied storm::storage::MemoryStructure memory = storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(model); @@ -285,7 +287,7 @@ namespace storm { } template - storm::models::sparse::Mdp const& ProductModel::getProduct() const { + storm::models::sparse::Model const& ProductModel::getProduct() const { return *product; } @@ -341,7 +343,7 @@ namespace storm { for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { auto const& formula = *objectives[objIndex].formula; if (formula.isProbabilityOperatorFormula()) { - storm::modelchecker::SparsePropositionalModelChecker> mc(getProduct()); + storm::modelchecker::SparsePropositionalModelChecker> mc(getProduct()); std::vector dimensionIndexMap; for (auto const& globalDimensionIndex : objectiveDimensions[objIndex]) { dimensionIndexMap.push_back(globalDimensionIndex); diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.h b/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.h index 4aaf90796..3f5b2a9a7 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.h +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.h @@ -7,7 +7,7 @@ #include "storm/modelchecker/prctl/helper/rewardbounded/EpochManager.h" #include "storm/modelchecker/prctl/helper/rewardbounded/MemoryStateManager.h" #include "storm/modelchecker/prctl/helper/rewardbounded/Dimension.h" -#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/Model.h" #include "storm/utility/vector.h" #include "storm/storage/memorystructure/MemoryStructure.h" #include "storm/storage/memorystructure/SparseModelMemoryProduct.h" @@ -26,9 +26,9 @@ namespace storm { typedef typename MemoryStateManager::MemoryState MemoryState; - ProductModel(storm::models::sparse::Mdp const& model, std::vector> const& objectives, std::vector> const& dimensions, std::vector const& objectiveDimensions, EpochManager const& epochManager, std::vector const& originalModelSteps); + ProductModel(storm::models::sparse::Model const& model, std::vector> const& objectives, std::vector> const& dimensions, std::vector const& objectiveDimensions, EpochManager const& epochManager, std::vector const& originalModelSteps); - storm::models::sparse::Mdp const& getProduct() const; + storm::models::sparse::Model const& getProduct() const; std::vector const& getSteps() const; bool productStateExists(uint64_t const& modelState, uint64_t const& memoryState) const; @@ -50,7 +50,7 @@ namespace storm { private: - storm::storage::MemoryStructure computeMemoryStructure(storm::models::sparse::Mdp const& model, std::vector> const& objectives) const; + storm::storage::MemoryStructure computeMemoryStructure(storm::models::sparse::Model const& model, std::vector> const& objectives) const; std::vector computeMemoryStateMap(storm::storage::MemoryStructure const& memory) const; @@ -66,7 +66,7 @@ namespace storm { EpochManager const& epochManager; MemoryStateManager memoryStateManager; - std::shared_ptr> product; + std::shared_ptr> product; std::vector steps; std::map reachableStates; std::map inStates; From ea6c957030a843892d527caf7df8765fbcd4b7e8 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 20 Dec 2017 10:46:56 +0100 Subject: [PATCH 11/18] tests for multi-dimensional cost bounded DTMCs --- .../testfiles/dtmc/crowds_cost_bounded.pm | 260 ++++++++++++++++++ ...tmcMultiDimensionalRewardUnfoldingTest.cpp | 99 +++++++ 2 files changed, 359 insertions(+) create mode 100644 resources/examples/testfiles/dtmc/crowds_cost_bounded.pm create mode 100644 src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp diff --git a/resources/examples/testfiles/dtmc/crowds_cost_bounded.pm b/resources/examples/testfiles/dtmc/crowds_cost_bounded.pm new file mode 100644 index 000000000..d781dadc9 --- /dev/null +++ b/resources/examples/testfiles/dtmc/crowds_cost_bounded.pm @@ -0,0 +1,260 @@ +// CROWDS [Reiter,Rubin] +// Vitaly Shmatikov, 2002 + +// Note: +// Change everything marked CWDSIZ when changing the size of the crowd +// Change everything marked CWDMAX when increasing max size of the crowd + +dtmc + +// Probability of forwarding +const double PF = 0.8; + +// Probability that a crowd member is bad +const double badC = 0.091; +// const double badC = 0.167; + +const int CrowdSize; // CWDSIZ: actual number of good crowd members +const int MaxGood=20; // CWDMAX: maximum number of good crowd members + +// Process definitions +module crowds + + // Auxiliary variables + launch: bool init true; // Start modeling? + new: bool init false; // Initialize a new protocol instance? + start: bool init false; // Start the protocol? + run: bool init false; // Run the protocol? + lastSeen: [0..MaxGood] init MaxGood; // Last crowd member to touch msg + good: bool init false; // Crowd member is good? + bad: bool init false; // ... bad? + recordLast: bool init false; // Record last seen crowd member? + badObserve: bool init false; // Bad members observes who sent msg? + deliver: bool init false; // Deliver message to destination? + done: bool init false; // Protocol instance finished? + + [] launch -> (new'=true) & (launch'=false); + // Set up a new protocol instance + [newrun] new -> (new'=false) & (start'=true); + + // SENDER + // Start the protocol + [] start -> (lastSeen'=0) & (run'=true) & (deliver'=false) & (start'=false); + + // CROWD MEMBERS + // Good or bad crowd member? + [] !good & !bad & !deliver & run -> + 1-badC : (good'=true) & (recordLast'=true) & (run'=false) + + badC : (bad'=true) & (badObserve'=true) & (run'=false); + + // GOOD MEMBERS + // Forward with probability PF, else deliver + [] good & !deliver & run -> PF : (good'=false) + 1-PF : (deliver'=true); + // Record the last crowd member who touched the msg; + // all good members may appear with equal probability + // Note: This is backward. In the real protocol, each honest + // forwarder randomly chooses the next forwarder. + // Here, the identity of an honest forwarder is randomly + // chosen *after* it has forwarded the message. + [] recordLast & CrowdSize=2 -> + 1/2 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + + 1/2 : (lastSeen'=1) & (recordLast'=false) & (run'=true); + [] recordLast & CrowdSize=4 -> + 1/4 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + + 1/4 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + + 1/4 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + + 1/4 : (lastSeen'=3) & (recordLast'=false) & (run'=true); + [] recordLast & CrowdSize=5 -> + 1/5 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + + 1/5 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + + 1/5 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + + 1/5 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + + 1/5 : (lastSeen'=4) & (recordLast'=false) & (run'=true); + [] recordLast & CrowdSize=10 -> + 1/10 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=4) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=5) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=6) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=7) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=8) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=9) & (recordLast'=false) & (run'=true); + [] recordLast & CrowdSize=15 -> + 1/15 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=4) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=5) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=6) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=7) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=8) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=9) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=10) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=11) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=12) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=13) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=14) & (recordLast'=false) & (run'=true); + [] recordLast & CrowdSize=20 -> + 1/20 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=4) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=5) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=6) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=7) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=8) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=9) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=10) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=11) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=12) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=13) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=14) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=15) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=16) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=17) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=18) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=19) & (recordLast'=false) & (run'=true); + + // BAD MEMBERS + // Remember from whom the message was received and deliver + // CWDMAX: 1 rule per each good crowd member + [obs0] lastSeen=0 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs1] lastSeen=1 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs2] lastSeen=2 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs3] lastSeen=3 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs4] lastSeen=4 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs5] lastSeen=5 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs6] lastSeen=6 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs7] lastSeen=7 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs8] lastSeen=8 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs9] lastSeen=9 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs10] lastSeen=10 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs11] lastSeen=11 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs12] lastSeen=12 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs13] lastSeen=13 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs14] lastSeen=14 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs15] lastSeen=15 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs16] lastSeen=16 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs17] lastSeen=17 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs18] lastSeen=18 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs19] lastSeen=19 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + + // RECIPIENT + // Delivery to destination + [] deliver & run -> (done'=true) & (deliver'=false) & (run'=false) & (good'=false) & (bad'=false); + // Start a new instance + [] done -> (new'=true) & (done'=false) & (run'=false) & (lastSeen'=MaxGood); + +endmodule + +rewards "num_runs" + [newrun] true : 1; +endrewards + +rewards "observe0" + [obs0] true : 1; +endrewards + +rewards "observe1" + [obs1] true : 1; +endrewards + +rewards "observe2" + [obs2] true : 1; +endrewards + +rewards "observe3" + [obs3] true : 1; +endrewards + +rewards "observe4" + [obs4] true : 1; +endrewards + +rewards "observe5" + [obs5] true : 1; +endrewards + +rewards "observe6" + [obs6] true : 1; +endrewards + +rewards "observe7" + [obs7] true : 1; +endrewards + +rewards "observe8" + [obs8] true : 1; +endrewards + +rewards "observe9" + [obs9] true : 1; +endrewards + +rewards "observe10" + [obs10] true : 1; +endrewards + +rewards "observe11" + [obs11] true : 1; +endrewards + +rewards "observe12" + [obs12] true : 1; +endrewards + +rewards "observe13" + [obs13] true : 1; +endrewards + +rewards "observe14" + [obs14] true : 1; +endrewards + +rewards "observe15" + [obs15] true : 1; +endrewards + +rewards "observe16" + [obs16] true : 1; +endrewards + +rewards "observe17" + [obs17] true : 1; +endrewards + +rewards "observe18" + [obs18] true : 1; +endrewards + +rewards "observe19" + [obs19] true : 1; +endrewards + +rewards "observeI" + [obs1] true : 1; + [obs2] true : 1; + [obs3] true : 1; + [obs4] true : 1; + [obs5] true : 1; + [obs6] true : 1; + [obs7] true : 1; + [obs8] true : 1; + [obs9] true : 1; + [obs10] true : 1; + [obs11] true : 1; + [obs12] true : 1; + [obs13] true : 1; + [obs14] true : 1; + [obs15] true : 1; + [obs16] true : 1; + [obs17] true : 1; + [obs18] true : 1; + [obs19] true : 1; +endrewards + + diff --git a/src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp new file mode 100644 index 000000000..36ca41ff0 --- /dev/null +++ b/src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp @@ -0,0 +1,99 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/models/sparse/Dtmc.h" +#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/SettingsManager.h" +#include "storm/utility/constants.h" +#include "storm/api/storm.h" +#include "storm/environment/Environment.h" + +TEST(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_die) { + storm::Environment env; + std::string programFile = STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"; + std::string formulasAsString = "P=? [ F{\"coin_flips\"}<=2 \"two\" ] "; + formulasAsString += "; P=? [ F{\"coin_flips\"}<=3 \"two\" ] "; + formulasAsString += "; P=? [ F{\"coin_flips\"}<=8 \"two\" ] "; + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> dtmc = storm::api::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *dtmc->getInitialStates().begin();; + std::unique_ptr result; + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[0], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("0")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[1], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("1/8")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[2], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("21/128")), result->asExplicitQuantitativeCheckResult()[initState]); +} + +TEST(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_leader) { + storm::Environment env; + std::string programFile = STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"; + std::string formulasAsString = "P=? [ F{\"num_rounds\"}<=1 \"elected\" ] "; + formulasAsString += "; P=? [ F{\"num_rounds\"}<=2 \"elected\" ] "; + formulasAsString += "; P=? [ F{\"num_rounds\"}>2 \"elected\" ] "; + formulasAsString += "; P=? [ F{\"num_rounds\"}>=2,{\"num_rounds\"}<3 \"elected\" ] "; + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> dtmc = storm::api::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *dtmc->getInitialStates().begin();; + std::unique_ptr result; + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[0], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("24/25")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[1], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("624/625")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[2], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("1/625")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[3], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("24/625")), result->asExplicitQuantitativeCheckResult()[initState]); +} + +TEST(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_crowds) { + storm::Environment env; + std::string programFile = STORM_TEST_RESOURCES_DIR "/dtmc/crowds_cost_bounded.pm"; + std::string formulasAsString = "P=? [F{\"num_runs\"}<=3,{\"observe0\"}>1 true]"; + formulasAsString += "; P=? [F{\"num_runs\"}<=3,{\"observe1\"}>1 true]"; + formulasAsString += "; R{\"observe0\"}=? [C{\"num_runs\"}<=3]"; + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, "CrowdSize=4"); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> dtmc = storm::api::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *dtmc->getInitialStates().begin();; + std::unique_ptr result; + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[0], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("78686542099694893/1268858272000000000")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[1], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("13433618626105041/1268858272000000000")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[2], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("620529/1364000")), result->asExplicitQuantitativeCheckResult()[initState]); +} From 0ce91b7eb42099d0d4c213e0db0752b637d778ec Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 20 Dec 2017 11:23:45 +0100 Subject: [PATCH 12/18] updated changelog --- CHANGELOG.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 8218b4c83..5832b1e35 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,9 @@ The releases of major and minor versions contain an overview of changes since th Version 1.2.x ------------- +### Version 1.2.1 (to be released) +- Multi-dimensional reward bounded reachability properties for DTMCs. + ### Version 1.2.0 (2017/12) - C++ api changes: Building model takes `BuilderOptions` instead of extended list of Booleans, does not depend on settings anymore. - `storm-cli-utilities` now contains cli related stuff, instead of `storm-lib` From d1641f09eba6bb99b7bae00d0fe3583bd7c58b4d Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 20 Dec 2017 11:24:38 +0100 Subject: [PATCH 13/18] added a script to check multiple cmake configurations and updated the release checklist --- doc/checklist_new_release.md | 1 + doc/scripts/test_build_configurations.py | 118 ++++++++++++++++++++++ doc/scripts/test_build_configurations.txt | 5 + 3 files changed, 124 insertions(+) create mode 100644 doc/scripts/test_build_configurations.py create mode 100644 doc/scripts/test_build_configurations.txt diff --git a/doc/checklist_new_release.md b/doc/checklist_new_release.md index 5fda82ab5..05be534aa 100644 --- a/doc/checklist_new_release.md +++ b/doc/checklist_new_release.md @@ -13,6 +13,7 @@ Note that in most case a simultaneous release of [carl](https://github.com/smtra 3. Check that storm builds without errors and all tests are successful * [Travis](https://travis-ci.org/moves-rwth/storm) should run successfully + * Invoke the script test_build_configurations.py to build and check different cmake configurations 4. Set new storm version: * Set new storm version in `version.cmake` diff --git a/doc/scripts/test_build_configurations.py b/doc/scripts/test_build_configurations.py new file mode 100644 index 000000000..56baccf0d --- /dev/null +++ b/doc/scripts/test_build_configurations.py @@ -0,0 +1,118 @@ +import subprocess +import os +import shutil +import time +import math +import sys + +logfileDir = "test_build_configurations_logs" +pathToConfigFile = "" +globalCmakeArguments = "" +globalMakeArguments = "" + +if len(sys.argv) == 1 or len(sys.argv) > 5: + print "Usage: " + sys.argv[0] + "/path/to/storm /path/to/configurations.txt \"optional make arguments\" \"optional cmake arguments\"" + print "Example: " + sys.argv[0] + " ~/storm test_build_configurations.txt \"-j 48 -k\" \"-DZ3_ROOT=/path/to/z3/\"" + sys.exit(0) + +pathToStorm = sys.argv[1] +pathToConfigFile = sys.argv[2] + +if len(sys.argv) > 3: + globalMakeArguments = sys.argv[3] + print globalMakeArguments +if len(sys.argv) > 4: + globalCmakeArguments = sys.argv[4] + print globalCmakeArguments + +# create directory for log files +if not os.path.exists(logfileDir): + os.makedirs(logfileDir) + +unsuccessfulConfigs = "" +globalStartTime = time.time() + +with open(pathToConfigFile) as configfile: + localStartTime = time.time() + configId=0 + for localCmakeArguments in configfile: + + cmakeArguments = globalCmakeArguments + " " + localCmakeArguments.strip('\n') + buildDir = os.path.join(pathToStorm, "build{}".format(configId)) + logfilename = os.path.join(logfileDir, "build{}".format(configId) + "_" + time.strftime("%Y-%m-%d-%H-%M-%S") + ".log") + + + print "Building configuration {} with cmake options ".format(configId) + cmakeArguments + print "\tCreating log file " + logfilename + " ..." + with open(logfilename, "w") as logfile: + success=True + logfile.write("Log for test configuration " + cmakeArguments + "\n") + + print "\tCreating build directory" + buildDir + " ..." + if os.path.exists(buildDir): + print "\t\tRemoving existing directory " + buildDir + shutil.rmtree(buildDir, ignore_errors=True) + os.makedirs(buildDir) + logfile.write("Build directory is " + buildDir + "\n") + print "\t\tdone" + + if success: + print "\tInvoking cmake ..." + cmakeCommand = "cmake .. {}".format(cmakeArguments) + logfile.write ("\n\n CALLING CMAKE \n\n" + cmakeCommand + "\n") + try: + cmakeOutput = subprocess.check_output("cd " + buildDir + "; " + cmakeCommand , shell=True,stderr=subprocess.STDOUT) + print "\t\tdone" + logfile.write(cmakeOutput) + except subprocess.CalledProcessError as e: + success=False + print "\t\tfail" + print e.output + logfile.write(e.output) + + if success: + print "\tInvoking make ..." + makeCommand = "make {}".format(globalMakeArguments) + logfile.write ("\n\n CALLING MAKE \n\n" + makeCommand + "\n") + try: + makeOutput = subprocess.check_output("cd " + buildDir + "; " + makeCommand , shell=True,stderr=subprocess.STDOUT) + print "\t\tdone" + logfile.write(makeOutput) + except subprocess.CalledProcessError as e: + success=False + print "\t\tfail" + print e.output + logfile.write(e.output) + + if success: + print "\tInvoking make check..." + makeCheckCommand = "make check" + logfile.write ("\n\n CALLING MAKE CHECK \n\n" + makeCheckCommand + "\n") + try: + makeCheckOutput = subprocess.check_output("cd " + buildDir + "; " + makeCheckCommand , shell=True,stderr=subprocess.STDOUT) + print "\t\tdone" + logfile.write(makeCheckOutput) + except subprocess.CalledProcessError as e: + success=False + print "\t\tfail" + print e.output + logfile.write(e.output) + + localEndTime = time.time() + if success: + print "\tConfiguration build and tested successfully within {} minutes.".format(int((localEndTime - localStartTime)/60)) + else: + print "\tAn error occurred for this configuration." + unsuccessfulConfigs += buildDir + " with arguments " + cmakeArguments + "\n" + + configId += 1 +globalEndTime = time.time() +print "All tests completed after {} minutes.".format(int((globalEndTime - globalStartTime)/60)) +if unsuccessfulConfigs == "": + print "All configurations were build and tested successfully." +else: + print "The following configurations failed: \n" + unsuccessfulConfigs + + + + diff --git a/doc/scripts/test_build_configurations.txt b/doc/scripts/test_build_configurations.txt new file mode 100644 index 000000000..3688e8eab --- /dev/null +++ b/doc/scripts/test_build_configurations.txt @@ -0,0 +1,5 @@ +-DSTORM_USE_CLN_EA=OFF -DSTORM_USE_CLN_RF=OFF +-DSTORM_USE_CLN_EA=OFF -DSTORM_USE_CLN_RF=ON +-DSTORM_USE_CLN_EA=ON -DSTORM_USE_CLN_RF=OFF +-DSTORM_USE_CLN_EA=ON -DSTORM_USE_CLN_RF=ON +-DCMAKE_BUILD_TYPE=DEBUG -DSTORM_DEVELOPER=ON \ No newline at end of file From 8646d614d4197d4e94b46a93fb82a725b02b2a01 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 20 Dec 2017 20:45:47 +0100 Subject: [PATCH 14/18] reduced the number of initial buckets for the hash map used in explicit model building --- src/storm/storage/sparse/StateStorage.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/storage/sparse/StateStorage.cpp b/src/storm/storage/sparse/StateStorage.cpp index a007ab2ea..a3ea05f4f 100644 --- a/src/storm/storage/sparse/StateStorage.cpp +++ b/src/storm/storage/sparse/StateStorage.cpp @@ -5,7 +5,7 @@ namespace storm { namespace sparse { template - StateStorage::StateStorage(uint64_t bitsPerState) : stateToId(bitsPerState, 10000000), initialStateIndices(), deadlockStateIndices(), bitsPerState(bitsPerState) { + StateStorage::StateStorage(uint64_t bitsPerState) : stateToId(bitsPerState, 100000), initialStateIndices(), deadlockStateIndices(), bitsPerState(bitsPerState) { // Intentionally left empty. } From 91d0cdf41db65be6afcb18044f156d72be864663 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 21 Dec 2017 00:36:57 +0100 Subject: [PATCH 15/18] fix non-terminating while loop in high level counterexamples --- src/storm/counterexamples/SMTMinimalLabelSetGenerator.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h index e8f2464a9..63f8b6ff8 100644 --- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h @@ -1709,6 +1709,9 @@ namespace storm { // Set up some variables for the iterations. boost::container::flat_set commandSet(relevancyInformation.relevantLabels); + if (relevancyInformation.relevantLabels.empty()) { + return commandSet; + } bool done = false; uint_fast64_t iterations = 0; uint_fast64_t currentBound = 0; From 8ce3eaddc37417ec7070bdba7e41eb64eb12ba64 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 21 Dec 2017 00:37:31 +0100 Subject: [PATCH 16/18] PrismProgram -- Used Constants --- src/storm/storage/prism/Program.cpp | 74 ++++++++++++++++++++++++++++- src/storm/storage/prism/Program.h | 6 +++ 2 files changed, 79 insertions(+), 1 deletion(-) diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index edd17c3d0..aea47fd09 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -1552,7 +1552,79 @@ namespace storm { storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, newCommands, this->getFilename(), 0); return Program(manager, this->getModelType(), this->getConstants(), std::vector(), std::vector(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true); } - + + std::vector Program::usedConstants() const { + std::unordered_set vars; + for(auto const& m : this->modules) { + for(auto const& c : m.getCommands()) { + auto const& found_gex = c.getGuardExpression().getVariables(); + vars.insert(found_gex.begin(), found_gex.end()); + for (auto const& u : c.getUpdates()) { + auto const& found_lex = u.getLikelihoodExpression().getVariables(); + vars.insert(found_lex.begin(), found_lex.end()); + for (auto const& a : u.getAssignments()) { + auto const& found_ass = a.getExpression().getVariables(); + vars.insert(found_ass.begin(), found_ass.end()); + } + } + } + for (auto const& v : m.getBooleanVariables()) { + if (v.hasInitialValue()) { + auto const& found_def = v.getInitialValueExpression().getVariables(); + vars.insert(found_def.begin(), found_def.end()); + } + } + for (auto const& v : m.getIntegerVariables()) { + if (v.hasInitialValue()) { + auto const& found_def = v.getInitialValueExpression().getVariables(); + vars.insert(found_def.begin(), found_def.end()); + } + } + } + + for (auto const& f : this->formulas) { + auto const& found_def = f.getExpression().getVariables(); + vars.insert(found_def.begin(), found_def.end()); + } + + for (auto const& v : this->constants) { + if (v.isDefined()) { + auto const& found_def = v.getExpression().getVariables(); + vars.insert(found_def.begin(), found_def.end()); + } + } + + for (auto const& v : this->globalBooleanVariables) { + if (v.hasInitialValue()) { + auto const& found_def = v.getExpression().getVariables(); + vars.insert(found_def.begin(), found_def.end()); + } + } + + for (auto const& v : this->globalIntegerVariables) { + if (v.hasInitialValue()) { + auto const& found_def = v.getExpression().getVariables(); + vars.insert(found_def.begin(), found_def.end()); + } + } + + + std::unordered_set varIndices; + for (auto const& v : vars) { + varIndices.insert(v.getIndex()); + } + + std::vector usedConstants; + for(auto const& c : this->constants) { + if (varIndices.count(c.getExpressionVariable().getIndex())) { + usedConstants.push_back(c); + } + } + + return usedConstants; + + } + std::unordered_map Program::buildCommandIndexToActionNameMap() const { std::unordered_map res; for(auto const& m : this->modules) { diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index 46d704803..7dedc6667 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -151,6 +151,12 @@ namespace storm { * @return The number of constants defined in the program. */ std::size_t getNumberOfConstants() const; + + /*! + * Retrieves the constants that are actually used in the program. + * @return + */ + std::vector usedConstants() const; /*! * Retrieves whether a global Boolean variable with the given name exists From 284a792c1aeea09ab1687e667984259d7d382ba5 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 21 Dec 2017 00:37:51 +0100 Subject: [PATCH 17/18] highlevel counterexamples for smt: get conflict set directly --- .../SMTMinimalLabelSetGenerator.h | 37 +++++++++++-------- 1 file changed, 21 insertions(+), 16 deletions(-) diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h index 63f8b6ff8..0237985f0 100644 --- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h @@ -1859,11 +1859,10 @@ namespace storm { auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Extended command for lower bounded property to size " << commandSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; } - - static std::shared_ptr computeCounterexample(Environment const& env, storm::prism::Program program, storm::models::sparse::Mdp const& mdp, std::shared_ptr const& formula) { -#ifdef STORM_HAVE_Z3 + + static boost::container::flat_set computeCounterexampleCommandSet(Environment const& env, storm::prism::Program program, storm::models::sparse::Mdp const& mdp, std::shared_ptr const& formula) { std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl; - + STORM_LOG_THROW(formula->isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException, "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element."); storm::logic::ProbabilityOperatorFormula const& probabilityOperator = formula->asProbabilityOperatorFormula(); STORM_LOG_THROW(probabilityOperator.hasBound(), storm::exceptions::InvalidPropertyException, "Counterexample generation only supports bounded formulas."); @@ -1872,34 +1871,34 @@ namespace storm { storm::logic::ComparisonType comparisonType = probabilityOperator.getComparisonType(); bool strictBound = comparisonType == storm::logic::ComparisonType::Less; double threshold = probabilityOperator.getThresholdAs(); - + storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(mdp); - + if (probabilityOperator.getSubformula().isUntilFormula()) { STORM_LOG_THROW(!storm::logic::isLowerBound(comparisonType), storm::exceptions::NotSupportedException, "Lower bounds in counterexamples are only supported for eventually formulas."); storm::logic::UntilFormula const& untilFormula = probabilityOperator.getSubformula().asUntilFormula(); - + std::unique_ptr leftResult = modelchecker.check(env, untilFormula.getLeftSubformula()); std::unique_ptr rightResult = modelchecker.check(env, untilFormula.getRightSubformula()); - + storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult->asExplicitQualitativeCheckResult(); storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult->asExplicitQualitativeCheckResult(); - + phiStates = leftQualitativeResult.getTruthValuesVector(); psiStates = rightQualitativeResult.getTruthValuesVector(); } else if (probabilityOperator.getSubformula().isEventuallyFormula()) { storm::logic::EventuallyFormula const& eventuallyFormula = probabilityOperator.getSubformula().asEventuallyFormula(); - + std::unique_ptr subResult = modelchecker.check(env, eventuallyFormula.getSubformula()); - + storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult(); - + phiStates = storm::storage::BitVector(mdp.getNumberOfStates(), true); psiStates = subQualitativeResult.getTruthValuesVector(); } - + bool lowerBoundedFormula = false; if (storm::logic::isLowerBound(comparisonType)) { // If the formula specifies a lower bound, we need to modify the phi and psi states. @@ -1915,7 +1914,7 @@ namespace storm { // Modify bound appropriately. comparisonType = storm::logic::invertPreserveStrictness(comparisonType); threshold = storm::utility::one() - threshold; - + // Modify the phi and psi states appropriately. storm::storage::BitVector statesWithProbability0E = storm::utility::graph::performProb0E(mdp.getTransitionMatrix(), mdp.getTransitionMatrix().getRowGroupIndices(), mdp.getBackwardTransitions(), phiStates, psiStates); phiStates = ~psiStates; @@ -1925,17 +1924,23 @@ namespace storm { // have a strategy that voids a states. lowerBoundedFormula = true; } - + // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); auto commandSet = getMinimalCommandSet(env, program, mdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isEncodeReachabilitySet()); auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Computed minimal command set of size " << commandSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; - + // Extend the command set properly. if (lowerBoundedFormula) { extendCommandSetLowerBound(mdp, commandSet, phiStates, psiStates); } + return commandSet; + } + + static std::shared_ptr computeCounterexample(Environment const& env, storm::prism::Program program, storm::models::sparse::Mdp const& mdp, std::shared_ptr const& formula) { +#ifdef STORM_HAVE_Z3 + auto commandSet = computeCounterexampleCommandSet(env, program, mdp, formula); return std::make_shared(program.restrictCommands(commandSet)); From f90eb4708d3a360aa22830d3d0b0b5cc494e4653 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 21 Dec 2017 13:08:18 +0100 Subject: [PATCH 18/18] fix for boost 1.66 --- src/storm-pars-cli/storm-pars.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 8a8c9fa6a..8546f81d1 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -165,7 +165,8 @@ namespace storm { auto parametricSettings = storm::settings::getModule(); if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) { auto dtmc = model->template as>(); - storm::api::exportParametricResultToFile(boost::make_optional(result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]),storm::analysis::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); + boost::optional rationalFunction = result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; + storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); } }); }