sp
/
tempestpy
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

model checking routines take optional environment

refactoring
Sebastian Junges 6 years ago
parent
5aab3cbe3e
commit
30f6b4395d
3 changed files with 26 additions and 24 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 22
      lib/stormpy/__init__.py
  2. 25
      src/core/modelchecking.cpp
  3. 3
      src/mod_core.cpp

22
lib/stormpy/__init__.py
View File

@ -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):
"""

25
src/core/modelchecking.cpp
View File

@ -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<typename ValueType>
using CheckTask = storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>;
// Thin wrapper for model checking using sparse engine
template<typename ValueType>
std::shared_ptr<storm::modelchecker::CheckResult> modelCheckingSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, CheckTask<ValueType> const& task) {
return storm::api::verifyWithSparseEngine<ValueType>(model, task);
std::shared_ptr<storm::modelchecker::CheckResult> modelCheckingSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, CheckTask<ValueType> const& task, storm::Environment const& env) {
return storm::api::verifyWithSparseEngine<ValueType>(env, model, task);
}
// Thin wrapper for model checking using dd engine
template<storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::modelchecker::CheckResult> modelCheckingDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> model, CheckTask<ValueType> const& task) {
return storm::api::verifyWithDdEngine<DdType, ValueType>(model, task);
std::shared_ptr<storm::modelchecker::CheckResult> modelCheckingDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> model, CheckTask<ValueType> const& task, storm::Environment const& env) {
return storm::api::verifyWithDdEngine<DdType, ValueType>(env, model, task);
}
// Thin wrapper for model checking using hybrid engine
template<storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::modelchecker::CheckResult> modelCheckingHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> model, CheckTask<ValueType> const& task) {
return storm::api::verifyWithHybridEngine<DdType, ValueType>(model, task);
std::shared_ptr<storm::modelchecker::CheckResult> modelCheckingHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> model, CheckTask<ValueType> const& task, storm::Environment const& env) {
return storm::api::verifyWithHybridEngine<DdType, ValueType>(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<double>, "Perform model checking using the sparse engine", py::arg("model"), py::arg("task"));
m.def("_parametric_model_checking_sparse_engine", &modelCheckingSparseEngine<storm::RationalFunction>, "Perform parametric model checking using the sparse engine", py::arg("model"), py::arg("task"));
m.def("_model_checking_dd_engine", &modelCheckingDdEngine<storm::dd::DdType::Sylvan, double>, "Perform model checking using the dd engine", py::arg("model"), py::arg("task"));
m.def("_parametric_model_checking_dd_engine", &modelCheckingDdEngine<storm::dd::DdType::Sylvan, storm::RationalFunction>, "Perform parametric model checking using the dd engine", py::arg("model"), py::arg("task"));
m.def("_model_checking_hybrid_engine", &modelCheckingHybridEngine<storm::dd::DdType::Sylvan, double>, "Perform model checking using the hybrid engine", py::arg("model"), py::arg("task"));
m.def("_parametric_model_checking_hybrid_engine", &modelCheckingHybridEngine<storm::dd::DdType::Sylvan, storm::RationalFunction>, "Perform parametric model checking using the hybrid engine", py::arg("model"), py::arg("task"));
m.def("_model_checking_sparse_engine", &modelCheckingSparseEngine<double>, "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<storm::RationalFunction>, "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<storm::dd::DdType::Sylvan, double>, "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<storm::dd::DdType::Sylvan, storm::RationalFunction>, "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<storm::dd::DdType::Sylvan, double>, "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<storm::dd::DdType::Sylvan, storm::RationalFunction>, "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<double>, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states"));
m.def("_compute_prob01states_rationalfunc", &computeProb01<storm::RationalFunction>, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states"));
m.def("_compute_prob01states_min_double", &computeProb01min<double>, "Compute prob-0-1 states (min)", py::arg("model"), py::arg("phi_states"), py::arg("psi_states"));

3
src/mod_core.cpp
View File

@ -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);
}
Write Preview
Loading…
Cancel
Save