From 2a753da0fd2f2f3b69e59811fb008233af11d2c0 Mon Sep 17 00:00:00 2001 From: Linus Heck Date: Tue, 18 Aug 2026 11:56:05 +0200 Subject: [PATCH 1/2] Towards generating stubs: attempt at fixing C++ name leaks by first declaring, then defining --- CMakeLists.txt | 24 ++++-- cmake/core_config.py.in | 4 + lib/stormpy/__init__.py | 4 +- lib/stormpy/logic/__init__.py | 4 +- lib/stormpy/storage/__init__.py | 3 +- lib/stormpy/utility/__init__.py | 4 +- src/common.h | 5 ++ src/core/bisimulation.cpp | 24 +++++- src/core/core.cpp | 6 ++ src/mod_bindings.cpp | 54 ++++++++++++ src/mod_core.cpp | 13 ++- src/mod_logic.cpp | 13 ++- src/mod_storage.cpp | 17 ++-- src/mod_utility.cpp | 13 ++- src/module_bindings.h | 12 +++ src/registration.h | 138 +++++++++++++++++++++++++++++++ src/storage/dd.cpp | 8 +- src/storage/distribution.cpp | 2 + src/storage/jani.cpp | 18 ++++ src/storage/matrix.cpp | 2 + tests/test_registration_order.py | 61 ++++++++++++++ 21 files changed, 383 insertions(+), 46 deletions(-) create mode 100644 src/mod_bindings.cpp create mode 100644 src/module_bindings.h create mode 100644 src/registration.h create mode 100644 tests/test_registration_order.py diff --git a/CMakeLists.txt b/CMakeLists.txt index 4459836e84..a3651e3f4b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -332,14 +332,28 @@ configure_file(${CMAKE_CURRENT_SOURCE_DIR}/src/pycarl/definitions.h.in ${CMAKE_C # Build stormpy ###### -# Build stormpy modules -stormpy_module(core "." "${storm-counterexamples_INCLUDE_DIR}" storm-counterexamples) +# Build the mutually dependent core bindings in one extension. The extension +# registers the public native modules in two passes: all Python types first, +# followed by their methods and free functions. +build_stormpy_module(stormpy_bindings + "." "bindings" + "mod_bindings.cpp" "core/*.cpp" + "${storm-counterexamples_INCLUDE_DIR}" + "storm-counterexamples") +file(GLOB_RECURSE STORMPY_BINDINGS_EXTRA_SOURCES + "${CMAKE_CURRENT_SOURCE_DIR}/src/logic/*.cpp" + "${CMAKE_CURRENT_SOURCE_DIR}/src/storage/*.cpp" + "${CMAKE_CURRENT_SOURCE_DIR}/src/utility/*.cpp") +target_sources(stormpy_bindings PRIVATE ${STORMPY_BINDINGS_EXTRA_SOURCES}) +target_sources(stormpy_bindings PRIVATE + "${CMAKE_CURRENT_SOURCE_DIR}/src/mod_core.cpp" + "${CMAKE_CURRENT_SOURCE_DIR}/src/mod_logic.cpp" + "${CMAKE_CURRENT_SOURCE_DIR}/src/mod_storage.cpp" + "${CMAKE_CURRENT_SOURCE_DIR}/src/mod_utility.cpp") +target_compile_definitions(stormpy_bindings PRIVATE STORMPY_REGISTRATION_TWO_PASS) configure_file(${CMAKE_CURRENT_SOURCE_DIR}/cmake/core_config.py.in ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/_config.py @ONLY) stormpy_module(info info "${storm-version-info_INCLUDE_DIR}" storm-version-info) configure_file(${CMAKE_CURRENT_SOURCE_DIR}/cmake/info_config.py.in ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/info/_config.py @ONLY) -stormpy_module(logic logic "" "") -stormpy_module(storage storage "" "") -stormpy_module(utility utility "" "") # Build optional stormpy modules stormpy_optional_module(dft "DFT") diff --git a/cmake/core_config.py.in b/cmake/core_config.py.in index dfdab957b7..43c83abcd0 100644 --- a/cmake/core_config.py.in +++ b/cmake/core_config.py.in @@ -8,3 +8,7 @@ Polynomial = pycarl.@PYCARL_RF_PACKAGE@.Polynomial FactorizedPolynomial = pycarl.@PYCARL_RF_PACKAGE@.FactorizedPolynomial RationalFunction = pycarl.@PYCARL_RF_PACKAGE@.RationalFunction FactorizedRationalFunction = pycarl.@PYCARL_RF_PACKAGE@.FactorizedRationalFunction + +# Register the formula type used by Storm's parametric graph analysis before +# the native Storm APIs are bound. +from stormpy.pycarl.@PYCARL_RF_PACKAGE@ import formula as _pycarl_formula diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 8ecec5a99f..6205d1aab2 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -1,6 +1,8 @@ from ._config import * -from . import _core +from . import _bindings + +_core = _bindings._core from ._core import * from . import storage from .storage import * diff --git a/lib/stormpy/logic/__init__.py b/lib/stormpy/logic/__init__.py index 863bdcacf1..84a4300a5c 100644 --- a/lib/stormpy/logic/__init__.py +++ b/lib/stormpy/logic/__init__.py @@ -1,2 +1,4 @@ -from . import _logic +import stormpy + +_logic = stormpy._bindings._logic from ._logic import * diff --git a/lib/stormpy/storage/__init__.py b/lib/stormpy/storage/__init__.py index 9379403e0f..510ee0bc3c 100644 --- a/lib/stormpy/storage/__init__.py +++ b/lib/stormpy/storage/__init__.py @@ -1,5 +1,6 @@ import stormpy.utility -from . import _storage + +_storage = stormpy._bindings._storage from ._storage import * from deprecated.sphinx import deprecated diff --git a/lib/stormpy/utility/__init__.py b/lib/stormpy/utility/__init__.py index 2afcea3bf1..e025d1b169 100644 --- a/lib/stormpy/utility/__init__.py +++ b/lib/stormpy/utility/__init__.py @@ -1,4 +1,6 @@ -from . import _utility +import stormpy + +_utility = stormpy._bindings._utility from ._utility import * # Extend JSON container for simplified access diff --git a/src/common.h b/src/common.h index 576b955b89..8b1eb4d50e 100644 --- a/src/common.h +++ b/src/common.h @@ -8,7 +8,12 @@ #include #include +#ifdef STORMPY_REGISTRATION_TWO_PASS +#include "src/registration.h" +namespace py = stormpy::registration; +#else namespace py = pybind11; +#endif using namespace pybind11::literals; PYBIND11_DECLARE_HOLDER_TYPE(T, std::shared_ptr) diff --git a/src/core/bisimulation.cpp b/src/core/bisimulation.cpp index 5755f5410e..c74fa30d4a 100644 --- a/src/core/bisimulation.cpp +++ b/src/core/bisimulation.cpp @@ -4,10 +4,11 @@ #include template -std::shared_ptr> performBisimulationMinimization( - std::shared_ptr> const& model, std::vector> const& formulas, - storm::storage::BisimulationType const& bisimulationType, storm::dd::bisimulation::QuotientFormat const& quotientFormat, - storm::dd::bisimulation::BisimulationOptions const& bisimulationOptions) { +std::shared_ptr performBisimulationMinimization(std::shared_ptr> const& model, + std::vector> const& formulas, + storm::storage::BisimulationType const& bisimulationType, + storm::dd::bisimulation::QuotientFormat const& quotientFormat, + storm::dd::bisimulation::BisimulationOptions const& bisimulationOptions) { return storm::api::performBisimulationMinimization( model, formulas, bisimulationType, storm::dd::bisimulation::SignatureMode::Eager, quotientFormat, bisimulationOptions); } @@ -37,6 +38,21 @@ void define_bisimulation(py::module& m) { .value("DD", storm::dd::bisimulation::QuotientFormat::Dd) .finalize(); + py::native_enum(m, "BisimulationReuseMode", "enum.Enum") + .value("NONE", storm::dd::bisimulation::ReuseMode::None) + .value("BLOCK_NUMBERS", storm::dd::bisimulation::ReuseMode::BlockNumbers) + .finalize(); + + py::native_enum(m, "BisimulationRefinementMode", "enum.Enum") + .value("FULL", storm::dd::bisimulation::RefinementMode::Full) + .value("CHANGED_STATES", storm::dd::bisimulation::RefinementMode::ChangedStates) + .finalize(); + + py::native_enum(m, "BisimulationInitialPartitionMode", "enum.Enum") + .value("REGULAR", storm::dd::bisimulation::InitialPartitionMode::Regular) + .value("FINER", storm::dd::bisimulation::InitialPartitionMode::Finer) + .finalize(); + py::class_(m, "BisimulationOptionsDd", "Options for Dd bisimulation") .def(py::init<>(), "Create") .def_readwrite("reuse_mode", &storm::dd::bisimulation::BisimulationOptions::reuseMode, "Reuse mode") diff --git a/src/core/core.cpp b/src/core/core.cpp index e34c66e71c..5b16639672 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -180,6 +180,9 @@ void define_build_sparse_model_defs(py::module& m) { m.def("make_sparse_model_builder_exact", &storm::api::makeExplicitModelBuilder, "Construct a builder instance", py::arg("model_description"), py::arg("options"), py::arg("action_mask") = nullptr, py::arg("exploration_options") = typename storm::builder::ExplicitModelBuilder::Options()); + py::class_>(m, "ExplicitExactModelBuilder", "Model builder for exact sparse models") + .def("build", &storm::builder::ExplicitModelBuilder::build, "Build the model", py::call_guard()) + .def("export_lookup", &storm::builder::ExplicitModelBuilder::exportExplicitStateLookup, "Export a lookup model"); } } @@ -242,6 +245,9 @@ void define_build(py::module& m) { py::arg("new_value") = true); py::class_, std::shared_ptr>> actionmask(m, "ActionMaskDouble"); + py::class_, std::shared_ptr>>(m, "ActionMaskExact"); + py::class_, std::shared_ptr>>( + m, "ActionMaskParametric"); py::class_, std::shared_ptr>> actfuncmask( m, "StateValuationFunctionActionMaskDouble", actionmask); actfuncmask.def(py::init>(), py::arg("f")); diff --git a/src/mod_bindings.cpp b/src/mod_bindings.cpp new file mode 100644 index 0000000000..5857d54ff1 --- /dev/null +++ b/src/mod_bindings.cpp @@ -0,0 +1,54 @@ +#include "src/module_bindings.h" + +namespace { + +pybind11::module_ createModule(pybind11::module_ const& parent, char const* name, char const* doc) { + pybind11::object moduleType = pybind11::module_::import("types").attr("ModuleType"); + pybind11::module_ result = moduleType(name, doc).cast(); + result.attr("__package__") = std::string(name).substr(0, std::string(name).rfind('.')); + result.attr("__loader__") = pybind11::none(); + result.attr("__spec__") = pybind11::module_::import("importlib.machinery").attr("ModuleSpec")(name, pybind11::none()); + if (pybind11::hasattr(parent, "__file__")) { + result.attr("__file__") = parent.attr("__file__"); + result.attr("__spec__").attr("origin") = parent.attr("__file__"); + } + pybind11::module_::import("sys").attr("modules")[pybind11::str(name)] = result; + return result; +} + +void bindAll(pybind11::module_ const& core, pybind11::module_ const& storage, pybind11::module_ const& logic, pybind11::module_ const& utility, + py::Phase phase) { + py::module utilityBindings(utility, phase); + py::module storageBindings(storage, phase); + py::module logicBindings(logic, phase); + py::module coreBindings(core, phase); + + stormpy::bindings::bindUtility(utilityBindings); + stormpy::bindings::bindStorage(storageBindings); + stormpy::bindings::bindLogic(logicBindings); + stormpy::bindings::bindCore(coreBindings); +} + +} // namespace + +PYBIND11_MODULE(_bindings, m) { + m.doc() = "Native Storm bindings"; + +#ifdef STORMPY_DISABLE_SIGNATURE_DOC + pybind11::options options; + options.disable_function_signatures(); +#endif + + pybind11::module_ core = createModule(m, "stormpy._core", "Core Storm APIs"); + pybind11::module_ storage = createModule(m, "stormpy.storage._storage", "Data structures in Storm"); + pybind11::module_ logic = createModule(m, "stormpy.logic._logic", "Logic module for Storm"); + pybind11::module_ utility = createModule(m, "stormpy.utility._utility", "Utilities for Storm"); + + m.attr("_core") = core; + m.attr("_storage") = storage; + m.attr("_logic") = logic; + m.attr("_utility") = utility; + + bindAll(core, storage, logic, utility, py::Phase::Declare); + bindAll(core, storage, logic, utility, py::Phase::Define); +} diff --git a/src/mod_core.cpp b/src/mod_core.cpp index 7e069428fc..7446d94985 100644 --- a/src/mod_core.cpp +++ b/src/mod_core.cpp @@ -1,6 +1,5 @@ #include -#include "src/common.h" #include "src/core/analysis.h" #include "src/core/bisimulation.h" #include "src/core/core.h" @@ -12,15 +11,11 @@ #include "src/core/result.h" #include "src/core/simulator.h" #include "src/core/transformation.h" +#include "src/module_bindings.h" -PYBIND11_MODULE(_core, m) { - m.doc() = "core"; - -#ifdef STORMPY_DISABLE_SIGNATURE_DOC - py::options options; - options.disable_function_signatures(); -#endif +namespace stormpy::bindings { +void bindCore(py::module& m) { define_environment(m); define_core(m); @@ -55,3 +50,5 @@ PYBIND11_MODULE(_core, m) { define_sparse_model_simulator(m, "Exact"); define_prism_program_simulator(m, "Double"); } + +} // namespace stormpy::bindings diff --git a/src/mod_logic.cpp b/src/mod_logic.cpp index 1f9f7294c4..e30a1acede 100644 --- a/src/mod_logic.cpp +++ b/src/mod_logic.cpp @@ -1,13 +1,10 @@ -#include "src/common.h" #include "src/logic/formulae.h" +#include "src/module_bindings.h" -PYBIND11_MODULE(_logic, m) { - m.doc() = "Logic module for Storm"; - -#ifdef STORMPY_DISABLE_SIGNATURE_DOC - py::options options; - options.disable_function_signatures(); -#endif +namespace stormpy::bindings { +void bindLogic(py::module& m) { define_formulae(m); } + +} // namespace stormpy::bindings diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 765bfdf72e..58e4871840 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -1,7 +1,7 @@ #include #include -#include "src/common.h" +#include "src/module_bindings.h" #include "src/storage/bitvector.h" #include "src/storage/choiceorigins.h" #include "src/storage/dd.h" @@ -21,17 +21,14 @@ #include "src/storage/umb.h" #include "src/storage/valuation.h" -PYBIND11_MODULE(_storage, m) { - m.doc() = "Data structures in Storm"; - -#ifdef STORMPY_DISABLE_SIGNATURE_DOC - py::options options; - options.disable_function_signatures(); -#endif +namespace stormpy::bindings { +void bindStorage(py::module& m) { define_bitvector(m); auto ddSylvan = define_dd(m, "Sylvan"); define_dd_typed(m, "Sylvan", "_Double", ddSylvan); + define_dd_typed(m, "Sylvan", "_Exact", ddSylvan); + define_dd_typed(m, "Sylvan", "_Parametric", ddSylvan); define_dd_nt(m); define_model(m); define_sparse_model(m, ""); @@ -47,6 +44,7 @@ PYBIND11_MODULE(_storage, m) { define_sparse_matrix(m, "Interval"); define_sparse_matrix(m, "RationalInterval"); define_sparse_matrix(m, "Parametric"); + define_sparse_matrix(m, "StateType"); define_sparse_matrix_nt(m); define_symbolic_model(m, "Sylvan"); define_symbolic_model(m, "SylvanExact"); @@ -76,6 +74,7 @@ PYBIND11_MODULE(_storage, m) { define_distribution(m, "Exact"); define_distribution(m, "Interval"); define_distribution(m, "RationalInterval"); + define_distribution(m, "Parametric"); define_sparse_model_components(m, ""); define_sparse_model_components(m, "Exact"); define_sparse_model_components(m, "Interval"); @@ -92,3 +91,5 @@ PYBIND11_MODULE(_storage, m) { define_maximal_end_component_decomposition(m, "_ratfunc"); define_umb(m); } + +} // namespace stormpy::bindings diff --git a/src/mod_utility.cpp b/src/mod_utility.cpp index 93d58c00b8..5442d9803a 100644 --- a/src/mod_utility.cpp +++ b/src/mod_utility.cpp @@ -1,20 +1,15 @@ #include -#include "src/common.h" +#include "src/module_bindings.h" #include "src/utility/chrono.h" #include "src/utility/json.h" #include "src/utility/kwekMehlhorn.h" #include "src/utility/shortestPaths.h" #include "src/utility/smtsolver.h" -PYBIND11_MODULE(_utility, m) { - m.doc() = "Utilities for Storm"; - -#ifdef STORMPY_DISABLE_SIGNATURE_DOC - py::options options; - options.disable_function_signatures(); -#endif +namespace stormpy::bindings { +void bindUtility(py::module& m) { define_ksp(m); define_smt(m); define_chrono(m); @@ -22,3 +17,5 @@ PYBIND11_MODULE(_utility, m) { define_json(m, "Rational"); define_kwek_mehlhorn(m, ""); } + +} // namespace stormpy::bindings diff --git a/src/module_bindings.h b/src/module_bindings.h new file mode 100644 index 0000000000..6ca0a9ae9c --- /dev/null +++ b/src/module_bindings.h @@ -0,0 +1,12 @@ +#pragma once + +#include "src/common.h" + +namespace stormpy::bindings { + +void bindCore(py::module& module); +void bindLogic(py::module& module); +void bindStorage(py::module& module); +void bindUtility(py::module& module); + +} // namespace stormpy::bindings diff --git a/src/registration.h b/src/registration.h new file mode 100644 index 0000000000..fb661da23b --- /dev/null +++ b/src/registration.h @@ -0,0 +1,138 @@ +#pragma once + +#include +#include + +namespace stormpy::registration { + +// This facade lets the existing binding functions participate in two global +// passes without duplicating their declarations. The declaration pass creates +// every Python class and enum; the definition pass looks those classes up and +// attaches methods and free functions. Binding argument expressions are still +// evaluated in both passes, so binding functions must otherwise be declarative. +using namespace pybind11; + +enum class Phase { Declare, Define }; + +class module { + public: + module(pybind11::module_ const& implementation, Phase phase) :implementation_(implementation), phase_(phase) {} + + Phase phase() const { + return phase_; + } + pybind11::module_ const& raw() const { + return implementation_; + } + + template + void def(Args&&... args) { + if (phase_ == Phase::Define) { + implementation_.def(std::forward(args)...); + } + } + + private: + pybind11::module_ implementation_; + Phase phase_; +}; + +template +class class_; + +template +Value const& unwrap(Value const& value) { + return value; +} + +template +pybind11::handle unwrap(class_ const& value); + +template +class class_ { + public: + using RawClass = pybind11::class_; + + template + class_(module const& parent, char const* name, Extra const&... extra) : implementation_(acquire(parent, name, extra...)), phase_(parent.phase()) {} + + Phase phase() const { + return phase_; + } + RawClass const& raw() const { + return implementation_; + } + +#define STORMPY_FORWARD_CLASS_METHOD(method) \ + template \ + class_& method(Args&&... args) { \ + if (phase_ == Phase::Define) { \ + implementation_.method(std::forward(args)...); \ + } \ + return *this; \ + } + + STORMPY_FORWARD_CLASS_METHOD(def) + STORMPY_FORWARD_CLASS_METHOD(def_property) + STORMPY_FORWARD_CLASS_METHOD(def_property_readonly) + STORMPY_FORWARD_CLASS_METHOD(def_readonly) + STORMPY_FORWARD_CLASS_METHOD(def_readwrite) + STORMPY_FORWARD_CLASS_METHOD(def_static) + +#undef STORMPY_FORWARD_CLASS_METHOD + + private: + template + static RawClass acquire(module const& parent, char const* name, Extra const&... extra) { + if (parent.phase() == Phase::Declare) { + return RawClass(parent.raw(), name, unwrap(extra)...); + } + // Reuse the Python type registered in the declaration pass. Constructing + // another pybind11::class_ would attempt to register the C++ type twice. + return pybind11::reinterpret_borrow(parent.raw().attr(name)); + } + + RawClass implementation_; + Phase phase_; +}; + +template +pybind11::handle unwrap(class_ const& value) { + return value.raw(); +} + +template +class native_enum { + public: + template + native_enum(Parent const& parent, char const* name, char const* nativeTypeName, char const* classDoc = "") { + if (parent.phase() == Phase::Declare) { + implementation_ = std::make_unique>(parent.raw(), name, nativeTypeName, classDoc); + } + } + + native_enum& value(char const* name, EnumType value, char const* doc = nullptr) { + if (implementation_) { + implementation_->value(name, value, doc); + } + return *this; + } + + native_enum& export_values() { + if (implementation_) { + implementation_->export_values(); + } + return *this; + } + + void finalize() { + if (implementation_) { + implementation_->finalize(); + } + } + + private: + std::unique_ptr> implementation_; +}; + +} // namespace stormpy::registration diff --git a/src/storage/dd.cpp b/src/storage/dd.cpp index 201cc4e54a..79b8453120 100644 --- a/src/storage/dd.cpp +++ b/src/storage/dd.cpp @@ -1,5 +1,7 @@ #include "dd.h" +#include +#include #include #include #include @@ -54,4 +56,8 @@ void define_dd_nt(py::module& m) { template py::class_> define_dd(py::module& m, std::string const& libstring); template void define_dd_typed(py::module&, std::string const&, std::string const&, - py::class_> const&); \ No newline at end of file + py::class_> const&); +template void define_dd_typed(py::module&, std::string const&, std::string const&, + py::class_> const&); +template void define_dd_typed(py::module&, std::string const&, std::string const&, + py::class_> const&); diff --git a/src/storage/distribution.cpp b/src/storage/distribution.cpp index d5e6b588d4..5e6aec892a 100644 --- a/src/storage/distribution.cpp +++ b/src/storage/distribution.cpp @@ -1,6 +1,7 @@ #include "distribution.h" #include +#include #include #include @@ -19,3 +20,4 @@ template void define_distribution(py::module&, std::string vt_suffix); template void define_distribution(py::module&, std::string vt_suffix); template void define_distribution(py::module&, std::string vt_suffix); template void define_distribution(py::module&, std::string vt_suffix); +template void define_distribution(py::module&, std::string vt_suffix); diff --git a/src/storage/jani.cpp b/src/storage/jani.cpp index 3e55e62c81..4fa0d87d51 100644 --- a/src/storage/jani.cpp +++ b/src/storage/jani.cpp @@ -163,8 +163,17 @@ void define_jani(py::module& m) { .def_property_readonly("is_continuous_type", &JaniType::isContinuousType) .def("__str__", &JaniType::getStringRepresentation); py::class_> basicType(m, "BasicType", "A basic type in JANI", janiType); + py::native_enum(basicType, "Type", "enum.Enum") + .value("BOOL", BasicType::Type::Bool) + .value("INT", BasicType::Type::Int) + .value("REAL", BasicType::Type::Real) + .finalize(); basicType.def_property_readonly("inner_type", &BasicType::get, "the inner type"); py::class_> boundedType(m, "BoundedType", "A bounded type in JANI", janiType); + py::native_enum(boundedType, "BaseType", "enum.Enum") + .value("INT", BoundedType::BaseType::Int) + .value("REAL", BoundedType::BaseType::Real) + .finalize(); boundedType.def_property_readonly("base_type", &BoundedType::getBaseType, "the base type") .def_property_readonly( "lower_bound", [](const BoundedType& tp) -> storm::expressions::Expression const& { return tp.getLowerBound(); }, "the lower bound") @@ -219,6 +228,15 @@ void define_jani(py::module& m) { } void define_jani_transformers(py::module& m) { + py::class_(m, "JaniLocationExpansionNewIndices") + .def_readonly("location_variable_value_map", &JaniLocationExpander::NewIndices::locationVariableValueMap) + .def_readonly("variable_domain", &JaniLocationExpander::NewIndices::variableDomain) + .def_readonly("excluded_locations_to_new_indices", &JaniLocationExpander::NewIndices::excludedLocationsToNewIndices); + + py::class_(m, "JaniLocationExpansionResult") + .def_readonly("model", &JaniLocationExpander::ReturnType::newModel) + .def_readonly("new_indices", &JaniLocationExpander::ReturnType::newIndices); + py::class_(m, "JaniLocationExpander", "A transformer for Jani expanding variables into locations") .def(py::init(), py::arg("model")) .def("transform", &JaniLocationExpander::transform, py::arg("automaton_name"), py::arg("variable_name")); diff --git a/src/storage/matrix.cpp b/src/storage/matrix.cpp index bad12bfd7c..def70eea22 100644 --- a/src/storage/matrix.cpp +++ b/src/storage/matrix.cpp @@ -4,6 +4,7 @@ #include #include #include +#include #include #include "src/helpers.h" @@ -184,3 +185,4 @@ template void define_sparse_matrix(py::module& m, std::st template void define_sparse_matrix(py::module& m, std::string const& vtSuffix); template void define_sparse_matrix(py::module& m, std::string const& vtSuffix); template void define_sparse_matrix(py::module& m, std::string const& vtSuffix); +template void define_sparse_matrix(py::module& m, std::string const& vtSuffix); diff --git a/tests/test_registration_order.py b/tests/test_registration_order.py new file mode 100644 index 0000000000..3ccb082bc2 --- /dev/null +++ b/tests/test_registration_order.py @@ -0,0 +1,61 @@ +import importlib +import inspect + +import pytest + +import stormpy + + +def test_native_modules_keep_their_public_names(): + expected_modules = { + "stormpy._core": stormpy._core, + "stormpy.storage._storage": stormpy.storage._storage, + "stormpy.logic._logic": stormpy.logic._logic, + "stormpy.utility._utility": stormpy.utility._utility, + } + + for name, module in expected_modules.items(): + assert module.__name__ == name + assert module.__spec__.name == name + assert module.__file__ == stormpy._bindings.__file__ + assert importlib.import_module(name) is module + + +@pytest.mark.parametrize( + "binding", + [ + stormpy.ExpressionManager.create_boolean, + stormpy.storage._storage._ModelBase._as_sparse_dtmc, + stormpy.storage.JaniModel.get_automaton, + stormpy.storage.PrismProgram.to_jani, + stormpy.storage.JaniLocationExpander.transform, + stormpy.storage.SchedulerChoiceParametric.get_choice, + stormpy._core._build_sparse_model_from_symbolic_description, + stormpy._core._perform_symbolic_bisimulation, + stormpy._core.make_sparse_model_builder_exact, + stormpy._core.SymbolicExactQuantitativeCheckResult.get_values, + stormpy._core.parse_properties_for_prism_program, + stormpy.utility.SmtSolver.add, + ], +) +def test_cross_module_signatures_use_python_type_names(binding): + signature = binding.__doc__.splitlines()[0] + + assert "::" not in signature + assert "stormpy." in signature + + +def test_native_callable_signatures_do_not_contain_cpp_qualified_names(): + modules = (stormpy._core, stormpy.storage._storage, stormpy.logic._logic, stormpy.utility._utility) + signature_lines = [] + + for module in modules: + for _, obj in inspect.getmembers(module): + members = inspect.getmembers(obj) if inspect.isclass(obj) else ((obj.__name__, obj),) if callable(obj) else () + for _, member in members: + doc = getattr(member, "__doc__", None) + if doc: + signature_lines.extend(line.strip() for line in doc.splitlines() if " -> " in line and not line.lstrip().startswith(":")) + + leaked_signatures = [line for line in signature_lines if "::" in line] + assert leaked_signatures == [] From 9a601e29cc20c4d7e985d56559a4bc4feccbd4f7 Mon Sep 17 00:00:00 2001 From: Linus Heck Date: Tue, 18 Aug 2026 13:04:49 +0200 Subject: [PATCH 2/2] Two phase definition for all modules --- CMakeLists.txt | 2 ++ src/gspn/gspn.cpp | 13 ++++++++ src/mod_dft.cpp | 22 +++++++++---- src/mod_gspn.cpp | 12 +++++-- src/mod_pars.cpp | 20 ++++++++---- src/mod_pomdp.cpp | 21 ++++++++---- src/pars/pla.cpp | 8 +++++ src/pycarl/mod_cln.cpp | 15 ++++++--- src/pycarl/mod_core.cpp | 12 +++++-- src/pycarl/mod_formula.cpp | 12 +++++-- src/pycarl/mod_gmp.cpp | 14 ++++++-- src/pycarl/mod_typed_formula.cpp | 20 +++++++++--- src/pycarl/typed_core/rational.cpp | 10 ++++-- src/registration.h | 13 ++++++++ tests/test_registration_order.py | 51 ++++++++++++++++++++++++------ 15 files changed, 197 insertions(+), 48 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index a3651e3f4b..9d8368ac53 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -294,6 +294,7 @@ function(stormpy_optional_module MOD_NAME DESCRIPTION) "mod_${MOD_NAME}.cpp" "${MOD_NAME}/*.cpp" "${storm-${MOD_NAME}_INCLUDE_DIR}" "storm-${MOD_NAME}") + target_compile_definitions("stormpy_${MOD_NAME}" PRIVATE STORMPY_REGISTRATION_TWO_PASS) MESSAGE(STATUS "Stormpy - Support for ${DESCRIPTION} found and included.") else() MESSAGE(WARNING "Stormpy - No support for ${DESCRIPTION}!") @@ -307,6 +308,7 @@ function(build_pycarl_module MOD_NAME OUT_DIR OUT_NAME MOD_FILE SOURCE_PATH ADDI "${MOD_FILE}" "${SOURCE_PATH}" "${carl_INCLUDE_DIR};${ADDITIONAL_INCLUDES}" "lib_carl;${ADDITIONAL_LIBS}") + target_compile_definitions(${MOD_NAME} PRIVATE STORMPY_REGISTRATION_TWO_PASS) endfunction(build_pycarl_module) function(pycarl_module MOD_NAME ADDITIONAL_INCLUDES ADDITIONAL_LIBS) build_pycarl_module("pycarl_${MOD_NAME}" diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp index d25349f899..c0b440395d 100644 --- a/src/gspn/gspn.cpp +++ b/src/gspn/gspn.cpp @@ -2,6 +2,7 @@ #include #include +#include #include #include @@ -10,6 +11,7 @@ using GSPN = storm::gspn::GSPN; using GSPNBuilder = storm::gspn::GspnBuilder; using LayoutInfo = storm::gspn::LayoutInfo; +using Marking = storm::gspn::Marking; using Place = storm::gspn::Place; using TimedTransition = storm::gspn::TimedTransition; using ImmediateTransition = storm::gspn::ImmediateTransition; @@ -29,6 +31,17 @@ void gspnToFile(GSPN const& gspn, std::string const& filepath, bool toPnpro) { } void define_gspn(py::module& m) { + py::class_(m, "Marking", "Token distribution over the places of a GSPN") + .def(py::init const&, uint_fast64_t const&>(), py::arg("number_of_places"), + py::arg("number_of_bits"), py::arg("number_of_total_bits")) + .def(py::init const&, storm::storage::BitVector const&>(), py::arg("number_of_places"), + py::arg("number_of_bits"), py::arg("bitvector")) + .def_property_readonly("number_of_places", &Marking::getNumberOfPlaces) + .def("set_number_of_tokens", &Marking::setNumberOfTokensAt, py::arg("place"), py::arg("number_of_tokens")) + .def("get_number_of_tokens", &Marking::getNumberOfTokensAt, py::arg("place")) + .def_property_readonly("bitvector", &Marking::getBitVector) + .def(py::self == py::self); + // GSPN_Builder class py::class_>(m, "GSPNBuilder", "Generalized Stochastic Petri Net Builder") .def(py::init(), "Constructor") diff --git a/src/mod_dft.cpp b/src/mod_dft.cpp index de16a5cec1..a84feb9400 100644 --- a/src/mod_dft.cpp +++ b/src/mod_dft.cpp @@ -8,14 +8,9 @@ #include "src/dft/simulator.h" #include "src/dft/transformations.h" -PYBIND11_MODULE(_dft, m) { - m.doc() = "Functionality for DFT analysis"; - -#ifdef STORMPY_DISABLE_SIGNATURE_DOC - py::options options; - options.disable_function_signatures(); -#endif +namespace { +void bindDft(py::module& m) { define_symmetries(m); // Must be before define_analysis_typed define_analysis(m); define_analysis_typed(m, "_double"); @@ -37,3 +32,16 @@ PYBIND11_MODULE(_dft, m) { define_simulator_typed(m, "_ratfunc"); define_transformations(m); } + +} // namespace + +PYBIND11_MODULE(_dft, m) { + m.doc() = "Functionality for DFT analysis"; + +#ifdef STORMPY_DISABLE_SIGNATURE_DOC + py::options options; + options.disable_function_signatures(); +#endif + + py::bindModule(m, bindDft); +} diff --git a/src/mod_gspn.cpp b/src/mod_gspn.cpp index 7ed12d22a4..67ccc27ff6 100644 --- a/src/mod_gspn.cpp +++ b/src/mod_gspn.cpp @@ -2,6 +2,15 @@ #include "src/gspn/gspn.h" #include "src/gspn/gspn_io.h" +namespace { + +void bindGspn(py::module& m) { + define_gspn(m); + define_gspn_io(m); +} + +} // namespace + PYBIND11_MODULE(_gspn, m) { m.doc() = "Support for GSPNs"; @@ -10,6 +19,5 @@ PYBIND11_MODULE(_gspn, m) { options.disable_function_signatures(); #endif - define_gspn(m); - define_gspn_io(m); + py::bindModule(m, bindGspn); } diff --git a/src/mod_pars.cpp b/src/mod_pars.cpp index 6e5c3851d4..bc05e3d623 100644 --- a/src/mod_pars.cpp +++ b/src/mod_pars.cpp @@ -3,6 +3,19 @@ #include "src/pars/pars.h" #include "src/pars/pla.h" +namespace { + +void bindPars(py::module& m) { + define_pars(m); + define_pla(m); + define_model_instantiator(m); + define_model_instantiator(m); + define_model_instantiation_checker(m); + define_model_instantiation_checker(m); +} + +} // namespace + PYBIND11_MODULE(_pars, m) { m.doc() = "Functionality for parametric analysis"; @@ -11,10 +24,5 @@ PYBIND11_MODULE(_pars, m) { options.disable_function_signatures(); #endif - define_pars(m); - define_pla(m); - define_model_instantiator(m); - define_model_instantiator(m); - define_model_instantiation_checker(m); - define_model_instantiation_checker(m); + py::bindModule(m, bindPars); } diff --git a/src/mod_pomdp.cpp b/src/mod_pomdp.cpp index 68279f38b7..e97b5e3b90 100644 --- a/src/mod_pomdp.cpp +++ b/src/mod_pomdp.cpp @@ -11,13 +11,9 @@ #include "src/pomdp/tracker.h" #include "src/pomdp/transformations.h" -PYBIND11_MODULE(_pomdp, m) { - m.doc() = "Functionality for POMDP analysis"; +namespace { -#ifdef STORMPY_DISABLE_SIGNATURE_DOC - py::options options; - options.disable_function_signatures(); -#endif +void bindPomdp(py::module& m) { define_tracker(m, "Double"); define_tracker(m, "Exact"); define_qualitative_policy_search(m, "Double"); @@ -39,3 +35,16 @@ PYBIND11_MODULE(_pomdp, m) { define_verimon_generator(m, "Double"); define_verimon_generator(m, "Exact"); } + +} // namespace + +PYBIND11_MODULE(_pomdp, m) { + m.doc() = "Functionality for POMDP analysis"; + +#ifdef STORMPY_DISABLE_SIGNATURE_DOC + py::options options; + options.disable_function_signatures(); +#endif + + py::bindModule(m, bindPomdp); +} diff --git a/src/pars/pla.cpp b/src/pars/pla.cpp index b4f6893d5b..0714b67db2 100644 --- a/src/pars/pla.cpp +++ b/src/pars/pla.cpp @@ -2,6 +2,7 @@ #include #include +#include #include #include #include @@ -96,6 +97,13 @@ std::set gatherDerivatives(storm::models::sparse::Model(m, "RegionSplitEstimateKind", "enum.Enum", "Methods for estimating region splits") + .value("DISTANCE", storm::modelchecker::RegionSplitEstimateKind::Distance) + .value("STATE_VALUE_DELTA", storm::modelchecker::RegionSplitEstimateKind::StateValueDelta) + .value("STATE_VALUE_DELTA_WEIGHTED", storm::modelchecker::RegionSplitEstimateKind::StateValueDeltaWeighted) + .value("DERIVATIVE", storm::modelchecker::RegionSplitEstimateKind::Derivative) + .finalize(); + // RegionResult py::native_enum(m, "RegionResult", "enum.Enum", "Types of region check results") .value("EXISTSSAT", storm::modelchecker::RegionResult::ExistsSat) diff --git a/src/pycarl/mod_cln.cpp b/src/pycarl/mod_cln.cpp index fb5e524bea..dfc5e3bf1b 100644 --- a/src/pycarl/mod_cln.cpp +++ b/src/pycarl/mod_cln.cpp @@ -10,11 +10,9 @@ #include "src/pycarl/typed_core/term.h" #include "src/pycarl/types.h" -PYBIND11_MODULE(_cln, m) { - m.attr("__name__") = "stormpy.pycarl.cln"; - - m.doc() = "pycarl core cln-typed data and functions"; +namespace { +void bindCln(py::module& m) { define_cln_integer(m); define_cln_rational(m); define_term(m); @@ -27,3 +25,12 @@ PYBIND11_MODULE(_cln, m) { define_interval(m); } + +} // namespace + +PYBIND11_MODULE(_cln, m) { + m.attr("__name__") = "stormpy.pycarl.cln"; + m.doc() = "pycarl core cln-typed data and functions"; + + py::bindModule(m, bindCln); +} diff --git a/src/pycarl/mod_core.cpp b/src/pycarl/mod_core.cpp index 8e9c9a165e..47e6dda7ef 100644 --- a/src/pycarl/mod_core.cpp +++ b/src/pycarl/mod_core.cpp @@ -4,14 +4,22 @@ #include "src/pycarl/core/variable.h" #include "src/pycarl/typed_core/interval.h" -PYBIND11_MODULE(_pycarl_core, m) { - m.doc() = "pycarl core untyped functions"; +namespace { +void bindCore(py::module& m) { define_variabletype(m); define_variable(m); define_monomial(m); define_boundtype(m); define_interval(m); +} + +} // namespace + +PYBIND11_MODULE(_pycarl_core, m) { + m.doc() = "pycarl core untyped functions"; + + py::bindModule(m, bindCore); py::register_exception(m, "NoPicklingSupport"); } diff --git a/src/pycarl/mod_formula.cpp b/src/pycarl/mod_formula.cpp index 569355d941..88ceff1f30 100644 --- a/src/pycarl/mod_formula.cpp +++ b/src/pycarl/mod_formula.cpp @@ -3,6 +3,15 @@ #include "src/pycarl/formula/formula_type.h" #include "src/pycarl/formula/relation.h" +namespace { + +void bindFormula(py::module& m) { + define_relation(m); + define_formula_type(m); +} + +} // namespace + PYBIND11_MODULE(_formula, m) { m.attr("__name__") = "stormpy.pycarl.formula"; m.doc() = "pycarl formula untyped functions"; @@ -10,6 +19,5 @@ PYBIND11_MODULE(_formula, m) { // Constraint relies on Rational m.import("stormpy.pycarl"); - define_relation(m); - define_formula_type(m); + py::bindModule(m, bindFormula); } diff --git a/src/pycarl/mod_gmp.cpp b/src/pycarl/mod_gmp.cpp index 0d2ffa0939..80be6c4893 100644 --- a/src/pycarl/mod_gmp.cpp +++ b/src/pycarl/mod_gmp.cpp @@ -10,10 +10,9 @@ #include "src/pycarl/typed_core/term.h" #include "src/pycarl/types.h" -PYBIND11_MODULE(_gmp, m) { - m.attr("__name__") = "stormpy.pycarl.gmp"; - m.doc() = "pycarl core gmp-typed data and functions"; +namespace { +void bindGmp(py::module& m) { define_gmp_integer(m); define_gmp_rational(m); define_term(m); @@ -26,3 +25,12 @@ PYBIND11_MODULE(_gmp, m) { define_interval(m); } + +} // namespace + +PYBIND11_MODULE(_gmp, m) { + m.attr("__name__") = "stormpy.pycarl.gmp"; + m.doc() = "pycarl core gmp-typed data and functions"; + + py::bindModule(m, bindGmp); +} diff --git a/src/pycarl/mod_typed_formula.cpp b/src/pycarl/mod_typed_formula.cpp index bc004fd088..72651a48a6 100644 --- a/src/pycarl/mod_typed_formula.cpp +++ b/src/pycarl/mod_typed_formula.cpp @@ -3,15 +3,27 @@ #include "src/pycarl/typed_formula/constraint.h" #include "src/pycarl/typed_formula/formula.h" +namespace { + +void bindTypedFormula(py::module& m) { + define_constraint(m); + define_simple_constraint(m); + define_formula(m); +} + +} // namespace + PYBIND11_MODULE(_formula, m) { - m.attr("__name__") = "stormpy.pycarl.formula"; +#ifdef PYCARL_USE_CLN + m.attr("__name__") = "stormpy.pycarl.cln.formula"; +#else + m.attr("__name__") = "stormpy.pycarl.gmp.formula"; +#endif m.doc() = "pycarl formula typed functions"; // Constraint relies on Rational m.import("stormpy.pycarl"); m.import("stormpy.pycarl.formula"); - define_constraint(m); - define_simple_constraint(m); - define_formula(m); + py::bindModule(m, bindTypedFormula); } diff --git a/src/pycarl/typed_core/rational.cpp b/src/pycarl/typed_core/rational.cpp index a9a9563e2d..b9b076a992 100644 --- a/src/pycarl/typed_core/rational.cpp +++ b/src/pycarl/typed_core/rational.cpp @@ -183,7 +183,9 @@ void define_cln_rational(py::module& m) { return h(v); }); - py::implicitly_convertible(); + if (m.phase() == py::Phase::Define) { + py::implicitly_convertible(); + } #endif } @@ -298,6 +300,8 @@ void define_gmp_rational(py::module& m) { return h(v); }); - py::implicitly_convertible(); + if (m.phase() == py::Phase::Define) { + py::implicitly_convertible(); + } #endif -} \ No newline at end of file +} diff --git a/src/registration.h b/src/registration.h index fb661da23b..a8d85519da 100644 --- a/src/registration.h +++ b/src/registration.h @@ -25,6 +25,10 @@ class module { return implementation_; } + auto attr(char const* name) const { + return implementation_.attr(name); + } + template void def(Args&&... args) { if (phase_ == Phase::Define) { @@ -37,6 +41,15 @@ class module { Phase phase_; }; +template +void bindModule(pybind11::module_ const& implementation, BindingFunction&& bind) { + module declarations(implementation, Phase::Declare); + bind(declarations); + + module definitions(implementation, Phase::Define); + bind(definitions); +} + template class class_; diff --git a/tests/test_registration_order.py b/tests/test_registration_order.py index 3ccb082bc2..779ad0636f 100644 --- a/tests/test_registration_order.py +++ b/tests/test_registration_order.py @@ -5,6 +5,24 @@ import stormpy +NATIVE_MODULE_NAMES = ( + "stormpy._core", + "stormpy.storage._storage", + "stormpy.logic._logic", + "stormpy.utility._utility", + "stormpy.dft._dft", + "stormpy.gspn._gspn", + "stormpy.pars._pars", + "stormpy.pomdp._pomdp", + "stormpy.info._info", + "stormpy.pycarl._pycarl_core", + "stormpy.pycarl.gmp._gmp", + "stormpy.pycarl.cln._cln", + "stormpy.pycarl.formula._formula", + "stormpy.pycarl.gmp.formula._formula", + "stormpy.pycarl.cln.formula._formula", +) + def test_native_modules_keep_their_public_names(): expected_modules = { @@ -45,17 +63,32 @@ def test_cross_module_signatures_use_python_type_names(binding): assert "stormpy." in signature -def test_native_callable_signatures_do_not_contain_cpp_qualified_names(): - modules = (stormpy._core, stormpy.storage._storage, stormpy.logic._logic, stormpy.utility._utility) +@pytest.mark.parametrize("module_name", NATIVE_MODULE_NAMES) +def test_native_callable_signatures_do_not_contain_cpp_qualified_names(module_name): + try: + module = importlib.import_module(module_name) + except ImportError as error: + pytest.skip(str(error)) + signature_lines = [] - for module in modules: - for _, obj in inspect.getmembers(module): - members = inspect.getmembers(obj) if inspect.isclass(obj) else ((obj.__name__, obj),) if callable(obj) else () - for _, member in members: - doc = getattr(member, "__doc__", None) - if doc: - signature_lines.extend(line.strip() for line in doc.splitlines() if " -> " in line and not line.lstrip().startswith(":")) + for _, obj in inspect.getmembers(module): + members = inspect.getmembers(obj) if inspect.isclass(obj) else ((obj.__name__, obj),) if callable(obj) else () + for _, member in members: + doc = getattr(member, "__doc__", None) + if doc: + signature_lines.extend(line.strip() for line in doc.splitlines() if " -> " in line and not line.lstrip().startswith(":")) leaked_signatures = [line for line in signature_lines if "::" in line] assert leaked_signatures == [] + + +@pytest.mark.parametrize("backend", ("gmp", "cln")) +def test_typed_pycarl_formulas_use_their_backend_module(backend): + try: + module = importlib.import_module(f"stormpy.pycarl.{backend}.formula") + except ImportError as error: + pytest.skip(str(error)) + + assert module.Formula.__module__ == module.__name__ + assert module.Constraint.__module__ == module.__name__