ReForma 0.1.0

Python bindings for the RePA/ReForma probabilistic automaton tool

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

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

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

---

Quick Start

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

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):

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

# 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

# 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

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

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

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