From 6f62e8d402c31e0be5157e9918efe52fd5680968 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 6 Mar 2020 17:15:07 +0100 Subject: [PATCH] Support abort in model building --- .../parser/DirectEncodingParser.cpp | 20 ++++++--- src/storm/builder/ExplicitModelBuilder.cpp | 45 ++++++++++--------- .../BisimulationDecomposition.cpp | 21 ++++++--- 3 files changed, 54 insertions(+), 32 deletions(-) diff --git a/src/storm-parsers/parser/DirectEncodingParser.cpp b/src/storm-parsers/parser/DirectEncodingParser.cpp index 4814c77f5..adbc0482e 100644 --- a/src/storm-parsers/parser/DirectEncodingParser.cpp +++ b/src/storm-parsers/parser/DirectEncodingParser.cpp @@ -8,20 +8,23 @@ #include #include -#include "storm/models/sparse/MarkovAutomaton.h" -#include "storm/models/sparse/Ctmc.h" +#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/exceptions/AbortException.h" #include "storm/exceptions/FileIoException.h" -#include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/WrongFormatException.h" #include "storm/settings/SettingsManager.h" -#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/Ctmc.h" + #include "storm/utility/constants.h" #include "storm/utility/builder.h" -#include "storm/utility/macros.h" #include "storm/utility/file.h" +#include "storm/utility/macros.h" +#include "storm/utility/SignalHandler.h" namespace storm { @@ -352,6 +355,13 @@ namespace storm { STORM_LOG_THROW(target < stateSize, storm::exceptions::WrongFormatException, "Target state " << target << " is greater than state size " << stateSize); builder.addNextValue(row, target, value); } + + if (storm::utility::resources::isTerminate()) { + std::cout << "Parsed " << state << "/" << stateSize << " states before abort." << std::endl; + STORM_LOG_THROW(false, storm::exceptions::AbortException, "Aborted in state space exploration."); + break; + } + } // end state iteration STORM_LOG_TRACE("Finished parsing"); diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 63ebee7c9..0dad59191 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -2,41 +2,37 @@ #include -#include "storm/models/sparse/Dtmc.h" -#include "storm/models/sparse/Ctmc.h" -#include "storm/models/sparse/Mdp.h" -#include "storm/models/sparse/MarkovAutomaton.h" -#include "storm/models/sparse/StandardRewardModel.h" - -#include "storm/storage/expressions/ExpressionManager.h" - -#include "storm/settings/modules/BuildSettings.h" #include "storm/builder/RewardModelBuilder.h" #include "storm/builder/ChoiceInformationBuilder.h" +#include "storm/exceptions/AbortException.h" +#include "storm/exceptions/WrongFormatException.h" + #include "storm/generator/PrismNextStateGenerator.h" #include "storm/generator/JaniNextStateGenerator.h" +#include "storm/models/sparse/Dtmc.h" +#include "storm/models/sparse/Ctmc.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/StandardRewardModel.h" + +#include "storm/settings/modules/BuildSettings.h" -#include "storm/storage/jani/Edge.h" -#include "storm/storage/jani/EdgeDestination.h" +#include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/jani/Model.h" #include "storm/storage/jani/Automaton.h" -#include "storm/storage/jani/Location.h" #include "storm/storage/jani/AutomatonComposition.h" #include "storm/storage/jani/ParallelComposition.h" -#include "storm/storage/jani/CompositionInformationVisitor.h" -#include "storm/utility/prism.h" +#include "storm/utility/builder.h" #include "storm/utility/constants.h" +#include "storm/utility/prism.h" #include "storm/utility/macros.h" #include "storm/utility/ConstantsComparator.h" -#include "storm/utility/builder.h" +#include "storm/utility/SignalHandler.h" -#include "storm/exceptions/WrongFormatException.h" -#include "storm/exceptions/InvalidArgumentException.h" -#include "storm/exceptions/InvalidOperationException.h" namespace storm { namespace builder { @@ -245,11 +241,11 @@ namespace storm { } ++currentRowGroup; } - + + ++numberOfExploredStates; if (generator->getOptions().isShowProgressSet()) { ++numberOfExploredStatesSinceLastMessage; - ++numberOfExploredStates; - + auto now = std::chrono::high_resolution_clock::now(); auto durationSinceLastMessage = std::chrono::duration_cast(now - timeOfLastMessage).count(); if (static_cast(durationSinceLastMessage) >= generator->getOptions().getShowProgressDelay()) { @@ -260,6 +256,13 @@ namespace storm { numberOfExploredStatesSinceLastMessage = 0; } } + + if (storm::utility::resources::isTerminate()) { + auto durationSinceStart = std::chrono::duration_cast(std::chrono::high_resolution_clock::now() - timeOfStart).count(); + std::cout << "Explored " << numberOfExploredStates << " states in " << durationSinceStart << " seconds before abort." << std::endl; + STORM_LOG_THROW(false, storm::exceptions::AbortException, "Aborted in state space exploration."); + break; + } } if (markovianStates) { diff --git a/src/storm/storage/bisimulation/BisimulationDecomposition.cpp b/src/storm/storage/bisimulation/BisimulationDecomposition.cpp index 577e7e487..e71283e51 100644 --- a/src/storm/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storm/storage/bisimulation/BisimulationDecomposition.cpp @@ -2,25 +2,28 @@ #include +#include "storm/exceptions/AbortException.h" +#include "storm/exceptions/IllegalFunctionCallException.h" +#include "storm/exceptions/InvalidOptionException.h" + +#include "storm/logic/FormulaInformation.h" +#include "storm/logic/FragmentSpecification.h" + #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Ctmc.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/storage/bisimulation/DeterministicBlockData.h" - #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" -#include "storm/logic/FormulaInformation.h" -#include "storm/logic/FragmentSpecification.h" +#include "storm/storage/bisimulation/DeterministicBlockData.h" #include "storm/utility/macros.h" -#include "storm/exceptions/IllegalFunctionCallException.h" -#include "storm/exceptions/InvalidOptionException.h" +#include "storm/utility/SignalHandler.h" namespace storm { namespace storage { @@ -250,6 +253,12 @@ namespace storm { // Now refine the partition using the current splitter. refinePartitionBasedOnSplitter(*splitter, splitterQueue); + + if (storm::utility::resources::isTerminate()) { + std::cout << "Performed " << iterations << " iterations of partition refinement before abort." << std::endl; + STORM_LOG_THROW(false, storm::exceptions::AbortException, "Aborted in bisimulation computation."); + break; + } } }