Metadata-Version: 2.4
Name: ReForma
Version: 0.1.0
Summary: Python bindings for the RePA/ReForma probabilistic automaton tool
Author-email: Joshua Dourado <joshuadourado@ua.pt>
License: MIT
Classifier: Programming Language :: Python :: 3
Classifier: License :: OSI Approved :: MIT License
Classifier: Operating System :: OS Independent
Classifier: Topic :: Scientific/Engineering
Requires-Python: >=3.10
Description-Content-Type: text/markdown
Requires-Dist: networkx
Requires-Dist: matplotlib

# ReForma — Python bindings for the RePA/ReForma tool

A clean Python library that wraps the `ReFormaTool.jar` CLI via subprocess,
giving you a Pythonic interface for simulation, training, PDL/PCTL
verification, and export.

---

## Installation

```bash
# From the project root (where pyproject.toml lives)
pip install -e .
```

Requires **Python 3.10+** and a working `java` on your PATH.

---

## Quick Start

```python
from ReForma import ReForma

# Point to your compiled JAR
ReForma = ReForma("path/to/ReFormaTool.jar")

# Load a model
state = ReForma.load_file("examples/recommender.r")

print(state.current_states)   # ['Home']
print(state.enabled)          # [Transition('go_work': Home → Office, p=0.500), ...]

# Simulate
state = ReForma.step("go_work")
state = ReForma.step("easy_task")
state = ReForma.undo()            # undo last step

# Reset to initial state
ReForma.reset()
```

---

## Simulation

```python
state = ReForma.load_file("model.r")

# Check what's enabled
for t in state.enabled:
    print(f"{t.label}: {t.from_state} → {t.to_state}  (p={t.probability:.3f})")

# Take a step by label
state = ReForma.step("go_work")

# Undo / reset
state = ReForma.undo()
state = ReForma.reset()

# Inspect variables
print(state.variables)   # {'counter': 0, 'flag': 1}

# History of labels taken
print(ReForma.history)       # ['go_work']
```

---

## Training

Train the model on a batch of sessions (lists of event labels):

```python
ReForma.train([
    ["go_work", "easy_task", "easy_task", "go_home"],
    ["battery_low", "go_charge", "finish_charge", "socialize"],
    ["no_money", "go_work", "go_home"],
])

# Or train directly from a log file (one session per line, comma-separated)
ReForma.train_from_file("logs/sessions.txt")

# sessions.txt format:
#   go_work,easy_task,go_home
#   battery_low,go_charge,finish_charge

# Save the updated model with new weights
ReForma.save_source("model_trained.r")
```

---

## PDL / PCTL Verification

```python
# Quantitative: probability of eventually reaching Office
prob = ReForma.check_pdl_value("Home", "{P=?[F Office]}")
print(f"P(reach Office from Home) = {prob:.4f}")

# Qualitative: is it probable?
holds = ReForma.check_pdl_value("Home", "{P>=0.4[F Office]}")
print(f"P>=0.4? {holds}")   # True / False

# PDL: is there a path via go_work to Office?
holds = ReForma.check_pdl_value("Home", "<go_work>Office")
print(holds)   # True

# Get the raw string result
raw = ReForma.check_pdl("Home", "{P=?[F Office]}")
print(raw)  # "Result: 0.50000"
```

### Formula syntax reference

| Formula                     | Meaning                                        |
|-----------------------------|------------------------------------------------|
| `{P=?[F target]}`           | Probability of eventually reaching `target`    |
| `{P=?[G safe]}`             | Probability of staying in `safe` forever       |
| `{P=?[X next]}`             | Probability of reaching `next` in one step     |
| `{P=?[a U b]}`              | Probability of `a` until `b`                   |
| `{P>=0.5[F target]}`        | Is probability of reaching target ≥ 0.5?       |
| `<action>state`             | There exists a path via `action` to `state`    |
| `[action]state`             | All paths via `action` lead to `state`         |

---

## Export

```python
# PRISM DTMC
prism_code = ReForma.export_prism()
ReForma.save_prism("output/model.pm")

# mCRL2
mcrl2_code = ReForma.export_mcrl2()

# GLTS (imperative translation)
glts_code = ReForma.export_glts()

# Mermaid diagram (initial state)
diagram = ReForma.export_mermaid()

# Mermaid diagram (full LTS — all reachable states)
full_diagram = ReForma.export_mermaid(full_lts=True)
```

---

## Loading from a string

```python
source = """
name MyModel
init s0
s0 ---> s1: a (0.6)
s0 ---> s2: b (0.4)
s1 ---> s0: back (1.0)
"""

state = ReForma.load(source, name="MyModel")
```

---

## Running the tests

```bash
pip install pytest
pytest tests/ -v
```

---

## Project structure

```
ReForma/
├── __init__.py       # Public API exports
├── client.py         # ReForma — high-level Python API
├── jar_bridge.py     # JarBridge — low-level subprocess wrapper
└── model.py          # ReFormaModel, SimulationState, Transition data classes
tests/
└── test_ReForma.py       # Full test suite (mocked, no JAR needed)
pyproject.toml
README.md
```

---

## Error handling

```python
from ReForma.jar_bridge import JarError

try:
    result = ReForma.check_pdl("Home", "{P=?[F Office]}")
except JarError as e:
    print(f"JAR error: {e}")
except RuntimeError as e:
    print(f"Usage error: {e}")   # e.g. no model loaded, invalid transition
```
