Skip to content

Commit 8b6cd91

Browse files
Kiguliclaude
Kiguli
and
claude
committed
Add Sphinx documentation site with Furo theme and GitHub Pages deployment
Comprehensive docs covering installation (tabbed for Ubuntu/macOS/Docker), quick start guide, user guide (configuration, synthesis, I/O, makefiles), manual C++ API reference (MDP, IMDP, GPU synthesis, IO utilities), example walkthroughs grouped by specification type, and citation info. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
1 parent 1228824 commit 8b6cd91

25 files changed

+2306
-0
lines changed

‎.github/workflows/docs.yml‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
name: Deploy Documentation
2+
3+
on:
4+
push:
5+
branches: [main]
6+
paths:
7+
- 'docs/**'
8+
workflow_dispatch:
9+
10+
permissions:
11+
contents: read
12+
pages: write
13+
id-token: write
14+
15+
concurrency:
16+
group: "pages"
17+
cancel-in-progress: false
18+
19+
jobs:
20+
build:
21+
runs-on: ubuntu-latest
22+
steps:
23+
- uses: actions/checkout@v4
24+
25+
- name: Set up Python
26+
uses: actions/setup-python@v5
27+
with:
28+
python-version: '3.12'
29+
30+
- name: Install dependencies
31+
run: pip install -r docs/requirements.txt
32+
33+
- name: Build documentation
34+
run: sphinx-build docs/ docs/_build/html
35+
36+
- name: Upload artifact
37+
uses: actions/upload-pages-artifact@v3
38+
with:
39+
path: docs/_build/html
40+
41+
deploy:
42+
environment:
43+
name: github-pages
44+
url: ${{ steps.deployment.outputs.page_url }}
45+
runs-on: ubuntu-latest
46+
needs: build
47+
steps:
48+
- name: Deploy to GitHub Pages
49+
id: deployment
50+
uses: actions/deploy-pages@v4

‎.gitignore‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1 +1,3 @@
11
.DS_Store
2+
docs/_build/
3+
docs/.venv/

‎docs/Makefile‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
SPHINXOPTS ?=
2+
SPHINXBUILD ?= sphinx-build
3+
SOURCEDIR = .
4+
BUILDDIR = _build
5+
6+
help:
7+
@$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
8+
9+
.PHONY: help Makefile
10+
11+
%: Makefile
12+
@$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)

‎docs/_static/css/custom.css‎

Lines changed: 111 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,111 @@
1+
/* Custom styles for IMPaCT documentation */
2+
3+
/* === Code Blocks === */
4+
pre {
5+
font-size: 0.85em;
6+
border-left: 3px solid var(--color-brand-primary);
7+
border-radius: 0 4px 4px 0;
8+
}
9+
10+
code.literal {
11+
padding: 1px 4px;
12+
}
13+
14+
/* === Section headings === */
15+
.content h2 {
16+
padding-left: 0.6rem;
17+
border-left: 3px solid var(--color-brand-primary);
18+
}
19+
20+
/* === Card styling === */
21+
.sd-card {
22+
transition: box-shadow 0.2s ease, transform 0.15s ease;
23+
border-top: 2px solid transparent;
24+
}
25+
26+
.sd-card:hover {
27+
box-shadow: 0 4px 12px rgba(0, 0, 0, 0.12);
28+
transform: translateY(-2px);
29+
border-top-color: var(--color-brand-primary);
30+
}
31+
32+
/* === Performance tables === */
33+
table.docutils td:last-child {
34+
font-weight: 600;
35+
color: var(--color-brand-primary);
36+
}
37+
38+
table.docutils tbody tr:nth-child(even) {
39+
background-color: var(--color-background-secondary);
40+
}
41+
42+
table.docutils thead th {
43+
background-color: var(--color-brand-primary);
44+
color: white;
45+
font-weight: 600;
46+
}
47+
48+
/* === Admonition accents === */
49+
.admonition.note {
50+
border-left-color: var(--color-brand-primary);
51+
}
52+
53+
.admonition.warning {
54+
border-left-color: #ff9800;
55+
}
56+
57+
.admonition.tip {
58+
border-left-color: #4caf50;
59+
}
60+
61+
/* === Horizontal rules === */
62+
hr {
63+
margin: 2.5rem 0;
64+
border: none;
65+
border-top: 2px solid var(--color-brand-primary);
66+
opacity: 0.2;
67+
}
68+
69+
/* === Hero accent bar === */
70+
.page-content > .content > section:first-child > p:first-of-type {
71+
font-size: 1.15em;
72+
color: var(--color-foreground-secondary);
73+
}
74+
75+
/* === Badge polish === */
76+
.sd-badge {
77+
font-weight: 600;
78+
letter-spacing: 0.02em;
79+
}
80+
81+
/* === Scrollbar === */
82+
::-webkit-scrollbar {
83+
width: 8px;
84+
}
85+
86+
::-webkit-scrollbar-thumb {
87+
background: var(--color-brand-primary);
88+
border-radius: 4px;
89+
opacity: 0.5;
90+
}
91+
92+
::-webkit-scrollbar-thumb:hover {
93+
opacity: 0.8;
94+
}
95+
96+
::-webkit-scrollbar-track {
97+
background: var(--color-background-secondary);
98+
}
99+
100+
/* === Dark mode adjustments === */
101+
body[data-theme="dark"] table.docutils td:last-child {
102+
color: var(--color-brand-content);
103+
}
104+
105+
body[data-theme="dark"] table.docutils thead th {
106+
background-color: #0d3b66;
107+
}
108+
109+
body[data-theme="dark"] .sd-card:hover {
110+
border-top-color: var(--color-brand-content);
111+
}

