ReForma 0.1.1

Python bindings for the RePA/ReForma probabilistic automaton tool

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

pip install reforma

For visualization features (offline PNGs and interactive Jupyter graphs), install the required extras:

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

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.

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

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:

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

# 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

# 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

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

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