From 16b227b85f558d9e6e6741c250b0d36a58acfe55 Mon Sep 17 00:00:00 2001
From: Linus Heck <linus.heck@ru.nl>
Date: Thu, 20 Aug 2026 10:39:43 +0200
Subject: [PATCH 1/7] Better Sphinx docs: example improvement on logic

---
 .gitignore                                  |  1 +
 doc/source/_templates/autosummary/class.rst |  9 +++
 doc/source/api/logic.rst                    | 87 +++++++++++++++++++--
 doc/source/conf.py                          | 21 +++++
 lib/stormpy/__init__.py                     |  5 +-
 5 files changed, 115 insertions(+), 8 deletions(-)
 create mode 100644 doc/source/_templates/autosummary/class.rst

diff --git a/.gitignore b/.gitignore
index 894675ce32..bffa7be344 100644
--- a/.gitignore
+++ b/.gitignore
@@ -14,3 +14,4 @@ cmake-build-debug/
 .cache/
 .DS_Store
 .venv/
+doc/source/api/generated/
diff --git a/doc/source/_templates/autosummary/class.rst b/doc/source/_templates/autosummary/class.rst
new file mode 100644
index 0000000000..e15788cd7c
--- /dev/null
+++ b/doc/source/_templates/autosummary/class.rst
@@ -0,0 +1,9 @@
+{{ fullname | escape | underline }}
+
+.. currentmodule:: {{ module }}
+
+.. autoclass:: {{ objname }}
+   :members:
+   :undoc-members:
+   :inherited-members:
+   :show-inheritance:
diff --git a/doc/source/api/logic.rst b/doc/source/api/logic.rst
index ea8ddacc3e..7a52961ab3 100644
--- a/doc/source/api/logic.rst
+++ b/doc/source/api/logic.rst
@@ -1,8 +1,83 @@
 Stormpy.logic
-**************************
+*************
 
-.. automodule:: stormpy.logic
-   :members:
-   :undoc-members:
-   :imported-members:
-   :exclude-members: deprecated
+``stormpy.logic`` contains the formula classes used to represent properties.
+The pages below show each class's inheritance hierarchy and include inherited
+members, so that the complete interface of concrete formulas is visible.
+
+Base classes
+============
+
+.. autosummary::
+   :toctree: generated/logic
+   :template: autosummary/class.rst
+
+   stormpy.logic.Formula
+   stormpy.logic.StateFormula
+   stormpy.logic.PathFormula
+   stormpy.logic.UnaryStateFormula
+   stormpy.logic.BinaryStateFormula
+   stormpy.logic.UnaryPathFormula
+   stormpy.logic.BinaryPathFormula
+
+Atomic and Boolean formulas
+===========================
+
+.. autosummary::
+   :toctree: generated/logic
+   :template: autosummary/class.rst
+
+   stormpy.logic.AtomicExpressionFormula
+   stormpy.logic.AtomicLabelFormula
+   stormpy.logic.BooleanLiteralFormula
+   stormpy.logic.UnaryBooleanStateFormula
+   stormpy.logic.BooleanBinaryStateFormula
+
+Path formulas
+=============
+
+.. autosummary::
+   :toctree: generated/logic
+   :template: autosummary/class.rst
+
+   stormpy.logic.EventuallyFormula
+   stormpy.logic.GloballyFormula
+   stormpy.logic.UntilFormula
+   stormpy.logic.BoundedUntilFormula
+   stormpy.logic.ConditionalFormula
+
+Operator formulas
+=================
+
+.. autosummary::
+   :toctree: generated/logic
+   :template: autosummary/class.rst
+
+   stormpy.logic.OperatorFormula
+   stormpy.logic.ProbabilityOperator
+   stormpy.logic.RewardOperator
+   stormpy.logic.TimeOperator
+   stormpy.logic.LongRunAvarageOperator
+   stormpy.logic.MultiObjectiveFormula
+   stormpy.logic.GameFormula
+
+Reward formulas
+===============
+
+.. autosummary::
+   :toctree: generated/logic
+   :template: autosummary/class.rst
+
+   stormpy.logic.CumulativeRewardFormula
+   stormpy.logic.InstantaneousRewardFormula
+   stormpy.logic.LongRunAverageRewardFormula
+
+Enumerations
+============
+
+.. autosummary::
+   :toctree: generated/logic
+   :template: autosummary/class.rst
+
+   stormpy.logic.ComparisonType
+   stormpy.logic.BinaryBooleanOperatorType
diff --git a/doc/source/conf.py b/doc/source/conf.py
index 4f2469cdd8..9913eca26a 100644
--- a/doc/source/conf.py
+++ b/doc/source/conf.py
@@ -4,6 +4,8 @@
 # https://www.sphinx-doc.org/en/master/usage/configuration.html
 
 # Needed for version information
+import re
+
 import stormpy
 
 # -- Project information -----------------------------------------------------
