Towards generating good stubs: attempt at fixing C++ name leaks by first declaring, then defining

CMakeLists.txt

@@ -49,7 +49,7 @@
 
 # Helper function to print path where library was found and check whether hint was used
 function(check_hint NAME DIR_FOUND HINT_DIR FOUND_VERSION)
     # Get absolute path
     get_filename_component(PATH_FOUND ${DIR_FOUND} ABSOLUTE)
     # Print path
     if (NOT "${FOUND_VERSION}" STREQUAL "")
@@ -294,6 +294,7 @@
                              "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 @@
                  "${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}"
@@ -332,14 +334,28 @@
 
 # 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")

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

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 *

lib/stormpy/logic/__init__.py

@@ -1,2 +1,4 @@
-from . import _logic
+import stormpy
+
+_logic = stormpy._bindings._logic
 from ._logic import *

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
 

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

src/common.h

@@ -8,7 +8,12 @@
 #include <pybind11/stl.h>
 #include <tuple>
 
+#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<T>)

src/core/bisimulation.cpp

@@ -4,10 +4,11 @@
 #include <storm/models/symbolic/StandardRewardModel.h>
 
 template<storm::dd::DdType DdType, typename ValueType>
-std::shared_ptr<storm::models::Model<ValueType>> performBisimulationMinimization(
-    std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas,
-    storm::storage::BisimulationType const& bisimulationType, storm::dd::bisimulation::QuotientFormat const& quotientFormat,
-    storm::dd::bisimulation::BisimulationOptions const& bisimulationOptions) {
+std::shared_ptr<storm::models::ModelBase> performBisimulationMinimization(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model,
+                                                                          std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas,
+                                                                          storm::storage::BisimulationType const& bisimulationType,
+                                                                          storm::dd::bisimulation::QuotientFormat const& quotientFormat,
+                                                                          storm::dd::bisimulation::BisimulationOptions const& bisimulationOptions) {
     return storm::api::performBisimulationMinimization<DdType, ValueType, ValueType>(
         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<storm::dd::bisimulation::ReuseMode>(m, "BisimulationReuseMode", "enum.Enum")
+        .value("NONE", storm::dd::bisimulation::ReuseMode::None)
+        .value("BLOCK_NUMBERS", storm::dd::bisimulation::ReuseMode::BlockNumbers)
+        .finalize();
+
+    py::native_enum<storm::dd::bisimulation::RefinementMode>(m, "BisimulationRefinementMode", "enum.Enum")
+        .value("FULL", storm::dd::bisimulation::RefinementMode::Full)
+        .value("CHANGED_STATES", storm::dd::bisimulation::RefinementMode::ChangedStates)
+        .finalize();
+
+    py::native_enum<storm::dd::bisimulation::InitialPartitionMode>(m, "BisimulationInitialPartitionMode", "enum.Enum")
+        .value("REGULAR", storm::dd::bisimulation::InitialPartitionMode::Regular)
+        .value("FINER", storm::dd::bisimulation::InitialPartitionMode::Finer)
+        .finalize();
+
     py::class_<storm::dd::bisimulation::BisimulationOptions>(m, "BisimulationOptionsDd", "Options for Dd bisimulation")
         .def(py::init<>(), "Create")
         .def_readwrite("reuse_mode", &storm::dd::bisimulation::BisimulationOptions::reuseMode, "Reuse mode")

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<storm::RationalNumber>, "Construct a builder instance",
               py::arg("model_description"), py::arg("options"), py::arg("action_mask") = nullptr,
               py::arg("exploration_options") = typename storm::builder::ExplicitModelBuilder<ValueType>::Options());
+        py::class_<storm::builder::ExplicitModelBuilder<storm::RationalNumber>>(m, "ExplicitExactModelBuilder", "Model builder for exact sparse models")
+            .def("build", &storm::builder::ExplicitModelBuilder<storm::RationalNumber>::build, "Build the model", py::call_guard<py::gil_scoped_release>())
+            .def("export_lookup", &storm::builder::ExplicitModelBuilder<storm::RationalNumber>::exportExplicitStateLookup, "Export a lookup model");
     }
 }
 
@@ -242,6 +245,9 @@ void define_build(py::module& m) {
              py::arg("new_value") = true);
 
     py::class_<storm::generator::ActionMask<double>, std::shared_ptr<storm::generator::ActionMask<double>>> actionmask(m, "ActionMaskDouble");
+    py::class_<storm::generator::ActionMask<storm::RationalNumber>, std::shared_ptr<storm::generator::ActionMask<storm::RationalNumber>>>(m, "ActionMaskExact");
+    py::class_<storm::generator::ActionMask<storm::RationalFunction>, std::shared_ptr<storm::generator::ActionMask<storm::RationalFunction>>>(
+        m, "ActionMaskParametric");
     py::class_<storm::generator::StateValuationFunctionMask<double>, std::shared_ptr<storm::generator::StateValuationFunctionMask<double>>> actfuncmask(
         m, "StateValuationFunctionActionMaskDouble", actionmask);
     actfuncmask.def(py::init<std::function<bool(storm::expressions::SimpleValuation const&, uint64_t)>>(), py::arg("f"));

src/gspn/gspn.cpp

@@ -2,6 +2,7 @@
 
 #include <storm-gspn/storage/gspn/GSPN.h>
 #include <storm-gspn/storage/gspn/GspnBuilder.h>
+#include <storm-gspn/storage/gspn/Marking.h>
 #include <storm/io/file.h>
 #include <storm/settings/SettingsManager.h>
 
@@ -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<GSPN::RateType>;
 using ImmediateTransition = storm::gspn::ImmediateTransition<GSPN::WeightType>;
@@ -29,6 +31,17 @@ void gspnToFile(GSPN const& gspn, std::string const& filepath, bool toPnpro) {
 }
 
 void define_gspn(py::module& m) {
+    py::class_<Marking>(m, "Marking", "Token distribution over the places of a GSPN")
+        .def(py::init<uint_fast64_t const&, std::map<uint_fast64_t, uint_fast64_t> const&, uint_fast64_t const&>(), py::arg("number_of_places"),
+             py::arg("number_of_bits"), py::arg("number_of_total_bits"))
+        .def(py::init<uint_fast64_t const&, std::map<uint_fast64_t, uint_fast64_t> 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_<GSPNBuilder, std::shared_ptr<GSPNBuilder>>(m, "GSPNBuilder", "Generalized Stochastic Petri Net Builder")
         .def(py::init(), "Constructor")

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<pybind11::module_>();
+    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);
+}

src/mod_core.cpp

@@ -1,6 +1,5 @@
 #include <storm/adapters/IntervalAdapter.h>
 
-#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<storm::RationalNumber>(m, "Exact");
     define_prism_program_simulator<double>(m, "Double");
 }
+
+}  // namespace stormpy::bindings

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<double>(m, "_double");
@@ -37,3 +32,16 @@ PYBIND11_MODULE(_dft, m) {
     define_simulator_typed<storm::RationalFunction>(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);
+}

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);
 }

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

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<double>(m);
+    define_model_instantiator<storm::RationalFunction>(m);
+    define_model_instantiation_checker<double>(m);
+    define_model_instantiation_checker<storm::RationalNumber>(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<double>(m);
-    define_model_instantiator<storm::RationalFunction>(m);
-    define_model_instantiation_checker<double>(m);
-    define_model_instantiation_checker<storm::RationalNumber>(m);
+    py::bindModule(m, bindPars);
 }