Metadata-Version: 2.4
Name: uppaal-gym
Version: 1.0.1
Summary: Gymnasium environments for UPPAAL hybrid-system benchmark models
Project-URL: Homepage, https://github.com/andreashhpetersen/uppaal-gym
Project-URL: Source, https://github.com/andreashhpetersen/uppaal-gym
Project-URL: Bug Tracker, https://github.com/andreashhpetersen/uppaal-gym/issues
Author-email: Andreas Holck Høeg-Petersen <andreashhpetersen@me.com>
License: MIT License
        
        Copyright (c) 2026 Andreas Holck Høeg-Petersen
        
        Permission is hereby granted, free of charge, to any person obtaining a copy
        of this software and associated documentation files (the "Software"), to deal
        in the Software without restriction, including without limitation the rights
        to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
        copies of the Software, and to permit persons to whom the Software is
        furnished to do so, subject to the following conditions:
        
        The above copyright notice and this permission notice shall be included in all
        copies or substantial portions of the Software.
        
        THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
        IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
        FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
        AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
        LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
        OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
        SOFTWARE.
License-File: LICENSE
Keywords: UPPAAL,benchmark,control-theory,formal-methods,gymnasium,hybrid-systems,reinforcement-learning
Classifier: Development Status :: 5 - Production/Stable
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: MIT License
Classifier: Operating System :: OS Independent
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.8
Classifier: Programming Language :: Python :: 3.9
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Scientific/Engineering :: Artificial Intelligence
Requires-Python: >=3.8
Requires-Dist: gymnasium
Requires-Dist: matplotlib
Requires-Dist: numpy
Requires-Dist: scipy
Description-Content-Type: text/markdown

# uppaal-gym