‎docs/api/gpu-synthesis.rst‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
=============
2+
GPU Synthesis
3+
=============
4+
5+
GPU-accelerated synthesis functions are implemented in ``src/GPU_synthesis.cpp``
6+
using SYCL via AdaptiveCpp. These are the **sorted** variants of the standard
7+
synthesis algorithms.
8+
9+
Overview
10+
========
11+
12+
The sorted approach:
13+
14+
1. Sorts states by transition probability, enabling efficient parallel reduction
15+
2. Removes the dependency on the GLPK linear programming library
16+
3. Enables execution on GPUs (NVIDIA, Intel, etc.) via SYCL
17+
18+
All sorted synthesis functions are methods of the :cpp:class:`IMDP` class.
19+
See :doc:`imdp` for the full function signatures.
20+
21+
Usage
22+
=====
23+
24+
To use GPU synthesis:
25+
26+
1. **Compute abstraction on CPU** and save to HDF5 files
27+
2. **Update the Makefile**: replace ``IMDP.cpp`` with ``GPU_synthesis.cpp``
28+
and change ``--acpp-targets`` to your GPU target
29+
3. **Load abstraction** from files and call sorted synthesis functions
30+
31+
.. code-block:: cpp
32+
33+
IMDP imdp(dim_x, dim_u, dim_w);
34+
35+
// Load pre-computed data
36+
imdp.loadStateSpace("ss.h5");
37+
imdp.loadInputSpace("is.h5");
38+
imdp.loadMinTransitionMatrix("minTM.h5");
39+
imdp.loadMaxTransitionMatrix("maxTM.h5");
40+
// ... load other vectors ...
41+
42+
// GPU-accelerated synthesis
43+
imdp.infiniteHorizonReachControllerSorted(true);
44+
imdp.saveController();
45+
46+
Makefile Configuration
47+
======================
48+
49+
.. code-block:: makefile
50+
51+
CC = acpp
52+
CFLAGS = --acpp-targets="cuda:sm_70" -O3 \
53+
-lnlopt -lm \
54+
-I/usr/include/hdf5/serial \
55+
-L/usr/lib/x86_64-linux-gnu/hdf5/serial \
56+
-lhdf5 -lgsl -lgslcblas \
57+
-DH5_USE_110_API -larmadillo
58+
59+
SRCS = example.cpp ../../src/GPU_synthesis.cpp ../../src/MDP.cpp
60+
61+
Note: ``-lglpk`` is not needed for sorted synthesis.
62+
63+
See :doc:`/getting-started/gpu` for full GPU setup instructions.

‎docs/api/imdp.rst‎

