diff --git a/src/storm/settings/modules/ResourceSettings.cpp b/src/storm/settings/modules/ResourceSettings.cpp index 572b71556..a8cc9a44e 100644 --- a/src/storm/settings/modules/ResourceSettings.cpp +++ b/src/storm/settings/modules/ResourceSettings.cpp @@ -15,11 +15,14 @@ namespace storm { const std::string ResourceSettings::timeoutOptionShortName = "t"; const std::string ResourceSettings::printTimeAndMemoryOptionName = "timemem"; const std::string ResourceSettings::printTimeAndMemoryOptionShortName = "tm"; + const std::string ResourceSettings::signalWaitingTimeOptionName = "signal-timeout"; ResourceSettings::ResourceSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, timeoutOptionName, false, "If given, computation will abort after the timeout has been reached.").setIsAdvanced().setShortName(timeoutOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("time", "Seconds after which to timeout.").setDefaultValueUnsignedInteger(0).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, printTimeAndMemoryOptionName, false, "Prints CPU time and memory consumption at the end.").setShortName(printTimeAndMemoryOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, signalWaitingTimeOptionName, false, "If given, computation will abort after the timeout has been reached.").setIsAdvanced() + .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("time", "Seconds after which to exit the program.").setDefaultValueUnsignedInteger(3).build()).build()); } bool ResourceSettings::isTimeoutSet() const { @@ -34,6 +37,10 @@ namespace storm { return this->getOption(printTimeAndMemoryOptionName).getHasOptionBeenSet(); } + uint_fast64_t ResourceSettings::getSignalWaitingTimeInSeconds() const { + return this->getOption(signalWaitingTimeOptionName).getArgumentByName("time").getValueAsUnsignedInteger(); + } + } } } diff --git a/src/storm/settings/modules/ResourceSettings.h b/src/storm/settings/modules/ResourceSettings.h index c92d9315b..0dd3341c3 100644 --- a/src/storm/settings/modules/ResourceSettings.h +++ b/src/storm/settings/modules/ResourceSettings.h @@ -39,6 +39,15 @@ namespace storm { */ uint_fast64_t getTimeoutInSeconds() const; + /*! + * Retrieves the waiting time of the program after a signal. + * If a signal to abort is handled, the program should terminate. + * However, it waits the given number of seconds before it is killed to allow for printing preliminary results. + * + * @return The number of seconds after which to exit the program. + */ + uint_fast64_t getSignalWaitingTimeInSeconds() const; + // The name of the module. static const std::string moduleName; @@ -48,6 +57,7 @@ namespace storm { static const std::string timeoutOptionShortName; static const std::string printTimeAndMemoryOptionName; static const std::string printTimeAndMemoryOptionShortName; + static const std::string signalWaitingTimeOptionName; }; } } diff --git a/src/storm/utility/SignalHandler.cpp b/src/storm/utility/SignalHandler.cpp index 13cdcae08..d3cc187e5 100644 --- a/src/storm/utility/SignalHandler.cpp +++ b/src/storm/utility/SignalHandler.cpp @@ -3,12 +3,15 @@ #include #include +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/ResourceSettings.h" + namespace storm { namespace utility { namespace resources { // Maximal waiting time after abort signal before terminating - const int maxWaitTime = 3; + int maxWaitTime = 0; SignalInformation::SignalInformation() : terminate(false), lastSignal(0) { } @@ -57,6 +60,9 @@ namespace storm { } void installSignalHandler() { + // Set the waiting time + maxWaitTime = storm::settings::getModule().getSignalWaitingTimeInSeconds(); + // We use the newer sigaction instead of signal struct sigaction sa; sa.sa_handler = signalHandler;