From cf15015421e0e20f9da55bfda5ce143a453fdca5 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 22 Jan 2016 17:56:55 +0100
Subject: [PATCH] some more work on games
Former-commit-id: 6741b1f0bc1aed1da636fbd5aab886f3defde091
---
CMakeLists.txt | 1 -
src/CMakeLists.txt | 2 +
src/cli/cli.cpp | 10 ++-
src/cli/entrypoints.h | 18 ++--
.../GameBasedMdpModelChecker.cpp} | 36 ++++----
.../GameBasedMdpModelChecker.h} | 34 +++-----
src/utility/resources.h | 84 +++++++++++++++++++
src/utility/solver.h | 4 +-
src/utility/storm.h | 11 ++-
9 files changed, 154 insertions(+), 46 deletions(-)
rename src/modelchecker/{reachability/MenuGameMdpModelChecker.cpp => abstraction/GameBasedMdpModelChecker.cpp} (54%)
rename src/modelchecker/{reachability/MenuGameMdpModelChecker.h => abstraction/GameBasedMdpModelChecker.h} (55%)
create mode 100644 src/utility/resources.h
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 9f6a50f70..cbc32aed4 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -456,7 +456,6 @@ endif()
if(STORM_HAVE_CARL)
message(STATUS "StoRM - Linking with carl.")
- message("${carl_INCLUDE_DIR}")
include_directories("${carl_INCLUDE_DIR}")
list(APPEND STORM_LINK_LIBRARIES ${carl_LIBRARIES})
endif()
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index f5f633aea..49ce1c6f3 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -21,6 +21,7 @@ file(GLOB STORM_MODELCHECKER_CSL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/cs
file(GLOB_RECURSE STORM_MODELCHECKER_CSL_HELPER_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/helper/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/helper/*.cpp)
file(GLOB_RECURSE STORM_MODELCHECKER_REACHABILITY_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.cpp)
file(GLOB_RECURSE STORM_MODELCHECKER_PROPOSITIONAL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.cpp)
+file(GLOB_RECURSE STORM_MODELCHECKER_ABSTRACTION_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/abstraction/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/abstraction/*.cpp)
file(GLOB_RECURSE STORM_MODELCHECKER_RESULTS_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.cpp)
file(GLOB_RECURSE STORM_COUNTEREXAMPLES_FILES ${PROJECT_SOURCE_DIR}/src/counterexamples/*.h ${PROJECT_SOURCE_DIR}/src/counterexamples/*.cpp)
file(GLOB_RECURSE STORM_PERMISSIVESCHEDULER_FILES ${PROJECT_SOURCE_DIR}/src/permissivesched/*.h ${PROJECT_SOURCE_DIR}/src/permissivesched/*.cpp)
@@ -69,6 +70,7 @@ source_group(modelchecker\\csl FILES ${STORM_MODELCHECKER_CSL_FILES})
source_group(modelchecker\\csl\\helper FILES ${STORM_MODELCHECKER_CSL_HELPER_FILES})
source_group(modelchecker\\reachability FILES ${STORM_MODELCHECKER_REACHABILITY_FILES})
source_group(modelchecker\\propositional FILES ${STORM_MODELCHECKER_PROPOSITIONAL_FILES})
+source_group(modelchecker\\abstraction FILES ${STORM_MODELCHECKER_ABSTRACTION_FILES})
source_group(modelchecker\\results FILES ${STORM_MODELCHECKER_RESULTS_FILES})
source_group(counterexamples FILES ${STORM_COUNTEREXAMPLES_FILES})
source_group(permissiveschedulers FILES ${STORM_PERMISSIVESCHEDULER_FILES})
diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp
index 54643d32a..3c456b1bd 100644
--- a/src/cli/cli.cpp
+++ b/src/cli/cli.cpp
@@ -7,7 +7,7 @@
#include "src/exceptions/OptionParserException.h"
#include "src/utility/storm-version.h"
-
+#include "src/utility/resources.h"
// Includes for the linked libraries and versions header.
#ifdef STORM_HAVE_INTELTBB
@@ -209,8 +209,14 @@ namespace storm {
if (storm::settings::debugSettings().isLogfileSet()) {
storm::utility::initializeFileLogging();
}
-
+
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 we have to build the model from a symbolic representation, we need to parse the representation first.
boost::optional<storm::prism::Program> program;
diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h
index 79de987ee..6996e5fd4 100644
--- a/src/cli/entrypoints.h
+++ b/src/cli/entrypoints.h
@@ -3,8 +3,6 @@
#include "src/utility/storm.h"
-#include "src/exceptions/NotImplementedException.h"
-
namespace storm {
namespace cli {
@@ -49,9 +47,19 @@ namespace storm {
}
#endif
- template<storm::dd::DdType DdType>
+ template<typename ValueType, storm::dd::DdType DdType>
void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Abstraction Refinement is not yet implemented.");
+ for (auto const& formula : formulas) {
+ std::cout << std::endl << "Model checking property: " << *formula << " ...";
+ std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifyProgramWithAbstractionRefinementEngine<DdType, ValueType>(program, formula));
+ if (result) {
+ std::cout << " done." << std::endl;
+ std::cout << "Result (initial states): ";
+ std::cout << *result << std::endl;
+ } else {
+ std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+ }
+ }
}
template<storm::dd::DdType DdType>
@@ -118,7 +126,7 @@ namespace storm {
storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement) {
- verifySymbolicModelWithAbstractionRefinementEngine<LibraryType>(program, formulas);
+ verifySymbolicModelWithAbstractionRefinementEngine<ValueType, LibraryType>(program, formulas);
} else {
storm::storage::ModelProgramPair modelProgramPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
STORM_LOG_THROW(modelProgramPair.model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
diff --git a/src/modelchecker/reachability/MenuGameMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
similarity index 54%
rename from src/modelchecker/reachability/MenuGameMdpModelChecker.cpp
rename to src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
index 09ad129d3..1e603b6e8 100644
--- a/src/modelchecker/reachability/MenuGameMdpModelChecker.cpp
+++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
@@ -1,4 +1,4 @@
-#include "src/modelchecker/reachability/MenuGameMdpModelChecker.h"
+#include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h"
#include "src/utility/macros.h"
@@ -8,18 +8,25 @@
namespace storm {
namespace modelchecker {
- MenuGameMdpModelChecker::MenuGameMdpModelChecker(storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory) : originalProgram(program), smtSolverFactory(std::move(smtSolverFactory)) {
+ template<storm::dd::DdType Type, typename ValueType>
+ GameBasedMdpModelChecker<Type, ValueType>::GameBasedMdpModelChecker(storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory) : originalProgram(program), smtSolverFactory(std::move(smtSolverFactory)) {
STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only MDPs are supported by the game-based model checker.");
-
+
// Start by preparing the program. That is, we flatten the modules if there is more than one.
if (originalProgram.getNumberOfModules() > 1) {
- preprocessedProgram = originalProgram.flattenModules(smtSolverFactory);
+ preprocessedProgram = originalProgram.flattenModules(this->smtSolverFactory);
} else {
preprocessedProgram = originalProgram;
}
}
-
- bool MenuGameMdpModelChecker::canHandle(storm::logic::Formula const& formula) const {
+
+ template<storm::dd::DdType Type, typename ValueType>
+ GameBasedMdpModelChecker<Type, ValueType>::~GameBasedMdpModelChecker() {
+ // Intentionally left empty.
+ }
+
+ template<storm::dd::DdType Type, typename ValueType>
+ bool GameBasedMdpModelChecker<Type, ValueType>::canHandle(storm::logic::Formula const& formula) const {
if (formula.isProbabilityOperatorFormula()) {
storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula();
return this->canHandle(probabilityOperatorFormula.getSubformula());
@@ -39,23 +46,24 @@ namespace storm {
return false;
}
- std::unique_ptr<CheckResult> MenuGameMdpModelChecker::checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula) {
+ template<storm::dd::DdType Type, typename ValueType>
+ std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula) {
// Depending on whether or not there is a bound, we do something slightly different here.
-
return nullptr;
}
- std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
+ template<storm::dd::DdType Type, typename ValueType>
+ std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
// TODO
-
return nullptr;
}
-
- std::unique_ptr<CheckResult> computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
+
+ template<storm::dd::DdType Type, typename ValueType>
+ std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
// TODO
-
return nullptr;
}
-
+
+ template class GameBasedMdpModelChecker<storm::dd::DdType::CUDD, double>;
}
}
\ No newline at end of file
diff --git a/src/modelchecker/reachability/MenuGameMdpModelChecker.h b/src/modelchecker/abstraction/GameBasedMdpModelChecker.h
similarity index 55%
rename from src/modelchecker/reachability/MenuGameMdpModelChecker.h
rename to src/modelchecker/abstraction/GameBasedMdpModelChecker.h
index 7919d1bed..3edae3d71 100644
--- a/src/modelchecker/reachability/MenuGameMdpModelChecker.h
+++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.h
@@ -1,15 +1,18 @@
-#ifndef STORM_MODELCHECKER_MENUGAMEMDPMODELCHECKER_H_
-#define STORM_MODELCHECKER_MENUGAMEMDPMODELCHECKER_H_
+#ifndef STORM_MODELCHECKER_GAMEBASEDMDPMODELCHECKER_H_
+#define STORM_MODELCHECKER_GAMEBASEDMDPMODELCHECKER_H_
#include "src/modelchecker/AbstractModelChecker.h"
+#include "src/utility/solver.h"
+
#include "src/storage/prism/Program.h"
-#include "src/utility/solver.h"
+#include "src/storage/dd/DdType.h"
namespace storm {
namespace modelchecker {
- class MenuGameMdpModelChecker : public AbstractModelChecker {
+ template<storm::dd::DdType Type, typename ValueType>
+ class GameBasedMdpModelChecker : public AbstractModelChecker {
public:
/*!
* Constructs a model checker whose underlying model is implicitly given by the provided program. All
@@ -18,31 +21,18 @@ namespace storm {
* @param program The program that implicitly specifies the model to check.
* @param smtSolverFactory A factory used to create SMT solver when necessary.
*/
- explicit MenuGameMdpModelChecker(storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory);
+ explicit GameBasedMdpModelChecker(storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory = std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+ virtual ~GameBasedMdpModelChecker() override;
+
virtual bool canHandle(storm::logic::Formula const& formula) const override;
virtual std::unique_ptr<CheckResult> checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula) override;
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;
virtual std::unique_ptr<CheckResult> computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;
-
- private:
- /*!
- * Performs game-based abstraction refinement on the model until either the precision is met or the provided
- * proof goal was successfully proven.
- *
- * @param filterPredicate A predicate that needs to hold until the target predicate holds.
- * @param targetPredicate A predicate characterizing the target states.
- * @param precision The precision to use. This governs what difference between lower and upper bounds is
- * acceptable.
- * @param proofGoal A proof goal that says the probability must only be established to be above/below a given
- * threshold. If the proof goal is met before the precision is achieved, the refinement procedure will abort
- * and return the current result.
- * @return A pair of values, that are under- and over-approximations of the actual probability, respectively.
- */
- std::pair<double, double> performGameBasedRefinement(storm::expressions::Expression const& filterPredicate, storm::expressions::Expression const& targetPredicate, double precision, boost::optional<std::pair<double, storm::logic::ComparisonType>> const& proofGoal);
+ private:
// The original program that was used to create this model checker.
storm::prism::Program originalProgram;
@@ -56,4 +46,4 @@ namespace storm {
}
}
-#endif /* STORM_MODELCHECKER_MENUGAMEMDPMODELCHECKER_H_ */
\ No newline at end of file
+#endif /* STORM_MODELCHECKER_GAMEBASEDMDPMODELCHECKER_H_ */
\ No newline at end of file
diff --git a/src/utility/resources.h b/src/utility/resources.h
new file mode 100644
index 000000000..0b9dd80ad
--- /dev/null
+++ b/src/utility/resources.h
@@ -0,0 +1,84 @@
+#ifndef STORM_UTILITY_RESOURCES_H_
+#define STORM_UTILITY_RESOURCES_H_
+
+#include <cstdlib>
+#include <csignal>
+#include <sys/time.h>
+#include <sys/times.h>
+#include <sys/resource.h>
+
+#include "storm-config.h"
+
+#include "src/utility/OsDetection.h"
+
+namespace storm {
+ namespace utility {
+ namespace resources {
+
+ static const int STORM_EXIT_GENERALERROR = -1;
+ static const int STORM_EXIT_TIMEOUT = -2;
+ static const int STORM_EXIT_MEMOUT = -3;
+
+ inline void setCPULimit(std::size_t seconds) {
+ rlimit rl;
+ getrlimit(RLIMIT_CPU, &rl);
+ rl.rlim_cur = seconds;
+ setrlimit(RLIMIT_CPU, &rl);
+ }
+
+ inline std::size_t getCPULimit() {
+ rlimit rl;
+ getrlimit(RLIMIT_CPU, &rl);
+ return rl.rlim_cur;
+ }
+
+ inline std::size_t usedCPU() {
+ return std::size_t(clock()) / CLOCKS_PER_SEC;
+ }
+
+ inline void setMemoryLimit(std::size_t megabytes) {
+ rlimit rl;
+ getrlimit(RLIMIT_AS, &rl);
+ rl.rlim_cur = megabytes * 1024 * 1024;
+ setrlimit(RLIMIT_AS, &rl);
+ }
+
+ inline std::size_t getMemoryLimit() {
+ rlimit rl;
+ getrlimit(RLIMIT_AS, &rl);
+ return rl.rlim_cur;
+ }
+
+ inline void quick_exit_if_available(int errorCode) {
+#ifdef LINUX
+ std::quick_exit(errorCode);
+#elseif MACOS
+ std::_Exit(errorCode);
+#else
+ std::abort();
+#endif
+ }
+
+ inline void signalHandler(int signal) {
+ if (signal == SIGXCPU) {
+ std::cerr << "Timeout." << std::endl;
+ quick_exit_if_available(STORM_EXIT_TIMEOUT);
+ } else if (signal == ENOMEM) {
+ std::cerr << "Out of memory" << std::endl;
+ quick_exit_if_available(STORM_EXIT_MEMOUT);
+ } else {
+ std::cerr << "Unknown abort in resource limitation module." << std::endl;
+ quick_exit_if_available(STORM_EXIT_GENERALERROR);
+ }
+ }
+
+ inline void installSignalHandler() {
+ std::signal(SIGXCPU, signalHandler);
+ std::signal(ENOMEM, signalHandler);
+ }
+
+ }
+ }
+}
+
+#endif /* STORM_UTILITY_RESOURCES_H_ */
\ No newline at end of file
diff --git a/src/utility/solver.h b/src/utility/solver.h
index cf2c63663..c93ad65ef 100644
--- a/src/utility/solver.h
+++ b/src/utility/solver.h
@@ -1,6 +1,8 @@
#ifndef STORM_UTILITY_SOLVER_H_
#define STORM_UTILITY_SOLVER_H_
+#include <iostream>
+
#include <set>
#include <vector>
#include <memory>
@@ -174,7 +176,7 @@ namespace storm {
public:
virtual std::unique_ptr<storm::solver::SmtSolver> create(storm::expressions::ExpressionManager& manager) const;
};
-
+
class MathsatSmtSolverFactory : public SmtSolverFactory {
public:
virtual std::unique_ptr<storm::solver::SmtSolver> create(storm::expressions::ExpressionManager& manager) const;
diff --git a/src/utility/storm.h b/src/utility/storm.h
index 03e297ca5..00b288cf6 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -56,6 +56,7 @@
#include "src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
#include "src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
#include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
+#include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h"
#include "src/modelchecker/csl/SparseCtmcCslModelChecker.h"
#include "src/modelchecker/csl/HybridCtmcCslModelChecker.h"
#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
@@ -337,7 +338,6 @@ namespace storm {
return result;
}
-
template<storm::dd::DdType DdType>
std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
std::unique_ptr<storm::modelchecker::CheckResult> result;
@@ -358,6 +358,15 @@ namespace storm {
}
return result;
}
+
+ template<storm::dd::DdType DdType, typename ValueType>
+ std::unique_ptr<storm::modelchecker::CheckResult> verifyProgramWithAbstractionRefinementEngine(storm::prism::Program const& program, std::shared_ptr<storm::logic::Formula> const& formula) {
+ STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Cannot treat non-MDP model using the abstraction refinement engine.");
+
+ // FIXME: Cudd -> ValueType, double -> ValueType
+ storm::modelchecker::GameBasedMdpModelChecker<storm::dd::DdType::CUDD, double> modelchecker(program);
+ return modelchecker.check(*formula);
+ }
template<typename ValueType>
void exportMatrixToFile(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::string const& filepath) {