Lines changed: 153 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,153 @@
1+
=============================
2+
IMDP (``class IMDP``)
3+
=============================
4+
5+
.. cpp:class:: IMDP : public MDP
6+
7+
Interval MDP class for abstraction, controller synthesis, and data management.
8+
Inherits all functionality from :cpp:class:`MDP`.
9+
10+
Defined in ``src/IMDP.h`` with implementations in ``src/IMDP.cpp``.
11+
12+
Constructor
13+
-----------
14+
15+
Inherits the :cpp:class:`MDP` constructor:
16+
17+
.. code-block:: cpp
18+
19+
IMDP imdp(dim_x, dim_u, dim_w);
20+
21+
Optimization Algorithm
22+
----------------------
23+
24+
.. cpp:function:: void setAlgorithm(nlopt::algorithm alg)
25+
26+
Set the nonlinear optimization algorithm used during abstraction.
27+
28+
:param alg: An NLopt algorithm (default: ``nlopt::LN_SBPLX``).
29+
30+
See `NLopt Algorithms <https://nlopt.readthedocs.io/en/latest/NLopt_Algorithms/>`_
31+
for all options.
32+
33+
Abstraction
34+
===========
35+
36+
Transition Matrix
37+
-----------------
38+
39+
.. cpp:function:: void minTransitionMatrix()
40+
41+
Compute the minimal transition probability matrix for state-to-state transitions.
42+
43+
.. cpp:function:: void maxTransitionMatrix()
44+
45+
Compute the maximal transition probability matrix for state-to-state transitions.
46+
47+
.. cpp:function:: void transitionMatrixBounds()
48+
49+
Compute both min and max transition matrices efficiently.
50+
Exploits sparsity: if max is zero, min is skipped. Use this instead of
51+
calling ``minTransitionMatrix()`` and ``maxTransitionMatrix()`` separately.
52+
53+
Target Transition Vector
54+
------------------------
55+
56+
.. cpp:function:: void minTargetTransitionVector()
57+
58+
Compute the minimal transition probability vector to the target region.
59+
60+
.. cpp:function:: void maxTargetTransitionVector()
61+
62+
Compute the maximal transition probability vector to the target region.
63+
64+
.. cpp:function:: void targetTransitionVectorBounds()
65+
66+
Compute both min and max target vectors efficiently with sparsity exploitation.
67+
68+
Avoid Transition Vector
69+
-----------------------
70+
71+
.. cpp:function:: void minAvoidTransitionVector()
72+
73+
Compute the minimal transition probability vector to outside the state space
74+
(including the avoid region).
75+
76+
.. cpp:function:: void maxAvoidTransitionVector()
77+
78+
Compute the maximal transition probability vector to outside the state space.
79+
80+
.. note::
81+
82+
Avoid vectors are always required, even when no avoid region is defined, as they
83+
capture transitions out of the state space.
84+
85+
Controller Synthesis
86+
====================
87+
88+
All synthesis functions take ``IMDP_lower``:
89+
90+
- ``true`` --- pessimistic (worst-case noise first, then fix for upper bound)
91+
- ``false`` --- optimistic (best-case noise first, then fix for lower bound)
92+
93+
Standard Synthesis
94+
------------------
95+
96+
.. cpp:function:: void infiniteHorizonReachController(bool IMDP_lower)
97+
98+
Synthesize a reachability (or reach-avoid) controller over an infinite horizon
99+
using the interval iteration algorithm.
100+
101+
.. cpp:function:: void infiniteHorizonSafeController(bool IMDP_lower)
102+
103+
Synthesize a safety controller over an infinite horizon.
104+
105+
.. cpp:function:: void finiteHorizonReachController(bool IMDP_lower, size_t timeHorizon)
106+
107+
Synthesize a reachability (or reach-avoid) controller for a finite number of steps
108+
using value iteration.
109+
110+
.. cpp:function:: void finiteHorizonSafeController(bool IMDP_lower, size_t timeHorizon)
111+
112+
Synthesize a safety controller for a finite number of steps.
113+
114+
Sorted Synthesis (GPU-Compatible)
115+
---------------------------------
116+
117+
Sorted variants eliminate the GLPK dependency and support GPU execution
118+
(implemented in ``src/GPU_synthesis.cpp``):
119+
120+
.. cpp:function:: void infiniteHorizonReachControllerSorted(bool IMDP_lower)
121+
.. cpp:function:: void infiniteHorizonSafeControllerSorted(bool IMDP_lower)
122+
.. cpp:function:: void finiteHorizonReachControllerSorted(bool IMDP_lower, size_t timeHorizon)
123+
.. cpp:function:: void finiteHorizonSafeControllerSorted(bool IMDP_lower, size_t timeHorizon)
124+
125+
.. cpp:function:: void finiteHorizonReachControllerSortedStoreMDP(bool IMDP_lower, size_t timeHorizon)
126+
127+
Sorted finite-horizon reachability with intermediate MDP data storage.
128+
129+
Save Functions
130+
==============
131+
132+
.. cpp:function:: void saveMinTransitionMatrix()
133+
.. cpp:function:: void saveMaxTransitionMatrix()
134+
.. cpp:function:: void saveMinTargetTransitionVector()
135+
.. cpp:function:: void saveMaxTargetTransitionVector()
136+
.. cpp:function:: void saveMinAvoidTransitionVector()
137+
.. cpp:function:: void saveMaxAvoidTransitionVector()
138+
.. cpp:function:: void saveController()
139+
140+
Save the synthesized controller to ``controller.h5``.
141+
142+
Load Functions
143+
==============
144+
145+
.. cpp:function:: void loadMinTransitionMatrix(string filename)
146+
.. cpp:function:: void loadMaxTransitionMatrix(string filename)
147+
.. cpp:function:: void loadMinTargetTransitionVector(string filename)
148+
.. cpp:function:: void loadMaxTargetTransitionVector(string filename)
149+
.. cpp:function:: void loadMinAvoidTransitionVector(string filename)
150+
.. cpp:function:: void loadMaxAvoidTransitionVector(string filename)
151+
.. cpp:function:: void loadController(string filename)
152+
153+
Load a previously saved controller from HDF5.

0 commit comments

Comments
 (0)