From 756ac1cad7b744b60c4a3f264979b5a4e0b5d2c9 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 25 Jan 2016 13:05:17 +0100
Subject: [PATCH] added timeout and memout flags. memout is, however, not
 supported by Mac OS

Former-commit-id: fc067d906c1825189a15d501e6c710cc0cb99cb3
---
 src/cli/cli.cpp                          |  8 +++--
 src/settings/modules/GeneralSettings.cpp | 16 +++++++--
 src/settings/modules/GeneralSettings.h   | 16 +++++++++
 src/utility/OsDetection.h                |  1 +
 src/utility/resources.h                  | 45 +++++++++++++++---------
 5 files changed, 64 insertions(+), 22 deletions(-)

diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp
index 3c456b1bd..391392b31 100644
--- a/src/cli/cli.cpp
+++ b/src/cli/cli.cpp
@@ -213,9 +213,11 @@ namespace storm {
                 storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
 
                 // If we were given a time or memory limit, we put it in place now.
-                // FIXME: insert actual option.
-                if (false) {
-                    
+                if (settings.isTimeoutSet()) {
+                    storm::utility::resources::setCPULimit(settings.getTimeoutInSeconds());
+                }
+                if (settings.isMemoutSet()) {
+                    storm::utility::resources::setMemoryLimit(settings.getMemoutInMegabytes());
                 }
                 
                 // If we have to build the model from a symbolic representation, we need to parse the representation first.
diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp
index ee76dff86..fe61401c2 100644
--- a/src/settings/modules/GeneralSettings.cpp
+++ b/src/settings/modules/GeneralSettings.cpp
@@ -43,7 +43,9 @@ namespace storm {
             const std::string GeneralSettings::dontFixDeadlockOptionName = "no-fixdl";
             const std::string GeneralSettings::dontFixDeadlockOptionShortName = "ndl";
             const std::string GeneralSettings::timeoutOptionName = "timeout";
-            const std::string GeneralSettings::timeoutOptionShortName = "t";
+            const std::string GeneralSettings::timeoutOptionShortName = "to";
+            const std::string GeneralSettings::memoutOptionName = "memout";
+            const std::string GeneralSettings::memoutOptionShortName = "mo";
             const std::string GeneralSettings::eqSolverOptionName = "eqsolver";
             const std::string GeneralSettings::lpSolverOptionName = "lpsolver";
             const std::string GeneralSettings::smtSolverOptionName = "smtsolver";
@@ -106,7 +108,9 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer. Available are: gmm++ and native.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, timeoutOptionName, false, "If given, computation will abort after the timeout has been reached.").setShortName(timeoutOptionShortName)
-                                .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("time", "The number of seconds after which to timeout.").setDefaultValueUnsignedInteger(0).build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("time", "The number of seconds after which to timeout. Note that this is measures in CPU time, not in wallclock time.").setDefaultValueUnsignedInteger(0).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, memoutOptionName, false, "If given, the computation will abort if the given memory is exceeded.").setShortName(memoutOptionShortName)
+                                .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("memory", "The amount of megabytes available.").setDefaultValueUnsignedInteger(0).build()).build());
                 
                 std::vector<std::string> ddLibraries = {"cudd", "sylvan"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, ddLibraryOptionName, false, "Sets which library is preferred for decision-diagram operations.")
