Metadata-Version: 2.4
Name: ReForma
Version: 0.1.3
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 — Reconfigurable Formal Automata in Python

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

---

## Installation

You can install it directly from PyPI (once published):
```bash
pip install reforma
```

For **visualization features** (offline PNGs and interactive Jupyter graphs), install the required extras:
```bash
pip install networkx matplotlib
```

*(Local Development: Run `pip install -e .` from the project root).* 
Requires **Python 3.10+** and a working `java` on your PATH.

---

## Quick Start

```python
from reforma import ReForma

modelo = ReForma()

# Load a model
state = modelo.load_file("recommender.r")

# Get a beautiful printout of the current state and probabilities
print(state.summary())

# Simulate
state = modelo.step("go_work")
state = modelo.step("easy_task")

# Undo last step
state = modelo.undo()            

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

---

## Visualization (Jupyter & Offline)

ReForma provides powerful graphing tools directly integrated into your workflow.

```python
from reforma import ReForma

modelo = ReForma()
modelo.load_file("model.r")

# 1. Interactive Jupyter View 
# Renders a drag-and-drop Cytoscape.js graph right inside your Notebook!
modelo.show_interactive()

# 2. Offline Static Images
# Renders a high-res graph using Matplotlib/NetworkX (no browser needed)
modelo.save_image_plt("output/my_graph.png")
```

---

## Simulation & State Inspection

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

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

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

# History of labels taken
print(modelo.history)    # ['go_work', 'easy_task']
```

---

## Training

Train the model on a batch of sessions (lists of event labels) to automatically update the weights:

```python
modelo.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)
modelo.train_from_file("logs/sessions.txt")

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

---

## PDL / PCTL Verification

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

# Qualitative: is it probable?
holds = modelo.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 = modelo.check_pdl_value("Home", "<go_work>Office")
print(holds)   # True

# Get the raw string result
raw = modelo.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 = modelo.export_prism()
modelo.save_prism("output/model.pm")

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

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

# Mermaid diagram (full LTS — all reachable states)
full_diagram = modelo.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 = modelo.load(source, name="MyModel")
```


---

## Error handling

```python
from reforma.jar_bridge import JarError

try:
    result = modelo.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
```
```
