From 88c6604ef571c12947d9da7307d87477283285f3 Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 23 May 2016 17:36:44 +0200 Subject: [PATCH] Moved files Former-commit-id: b5126633794455782dc7c29d08fefda37281d03a --- stormpy/lib/stormpy/__init__.py | 2 ++ stormpy/src/core/core.cpp | 15 +++++++++++++++ stormpy/src/core/core.h | 1 + stormpy/src/core/model.h | 8 -------- stormpy/src/mod_core.cpp | 3 +-- stormpy/src/mod_storage.cpp | 2 ++ stormpy/src/{core => storage}/model.cpp | 16 +++++----------- stormpy/src/storage/model.h | 8 ++++++++ stormpy/tests/storage/test_matrix.py | 1 - stormpy/tests/{core => storage}/test_model.py | 1 - 10 files changed, 34 insertions(+), 23 deletions(-) delete mode 100644 stormpy/src/core/model.h rename stormpy/src/{core => storage}/model.cpp (83%) create mode 100644 stormpy/src/storage/model.h rename stormpy/tests/{core => storage}/test_model.py (99%) diff --git a/stormpy/lib/stormpy/__init__.py b/stormpy/lib/stormpy/__init__.py index abe483980..0ecddd76e 100644 --- a/stormpy/lib/stormpy/__init__.py +++ b/stormpy/lib/stormpy/__init__.py @@ -32,6 +32,8 @@ It looks like you want to know about 'stormpy'. from . import core from .core import * +from . import storage +from .storage import * core.set_up("") diff --git a/stormpy/src/core/core.cpp b/stormpy/src/core/core.cpp index 3a57be8a6..f650151c0 100644 --- a/stormpy/src/core/core.cpp +++ b/stormpy/src/core/core.cpp @@ -23,3 +23,18 @@ void define_parse(py::module& m) { // Parse explicit models m.def("parse_explicit_model", &storm::parser::AutoParser<>::parseModel, "Parse explicit model", py::arg("transition_file"), py::arg("labeling_file"), py::arg("state_reward_file") = "", py::arg("transition_reward_file") = "", py::arg("choice_labeling_file") = ""); } + +// Thin wrapper for model building +template +std::shared_ptr buildModel(storm::prism::Program const& program, std::shared_ptr const& formula) { + return storm::buildSymbolicModel(program, std::vector>(1,formula)).model; +} + +void define_build(py::module& m) { + + // Build model + m.def("_build_model", &buildModel, "Build the model", py::arg("program"), py::arg("formula")); + m.def("_build_parametric_model", &buildModel, "Build the parametric model", py::arg("program"), py::arg("formula")); + m.def("build_model_from_prism_program", &storm::buildSymbolicModel, "Build the model", py::arg("program"), py::arg("formulas")); + m.def("build_parametric_model_from_prism_program", &storm::buildSymbolicModel, "Build the parametric model", py::arg("program"), py::arg("formulas")); +} diff --git a/stormpy/src/core/core.h b/stormpy/src/core/core.h index f163b6b45..ee3b3be7a 100644 --- a/stormpy/src/core/core.h +++ b/stormpy/src/core/core.h @@ -5,5 +5,6 @@ void define_core(py::module& m); void define_parse(py::module& m); +void define_build(py::module& m); #endif /* PYTHON_CORE_CORE_H_ */ diff --git a/stormpy/src/core/model.h b/stormpy/src/core/model.h deleted file mode 100644 index 9f5c279e6..000000000 --- a/stormpy/src/core/model.h +++ /dev/null @@ -1,8 +0,0 @@ -#ifndef PYTHON_CORE_MODEL_H_ -#define PYTHON_CORE_MODEL_H_ - -#include "common.h" - -void define_model(py::module& m); - -#endif /* PYTHON_CORE_MODEL_H_ */ diff --git a/stormpy/src/mod_core.cpp b/stormpy/src/mod_core.cpp index 843a607f9..a985aa228 100644 --- a/stormpy/src/mod_core.cpp +++ b/stormpy/src/mod_core.cpp @@ -1,7 +1,6 @@ #include "common.h" #include "core/core.h" -#include "core/model.h" #include "core/modelchecking.h" #include "core/bisimulation.h" #include "core/prism.h" @@ -10,7 +9,7 @@ PYBIND11_PLUGIN(core) { py::module m("core"); define_core(m); define_parse(m); - define_model(m); + define_build(m); define_modelchecking(m); define_bisimulation(m); define_prism(m); diff --git a/stormpy/src/mod_storage.cpp b/stormpy/src/mod_storage.cpp index 7f61007d8..835f1e7b2 100644 --- a/stormpy/src/mod_storage.cpp +++ b/stormpy/src/mod_storage.cpp @@ -1,9 +1,11 @@ #include "common.h" +#include "storage/model.h" #include "storage/matrix.h" PYBIND11_PLUGIN(storage) { py::module m("storage"); + define_model(m); define_sparse_matrix(m); return m.ptr(); } diff --git a/stormpy/src/core/model.cpp b/stormpy/src/storage/model.cpp similarity index 83% rename from stormpy/src/core/model.cpp rename to stormpy/src/storage/model.cpp index 0fd929c42..6445973b2 100644 --- a/stormpy/src/core/model.cpp +++ b/stormpy/src/storage/model.cpp @@ -1,10 +1,10 @@ #include "model.h" -// Thin wrapper for model building -template -std::shared_ptr buildModel(storm::prism::Program const& program, std::shared_ptr const& formula) { - return storm::buildSymbolicModel(program, std::vector>(1,formula)).model; -} +#include "src/models/ModelBase.h" +#include "src/models/sparse/Model.h" +#include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/Mdp.h" +#include "src/models/sparse/StandardRewardModel.h" // Thin wrapper for getting initial states template @@ -22,12 +22,6 @@ storm::storage::SparseMatrix getTransitionMatrix(storm::models::sparse:: // Define python bindings void define_model(py::module& m) { - - // Build model - m.def("_build_model", &buildModel, "Build the model", py::arg("program"), py::arg("formula")); - m.def("_build_parametric_model", &buildModel, "Build the parametric model", py::arg("program"), py::arg("formula")); - m.def("build_model_from_prism_program", &storm::buildSymbolicModel, "Build the model", py::arg("program"), py::arg("formulas")); - m.def("build_parametric_model_from_prism_program", &storm::buildSymbolicModel, "Build the parametric model", py::arg("program"), py::arg("formulas")); // ModelType py::enum_(m, "ModelType", "Type of the model") diff --git a/stormpy/src/storage/model.h b/stormpy/src/storage/model.h new file mode 100644 index 000000000..c779f26e7 --- /dev/null +++ b/stormpy/src/storage/model.h @@ -0,0 +1,8 @@ +#ifndef PYTHON_STORAGE_MODEL_H_ +#define PYTHON_STORAGE_MODEL_H_ + +#include "common.h" + +void define_model(py::module& m); + +#endif /* PYTHON_STORAGE_MODEL_H_ */ diff --git a/stormpy/tests/storage/test_matrix.py b/stormpy/tests/storage/test_matrix.py index b9414708c..becf477a4 100644 --- a/stormpy/tests/storage/test_matrix.py +++ b/stormpy/tests/storage/test_matrix.py @@ -1,5 +1,4 @@ import stormpy -import stormpy.storage class TestMatrix: def test_sparse_matrix(self): diff --git a/stormpy/tests/core/test_model.py b/stormpy/tests/storage/test_model.py similarity index 99% rename from stormpy/tests/core/test_model.py rename to stormpy/tests/storage/test_model.py index 1ab438ef6..1e54378cb 100644 --- a/stormpy/tests/core/test_model.py +++ b/stormpy/tests/storage/test_model.py @@ -3,7 +3,6 @@ import stormpy.logic class TestModel: def test_build_dtmc_from_prism_program(self): - stormpy.set_up("") program = stormpy.parse_prism_program("../examples/dtmc/die/die.pm") prop = "P=? [F \"one\"]" formulas = stormpy.parse_formulas_for_prism_program(prop, program)