From 30f6b4395d163af5937bade4e00fe93f295bf8c4 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 29 Nov 2018 11:39:16 +0100 Subject: [PATCH] model checking routines take optional environment --- lib/stormpy/__init__.py | 22 +++++++++++----------- src/core/modelchecking.cpp | 25 +++++++++++++------------ src/mod_core.cpp | 3 ++- 3 files changed, 26 insertions(+), 24 deletions(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 0f81f35..b3caa25 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -252,7 +252,7 @@ def perform_symbolic_bisimulation(model, properties): return core._perform_symbolic_bisimulation(model, formulae, bisimulation_type) -def model_checking(model, property, only_initial_states=False, extract_scheduler=False): +def model_checking(model, property, only_initial_states=False, extract_scheduler=False, environment=Environment()): """ Perform model checking on model for property. :param model: Model. @@ -263,10 +263,10 @@ def model_checking(model, property, only_initial_states=False, extract_scheduler :rtype: CheckResult """ return check_model_sparse(model, property, only_initial_states=only_initial_states, - extract_scheduler=extract_scheduler) + extract_scheduler=extract_scheduler, environment=environment) -def check_model_sparse(model, property, only_initial_states=False, extract_scheduler=False): +def check_model_sparse(model, property, only_initial_states=False, extract_scheduler=False, environment=Environment()): """ Perform model checking on model for property. :param model: Model. @@ -284,14 +284,14 @@ def check_model_sparse(model, property, only_initial_states=False, extract_sched if model.supports_parameters: task = core.ParametricCheckTask(formula, only_initial_states) task.set_produce_schedulers(extract_scheduler) - return core._parametric_model_checking_sparse_engine(model, task) + return core._parametric_model_checking_sparse_engine(model, task, environment=environment) else: task = core.CheckTask(formula, only_initial_states) task.set_produce_schedulers(extract_scheduler) - return core._model_checking_sparse_engine(model, task) + return core._model_checking_sparse_engine(model, task, environment=environment) -def check_model_dd(model, property, only_initial_states=False): +def check_model_dd(model, property, only_initial_states=False, environment=Environment()): """ Perform model checking using dd engine. :param model: Model. @@ -307,13 +307,13 @@ def check_model_dd(model, property, only_initial_states=False): if model.supports_parameters: task = core.ParametricCheckTask(formula, only_initial_states) - return core._parametric_model_checking_dd_engine(model, task) + return core._parametric_model_checking_dd_engine(model, task, environment=environment) else: task = core.CheckTask(formula, only_initial_states) - return core._model_checking_dd_engine(model, task) + return core._model_checking_dd_engine(model, task, environment=environment) -def check_model_hybrid(model, property, only_initial_states=False): +def check_model_hybrid(model, property, only_initial_states=False, environment=Environment()): """ Perform model checking using hybrid engine. :param model: Model. @@ -329,10 +329,10 @@ def check_model_hybrid(model, property, only_initial_states=False): if model.supports_parameters: task = core.ParametricCheckTask(formula, only_initial_states) - return core._parametric_model_checking_hybrid_engine(model, task) + return core._parametric_model_checking_hybrid_engine(model, task, environment=environment) else: task = core.CheckTask(formula, only_initial_states) - return core._model_checking_hybrid_engine(model, task) + return core._model_checking_hybrid_engine(model, task, environment=environment) def transform_to_sparse_model(model): """ diff --git a/src/core/modelchecking.cpp b/src/core/modelchecking.cpp index 862d4c3..684700a 100644 --- a/src/core/modelchecking.cpp +++ b/src/core/modelchecking.cpp @@ -2,26 +2,27 @@ #include "result.h" #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/modelchecker/results/CheckResult.h" +#include "storm/environment/Environment.h" template using CheckTask = storm::modelchecker::CheckTask; // Thin wrapper for model checking using sparse engine template -std::shared_ptr modelCheckingSparseEngine(std::shared_ptr> model, CheckTask const& task) { - return storm::api::verifyWithSparseEngine(model, task); +std::shared_ptr modelCheckingSparseEngine(std::shared_ptr> model, CheckTask const& task, storm::Environment const& env) { + return storm::api::verifyWithSparseEngine(env, model, task); } // Thin wrapper for model checking using dd engine template -std::shared_ptr modelCheckingDdEngine(std::shared_ptr> model, CheckTask const& task) { - return storm::api::verifyWithDdEngine(model, task); +std::shared_ptr modelCheckingDdEngine(std::shared_ptr> model, CheckTask const& task, storm::Environment const& env) { + return storm::api::verifyWithDdEngine(env, model, task); } // Thin wrapper for model checking using hybrid engine template -std::shared_ptr modelCheckingHybridEngine(std::shared_ptr> model, CheckTask const& task) { - return storm::api::verifyWithHybridEngine(model, task); +std::shared_ptr modelCheckingHybridEngine(std::shared_ptr> model, CheckTask const& task, storm::Environment const& env) { + return storm::api::verifyWithHybridEngine(env, model, task); } // Thin wrapper for computing prob01 states @@ -56,12 +57,12 @@ void define_modelchecking(py::module& m) { ; // Model checking - m.def("_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform model checking using the sparse engine", py::arg("model"), py::arg("task")); - m.def("_parametric_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform parametric model checking using the sparse engine", py::arg("model"), py::arg("task")); - m.def("_model_checking_dd_engine", &modelCheckingDdEngine, "Perform model checking using the dd engine", py::arg("model"), py::arg("task")); - m.def("_parametric_model_checking_dd_engine", &modelCheckingDdEngine, "Perform parametric model checking using the dd engine", py::arg("model"), py::arg("task")); - m.def("_model_checking_hybrid_engine", &modelCheckingHybridEngine, "Perform model checking using the hybrid engine", py::arg("model"), py::arg("task")); - m.def("_parametric_model_checking_hybrid_engine", &modelCheckingHybridEngine, "Perform parametric model checking using the hybrid engine", py::arg("model"), py::arg("task")); + m.def("_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform model checking using the sparse engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); + m.def("_parametric_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform parametric model checking using the sparse engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); + m.def("_model_checking_dd_engine", &modelCheckingDdEngine, "Perform model checking using the dd engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); + m.def("_parametric_model_checking_dd_engine", &modelCheckingDdEngine, "Perform parametric model checking using the dd engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); + m.def("_model_checking_hybrid_engine", &modelCheckingHybridEngine, "Perform model checking using the hybrid engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); + m.def("_parametric_model_checking_hybrid_engine", &modelCheckingHybridEngine, "Perform parametric model checking using the hybrid engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); m.def("_compute_prob01states_double", &computeProb01, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states")); m.def("_compute_prob01states_rationalfunc", &computeProb01, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states")); m.def("_compute_prob01states_min_double", &computeProb01min, "Compute prob-0-1 states (min)", py::arg("model"), py::arg("phi_states"), py::arg("psi_states")); diff --git a/src/mod_core.cpp b/src/mod_core.cpp index d3a752e..1c351f0 100644 --- a/src/mod_core.cpp +++ b/src/mod_core.cpp @@ -18,7 +18,9 @@ PYBIND11_MODULE(core, m) { // options.disable_function_signatures(); #endif + define_environment(m); define_core(m); + define_property(m); define_parse(m); define_build(m); @@ -30,6 +32,5 @@ PYBIND11_MODULE(core, m) { define_bisimulation(m); define_input(m); define_graph_constraints(m); - define_environment(m); define_transformation(m); }