Merge pull request #11 from KTH-SML/documentation-review

Adding documentation

Author: kaarmu

README.md

@@ -35,6 +35,7 @@ pip install -e ".[hj_reachability]"
 from pyspect.logics import *
 from pyspect.tlt import TLT, ContLTL
 from pyspect.impls.hj_reachability import TVHJImpl
+from pyspect.set_builder import BoundedSet, Union, HalfSpaceSet
 
 # 1) Pick primitives/fragment
 TLT.select(ContLTL) # Continuous-time LTL

docs/get_started.md

@@ -2,12 +2,16 @@
 
 Follow these steps to install **pyspect** and run your first spec.
 
+## 0. Prerequisites
+
+- Python **>= 3.12**
+
 ## 1. Installation
 
 ```bash
 pip install pyspect
 
-# With optional implementaion
+# With optional implementation
 pip install pyspect[hj_reachability]
 ```
 
@@ -16,8 +20,8 @@ pip install pyspect[hj_reachability]
 ```python
 from pyspect.logics import *
 from pyspect.tlt import TLT, ContLTL
-from pyspect.sets import BoundedSet, Union, HalfSpaceSet
-from pyspect.impls.hj_reachability import HJImpl
+from pyspect.set_builder import BoundedSet, Union, HalfSpaceSet
+from pyspect.impls.hj_reachability import TVHJImpl
 
 # Choose fragment
 TLT.select(ContLTL)
@@ -33,7 +37,7 @@ tlt = TLT(phi, where={
 })
 
 # Realize on a backend
-impl = HJImpl(...)
+impl = TVHJImpl(...)
 Phi = tlt.realize(impl)
 print("Satisfaction set:", Phi)
 ```

docs/implementations/hj_reachability.md

@@ -1,8 +1,3 @@
+## Reference
 
-*Documentation To Come...*
-
-<!-- ## Reference -->
-
-<!-- ::: pyspect.impls.hj_reachability
-    options:
-        show_root_head: false -->
+::: pyspect.impls.hj_reachability

docs/implementations/zonoOpt.md

@@ -1,2 +1,4 @@
 
-*Documentation To Come...*
+## Reference
+
+::: pyspect.impls.zonoopt

mkdocs.yml

@@ -36,10 +36,10 @@ nav:
     - hj_reachability: implementations/hj_reachability.md
     - ZonoOpt: implementations/zonoOpt.md
   - Helper Implementations:
-    - Base: implementations/base.md
-    - Axes: implementations/axes.md
-    - Plotly: implementations/plotly.md
-    - Debug: implementations/debug.md
+    - Base: implementations/dev/base.md
+    - Axes: implementations/dev/axes.md
+    - Plotly: implementations/dev/plotly.md
+    - Debug: implementations/dev/debug.md
 
 extra_javascript:
   - mathjax.js
@@ -52,6 +52,7 @@ plugins:
         python:
           options:
             show_root_heading: false
+            show_source: false
 
 markdown_extensions:
   admonition:

src/pyspect/impls/hj_reachability.py

@@ -1,9 +1,26 @@
-"""
-Hamilton-Jacobi reachability implementations using the hj_reachability package.
+"""Hamilton-Jacobi backend implementations.
+
+This module integrates the external ``hj_reachability`` package with
+``pyspect`` by providing a concrete backend for level-set operations and
+time-varying reachability queries used during TLT realization.
+
+Provided classes:
+    - ``TVHJImpl``: Main HJ backend operating on gridded level-set arrays.
+    - ``TVHJImplDebugger``: Debug helper for inspecting HJ backend behavior.
+
+Backend capabilities:
+    - Set operations: ``empty``, ``complement``, ``intersect``, ``union``
+    - Geometry: ``halfspace`` and axis-aware projections
+    - Reachability: ``pre``, ``reach``, ``avoid`` with time-varying
+      targets/constraints
+    - Visualization: Plotly-based bitmap/surface/isosurface transforms
 
 Requires:
-    - hj_reachability
-    - jax_tqdm
+    - ``hj_reachability``
+    - ``jax_tqdm``
+
+Notes:
+    - Uses JAX arrays as the underlying set/value representation.
 """
 
 import functools

src/pyspect/impls/zonoopt.py

@@ -1,3 +1,25 @@
+"""ZonoOpt backend implementations.
+
+This module integrates the external ``zonoopt`` library with ``pyspect`` by
+providing a concrete backend for set operations and reachability queries used
+during TLT realization.
+
+Provided classes:
+    - ``ZonoOptImpl``: Main backend operating on ``zono.HybZono`` sets.
+    - ``DoubleIntegrator``: Convenience linear dynamics model for examples.
+
+Backend capabilities:
+    - Set operations: ``empty``, ``complement``, ``intersect``, ``union``
+    - Geometry: ``halfspace``
+    - Reachability: ``pre``, ``reach``, ``reachF``
+
+Requires:
+    - ``zonoopt``
+
+Notes:
+    - Targets discrete-time linear dynamics workflows.
+"""
+
 import numpy as np
 import zonoopt as zono
 from scipy import sparse