@@ -251,6 +255,14 @@ namespace storm {
             uint_fast64_t GeneralSettings::getTimeoutInSeconds() const {
                 return this->getOption(timeoutOptionName).getArgumentByName("time").getValueAsUnsignedInteger();
             }
+
+            bool GeneralSettings::isMemoutSet() const {
+                return this->getOption(memoutOptionName).getHasOptionBeenSet();
+            }
+            
+            uint_fast64_t GeneralSettings::getMemoutInMegabytes() const {
+                return this->getOption(memoutOptionName).getArgumentByName("memory").getValueAsUnsignedInteger();
+            }
             
             storm::solver::EquationSolverType  GeneralSettings::getEquationSolver() const {
                 std::string equationSolverName = this->getOption(eqSolverOptionName).getArgumentByName("name").getValueAsString();
diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h
index 6dd9326e5..1302bcc97 100644
--- a/src/settings/modules/GeneralSettings.h
+++ b/src/settings/modules/GeneralSettings.h
@@ -259,6 +259,20 @@ namespace storm {
                  */
                 uint_fast64_t getTimeoutInSeconds() const;
 
+                /*!
+                 * Retrieves whether the memout option was set.
+                 *
+                 * @return True if the memout option was set.
+                 */
+                bool isMemoutSet() const;
+                
+                /*!
+                 * Retrieves the amount of megabytes available.
+                 *
+                 * @return The avail memory given in megabytes.
+                 */
+                uint_fast64_t getMemoutInMegabytes() const;
+                
                 /*!
                  * Retrieves the selected equation solver.
                  *
@@ -408,6 +422,8 @@ namespace storm {
                 static const std::string dontFixDeadlockOptionShortName;
                 static const std::string timeoutOptionName;
                 static const std::string timeoutOptionShortName;
+                static const std::string memoutOptionName;
+                static const std::string memoutOptionShortName;
                 static const std::string eqSolverOptionName;
                 static const std::string lpSolverOptionName;
                 static const std::string smtSolverOptionName;
diff --git a/src/utility/OsDetection.h b/src/utility/OsDetection.h
index d91d5595e..83d1f00bd 100644
--- a/src/utility/OsDetection.h
+++ b/src/utility/OsDetection.h
@@ -13,6 +13,7 @@
 #	define GetCurrentDir getcwd
 #elif defined TARGET_OS_MAC || defined __apple__ || defined __APPLE__
 #	define MACOSX
+#   define MACOS
 #   define NOEXCEPT noexcept
 #	define _DARWIN_USE_64_BIT_INODE
 #	include <sys/mman.h>
diff --git a/src/utility/resources.h b/src/utility/resources.h
index 0b9dd80ad..4dfc4a4d5 100644
--- a/src/utility/resources.h
+++ b/src/utility/resources.h
@@ -11,6 +11,8 @@
 
 #include "src/utility/OsDetection.h"
 
+#include "src/utility/macros.h"
+
 namespace storm {
     namespace utility {
         namespace resources {
@@ -19,40 +21,49 @@ namespace storm {
             static const int STORM_EXIT_TIMEOUT = -2;
             static const int STORM_EXIT_MEMOUT = -3;
             
-            inline void setCPULimit(std::size_t seconds) {
+            inline std::size_t getCPULimit() {
                 rlimit rl;
                 getrlimit(RLIMIT_CPU, &rl);
-                rl.rlim_cur = seconds;
-                setrlimit(RLIMIT_CPU, &rl);
+                return rl.rlim_cur;
             }
-            
-            inline std::size_t getCPULimit() {
+
+            inline void setCPULimit(std::size_t seconds) {
                 rlimit rl;
                 getrlimit(RLIMIT_CPU, &rl);
-                return rl.rlim_cur;
+                rl.rlim_cur = seconds;
+                setrlimit(RLIMIT_CPU, &rl);
             }
             
             inline std::size_t usedCPU() {
                 return std::size_t(clock()) / CLOCKS_PER_SEC;
             }
             
-            inline void setMemoryLimit(std::size_t megabytes) {
+            inline std::size_t getMemoryLimit() {
+#if defined LINUX
                 rlimit rl;
                 getrlimit(RLIMIT_AS, &rl);
-                rl.rlim_cur = megabytes * 1024 * 1024;
-                setrlimit(RLIMIT_AS, &rl);
+                return rl.rlim_cur;
+#else
+                STORM_LOG_WARN("Retrieving the memory limit is not supported for your operating system.");
+                return 0;
+#endif
             }
             
-            inline std::size_t getMemoryLimit() {
+            inline void setMemoryLimit(std::size_t megabytes) {
+#if defined LINUX
                 rlimit rl;
                 getrlimit(RLIMIT_AS, &rl);
-                return rl.rlim_cur;
+                rl.rlim_cur = megabytes * 1024 * 1024;
+                setrlimit(RLIMIT_AS, &rl);
+#else
+                STORM_LOG_WARN("Setting a memory limit is not supported for your operating system.");
+#endif
             }
             
-            inline void quick_exit_if_available(int errorCode) {
-#ifdef LINUX
+            inline void quickest_exit(int errorCode) {
+#if defined LINUX
                 std::quick_exit(errorCode);
-#elseif MACOS
+#elif defined MACOS
                 std::_Exit(errorCode);
 #else
                 std::abort();
@@ -62,13 +73,13 @@ namespace storm {
             inline void signalHandler(int signal) {
                 if (signal == SIGXCPU) {
                     std::cerr << "Timeout." << std::endl;
-                    quick_exit_if_available(STORM_EXIT_TIMEOUT);
+                    quickest_exit(STORM_EXIT_TIMEOUT);
                 } else if (signal == ENOMEM) {
                     std::cerr << "Out of memory" << std::endl;
-                    quick_exit_if_available(STORM_EXIT_MEMOUT);
+                    quickest_exit(STORM_EXIT_MEMOUT);
                 } else {
                     std::cerr << "Unknown abort in resource limitation module." << std::endl;
-                    quick_exit_if_available(STORM_EXIT_GENERALERROR);
+                    quickest_exit(STORM_EXIT_GENERALERROR);
                 }
             }