From 8aaa205c5711225d261cd86e23a4e7283796b5d9 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 11 Aug 2017 10:42:01 +0200 Subject: [PATCH 01/12] Added travis build status to README --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 92214ca57..921983387 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,6 @@ Storm ============================== +[![Build Status](https://travis-ci.org/moves-rwth/storm.svg?branch=master)](https://travis-ci.org/moves-rwth/storm) For more instructions, check out the documentation found in [Getting Started](http://www.stormchecker.org/getting-started.html). From 05e97917aa898a6732eca6200b6baa05c5a9a037 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 11 Aug 2017 10:54:56 +0200 Subject: [PATCH 02/12] Enable travis support for stable branch --- .travis.yml | 1 + travis/generate_travis.py | 1 + 2 files changed, 2 insertions(+) diff --git a/.travis.yml b/.travis.yml index 731783ddf..779e5bb69 100644 --- a/.travis.yml +++ b/.travis.yml @@ -6,6 +6,7 @@ branches: only: - master + - stable dist: trusty language: cpp diff --git a/travis/generate_travis.py b/travis/generate_travis.py index 0f52bb550..5ace5a47c 100644 --- a/travis/generate_travis.py +++ b/travis/generate_travis.py @@ -39,6 +39,7 @@ if __name__ == "__main__": s += "branches:\n" s += " only:\n" s += " - master\n" + s += " - stable\n" s += "dist: trusty\n" s += "language: cpp\n" s += "\n" From c8734591c3595ffd0633a7561df770ca448eed6a Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 11 Aug 2017 10:55:31 +0200 Subject: [PATCH 03/12] Enable travis notifications --- .travis.yml | 7 +++++++ travis/generate_travis.py | 8 ++++++++ 2 files changed, 15 insertions(+) diff --git a/.travis.yml b/.travis.yml index 779e5bb69..3d0168555 100644 --- a/.travis.yml +++ b/.travis.yml @@ -22,6 +22,13 @@ services: - docker sudo: required +notifications: + email: + on_failure: always + on_success: change + recipients: + secure: "Q9CW/PtyWkZwExDrfFFb9n1STGYsRfI6awv1bZHcGwfrDvhpXoMCuF8CwviIfilm7fFJJEoKizTtdRpY0HrOnY/8KY111xrtcFYosxdndv7xbESodIxQOUoIEFCO0mCNHwWYisoi3dAA7H3Yn661EsxluwHjzX5vY0xSbw0n229hlsFz092HwGLSU33zHl7eXpQk+BOFmBTRGlOq9obtDZ17zbHz1oXFZntHK/JDUIYP0b0uq8NvE2jM6CIVdcuSwmIkOhZJoO2L3Py3rBbPci+L2PSK4Smv2UjCPF8KusnOaFIyDB3LcNM9Jqq5ssJMrK/KaO6BiuYrOZXYWZ7KEg3Y/naC8HjOH1dzty+P7oW46sb9F03pTsufqD4R7wcK+9wROTztO6aJPDG/IPH7EWgrBTxqlOkVRwi2eYuQouZpZUW6EMClKbMHMIxCH2S8aOk/r1w2cNwmPEcunnP0nl413x/ByHr4fTPFykPj8pQxIsllYjpdWBRQfDOauKWGzk6LcrFW0qpWP+/aJ2vYu/IoZQMG5lMHbp6Y1Lg09pYm7Q983v3b7D+JvXhOXMyGq91HyPahA2wwKoG1GA4uoZ2I95/IFYNiKkelDd3WTBoFLNF9YFoEJNdCywm1fO2WY4WkyEFBuQcgDA+YpFMJJMxjTbivYk9jvHk2gji//2w=" + # # Configurations # diff --git a/travis/generate_travis.py b/travis/generate_travis.py index 5ace5a47c..bafb15c1d 100644 --- a/travis/generate_travis.py +++ b/travis/generate_travis.py @@ -55,6 +55,14 @@ if __name__ == "__main__": s += "- docker\n" s += "sudo: required\n" s += "\n" + + s += "notifications:\n" + s += " email:\n" + s += " on_failure: always\n" + s += " on_success: change\n" + s += " recipients:\n" + s += ' secure: "Q9CW/PtyWkZwExDrfFFb9n1STGYsRfI6awv1bZHcGwfrDvhpXoMCuF8CwviIfilm7fFJJEoKizTtdRpY0HrOnY/8KY111xrtcFYosxdndv7xbESodIxQOUoIEFCO0mCNHwWYisoi3dAA7H3Yn661EsxluwHjzX5vY0xSbw0n229hlsFz092HwGLSU33zHl7eXpQk+BOFmBTRGlOq9obtDZ17zbHz1oXFZntHK/JDUIYP0b0uq8NvE2jM6CIVdcuSwmIkOhZJoO2L3Py3rBbPci+L2PSK4Smv2UjCPF8KusnOaFIyDB3LcNM9Jqq5ssJMrK/KaO6BiuYrOZXYWZ7KEg3Y/naC8HjOH1dzty+P7oW46sb9F03pTsufqD4R7wcK+9wROTztO6aJPDG/IPH7EWgrBTxqlOkVRwi2eYuQouZpZUW6EMClKbMHMIxCH2S8aOk/r1w2cNwmPEcunnP0nl413x/ByHr4fTPFykPj8pQxIsllYjpdWBRQfDOauKWGzk6LcrFW0qpWP+/aJ2vYu/IoZQMG5lMHbp6Y1Lg09pYm7Q983v3b7D+JvXhOXMyGq91HyPahA2wwKoG1GA4uoZ2I95/IFYNiKkelDd3WTBoFLNF9YFoEJNdCywm1fO2WY4WkyEFBuQcgDA+YpFMJJMxjTbivYk9jvHk2gji//2w="\n' + s += "\n" s += "#\n" s += "# Configurations\n" s += "#\n" From 49447da43d97eb91d9b112dec20ec42f13abb747 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 11 Aug 2017 10:56:43 +0200 Subject: [PATCH 04/12] Disable Debian in travis as there was no difference to Ubuntu --- .travis.yml | 127 -------------------------------------- travis/generate_travis.py | 2 +- 2 files changed, 1 insertion(+), 128 deletions(-) diff --git a/.travis.yml b/.travis.yml index 3d0168555..c824cddf6 100644 --- a/.travis.yml +++ b/.travis.yml @@ -89,33 +89,6 @@ jobs: - docker cp storm:/storm/. . after_failure: - find build -iname '*err*.log' -type f -print -exec cat {} \; - # debian-9 - - stage: Build (1st run) - os: linux - compiler: gcc - env: CONFIG=DefaultDebug LINUX=debian-9 COMPILER=gcc-6 - install: - - rm -rf build - - travis/install_linux.sh - script: - - travis/build.sh Build1 - before_cache: - - docker cp storm:/storm/. . - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; - - stage: Build (1st run) - os: linux - compiler: gcc - env: CONFIG=DefaultRelease LINUX=debian-9 COMPILER=gcc-6 - install: - - rm -rf build - - travis/install_linux.sh - script: - - travis/build.sh Build1 - before_cache: - - docker cp storm:/storm/. . - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; ### # Stage: Build (2nd run) @@ -167,31 +140,6 @@ jobs: - docker cp storm:/storm/. . after_failure: - find build -iname '*err*.log' -type f -print -exec cat {} \; - # debian-9 - - stage: Build (2nd run) - os: linux - compiler: gcc - env: CONFIG=DefaultDebug LINUX=debian-9 COMPILER=gcc-6 - install: - - travis/install_linux.sh - script: - - travis/build.sh Build2 - before_cache: - - docker cp storm:/storm/. . - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; - - stage: Build (2nd run) - os: linux - compiler: gcc - env: CONFIG=DefaultRelease LINUX=debian-9 COMPILER=gcc-6 - install: - - travis/install_linux.sh - script: - - travis/build.sh Build2 - before_cache: - - docker cp storm:/storm/. . - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; ### # Stage: Build (3rd run) @@ -243,31 +191,6 @@ jobs: - docker cp storm:/storm/. . after_failure: - find build -iname '*err*.log' -type f -print -exec cat {} \; - # debian-9 - - stage: Build (3rd run) - os: linux - compiler: gcc - env: CONFIG=DefaultDebug LINUX=debian-9 COMPILER=gcc-6 - install: - - travis/install_linux.sh - script: - - travis/build.sh Build3 - before_cache: - - docker cp storm:/storm/. . - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; - - stage: Build (3rd run) - os: linux - compiler: gcc - env: CONFIG=DefaultRelease LINUX=debian-9 COMPILER=gcc-6 - install: - - travis/install_linux.sh - script: - - travis/build.sh Build3 - before_cache: - - docker cp storm:/storm/. . - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; ### # Stage: Build (4th run) @@ -319,31 +242,6 @@ jobs: - docker cp storm:/storm/. . after_failure: - find build -iname '*err*.log' -type f -print -exec cat {} \; - # debian-9 - - stage: Build (4th run) - os: linux - compiler: gcc - env: CONFIG=DefaultDebug LINUX=debian-9 COMPILER=gcc-6 - install: - - travis/install_linux.sh - script: - - travis/build.sh Build4 - before_cache: - - docker cp storm:/storm/. . - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; - - stage: Build (4th run) - os: linux - compiler: gcc - env: CONFIG=DefaultRelease LINUX=debian-9 COMPILER=gcc-6 - install: - - travis/install_linux.sh - script: - - travis/build.sh Build4 - before_cache: - - docker cp storm:/storm/. . - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; ### # Stage: Test all @@ -395,29 +293,4 @@ jobs: - docker cp storm:/storm/. . after_failure: - find build -iname '*err*.log' -type f -print -exec cat {} \; - # debian-9 - - stage: Test all - os: linux - compiler: gcc - env: CONFIG=DefaultDebug LINUX=debian-9 COMPILER=gcc-6 - install: - - travis/install_linux.sh - script: - - travis/build.sh TestAll - before_cache: - - docker cp storm:/storm/. . - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; - - stage: Test all - os: linux - compiler: gcc - env: CONFIG=DefaultRelease LINUX=debian-9 COMPILER=gcc-6 - install: - - travis/install_linux.sh - script: - - travis/build.sh TestAll - before_cache: - - docker cp storm:/storm/. . - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; diff --git a/travis/generate_travis.py b/travis/generate_travis.py index bafb15c1d..c47afac0c 100644 --- a/travis/generate_travis.py +++ b/travis/generate_travis.py @@ -3,7 +3,7 @@ configs_linux = [ # OS, compiler ("ubuntu-16.10", "gcc", "-6"), - ("debian-9", "gcc", "-6"), + #("debian-9", "gcc", "-6"), ] # Configurations for Mac From c903f738b3b06a271e9d8d663b7b0bab505306a1 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 11 Aug 2017 11:34:46 +0200 Subject: [PATCH 05/12] Fixed some typos --- .../transformer/SparseParametricModelSimplifier.cpp | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp b/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp index 1679bdcca..9385a24a9 100644 --- a/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp +++ b/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp @@ -45,7 +45,7 @@ namespace storm { } } // reaching this point means that the provided formula is not supported. Thus, no simplification is possible. - STORM_LOG_DEBUG("Simplification not possible because the formula is not suppoerted. Formula: " << formula); + STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); return false; } @@ -63,8 +63,8 @@ namespace storm { template bool SparseParametricModelSimplifier::simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { - // If this method was not overriden by any subclass, simplification is not possible - STORM_LOG_DEBUG("Simplification not possible because the formula is not suppoerted. Formula: " << formula); + // If this method was not overridden by any subclass, simplification is not possible + STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); return false; } @@ -77,21 +77,21 @@ namespace storm { template bool SparseParametricModelSimplifier::simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { - // If this method was not overriden by any subclass, simplification is not possible + // If this method was not overridden by any subclass, simplification is not possible STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); return false; } template bool SparseParametricModelSimplifier::simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula) { - // If this method was not overriden by any subclass, simplification is not possible + // If this method was not overridden by any subclass, simplification is not possible STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); return false; } template bool SparseParametricModelSimplifier::simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) { - // If this method was not overriden by any subclass, simplification is not possible + // If this method was not overridden by any subclass, simplification is not possible STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); return false; } @@ -100,7 +100,6 @@ namespace storm { std::shared_ptr SparseParametricModelSimplifier::eliminateConstantDeterministicStates(SparseModelType const& model, storm::storage::BitVector const& consideredStates, boost::optional const& rewardModelName) { storm::storage::SparseMatrix const& sparseMatrix = model.getTransitionMatrix(); - // get the action-based reward values std::vector actionRewards; if(rewardModelName) { From 2dba64705ec6502d01b226dd0d61c403570cb25c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 11 Aug 2017 14:36:28 +0200 Subject: [PATCH 06/12] Removed redundant info in CHANGELOG --- CHANGELOG.md | 1 - 1 file changed, 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 90c72cd28..7c55d776d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,7 +6,6 @@ The releases of major and minor versions contain an overview of changes since th Version 1.1.x ------------- -Long run average computation via LRA, LP based MDP model checking, parametric model checking has an own binary ### Version 1.1.0 (2017/8) From 1c2c4eb6123c7e42127d2fe08bdb78b8a83ab5ac Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 11 Aug 2017 14:54:07 +0200 Subject: [PATCH 07/12] Added subtitle to README --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 921983387..a415b376e 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,5 @@ -Storm -============================== +Storm - A Modern Probabilistic Model Checker +============================================ [![Build Status](https://travis-ci.org/moves-rwth/storm.svg?branch=master)](https://travis-ci.org/moves-rwth/storm) For more instructions, check out the documentation found in [Getting Started](http://www.stormchecker.org/getting-started.html). From bf6258bd868d3f3e75a813b0c7c6c8dd2a33c059 Mon Sep 17 00:00:00 2001 From: sjunges Date: Sun, 13 Aug 2017 14:53:11 +0200 Subject: [PATCH 08/12] builder options have uniform signature --- src/storm/builder/BuilderOptions.cpp | 8 ++++---- src/storm/builder/BuilderOptions.h | 12 ++++++------ 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp index 6e42745fd..b0d2641bd 100644 --- a/src/storm/builder/BuilderOptions.cpp +++ b/src/storm/builder/BuilderOptions.cpp @@ -157,8 +157,8 @@ namespace storm { return buildAllLabels; } - BuilderOptions& BuilderOptions::setBuildAllRewardModels() { - buildAllRewardModels = true; + BuilderOptions& BuilderOptions::setBuildAllRewardModels(bool newValue) { + buildAllRewardModels = newValue; return *this; } @@ -185,8 +185,8 @@ namespace storm { return *this; } - BuilderOptions& BuilderOptions::setBuildAllLabels() { - buildAllLabels = true; + BuilderOptions& BuilderOptions::setBuildAllLabels(bool newValue) { + buildAllLabels = newValue; return *this; } diff --git a/src/storm/builder/BuilderOptions.h b/src/storm/builder/BuilderOptions.h index a06de50eb..28660e4b5 100644 --- a/src/storm/builder/BuilderOptions.h +++ b/src/storm/builder/BuilderOptions.h @@ -97,17 +97,17 @@ namespace storm { bool isExplorationShowProgressSet() const; uint64_t getExplorationShowProgressDelay() const; - BuilderOptions& setBuildAllRewardModels(); + BuilderOptions& setBuildAllRewardModels(bool newValue = true); BuilderOptions& addRewardModel(std::string const& rewardModelName); - BuilderOptions& setBuildAllLabels(); + BuilderOptions& setBuildAllLabels(bool newValue = true); BuilderOptions& addLabel(storm::expressions::Expression const& expression); BuilderOptions& addLabel(std::string const& labelName); BuilderOptions& addTerminalExpression(storm::expressions::Expression const& expression, bool value); BuilderOptions& addTerminalLabel(std::string const& label, bool value); - BuilderOptions& setBuildChoiceLabels(bool newValue); - BuilderOptions& setBuildStateValuations(bool newValue); - BuilderOptions& setBuildChoiceOrigins(bool newValue); - BuilderOptions& setExplorationChecks(bool newValue); + BuilderOptions& setBuildChoiceLabels(bool newValue = true); + BuilderOptions& setBuildStateValuations(bool newValue = true); + BuilderOptions& setBuildChoiceOrigins(bool newValue = true); + BuilderOptions& setExplorationChecks(bool newValue = true); private: /// A flag that indicates whether all reward models are to be built. In this case, the reward model names are From 98d124bd06269129a0044945e257da0860607d60 Mon Sep 17 00:00:00 2001 From: sjunges Date: Sun, 13 Aug 2017 15:35:35 +0200 Subject: [PATCH 09/12] As the builder options now occur in the API, we should improve their documentation. --- src/storm/builder/BuilderOptions.h | 51 ++++++++++++++++++++++++++++-- 1 file changed, 49 insertions(+), 2 deletions(-) diff --git a/src/storm/builder/BuilderOptions.h b/src/storm/builder/BuilderOptions.h index 28660e4b5..f3a6edfbf 100644 --- a/src/storm/builder/BuilderOptions.h +++ b/src/storm/builder/BuilderOptions.h @@ -81,9 +81,21 @@ namespace storm { * model. */ void setTerminalStatesFromFormula(storm::logic::Formula const& formula); - + + /*! + * Which reward models are built + * @return + */ std::vector const& getRewardModelNames() const; + /*! + * Which labels are built + * @return + */ std::set const& getLabelNames() const; + /*! + * Which expression labels are built + * @return + */ std::vector const& getExpressionLabels() const; std::vector> const& getTerminalStates() const; bool hasTerminalStates() const; @@ -96,17 +108,52 @@ namespace storm { bool isExplorationChecksSet() const; bool isExplorationShowProgressSet() const; uint64_t getExplorationShowProgressDelay() const; - + + /** + * Should all reward models be built? If not set, only required reward models are build. + * @param newValue The new value (default true) + * @return this + */ BuilderOptions& setBuildAllRewardModels(bool newValue = true); + /** + * Add an additional reward model to build + * @param newValue The name of the extra reward model + * @return this + */ BuilderOptions& addRewardModel(std::string const& rewardModelName); + /** + * Should all reward models be built? If not set, only required reward models are build. + * @param newValue The new value (default true) + * @return this + */ BuilderOptions& setBuildAllLabels(bool newValue = true); BuilderOptions& addLabel(storm::expressions::Expression const& expression); BuilderOptions& addLabel(std::string const& labelName); BuilderOptions& addTerminalExpression(storm::expressions::Expression const& expression, bool value); BuilderOptions& addTerminalLabel(std::string const& label, bool value); + /** + * Should the choice labels be built? + * @param newValue The new value (default true) + * @return this + */ BuilderOptions& setBuildChoiceLabels(bool newValue = true); + /** + * Should the state valuation mapping be built? + * @param newValue The new value (default true) + * @return this + */ BuilderOptions& setBuildStateValuations(bool newValue = true); + /** + * Should the origins the different choices be built? + * @param newValue The new value (default true) + * @return this + */ BuilderOptions& setBuildChoiceOrigins(bool newValue = true); + /** + * Should extra checks be performed during exploration + * @param newValue The new value (default true) + * @return this + */ BuilderOptions& setExplorationChecks(bool newValue = true); private: From 2c2dc5acd89bcdeecf96d2640b6c0096b700bf68 Mon Sep 17 00:00:00 2001 From: sjunges Date: Sun, 13 Aug 2017 15:36:47 +0200 Subject: [PATCH 10/12] Changed API such that the command line settings do not occur in the settings anymore. Moreover, to prevent having 15 Boolean arguments, the build options are now part of the API. --- src/storm/api/builder.h | 35 ++++++++++++++--------------------- src/storm/cli/cli.cpp | 30 +++++++++++++++++++----------- 2 files changed, 33 insertions(+), 32 deletions(-) diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index 868c47bba..ca21f99fc 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -23,10 +23,6 @@ #include "storm/builder/ExplicitModelBuilder.h" #include "storm/builder/jit/ExplicitJitJaniModelBuilder.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/IOSettings.h" -#include "storm/settings/modules/JitBuilderSettings.h" - #include "storm/utility/macros.h" #include "storm/exceptions/NotSupportedException.h" @@ -62,29 +58,18 @@ namespace storm { } template - std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool buildChoiceLabels = false, bool buildChoiceOrigins = false, bool buildStateValuations = false) { - storm::builder::BuilderOptions options(formulas); - - if (storm::settings::getModule().isBuildFullModelSet()) { - options.setBuildAllLabels(); - options.setBuildAllRewardModels(); - options.clearTerminalStates(); - } - options.setBuildChoiceLabels(buildChoiceLabels); - options.setBuildChoiceOrigins(buildChoiceOrigins); - options.setBuildStateValuations(buildStateValuations); - - if (storm::settings::getModule().isJitSet()) { + std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& model, storm::builder::BuilderOptions const& options, bool jit = false, bool doctor = false) { + if (jit) { STORM_LOG_THROW(model.isJaniModel(), storm::exceptions::NotSupportedException, "Cannot use JIT-based model builder for non-JANI model."); - + storm::builder::jit::ExplicitJitJaniModelBuilder builder(model.asJaniModel(), options); - - if (storm::settings::getModule().isDoctorSet()) { + + if (doctor) { bool result = builder.doctor(); STORM_LOG_THROW(result, storm::exceptions::NotSupportedException, "The JIT-based model builder cannot be used on your system."); STORM_LOG_INFO("The JIT-based model builder seems to be working."); } - + return builder.build(); } else { std::shared_ptr> generator; @@ -99,6 +84,14 @@ namespace storm { return builder.build(); } } + + template + std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool jit = false, bool doctor = false) { + storm::builder::BuilderOptions options(formulas); + return buildSparseModel(model, options, jit, doctor); + + + } template> std::shared_ptr> buildSparseModel(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents&& components) { diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index 343006c6d..42a76a7b2 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -4,34 +4,34 @@ #include "storm/models/ModelBase.h" -#include "storm/settings/modules/DebugSettings.h" -#include "storm/settings/modules/IOSettings.h" -#include "storm/settings/modules/CoreSettings.h" #include "storm/exceptions/OptionParserException.h" -#include "storm/settings/modules/ResourceSettings.h" -#include "storm/settings/modules/JaniExportSettings.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/symbolic/StandardRewardModel.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/ResourceSettings.h" +#include "storm/settings/modules/JitBuilderSettings.h" +#include "storm/settings/modules/DebugSettings.h" +#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/ResourceSettings.h" +#include "storm/settings/modules/JaniExportSettings.h" + #include "storm/utility/resources.h" #include "storm/utility/file.h" #include "storm/utility/storm-version.h" -#include "storm/utility/cli.h" +#include "storm/utility/macros.h" #include "storm/utility/initialize.h" #include "storm/utility/Stopwatch.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/ResourceSettings.h" - #include #include "storm/api/storm.h" -#include "storm/utility/macros.h" // Includes for the linked libraries and versions header. #ifdef STORM_HAVE_INTELTBB @@ -370,7 +370,15 @@ namespace storm { template std::shared_ptr buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { auto counterexampleGeneratorSettings = storm::settings::getModule(); - return storm::api::buildSparseModel(input.model.get(), createFormulasToRespect(input.properties), ioSettings.isBuildChoiceLabelsSet(), counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet()); + storm::builder::BuilderOptions options(createFormulasToRespect(input.properties)); + options.setBuildChoiceLabels(ioSettings.isBuildChoiceLabelsSet()); + options.setBuildChoiceOrigins(counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet()); + options.setBuildAllLabels(ioSettings.isBuildFullModelSet()); + options.setBuildAllRewardModels(ioSettings.isBuildFullModelSet()); + if (ioSettings.isBuildFullModelSet()) { + options.clearTerminalStates(); + } + return storm::api::buildSparseModel(input.model.get(), options, ioSettings.isJitSet(), storm::settings::getModule().isDoctorSet()); } template From e718acffba9bd6fa47efe144551bfa978824bb3c Mon Sep 17 00:00:00 2001 From: sjunges Date: Sun, 13 Aug 2017 17:18:08 +0200 Subject: [PATCH 11/12] move cli stuff from storm lib to an own small lib --- src/CMakeLists.txt | 1 + src/storm-cli-utilities/CMakeLists.txt | 40 +++++++++++++++++++ .../cli => storm-cli-utilities}/cli.cpp | 6 +-- src/{storm/cli => storm-cli-utilities}/cli.h | 0 src/storm-dft-cli/CMakeLists.txt | 2 +- src/storm-dft-cli/storm-dyftee.cpp | 4 +- .../modelchecker/dft/DFTModelChecker.cpp | 2 + src/storm-gspn-cli/CMakeLists.txt | 2 +- src/storm-gspn-cli/storm-gspn.cpp | 4 +- src/storm-pgcl-cli/CMakeLists.txt | 2 +- src/storm-pgcl-cli/storm-pgcl.cpp | 2 +- src/storm/CMakeLists.txt | 2 +- src/storm/storm.cpp | 2 +- 13 files changed, 56 insertions(+), 13 deletions(-) create mode 100644 src/storm-cli-utilities/CMakeLists.txt rename src/{storm/cli => storm-cli-utilities}/cli.cpp (99%) rename src/{storm/cli => storm-cli-utilities}/cli.h (100%) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 38b884cf7..acf819119 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -5,6 +5,7 @@ set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin) add_custom_target(binaries) add_subdirectory(storm) +add_subdirectory(storm-cli-utilities) add_subdirectory(storm-pgcl) add_subdirectory(storm-pgcl-cli) add_subdirectory(storm-gspn) diff --git a/src/storm-cli-utilities/CMakeLists.txt b/src/storm-cli-utilities/CMakeLists.txt new file mode 100644 index 000000000..64c2848c7 --- /dev/null +++ b/src/storm-cli-utilities/CMakeLists.txt @@ -0,0 +1,40 @@ +file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-cli-utilities/*.h ${PROJECT_SOURCE_DIR}/src/storm-cli-utilities/*.cpp) + +register_source_groups_from_filestructure("${ALL_FILES}" storm-cli-utilities) + + + +file(GLOB_RECURSE STORM_CLI_UTIL_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-cli-utilities/*.cpp) +file(GLOB_RECURSE STORM_CLI_UTIL_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-cli-utilities/*.h) + + +# Create storm-pars. +add_library(storm-cli-utilities SHARED ${STORM_CLI_UTIL_SOURCES} ${STORM_CLI_UTIL_HEADERS}) + +# Remove define symbol for shared libstorm. +set_target_properties(storm-cli-utilities PROPERTIES DEFINE_SYMBOL "") +#add_dependencies(storm resources) +list(APPEND STORM_TARGETS storm-cli-utilities) +set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) + +target_link_libraries(storm-cli-utilities PUBLIC storm) + +# Install storm headers to include directory. +foreach(HEADER ${STORM_CLI_UTIL_HEADERS}) + string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) + string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) + string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) + add_custom_command( + OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} + COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} + COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} + DEPENDS ${HEADER} + ) + list(APPEND STORM_CLI_UTIL_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") +endforeach() +add_custom_target(copy_storm_cli_util_headers DEPENDS ${STORM_CLI_UTIL_OUTPUT_HEADERS} ${STORM_CLI_UTIL_HEADERS}) +add_dependencies(storm-cli-utilities copy_storm_pars_headers) + +# installation +install(TARGETS storm-cli-utilities RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) + diff --git a/src/storm/cli/cli.cpp b/src/storm-cli-utilities/cli.cpp similarity index 99% rename from src/storm/cli/cli.cpp rename to src/storm-cli-utilities/cli.cpp index 42a76a7b2..66d83ece7 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm-cli-utilities/cli.cpp @@ -1,4 +1,4 @@ -#include "storm/cli/cli.h" +#include "cli.h" #include "storm/storage/SymbolicModelDescription.h" @@ -65,12 +65,12 @@ namespace storm { storm::utility::setUp(); storm::cli::printHeader("Storm", argc, argv); storm::settings::initializeAll("Storm", "storm"); - + storm::utility::Stopwatch totalTimer(true); if (!storm::cli::parseOptions(argc, argv)) { return -1; } - + processOptions(); totalTimer.stop(); diff --git a/src/storm/cli/cli.h b/src/storm-cli-utilities/cli.h similarity index 100% rename from src/storm/cli/cli.h rename to src/storm-cli-utilities/cli.h diff --git a/src/storm-dft-cli/CMakeLists.txt b/src/storm-dft-cli/CMakeLists.txt index 0d104405e..b8cdbbd27 100644 --- a/src/storm-dft-cli/CMakeLists.txt +++ b/src/storm-dft-cli/CMakeLists.txt @@ -1,6 +1,6 @@ # Create storm-dft. add_executable(storm-dft-cli ${PROJECT_SOURCE_DIR}/src/storm-dft-cli/storm-dyftee.cpp) -target_link_libraries(storm-dft-cli storm-dft) # Adding headers for xcode +target_link_libraries(storm-dft-cli storm-dft storm-cli-utilities) # Adding headers for xcode set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft") add_dependencies(binaries storm-dft-cli) diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index b2dc40006..8eef6f0b5 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -1,12 +1,12 @@ #include "storm/logic/Formula.h" #include "storm/utility/initialize.h" #include "storm/api/storm.h" -#include "storm/cli/cli.h" +#include "storm-cli-utilities/cli.h" #include "storm/exceptions/BaseException.h" #include "storm/logic/Formula.h" -#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/GmmxxEquationSolverSettings.h" diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 8721efd7c..d6b7e9138 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -1,5 +1,6 @@ #include "DFTModelChecker.h" +#include "storm/settings/modules/IOSettings.h" #include "storm/builder/ParallelCompositionBuilder.h" #include "storm/utility/bitoperations.h" #include "storm/utility/DirectEncodingExporter.h" @@ -357,6 +358,7 @@ namespace storm { explorationTimer.stop(); // Export the model if required + // TODO move this outside of the model checker? if (storm::settings::getModule().isExportExplicitSet()) { std::ofstream stream; storm::utility::openFile(storm::settings::getModule().getExportExplicitFilename(), stream); diff --git a/src/storm-gspn-cli/CMakeLists.txt b/src/storm-gspn-cli/CMakeLists.txt index 72e51a6da..39d656a4c 100644 --- a/src/storm-gspn-cli/CMakeLists.txt +++ b/src/storm-gspn-cli/CMakeLists.txt @@ -1,5 +1,5 @@ add_executable(storm-gspn-cli ${PROJECT_SOURCE_DIR}/src/storm-gspn-cli/storm-gspn.cpp) -target_link_libraries(storm-gspn-cli storm-gspn) # Adding headers for xcode +target_link_libraries(storm-gspn-cli storm-gspn storm-cli-utilities) # Adding headers for xcode set_target_properties(storm-gspn-cli PROPERTIES OUTPUT_NAME "storm-gspn") add_dependencies(binaries storm-gspn-cli) diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index 9a77a56be..fc493391a 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/src/storm-gspn-cli/storm-gspn.cpp @@ -12,7 +12,7 @@ #include "storm/utility/initialize.h" #include "api/storm.h" -#include "storm/cli/cli.h" +#include "storm-cli-utilities/cli.h" #include "storm/parser/FormulaParser.h" @@ -27,7 +27,7 @@ #include "storm/exceptions/FileIoException.h" -#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/GSPNSettings.h" #include "storm/settings/modules/GSPNExportSettings.h" #include "storm/settings/modules/CoreSettings.h" diff --git a/src/storm-pgcl-cli/CMakeLists.txt b/src/storm-pgcl-cli/CMakeLists.txt index 0f051a1b4..4778d1e93 100644 --- a/src/storm-pgcl-cli/CMakeLists.txt +++ b/src/storm-pgcl-cli/CMakeLists.txt @@ -1,5 +1,5 @@ add_executable(storm-pgcl-cli ${PROJECT_SOURCE_DIR}/src/storm-pgcl-cli/storm-pgcl.cpp) -target_link_libraries(storm-pgcl-cli storm-pgcl) +target_link_libraries(storm-pgcl-cli storm-pgcl storm-cli-utilities) set_target_properties(storm-pgcl-cli PROPERTIES OUTPUT_NAME "storm-pgcl") # installation diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp index 423afb087..ce579938f 100644 --- a/src/storm-pgcl-cli/storm-pgcl.cpp +++ b/src/storm-pgcl-cli/storm-pgcl.cpp @@ -2,7 +2,7 @@ #include "logic/Formula.h" #include "utility/initialize.h" -#include "storm/cli/cli.h" +#include "storm-cli-utilities/cli.h" #include "storm/exceptions/BaseException.h" #include "storm/utility/macros.h" #include diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt index 193a6d4bb..0ed4b0d1c 100644 --- a/src/storm/CMakeLists.txt +++ b/src/storm/CMakeLists.txt @@ -49,7 +49,7 @@ set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) # Create storm. add_executable(storm-main ${STORM_MAIN_SOURCES} ${STORM_MAIN_HEADERS}) -target_link_libraries(storm-main PUBLIC storm) +target_link_libraries(storm-main PUBLIC storm storm-cli-utilities) set_target_properties(storm-main PROPERTIES OUTPUT_NAME "storm") # Install storm headers to include directory. diff --git a/src/storm/storm.cpp b/src/storm/storm.cpp index 8e915d6e7..3cba6dd3d 100644 --- a/src/storm/storm.cpp +++ b/src/storm/storm.cpp @@ -1,7 +1,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/BaseException.h" -#include "storm/cli/cli.h" +#include "storm-cli-utilities/cli.h" /*! * Main entry point of the executable storm. From b4a8833e3f5349d68bc3c34ee6650ecb70b59206 Mon Sep 17 00:00:00 2001 From: sjunges Date: Sun, 13 Aug 2017 17:18:37 +0200 Subject: [PATCH 12/12] towards getting rid of code duplication in storm-pars-cli --- src/storm-pars-cli/storm-pars.cpp | 49 +++++++++++++++---------------- 1 file changed, 23 insertions(+), 26 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 0836f1e0d..1ff2fabb6 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -6,7 +6,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/api/storm.h" -#include "storm/cli/cli.h" +#include "storm-cli-utilities/cli.h" #include "storm/models/ModelBase.h" #include "storm/storage/SymbolicModelDescription.h" #include "storm/utility/file.h" @@ -23,13 +23,13 @@ #include "storm/exceptions/InvalidSettingsException.h" #include "storm/exceptions/NotSupportedException.h" -#include "storm/cli/cli.cpp" +#include "storm-cli-utilities/cli.cpp" namespace storm { namespace pars { typedef typename storm::cli::SymbolicInput SymbolicInput; - + template std::shared_ptr buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { return storm::api::buildSparseModel(input.model.get(), storm::api::extractFormulasFromProperties(input.properties), ioSettings.isBuildChoiceLabelsSet()); @@ -50,7 +50,7 @@ namespace storm { STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input."); result = storm::cli::buildModelExplicit(ioSettings); } - + modelBuildingWatch.stop(); if (result) { STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl); @@ -335,27 +335,7 @@ namespace storm { processInputWithValueTypeAndDdlib(symbolicInput); } - - int64_t process(const int argc, const char** argv) { - storm::utility::setUp(); - storm::cli::printHeader("Storm-pars", argc, argv); - storm::settings::initializeParsSettings("Storm-pars", "storm-pars"); - - storm::utility::Stopwatch totalTimer(true); - if (!storm::cli::parseOptions(argc, argv)) { - return -1; - } - - processOptions(); - - totalTimer.stop(); - if (storm::settings::getModule().isPrintTimeAndMemorySet()) { - storm::cli::printTimeAndMemoryStatistics(totalTimer.getTimeInMilliseconds()); - } - - storm::utility::cleanUp(); - return 0; - } + } } @@ -366,7 +346,24 @@ namespace storm { int main(const int argc, const char** argv) { try { - return storm::pars::process(argc, argv); + storm::utility::setUp(); + storm::cli::printHeader("Storm-pars", argc, argv); + storm::settings::initializeParsSettings("Storm-pars", "storm-pars"); + + storm::utility::Stopwatch totalTimer(true); + if (!storm::cli::parseOptions(argc, argv)) { + return -1; + } + + storm::pars::processOptions(); + + totalTimer.stop(); + if (storm::settings::getModule().isPrintTimeAndMemorySet()) { + storm::cli::printTimeAndMemoryStatistics(totalTimer.getTimeInMilliseconds()); + } + + storm::utility::cleanUp(); + return 0; } catch (storm::exceptions::BaseException const& exception) { STORM_LOG_ERROR("An exception caused Storm-pars to terminate. The message of the exception is: " << exception.what()); return 1;