[Gymnasium](https://gymnasium.farama.org/) environments for classic UPPAAL hybrid-system benchmark models. Designed for research at the intersection of reinforcement learning and formal methods.

## Installation

```bash
pip install uppaal-gym
```

Or from source:

```bash
git clone https://github.com/andreashhpetersen/uppaal-gym
cd uppaal-gym
pip install -e .
```

## Environments

All environments follow the standard [Gymnasium API](https://gymnasium.farama.org/api/env/) and are registered automatically on `import uppaal_gym`.

| ID | Observation | Actions | Termination |
|----|------------|---------|-------------|
| `BouncingBall-v0` | position, velocity (2D continuous) | 0: do nothing, 1: hit ball | Ball stops (low position and velocity) |
| `CruiseControl-v0` | ego velocity, front velocity, distance (3D continuous) | 0: decelerate, 1: accelerate, 2: neutral | Collision (distance ≤ 0) |
| `DCDCBoostConverter-v0` | inductor current, capacitor voltage, resistance (3D continuous) | 0: switch off, 1: switch on | Safety constraint violated |
| `OilPump-v0` | cycle time, oil volume, pump status, latency (4D continuous) | 0: pump off, 1: pump on | Oil volume outside [4.9, 25.1] |
| `RandomWalk-v0` | position, time (2D continuous) | 0: slow, 1: fast | Goal reached (x ≥ 1) or timeout (t ≥ 1) |
| `Spiral-v0` | agent position, destination position (4D continuous) | 0: move outward, 1: move inward, 2: stay course | Rock collision or destination reached |

> `PasswordGuessing-v0` is also registered but requires `words` and `options` arguments — instantiate it directly via `PasswordEnv(words, options)`.

### Environment details

**BouncingBall-v0** — A ball bounces under gravity. The agent can hit the ball to add velocity. The episode ends when the ball loses enough energy to stop. The agent is penalised for hitting (`-1`) and heavily for termination (`-1000`).

**CruiseControl-v0** — An ego vehicle follows a front vehicle with stochastic acceleration. The agent controls ego acceleration to maintain a safe following distance. Reward is `-distance` each step; collision gives `-10000`.

**DCDCBoostConverter-v0** — A DC-DC boost converter must keep inductor current `x1` ∈ [0, 4] A and capacitor voltage `x2` ∈ [14.5, 15.5] V despite a randomly fluctuating load resistance. Reward is negative distance from target values `(x1_ref=0.35, x2_ref=15)`.

**OilPump-v0** — An oil pump refills a tank consumed at varying rates over a 20-second cycle. The pump has a 2-second switching latency. The agent must keep oil volume within [4.9, 25.1].

**RandomWalk-v0** — A 2D random walk where the agent must reach `x = 1` before `t = 1`. Fast moves cost more (`-3`) but advance position more; slow moves cost less (`-1`). Timeout incurs an extra penalty of `-20`.

**Spiral-v0** — An agent moves on a spiral trajectory in 2D space and must reach a randomly generated destination while avoiding five fixed obstacles (rocks). Actions adjust the radius of the spiral.

## Usage

```python
import gymnasium as gym
import uppaal_gym  # registers all environments

env = gym.make("BouncingBall-v0")
obs, info = env.reset(seed=42)

for _ in range(200):
    action = env.action_space.sample()
    obs, reward, terminated, truncated, info = env.step(action)
    if terminated or truncated:
        obs, info = env.reset()

env.close()
```

All environments expose two additional methods beyond the standard Gymnasium API:

```python
# Check which actions are safe in a given state
safe_actions = env.allowed_actions(obs)

# Compute a transition without updating internal state (useful for planning)
next_state, reward, terminated = env.step_from(obs, action)
```

## UPPAAL Models

The original UPPAAL model files (`.xml`) for each environment are included in the [`models/`](models/) directory. UPPAAL is available at [uppaal.org](https://uppaal.org/).

### Deviations from the original models

The gym environments are faithful adaptations but include deliberate deviations where necessary for use as RL benchmarks.

**BouncingBall-v0** — The initial position range is [8, 10) rather than the original [7, 10). States in [7, 8) cannot be guaranteed safe even under a perfect strategy, so they are excluded to ensure the task is feasible.

**CruiseControl-v0** — Two differences: (1) the sensor range is doubled from 100 to 200 to give the agent more time to react when the front car reappears; (2) the minimum velocity of the front car is −8 instead of −10, matching the observation space used in experiments.

**DCDCBoostConverter-v0** — Several differences: (1) `x1` and `x2` are initialised at their target values (0.35 A, 15 V) rather than 0, since starting at 0 immediately violates the safety constraints; (2) the load resistance `R` is initialised at 73 Ω and may vary over [30, 200] Ω with fluctuations of ±30 per step, compared to [60, 80] Ω and ±10 in the original — this substantially increases task difficulty; (3) the safety region is widened to `x1 ∈ [0, 4]`, `x2 ∈ [14.5, 15.5]` from the tighter query targets `x1 ∈ [0, 0.7]`, `x2 ∈ [14.8, 15.2]` used in the original model.

**OilPump-v0** — The consumption schedule, fluctuation range, inflow rate, latency, and time step all match the original exactly. The only deviation is in the termination condition: in the original model, a safety violation resets the oil volume to 10 and increments a death counter so the run continues; in the gym, a violation terminates the episode.

**RandomWalk-v0** — No significant deviations. The UPPAAL model has been updated to use the same step sizes (Δd: 0.17 fast, 0.10 slow; Δt: 0.05 fast, 0.12 slow) and noise magnitude (±0.04) as the gym implementation. Action indices also match: 0 = slow, 1 = fast.

## Citation

If you use `uppaal-gym` in your research, please cite:

```bibtex
@software{hoeeg-petersen_uppaal_gym_2026,
  author    = {Høeg-Petersen, Andreas Holck},
  title     = {uppaal-gym: Gymnasium Environments for UPPAAL Hybrid-System Benchmarks},
  year      = {2026},
  doi       = {10.5281/zenodo.20798359},
  url       = {https://doi.org/10.5281/zenodo.20798359},
  version   = {1.0.0},
}
```

## License

MIT — see [LICENSE](LICENSE).