@@ -21,6 +23,7 @@
 
 extensions = [
     "sphinx.ext.autodoc",
+    "sphinx.ext.autosummary",
     "sphinx.ext.autosectionlabel",
     #'sphinx.ext.intersphinx',
     "sphinx.ext.githubpages",
@@ -33,6 +36,11 @@
 # Autodoc options
 autoclass_content = "both"  # Add documentation for both the class and __init__
 
+# Display e.g. "BitVector" instead of "stormpy.storage.BitVector"
+python_use_unqualified_type_names = True
+# Wrap long signatures instead of scrolling them
+python_maximum_signature_line_length = 100
+
 templates_path = ["_templates"]
 exclude_patterns = []
 
@@ -138,3 +146,16 @@
 myst_enable_extensions = [
     "colon_fence",
 ]
+
+# The following code makes Sphinx display e.g. "Environment()" instead of "<stormpy.Environment object at 0x10abc123>"
+_PYBIND_OBJECT_REPR = re.compile(r"<(?P<type>[A-Za-z_]\w*(?:\.[A-Za-z_]\w*)*) object(?: at 0x[0-9a-fA-F]+)?>")
+
+
+def _stabilize_pybind_signatures(app, what, name, obj, options, signature, return_annotation):
+    if signature is not None:
+        signature = _PYBIND_OBJECT_REPR.sub(lambda match: f"{match.group('type').rsplit('.', 1)[-1]}()", signature)
+    return signature, return_annotation
+
+
+def setup(app):
+    app.connect("autodoc-process-signature", _stabilize_pybind_signatures)
diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py
index c54e6d0ed8..205c3d9b20 100644
--- a/lib/stormpy/__init__.py
+++ b/lib/stormpy/__init__.py
@@ -1,10 +1,11 @@
 from ._config import *
 
-from . import _core
-from ._core import *
 from . import storage
 from .storage import *
+from . import logic
 from .logic import *
+from . import _core
+from ._core import *
 from . import exceptions
 
 from enum import Enum

From d751e8ab48f91ce2fc4a7991ec9627f6f88a314c Mon Sep 17 00:00:00 2001
From: Linus Heck <linus.heck@ru.nl>
Date: Thu, 20 Aug 2026 10:43:05 +0200
Subject: [PATCH 2/7] remove weird logic description

---
 doc/source/api/logic.rst | 2 --
 1 file changed, 2 deletions(-)

diff --git a/doc/source/api/logic.rst b/doc/source/api/logic.rst
index 7a52961ab3..040b52c8f4 100644
--- a/doc/source/api/logic.rst
+++ b/doc/source/api/logic.rst
@@ -2,8 +2,6 @@ Stormpy.logic
 *************
 
 ``stormpy.logic`` contains the formula classes used to represent properties.
-The pages below show each class's inheritance hierarchy and include inherited
-members, so that the complete interface of concrete formulas is visible.
 
 Base classes
 ============

From 85ffcc3686e710708eda72db7600e08444cf2379 Mon Sep 17 00:00:00 2001
From: Linus Heck <linus.heck@ru.nl>
Date: Thu, 20 Aug 2026 10:53:13 +0200
Subject: [PATCH 3/7] Add test testing that we forget nothing in the .rst files

---
 tests/test_api_documentation.py | 92 +++++++++++++++++++++++++++++++++
 1 file changed, 92 insertions(+)
 create mode 100644 tests/test_api_documentation.py

diff --git a/tests/test_api_documentation.py b/tests/test_api_documentation.py
new file mode 100644
index 0000000000..d21f32f978
--- /dev/null
+++ b/tests/test_api_documentation.py
@@ -0,0 +1,92 @@
+import importlib
+import inspect
+import re
+from pathlib import Path
+
+import pytest
+
+
+API_REFERENCES = {
+    "core.rst": ("stormpy",),
+    "info.rst": ("stormpy.info",),
+    "exceptions.rst": ("stormpy.exceptions",),
+    "logic.rst": ("stormpy.logic",),
+    "storage.rst": ("stormpy.storage",),
+    "utility.rst": ("stormpy.utility",),
+    "dft.rst": ("stormpy.dft",),
+    "gspn.rst": ("stormpy.gspn",),
+    "pars.rst": ("stormpy.pars",),
+    "pomdp.rst": ("stormpy.pomdp",),
+    "pycarl/core.rst": ("stormpy.pycarl", "stormpy.pycarl.gmp", "stormpy.pycarl.cln"),
+    "pycarl/convert.rst": ("stormpy.pycarl.convert",),
+    "pycarl/formula.rst": ("stormpy.pycarl.formula", "stormpy.pycarl.gmp.formula", "stormpy.pycarl.cln.formula"),
+    "pycarl/parse.rst": ("stormpy.pycarl.parse", "stormpy.pycarl.gmp.parse", "stormpy.pycarl.cln.parse"),
+}
+
+
+def _api_root():
+    return Path(__file__).parents[1] / "doc" / "source" / "api"
+
+
+def test_all_api_reference_files_are_checked():
+    api_root = _api_root()
+    if not api_root.exists():
+        pytest.skip("source documentation is not part of the wheel test bundle")
+    reference_files = {
+        str(path.relative_to(api_root))
+        for path in api_root.rglob("*.rst")
+        if "generated" not in path.parts
+    }
+    assert reference_files == set(API_REFERENCES), (
+        f"API reference test manifest is out of sync. "
+        f"Missing: {sorted(reference_files - set(API_REFERENCES))}; "
+        f"stale: {sorted(set(API_REFERENCES) - reference_files)}"
+    )
+
+
+def _public_types(module_name):
+    module = importlib.import_module(module_name)
+    result = set()
+    for name, value in vars(module).items():
+        if name.startswith("_") or not inspect.isclass(value):
+            continue
+        owner = value.__module__
+        if module_name == "stormpy":
+            # The top-level package re-exports types documented by its submodules.
+            # Only types implemented directly in stormpy or stormpy._core belong
+            # to the core reference.
+            if owner == module_name or owner.startswith("stormpy._"):
+                result.add(name)
+        elif owner == module_name or owner.startswith(module_name + "."):
+            result.add(name)
+    return result
+
+
+@pytest.mark.parametrize(("reference_name", "module_names"), API_REFERENCES.items())
+def test_all_public_types_are_in_api_reference(reference_name, module_names):
+    """Keep curated API indices in sync with the types exported by their modules."""
+    reference = _api_root() / reference_name
+    if not reference.exists():
+        pytest.skip("source documentation is not part of the wheel test bundle")
+    reference_text = reference.read_text()
+
+    for module_name in module_names:
+        documented_types = set(
+            re.findall(rf"^\s+{re.escape(module_name)}\.([A-Za-z]\w*)\s*$", reference_text, flags=re.MULTILINE)
+        )
+
+        # An automodule directive discovers members dynamically. Once a module
+        # is converted to a curated autosummary, require an exhaustive list.
+        if not documented_types and re.search(rf"^\.\. automodule::\s+{re.escape(module_name)}\s*$", reference_text, flags=re.MULTILINE):
+            continue
+
+        try:
+            public_types = _public_types(module_name)
+        except ImportError as error:
+            pytest.skip(f"optional module {module_name} is unavailable: {error}")
+        missing_types = public_types - documented_types
+        stale_types = documented_types - public_types
+        assert not missing_types and not stale_types, (
+            f"API reference for {module_name} is out of sync. "
+            f"Missing: {sorted(missing_types)}; stale: {sorted(stale_types)}"
+        )

From e66087302ecdf1e089dff674829234154860c847 Mon Sep 17 00:00:00 2001
From: Linus Heck <linus.heck@ru.nl>
Date: Thu, 20 Aug 2026 10:55:18 +0200
Subject: [PATCH 4/7] Sidebar shows only class name

---
 doc/source/_templates/autosummary/class.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/source/_templates/autosummary/class.rst b/doc/source/_templates/autosummary/class.rst
index e15788cd7c..28572371a9 100644
--- a/doc/source/_templates/autosummary/class.rst
+++ b/doc/source/_templates/autosummary/class.rst
@@ -1,4 +1,4 @@
-{{ fullname | escape | underline }}
+{{ objname | escape | underline }}
 
 .. currentmodule:: {{ module }}
 

From 38cc008eb792a8cbba94314d019253b84bde315f Mon Sep 17 00:00:00 2001
From: Linus Heck <linus.heck@ru.nl>
Date: Thu, 20 Aug 2026 11:21:41 +0200
Subject: [PATCH 5/7] fix format

---
 tests/test_api_documentation.py | 14 +++-----------
 1 file changed, 3 insertions(+), 11 deletions(-)

diff --git a/tests/test_api_documentation.py b/tests/test_api_documentation.py
index d21f32f978..586220fb26 100644
--- a/tests/test_api_documentation.py
+++ b/tests/test_api_documentation.py
@@ -5,7 +5,6 @@
 
 import pytest
 
-
 API_REFERENCES = {
     "core.rst": ("stormpy",),
     "info.rst": ("stormpy.info",),
@@ -32,11 +31,7 @@ def test_all_api_reference_files_are_checked():
     api_root = _api_root()
     if not api_root.exists():
         pytest.skip("source documentation is not part of the wheel test bundle")
-    reference_files = {
-        str(path.relative_to(api_root))
-        for path in api_root.rglob("*.rst")
-        if "generated" not in path.parts
-    }
+    reference_files = {str(path.relative_to(api_root)) for path in api_root.rglob("*.rst") if "generated" not in path.parts}
     assert reference_files == set(API_REFERENCES), (
         f"API reference test manifest is out of sync. "
         f"Missing: {sorted(reference_files - set(API_REFERENCES))}; "
@@ -71,9 +66,7 @@ def test_all_public_types_are_in_api_reference(reference_name, module_names):
     reference_text = reference.read_text()
 
     for module_name in module_names:
-        documented_types = set(
-            re.findall(rf"^\s+{re.escape(module_name)}\.([A-Za-z]\w*)\s*$", reference_text, flags=re.MULTILINE)
-        )
+        documented_types = set(re.findall(rf"^\s+{re.escape(module_name)}\.([A-Za-z]\w*)\s*$", reference_text, flags=re.MULTILINE))
 
         # An automodule directive discovers members dynamically. Once a module
         # is converted to a curated autosummary, require an exhaustive list.
@@ -87,6 +80,5 @@ def test_all_public_types_are_in_api_reference(reference_name, module_names):
         missing_types = public_types - documented_types
         stale_types = documented_types - public_types
         assert not missing_types and not stale_types, (
-            f"API reference for {module_name} is out of sync. "
-            f"Missing: {sorted(missing_types)}; stale: {sorted(stale_types)}"
+            f"API reference for {module_name} is out of sync. " f"Missing: {sorted(missing_types)}; stale: {sorted(stale_types)}"
         )

From 61c9fad16d3da77196deef6b81d02562cd6ddeae Mon Sep 17 00:00:00 2001
From: Linus Heck <linus.heck@ru.nl>
Date: Fri, 21 Aug 2026 13:42:19 +0200
Subject: [PATCH 6/7] Autogenerate lists and separate pages for all of strompy

---
 doc/source/_templates/autosummary/module.rst | 57 +++++++++++++
 doc/source/api.md                            | 34 ++++----
 doc/source/api/core.rst                      |  8 --
 doc/source/api/dft.rst                       |  8 --
 doc/source/api/exceptions.rst                |  8 --
 doc/source/api/gspn.rst                      |  8 --
 doc/source/api/info.rst                      |  8 --
 doc/source/api/logic.rst                     | 81 -------------------
 doc/source/api/pars.rst                      |  8 --
 doc/source/api/pomdp.rst                     |  7 --
 doc/source/api/storage.rst                   |  8 --
 doc/source/api/utility.rst                   |  8 --
 doc/source/conf.py                           | 48 +++++++----
 tests/test_api_documentation.py              | 84 --------------------
 14 files changed, 108 insertions(+), 267 deletions(-)
 create mode 100644 doc/source/_templates/autosummary/module.rst
 delete mode 100644 doc/source/api/core.rst
 delete mode 100644 doc/source/api/dft.rst
 delete mode 100644 doc/source/api/exceptions.rst
 delete mode 100644 doc/source/api/gspn.rst
 delete mode 100644 doc/source/api/info.rst
 delete mode 100644 doc/source/api/logic.rst
 delete mode 100644 doc/source/api/pars.rst
 delete mode 100644 doc/source/api/pomdp.rst
 delete mode 100644 doc/source/api/storage.rst
 delete mode 100644 doc/source/api/utility.rst
 delete mode 100644 tests/test_api_documentation.py

diff --git a/doc/source/_templates/autosummary/module.rst b/doc/source/_templates/autosummary/module.rst
new file mode 100644
index 0000000000..ff78ddf561
--- /dev/null
+++ b/doc/source/_templates/autosummary/module.rst
@@ -0,0 +1,57 @@
+{#- Only list the members that belong to this module (see filter_api_members in conf.py) -#}
+{%- set attributes = filter_api_members(fullname, attributes) -%}
+{%- set functions = filter_api_members(fullname, functions) -%}
+{%- set classes = filter_api_members(fullname, classes) -%}
+{%- set exceptions = filter_api_members(fullname, exceptions) -%}
+{{ fullname | escape | underline}}
+
+.. automodule:: {{ fullname }}
+
+   {% block attributes %}
+   {%- if attributes %}
+   .. rubric:: {{ _('Module Attributes') }}
+
+   .. autosummary::
+      :toctree:
+   {% for item in attributes %}
+      {{ item }}
+   {%- endfor %}
+   {% endif %}
+   {%- endblock %}
+
+   {%- block functions %}
+   {%- if functions %}
+   .. rubric:: {{ _('Functions') }}
+
+   .. autosummary::
+      :toctree:
+   {% for item in functions %}
+      {{ item }}
+   {%- endfor %}
+   {% endif %}
+   {%- endblock %}
+
+   {%- block classes %}
+   {%- if classes %}
+   .. rubric:: {{ _('Classes') }}
+
+   .. autosummary::
+      :toctree:
+      :template: autosummary/class.rst
+   {% for item in classes %}
+      {{ item }}
+   {%- endfor %}
+   {% endif %}
+   {%- endblock %}
+
+   {%- block exceptions %}
+   {%- if exceptions %}
+   .. rubric:: {{ _('Exceptions') }}
+
+   .. autosummary::
+      :toctree:
+   {% for item in exceptions %}
+      {{ item }}
+   {%- endfor %}
+   {% endif %}
+   {%- endblock %}
diff --git a/doc/source/api.md b/doc/source/api.md
index b1cbb3b4ed..943d94c723 100644
--- a/doc/source/api.md
+++ b/doc/source/api.md
@@ -2,24 +2,30 @@
 
 Work in progress!
 
-:::{toctree}
-:maxdepth: 2
-:caption: Stormpy modules:
+```{eval-rst}
+.. autosummary::
+   :toctree: api/generated
+   :template: autosummary/module.rst
+   :caption: Stormpy modules:
 
-api/core
-api/info
-api/exceptions
-api/logic
-api/storage
-api/utility
+   stormpy
+   stormpy.storage
+   stormpy.logic
+   stormpy.dft
+   stormpy.gspn
+   stormpy.pars
+   stormpy.pomdp
+   stormpy.info
+   stormpy.exceptions
+   stormpy.utility
+```
 
-api/dft
-api/gspn
-api/pars
-api/pomdp
+:::{toctree}
+:maxdepth: 2
+:caption: Pycarl modules:
 
 api/pycarl/core
 api/pycarl/convert
 api/pycarl/formula
 api/pycarl/parse
-:::
\ No newline at end of file
+:::
diff --git a/doc/source/api/core.rst b/doc/source/api/core.rst
deleted file mode 100644
index 862d19ee42..0000000000
--- a/doc/source/api/core.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-Stormpy.core
-**************************
-
-.. automodule:: stormpy
-   :members:
-   :undoc-members:
-   :imported-members:
-   :exclude-members: deprecated
diff --git a/doc/source/api/dft.rst b/doc/source/api/dft.rst
deleted file mode 100644
index 1d2ab641df..0000000000
--- a/doc/source/api/dft.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-Stormpy.dft
-**************************
-
-.. automodule:: stormpy.dft
-   :members:
-   :undoc-members:
-   :imported-members:
-   :exclude-members: deprecated
diff --git a/doc/source/api/exceptions.rst b/doc/source/api/exceptions.rst
deleted file mode 100644
index ff37137a5a..0000000000
--- a/doc/source/api/exceptions.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-Stormpy.exceptions
-**************************
-
-.. automodule:: stormpy.exceptions
-   :members:
-   :undoc-members:
-   :imported-members:
-   :exclude-members: deprecated
diff --git a/doc/source/api/gspn.rst b/doc/source/api/gspn.rst
deleted file mode 100644
index f5317da559..0000000000
--- a/doc/source/api/gspn.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-Stormpy.gspn
-**************************
-
-.. automodule:: stormpy.gspn
-   :members:
-   :undoc-members:
-   :imported-members:
-   :exclude-members: deprecated
diff --git a/doc/source/api/info.rst b/doc/source/api/info.rst
deleted file mode 100644
index d7a6409fcd..0000000000
--- a/doc/source/api/info.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-Stormpy.info
-**************************
-
-.. automodule:: stormpy.info
-   :members:
-   :undoc-members:
-   :imported-members:
-   :exclude-members: deprecated
diff --git a/doc/source/api/logic.rst b/doc/source/api/logic.rst
deleted file mode 100644
index 040b52c8f4..0000000000
--- a/doc/source/api/logic.rst
+++ /dev/null
@@ -1,81 +0,0 @@
-Stormpy.logic
-*************
-
-``stormpy.logic`` contains the formula classes used to represent properties.
-
-Base classes
-============
-
-.. autosummary::
-   :toctree: generated/logic
-   :template: autosummary/class.rst
-
-   stormpy.logic.Formula
-   stormpy.logic.StateFormula
-   stormpy.logic.PathFormula
-   stormpy.logic.UnaryStateFormula
-   stormpy.logic.BinaryStateFormula
-   stormpy.logic.UnaryPathFormula
-   stormpy.logic.BinaryPathFormula
-
-Atomic and Boolean formulas
-===========================
-
-.. autosummary::
-   :toctree: generated/logic
-   :template: autosummary/class.rst
-
-   stormpy.logic.AtomicExpressionFormula
-   stormpy.logic.AtomicLabelFormula
-   stormpy.logic.BooleanLiteralFormula
-   stormpy.logic.UnaryBooleanStateFormula
-   stormpy.logic.BooleanBinaryStateFormula
-
-Path formulas
-=============
-
-.. autosummary::
-   :toctree: generated/logic
-   :template: autosummary/class.rst
-
-   stormpy.logic.EventuallyFormula
-   stormpy.logic.GloballyFormula
-   stormpy.logic.UntilFormula
-   stormpy.logic.BoundedUntilFormula
-   stormpy.logic.ConditionalFormula
-
-Operator formulas
-=================
-
-.. autosummary::
-   :toctree: generated/logic
-   :template: autosummary/class.rst
-
-   stormpy.logic.OperatorFormula
-   stormpy.logic.ProbabilityOperator
-   stormpy.logic.RewardOperator
-   stormpy.logic.TimeOperator
-   stormpy.logic.LongRunAvarageOperator
-   stormpy.logic.MultiObjectiveFormula
-   stormpy.logic.GameFormula
-
-Reward formulas
-===============
-
-.. autosummary::
-   :toctree: generated/logic
-   :template: autosummary/class.rst
-
-   stormpy.logic.CumulativeRewardFormula
-   stormpy.logic.InstantaneousRewardFormula
-   stormpy.logic.LongRunAverageRewardFormula
-
-Enumerations
-============
-
-.. autosummary::
-   :toctree: generated/logic
-   :template: autosummary/class.rst
-
-   stormpy.logic.ComparisonType
-   stormpy.logic.BinaryBooleanOperatorType
diff --git a/doc/source/api/pars.rst b/doc/source/api/pars.rst
deleted file mode 100644
index c0954de512..0000000000
--- a/doc/source/api/pars.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-Stormpy.pars
-**************************
-
-.. automodule:: stormpy.pars
-   :members:
-   :undoc-members:
-   :imported-members:
-   :exclude-members: deprecated
diff --git a/doc/source/api/pomdp.rst b/doc/source/api/pomdp.rst
deleted file mode 100644
index e8eb8cae36..0000000000
--- a/doc/source/api/pomdp.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-Stormpy.pomdp
-**************************
-
-.. automodule:: stormpy.pomdp
-   :members:
-   :undoc-members:
-   :imported-members:
diff --git a/doc/source/api/storage.rst b/doc/source/api/storage.rst
deleted file mode 100644
index f794517a03..0000000000
--- a/doc/source/api/storage.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-Stormpy.storage
-**************************
-
-.. automodule:: stormpy.storage
-   :members:
-   :undoc-members:
-   :imported-members:
-   :exclude-members: deprecated
diff --git a/doc/source/api/utility.rst b/doc/source/api/utility.rst
deleted file mode 100644
index 051cbdb1b7..0000000000
--- a/doc/source/api/utility.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-Stormpy.utility
-**************************
-
-.. automodule:: stormpy.utility
-   :members:
-   :undoc-members:
-   :imported-members:
-   :exclude-members: deprecated
diff --git a/doc/source/conf.py b/doc/source/conf.py
index 9913eca26a..3ac3862d08 100644
--- a/doc/source/conf.py
+++ b/doc/source/conf.py
@@ -4,8 +4,6 @@
 # https://www.sphinx-doc.org/en/master/usage/configuration.html
 
 # Needed for version information
-import re
-
 import stormpy
 
 # -- Project information -----------------------------------------------------
@@ -36,8 +34,37 @@
 # Autodoc options
 autoclass_content = "both"  # Add documentation for both the class and __init__
 
-# Display e.g. "BitVector" instead of "stormpy.storage.BitVector"
-python_use_unqualified_type_names = True
+# Autosummary options
+# Also list members that are re-exported (e.g. classes defined in the
+# compiled _logic module and imported into stormpy.logic)
+autosummary_imported_members = True
+
+# Modules whose members make up the core API of stormpy: the top-level package
+# itself (lib/stormpy/__init__.py) and the compiled _core extension module,
+# whose members are re-exported in the top-level namespace.
+_CORE_MODULES = frozenset({"stormpy", "stormpy._core"})
+
+
+def _filter_api_members(module, members):
+    """
+    Filter the members listed on the autosummary page of a module.
+
+    The top-level stormpy package also re-exports the members of several
+    submodules (e.g. storage and logic). To document every member only on the
+    page of the module it belongs to, the page of the top-level stormpy module
+    (the core API) only lists members defined in stormpy itself or in the
+    _core extension module. All other module pages list all members.
+    """
+    if module != "stormpy":
+        return members
+    return [name for name in members if getattr(getattr(stormpy, name, None), "__module__", None) in _CORE_MODULES]
+
+
+# Variables (and callables) available in autosummary templates
+autosummary_context = {
+    "filter_api_members": _filter_api_members,
+}
+
 # Wrap long signatures instead of scrolling them
 python_maximum_signature_line_length = 100
 
@@ -146,16 +173,3 @@
 myst_enable_extensions = [
     "colon_fence",
 ]
-
-# The following code makes Sphinx display e.g. "Environment()" instead of "<stormpy.Environment object at 0x10abc123>"
-_PYBIND_OBJECT_REPR = re.compile(r"<(?P<type>[A-Za-z_]\w*(?:\.[A-Za-z_]\w*)*) object(?: at 0x[0-9a-fA-F]+)?>")
-
-
-def _stabilize_pybind_signatures(app, what, name, obj, options, signature, return_annotation):
-    if signature is not None:
-        signature = _PYBIND_OBJECT_REPR.sub(lambda match: f"{match.group('type').rsplit('.', 1)[-1]}()", signature)
-    return signature, return_annotation
-
-
-def setup(app):
-    app.connect("autodoc-process-signature", _stabilize_pybind_signatures)
diff --git a/tests/test_api_documentation.py b/tests/test_api_documentation.py
deleted file mode 100644
index 586220fb26..0000000000
--- a/tests/test_api_documentation.py
+++ /dev/null
@@ -1,84 +0,0 @@
-import importlib
-import inspect
-import re
-from pathlib import Path
-
-import pytest
-
-API_REFERENCES = {
-    "core.rst": ("stormpy",),
-    "info.rst": ("stormpy.info",),
-    "exceptions.rst": ("stormpy.exceptions",),
-    "logic.rst": ("stormpy.logic",),
-    "storage.rst": ("stormpy.storage",),
-    "utility.rst": ("stormpy.utility",),
-    "dft.rst": ("stormpy.dft",),
-    "gspn.rst": ("stormpy.gspn",),
-    "pars.rst": ("stormpy.pars",),
-    "pomdp.rst": ("stormpy.pomdp",),
-    "pycarl/core.rst": ("stormpy.pycarl", "stormpy.pycarl.gmp", "stormpy.pycarl.cln"),
-    "pycarl/convert.rst": ("stormpy.pycarl.convert",),
-    "pycarl/formula.rst": ("stormpy.pycarl.formula", "stormpy.pycarl.gmp.formula", "stormpy.pycarl.cln.formula"),
-    "pycarl/parse.rst": ("stormpy.pycarl.parse", "stormpy.pycarl.gmp.parse", "stormpy.pycarl.cln.parse"),
-}
-
-
-def _api_root():
-    return Path(__file__).parents[1] / "doc" / "source" / "api"
-
-
-def test_all_api_reference_files_are_checked():
-    api_root = _api_root()
-    if not api_root.exists():
-        pytest.skip("source documentation is not part of the wheel test bundle")
-    reference_files = {str(path.relative_to(api_root)) for path in api_root.rglob("*.rst") if "generated" not in path.parts}
-    assert reference_files == set(API_REFERENCES), (
-        f"API reference test manifest is out of sync. "
-        f"Missing: {sorted(reference_files - set(API_REFERENCES))}; "
-        f"stale: {sorted(set(API_REFERENCES) - reference_files)}"
-    )
-
-
-def _public_types(module_name):
-    module = importlib.import_module(module_name)
-    result = set()
-    for name, value in vars(module).items():
-        if name.startswith("_") or not inspect.isclass(value):
-            continue
-        owner = value.__module__
-        if module_name == "stormpy":
-            # The top-level package re-exports types documented by its submodules.
-            # Only types implemented directly in stormpy or stormpy._core belong
-            # to the core reference.
-            if owner == module_name or owner.startswith("stormpy._"):
-                result.add(name)
-        elif owner == module_name or owner.startswith(module_name + "."):
-            result.add(name)
-    return result
-
-
-@pytest.mark.parametrize(("reference_name", "module_names"), API_REFERENCES.items())
-def test_all_public_types_are_in_api_reference(reference_name, module_names):
-    """Keep curated API indices in sync with the types exported by their modules."""
-    reference = _api_root() / reference_name
-    if not reference.exists():
-        pytest.skip("source documentation is not part of the wheel test bundle")
-    reference_text = reference.read_text()
-
-    for module_name in module_names:
-        documented_types = set(re.findall(rf"^\s+{re.escape(module_name)}\.([A-Za-z]\w*)\s*$", reference_text, flags=re.MULTILINE))
-
-        # An automodule directive discovers members dynamically. Once a module
-        # is converted to a curated autosummary, require an exhaustive list.
-        if not documented_types and re.search(rf"^\.\. automodule::\s+{re.escape(module_name)}\s*$", reference_text, flags=re.MULTILINE):
-            continue
-
-        try:
-            public_types = _public_types(module_name)
-        except ImportError as error:
-            pytest.skip(f"optional module {module_name} is unavailable: {error}")
-        missing_types = public_types - documented_types
-        stale_types = documented_types - public_types
-        assert not missing_types and not stale_types, (
-            f"API reference for {module_name} is out of sync. " f"Missing: {sorted(missing_types)}; stale: {sorted(stale_types)}"
-        )

From 45f7f5af60090ca84250e9ddd25d04d46821a785 Mon Sep 17 00:00:00 2001
From: Linus Heck <linus.heck@ru.nl>
Date: Fri, 21 Aug 2026 13:56:57 +0200
Subject: [PATCH 7/7] Also do this for pycarl

---
 .../_templates/autosummary/function.rst       |  5 +++
 doc/source/_templates/autosummary/module.rst  |  1 +
 doc/source/api.md                             | 22 +++++++----
 doc/source/api/pycarl/convert.rst             | 12 ------
 doc/source/api/pycarl/core.rst                | 30 ---------------
 doc/source/api/pycarl/formula.rst             | 30 ---------------
 doc/source/api/pycarl/parse.rst               | 30 ---------------
 doc/source/conf.py                            | 37 +++++++++++++------
 8 files changed, 46 insertions(+), 121 deletions(-)
 create mode 100644 doc/source/_templates/autosummary/function.rst
 delete mode 100644 doc/source/api/pycarl/convert.rst
 delete mode 100644 doc/source/api/pycarl/core.rst
 delete mode 100644 doc/source/api/pycarl/formula.rst
 delete mode 100644 doc/source/api/pycarl/parse.rst

diff --git a/doc/source/_templates/autosummary/function.rst b/doc/source/_templates/autosummary/function.rst
new file mode 100644
index 0000000000..3fe9858d79
--- /dev/null
+++ b/doc/source/_templates/autosummary/function.rst
@@ -0,0 +1,5 @@
+{{ objname | escape | underline }}
+
+.. currentmodule:: {{ module }}
+
+.. auto{{ objtype }}:: {{ objname }}
diff --git a/doc/source/_templates/autosummary/module.rst b/doc/source/_templates/autosummary/module.rst
index ff78ddf561..1db6de2679 100644
--- a/doc/source/_templates/autosummary/module.rst
+++ b/doc/source/_templates/autosummary/module.rst
@@ -50,6 +50,7 @@
 
    .. autosummary::
       :toctree:
+      :template: autosummary/class.rst
    {% for item in exceptions %}
       {{ item }}
    {%- endfor %}
diff --git a/doc/source/api.md b/doc/source/api.md
index 943d94c723..5d47201794 100644
--- a/doc/source/api.md
+++ b/doc/source/api.md
@@ -20,12 +20,18 @@ Work in progress!
    stormpy.utility
 ```
 
-:::{toctree}
-:maxdepth: 2
-:caption: Pycarl modules:
+```{eval-rst}
+.. autosummary::
+   :toctree: api/generated
+   :template: autosummary/module.rst
+   :caption: Pycarl modules:
 
-api/pycarl/core
-api/pycarl/convert
-api/pycarl/formula
-api/pycarl/parse
-:::
+   stormpy.pycarl
+   stormpy.pycarl.gmp
+   stormpy.pycarl.cln
+   stormpy.pycarl.formula
+   stormpy.pycarl.gmp.formula
+   stormpy.pycarl.cln.formula
+   stormpy.pycarl.parse
+   stormpy.pycarl.convert
+```
diff --git a/doc/source/api/pycarl/convert.rst b/doc/source/api/pycarl/convert.rst
deleted file mode 100644
index 0588011288..0000000000
--- a/doc/source/api/pycarl/convert.rst
+++ /dev/null
@@ -1,12 +0,0 @@
-Pycarl convert
-**************************
-
-
-Number conversion
----------------------------
-
-.. automodule:: stormpy.pycarl.convert
-   :members:
-   :undoc-members:
-   :imported-members:
-   :exclude-members: deprecated
diff --git a/doc/source/api/pycarl/core.rst b/doc/source/api/pycarl/core.rst
deleted file mode 100644
index d3a2ad954b..0000000000
--- a/doc/source/api/pycarl/core.rst
+++ /dev/null
@@ -1,30 +0,0 @@
-Pycarl core
-**************************
-
-
-Number independent types
----------------------------
-
-.. automodule:: stormpy.pycarl
-   :members:
-   :undoc-members:
-   :imported-members:
-   :exclude-members: deprecated
-
-Number dependent types (gmp)
-------------------------------
-
-.. automodule:: stormpy.pycarl.gmp
-   :members:
-   :undoc-members:
-   :imported-members:
-   :exclude-members: deprecated
-
-Number dependent types (cln)
-------------------------------
-
-.. automodule:: stormpy.pycarl.cln
-   :members:
-   :undoc-members:
-   :imported-members:
-   :exclude-members: deprecated
diff --git a/doc/source/api/pycarl/formula.rst b/doc/source/api/pycarl/formula.rst
deleted file mode 100644
index 44e1cd46cc..0000000000
--- a/doc/source/api/pycarl/formula.rst
+++ /dev/null
@@ -1,30 +0,0 @@
-Pycarl formula
-**************************
-
-
-Number independent types
----------------------------
-
-.. automodule:: stormpy.pycarl.formula
-   :members:
-   :undoc-members:
-   :imported-members:
-   :exclude-members: deprecated
-
-Number dependent types (gmp)
-------------------------------
-
-.. automodule:: stormpy.pycarl.gmp.formula
-   :members:
-   :undoc-members:
-   :imported-members:
-   :exclude-members: deprecated
-
-Number dependent types (cln)
-------------------------------
-
-.. automodule:: stormpy.pycarl.cln.formula
-   :members:
-   :undoc-members:
-   :imported-members:
-   :exclude-members: deprecated
diff --git a/doc/source/api/pycarl/parse.rst b/doc/source/api/pycarl/parse.rst
deleted file mode 100644
index 9076e6f9dc..0000000000
--- a/doc/source/api/pycarl/parse.rst
+++ /dev/null
@@ -1,30 +0,0 @@
-Pycarl parse
-**************************
-
-
-Number independent types
----------------------------
-
-.. automodule:: stormpy.pycarl.parse
-   :members:
-   :undoc-members:
-   :imported-members:
-   :exclude-members: deprecated
-
-Number dependent types (gmp)
-------------------------------
-
-.. automodule:: stormpy.pycarl.gmp.parse
-   :members:
-   :undoc-members:
-   :imported-members:
-   :exclude-members: deprecated
-
-Number dependent types (cln)
-------------------------------
-
-.. automodule:: stormpy.pycarl.cln.parse
-   :members:
-   :undoc-members:
-   :imported-members:
-   :exclude-members: deprecated
diff --git a/doc/source/conf.py b/doc/source/conf.py
index 3ac3862d08..255d43c68a 100644
--- a/doc/source/conf.py
+++ b/doc/source/conf.py
@@ -4,6 +4,8 @@
 # https://www.sphinx-doc.org/en/master/usage/configuration.html
 
 # Needed for version information
+import sys
+
 import stormpy
 
 # -- Project information -----------------------------------------------------
@@ -39,25 +41,38 @@
 # compiled _logic module and imported into stormpy.logic)
 autosummary_imported_members = True
 
-# Modules whose members make up the core API of stormpy: the top-level package
-# itself (lib/stormpy/__init__.py) and the compiled _core extension module,
-# whose members are re-exported in the top-level namespace.
-_CORE_MODULES = frozenset({"stormpy", "stormpy._core"})
+# For modules that re-export members of other modules: the members that should
+# be listed on the module's autosummary page, identified by their __module__.
+# All other module pages list all their members.
+_MEMBER_MODULES = {
+    # The top-level stormpy package also re-exports the members of several
+    # submodules (e.g. storage and logic). Its page (the core API) only lists
+    # the members defined in stormpy itself or in the compiled _core extension.
+    "stormpy": {"stormpy", "stormpy._core"},
+    # The number-independent core types live in the compiled _pycarl_core module.
+    "stormpy.pycarl": {"stormpy.pycarl", "stormpy.pycarl._pycarl_core"},
+    # The number-dependent formula types are bound under the shared formula module.
+    "stormpy.pycarl.gmp.formula": {"stormpy.pycarl.formula"},
+    "stormpy.pycarl.cln.formula": {"stormpy.pycarl.formula"},
+    # Utility modules re-export pycarl helpers.
+    "stormpy.pycarl.convert": {"stormpy.pycarl.convert"},
+    "stormpy.pycarl.parse": {"stormpy.pycarl.parse"},
+}
 
 
 def _filter_api_members(module, members):
     """
     Filter the members listed on the autosummary page of a module.
 
-    The top-level stormpy package also re-exports the members of several
-    submodules (e.g. storage and logic). To document every member only on the
-    page of the module it belongs to, the page of the top-level stormpy module
-    (the core API) only lists members defined in stormpy itself or in the
-    _core extension module. All other module pages list all members.
+    To document every member only on the page of the module it belongs to,
+    the pages of the modules in _MEMBER_MODULES (which re-export members of
+    other modules) only list the members defined in the given modules.
     """
-    if module != "stormpy":
+    accepted = _MEMBER_MODULES.get(module)
+    if accepted is None:
         return members
-    return [name for name in members if getattr(getattr(stormpy, name, None), "__module__", None) in _CORE_MODULES]
+    module_obj = sys.modules[module]
+    return [name for name in members if getattr(getattr(module_obj, name, None), "__module__", None) in accepted]
 
 
 # Variables (and callables) available in autosummary templates