diff --git a/src/app.py b/src/app.py
index d5ac57f..0d7b97d 100644
--- a/src/app.py
+++ b/src/app.py
@@ -22,7 +22,7 @@
 import uuid
 import requests
 from stepper import traceSatisfactionPerStep, getTraceRenderData
-import ltltoeng
+import ltltoeng_prose
 from authroutes import (
     authroutes,
     init_app,
@@ -412,7 +412,7 @@ def ltl_to_english():
         return jsonify({"error": "Missing required query parameter 'formula'."}), 400
     try:
         node = parse_ltl_string(formula)
-        english = ltltoeng.finalize_sentence(node.__to_english__())
+        english = ltltoeng_prose.translate(node)
     except Exception as e:
         return jsonify({"error": "Failed to translate formula.", "details": str(e)}), 400
 
@@ -516,7 +516,7 @@ def ltl_to_english_ui():
         else:
             try:
                 node = parse_ltl_string(input_formula)
-                translation = ltltoeng.finalize_sentence(node.__to_english__())
+                translation = ltltoeng_prose.translate(node)
             except Exception as e:
                 error = f"Failed to translate formula: {e}"
 
@@ -854,9 +854,11 @@ def loganswer(questiontype):
                 return {"error": "submission_limit", "message": "This exercise only allows one submission."}, 403
 
 
+    translation_mode = data.get('translation_mode', '')
     answer_logger.logStudentResponse(userId = userId, misconceptions = misconceptions, question_text = question_text,
                                       question_options = question_options, correct_answer = isCorrect,
-                                      questiontype=questiontype, mp_class = mp_class, exercise = exercise, course = courseId)
+                                      questiontype=questiontype, mp_class = mp_class, exercise = exercise, course = courseId,
+                                      translation_mode = translation_mode)
     
 
     if questiontype == "english_to_ltl":
diff --git a/src/exercisebuilder.py b/src/exercisebuilder.py
index a14e387..82786ca 100644
--- a/src/exercisebuilder.py
+++ b/src/exercisebuilder.py
@@ -7,7 +7,8 @@
 import random
 import re
 import math
-import ltltoeng
+import ltltoeng_prose
+import ltltoeng_contextualized
 from syntacticmutator import applyRandomMutationNotEquivalentTo
 
 
@@ -411,16 +412,33 @@ def contains_undersirable_lit(s):
 
         ## First generate a large pool from spot randltl
         pool_size = 2*num_questions
-        question_answers = spotutils.gen_rand_ltl(atoms = literals, 
-                                                  tree_size = tree_size, 
-                                                  ltl_priorities = self.ltl_priorities, 
+        question_answers = spotutils.gen_rand_ltl(atoms = literals,
+                                                  tree_size = tree_size,
+                                                  ltl_priorities = self.ltl_priorities,
                                                   num_formulae = pool_size)
-        
+
         ## Augment with template-generated formulas for pattern-specific misconceptions
         ## This helps ensure we get formulas that can actually be mutated with these misconceptions
         template_formulas = self.generate_template_formulas(literals, num_templates=max(1, num_questions // 4))
         question_answers.extend(template_formulas)
-        
+
+        ## A/B test: lazily generate a pool with r,g,b literals for contextualized questions
+        CONTEXTUALIZED_LITERALS = list(ltltoeng_contextualized.THEMES["lights"].literals.keys())
+        ctx_iter = None
+        def _get_ctx_iter():
+            nonlocal ctx_iter
+            if ctx_iter is None:
+                ctx_pool = spotutils.gen_rand_ltl(atoms = CONTEXTUALIZED_LITERALS,
+                                                  tree_size = tree_size,
+                                                  ltl_priorities = self.ltl_priorities,
+                                                  num_formulae = pool_size)
+                ctx_templates = self.generate_template_formulas(CONTEXTUALIZED_LITERALS, num_templates=max(1, num_questions // 4))
+                ctx_pool.extend(ctx_templates)
+                ctx_pool = [a for a in ctx_pool if not contains_undersirable_lit(a)]
+                random.shuffle(ctx_pool)
+                ctx_iter = iter(ctx_pool)
+            return ctx_iter
+
 
         def formula_choice_metric(formula):
 
@@ -447,7 +465,15 @@ def formula_choice_metric(formula):
             if kind == self.TRACESATMC:
                 question = self.build_tracesat_mc_question(answer)
             elif kind == self.ENGLISHTOLTL:
-                question = self.build_english_to_ltl_question(answer)
+                # A/B test: 50/50 abstract vs. contextualized
+                if random.random() < 0.5:
+                    ctx_answer = next(_get_ctx_iter(), None)
+                    if ctx_answer is not None:
+                        question = self.build_english_to_ltl_question(ctx_answer, contextualized=True)
+                    else:
+                        question = self.build_english_to_ltl_question(answer)
+                else:
+                    question = self.build_english_to_ltl_question(answer)
             elif kind == self.TRACESATYN:
                 question = self.build_tracesat_yn_question(answer)
 
@@ -490,16 +516,25 @@ def formula_choice_metric(formula):
 
     
     def gen_nl_question(self, formula):
+        as_node = ltlnode.parse_ltl_string(formula)
+        result = ltltoeng_prose.translate(as_node)
+        if not result or result.strip() == "":
+            return None
+        return result
 
+
+    def gen_nl_question_contextualized(self, formula):
+        """Generate a contextualized English question using the lights theme.
+
+        Expects the formula to already use r,g,b literals (matching the theme).
+        Returns None if translation fails.
+        """
+        LIGHTS_THEME = ltltoeng_contextualized.THEMES["lights"]
         as_node = ltlnode.parse_ltl_string(formula)
-        formula_eng = as_node.__to_english__()
-        if formula_eng is None or formula_eng == "":
+        result = ltltoeng_contextualized.translate(as_node, LIGHTS_THEME)
+        if not result or result.strip() == "":
             return None
-        
-        formula_eng_corrected = ltltoeng.correct_grammar(formula_eng)
-        ### If there are multiple '.' in a row, replace with a single '.'
-        formula_eng_corrected = re.sub(r'\.{2,}', '.', formula_eng_corrected)
-        return ltltoeng.finalize_sentence(formula_eng_corrected)
+        return result
 
 
     def get_options_with_misconceptions_as_formula(self, answer):
@@ -547,13 +582,22 @@ def get_options_with_misconceptions_as_formula(self, answer):
 
         return merged_options
 
-    def build_english_to_ltl_question(self, answer):
-        
+    def build_english_to_ltl_question(self, answer, contextualized=False):
+
         options = self.get_options_with_misconceptions_as_formula(answer)
         if options is None:
             return None
 
-        question = self.gen_nl_question(answer)
+        if contextualized:
+            question = self.gen_nl_question_contextualized(answer)
+            translation_mode = "contextualized"
+            # Fall back to abstract if contextualized translation fails
+            if question is None or question == "":
+                question = self.gen_nl_question(answer)
+                translation_mode = "abstract"
+        else:
+            question = self.gen_nl_question(answer)
+            translation_mode = "abstract"
 
         if question is None or question == "":
             print("Question generation failed unexpectedly.")
@@ -562,7 +606,8 @@ def build_english_to_ltl_question(self, answer):
         return {
             "question": question,
             "type": self.ENGLISHTOLTL,
-            "options": options
+            "options": options,
+            "translation_mode": translation_mode
         }
 
     def build_tracesat_mc_question(self, answer):
diff --git a/src/logger.py b/src/logger.py
index 389e3a0..76047de 100644
--- a/src/logger.py
+++ b/src/logger.py
@@ -52,6 +52,7 @@ class StudentResponse(Base):
     mp_class = Column(String)
     exercise = Column(String)
     course = Column(String, default="")
+    translation_mode = Column(String, default="")
 
 
 class GeneratedExercise(Base):
@@ -114,25 +115,25 @@ def __init__(self):
         if SENTENCE_PAIR_RATING_TABLE not in self.inspector.get_table_names():
             Base.metadata.tables[SENTENCE_PAIR_RATING_TABLE].create(self.engine)
 
-    def record(self, log):
-        with self.Session() as session:
-            print("Recording log")
-            session.add(log)
-            session.commit()
-
-    def getRatedEnglishFormulas(self, user_id):
-        """Return a set of LTL formulas this user has already rated."""
-        if not isinstance(user_id, str):
-            raise ValueError("user_id should be a string")
-
-        with self.Session() as session:
-            rows = session.query(EnglishLTLRating.ltl).filter(
-                EnglishLTLRating.user_id == user_id
-            ).all()
-            return {row.ltl for row in rows if row.ltl}
+    def record(self, log):
+        with self.Session() as session:
+            print("Recording log")
+            session.add(log)
+            session.commit()
+
+    def getRatedEnglishFormulas(self, user_id):
+        """Return a set of LTL formulas this user has already rated."""
+        if not isinstance(user_id, str):
+            raise ValueError("user_id should be a string")
+
+        with self.Session() as session:
+            rows = session.query(EnglishLTLRating.ltl).filter(
+                EnglishLTLRating.user_id == user_id
+            ).all()
+            return {row.ltl for row in rows if row.ltl}
 
     
-    def logStudentResponse(self, userId, misconceptions, question_text, question_options, correct_answer, questiontype, mp_class, exercise, course):
+    def logStudentResponse(self, userId, misconceptions, question_text, question_options, correct_answer, questiontype, mp_class, exercise, course, translation_mode=""):
 
         if not isinstance(userId, str):
             raise ValueError("userId should be a string")
@@ -154,9 +155,9 @@ def logStudentResponse(self, userId, misconceptions, question_text, question_opt
 
         ## We still want to log the response if there are no misconceptions
         if misconceptions == None or len(misconceptions) == 0:
-            log = StudentResponse(user_id=userId, timestamp=datetime.datetime.now(), 
+            log = StudentResponse(user_id=userId, timestamp=datetime.datetime.now(),
                                   misconception="", question_text=question_text, question_options=question_options, correct_answer=correct_answer,
-                                  question_type=questiontype, mp_class=mp_class, exercise=exercise, course=course)
+                                  question_type=questiontype, mp_class=mp_class, exercise=exercise, course=course, translation_mode=translation_mode)
             self.record(log)
 
 
@@ -165,9 +166,9 @@ def logStudentResponse(self, userId, misconceptions, question_text, question_opt
             if not isinstance(misconception, str):
                 raise ValueError("misconception should be a string")
 
-            log = StudentResponse(user_id=userId, timestamp=datetime.datetime.now(), 
+            log = StudentResponse(user_id=userId, timestamp=datetime.datetime.now(),
                                   misconception=misconception, question_text=question_text, question_options=question_options, correct_answer=correct_answer,
-                                  question_type=questiontype, mp_class=mp_class, exercise=exercise, course=course)
+                                  question_type=questiontype, mp_class=mp_class, exercise=exercise, course=course, translation_mode=translation_mode)
             self.record(log)
 
     
diff --git a/src/ltltoeng_contextualized.py b/src/ltltoeng_contextualized.py
new file mode 100644
index 0000000..6aee86c
--- /dev/null
+++ b/src/ltltoeng_contextualized.py
@@ -0,0 +1,516 @@
+"""
+Contextualized English translation for LTL formulas.
+
+Inspired by the Wason selection task: people reason far better about logical
+rules when framed in concrete, familiar terms rather than abstract symbols.
+
+This module translates LTL formulas using a concrete "theme" — a mapping from
+abstract proposition letters to real-world descriptions.  The default theme is
+a 3-light panel (red, green, blue), but custom themes can be supplied.
+
+Public API
+----------
+    translate(node, theme=None) -> str
+    THEMES: dict of built-in theme names -> Theme objects
+
+Example:
+    node = parse_ltl_string("G(r -> F g)")
+    translate(node, theme=THEMES["lights"])
+    # => "Whenever the red light turns on, then eventually the green light is on."
+"""
+
+from __future__ import annotations
+from dataclasses import dataclass, field
+from typing import Dict, Optional
+
+import ltlnode
+
+
+# ---------------------------------------------------------------------------
+# Theme definition
+# ---------------------------------------------------------------------------
+
+@dataclass
+class Theme:
+    """Maps abstract literals to concrete descriptions.
+
+    Attributes:
+        name:        Human-readable theme name.
+        description: One-line description of the scenario.
+        literals:    Maps literal names to (positive_phrase, negative_phrase).
+                     e.g. {"p": ("the red light is on", "the red light is off")}
+        event_form:  Maps literal names to an "event" phrasing for triggers.
+                     e.g. {"p": ("the red light turns on", "the red light turns off")}
+                     Falls back to the positive/negative phrase if not provided.
+    """
+    name: str
+    description: str
+    literals: Dict[str, tuple[str, str]]  # lit -> (positive, negative)
+    event_form: Dict[str, tuple[str, str]] = field(default_factory=dict)  # lit -> (becomes_true, becomes_false)
+
+    def positive(self, lit: str) -> str:
+        if lit in self.literals:
+            return self.literals[lit][0]
+        return f"'{lit}'"
+
+    def negative(self, lit: str) -> str:
+        if lit in self.literals:
+            return self.literals[lit][1]
+        return f"'{lit}' does not hold"
+
+    def event_on(self, lit: str) -> str:
+        """Event phrasing for when the literal becomes true."""
+        if lit in self.event_form:
+            return self.event_form[lit][0]
+        return self.positive(lit)
+
+    def event_off(self, lit: str) -> str:
+        """Event phrasing for when the literal becomes false."""
+        if lit in self.event_form:
+            return self.event_form[lit][1]
+        return self.negative(lit)
+
+
+# ---------------------------------------------------------------------------
+# Built-in themes
+# ---------------------------------------------------------------------------
+
+THEMES: Dict[str, Theme] = {}
+
+THEMES["lights"] = Theme(
+    name="Light Panel",
+    description="A panel with three colored lights: red, green, and blue.",
+    literals={
+        "r": ("the red light is on",    "the red light is off"),
+        "g": ("the green light is on",  "the green light is off"),
+        "b": ("the blue light is on",   "the blue light is off"),
+    },
+    event_form={
+        "r": ("the red light turns on",    "the red light turns off"),
+        "g": ("the green light turns on",  "the green light turns off"),
+        "b": ("the blue light turns on",   "the blue light turns off"),
+    },
+)
+
+
+
+# ---------------------------------------------------------------------------
+# Helpers
+# ---------------------------------------------------------------------------
+
+def _capitalize(text: str) -> str:
+    if not text:
+        return text
+    text = " ".join(text.split())
+    return text[0].upper() + text[1:] if len(text) > 1 else text.upper()
+
+
+def _ensure_period(text: str) -> str:
+    text = text.rstrip()
+    if text and text[-1] not in ".!?":
+        text += "."
+    return text
+
+
+def _join(*parts: str) -> str:
+    out = []
+    for p in parts:
+        p = p.strip()
+        if not p:
+            continue
+        p = _capitalize(p)
+        p = _ensure_period(p)
+        out.append(p)
+    return " ".join(out)
+
+
+def _same_literal(a: ltlnode.LTLNode, b: ltlnode.LTLNode) -> bool:
+    return (isinstance(a, ltlnode.LiteralNode) and
+            isinstance(b, ltlnode.LiteralNode) and
+            a.value == b.value)
+
+
+def _count_next(node: ltlnode.LTLNode) -> tuple[int, ltlnode.LTLNode]:
+    n = 0
+    while isinstance(node, ltlnode.NextNode):
+        n += 1
+        node = node.operand
+    return n, node
+
+
+def _steps(n: int) -> str:
+    if n == 1:
+        return "the very next step"
+    return f"{n} steps from now"
+
+
+# ---------------------------------------------------------------------------
+# Core translator
+# ---------------------------------------------------------------------------
+
+def _t(node: ltlnode.LTLNode, theme: Theme) -> str:
+    """Recursively translate *node* using *theme*.
+
+    Returns a sentence fragment (lowercase, no trailing period).
+    """
+
+    # --- Literal ---
+    if isinstance(node, ltlnode.LiteralNode):
+        return theme.positive(node.value)
+
+    # --- Not ---
+    if isinstance(node, ltlnode.NotNode):
+        return _t_not(node, theme)
+
+    # --- And ---
+    if isinstance(node, ltlnode.AndNode):
+        return _t_and(node, theme)
+
+    # --- Or ---
+    if isinstance(node, ltlnode.OrNode):
+        return _t_or(node, theme)
+
+    # --- Implies ---
+    if isinstance(node, ltlnode.ImpliesNode):
+        return _t_implies(node, theme)
+
+    # --- Equivalence ---
+    if isinstance(node, ltlnode.EquivalenceNode):
+        return _t_equiv(node, theme)
+
+    # --- Globally ---
+    if isinstance(node, ltlnode.GloballyNode):
+        return _t_globally(node, theme)
+
+    # --- Finally ---
+    if isinstance(node, ltlnode.FinallyNode):
+        return _t_finally(node, theme)
+
+    # --- Next ---
+    if isinstance(node, ltlnode.NextNode):
+        return _t_next(node, theme)
+
+    # --- Until ---
+    if isinstance(node, ltlnode.UntilNode):
+        return _t_until(node, theme)
+
+    return str(node)
+
+
+# --- NOT ------------------------------------------------------------------
+
+def _t_not(node: ltlnode.NotNode, theme: Theme) -> str:
+    inner = node.operand
+
+    if isinstance(inner, ltlnode.LiteralNode):
+        return theme.negative(inner.value)
+
+    # !(F p) -> never
+    if isinstance(inner, ltlnode.FinallyNode) and isinstance(inner.operand, ltlnode.LiteralNode):
+        return f"it is never the case that {theme.positive(inner.operand.value)}"
+
+    # !!p
+    if isinstance(inner, ltlnode.NotNode):
+        return _t(inner.operand, theme)
+
+    # !(p & q) -> not both
+    if isinstance(inner, ltlnode.AndNode):
+        return f"it is not the case that both {_t(inner.left, theme)} and {_t(inner.right, theme)}"
+
+    # !(p | q) -> neither/nor
+    if isinstance(inner, ltlnode.OrNode):
+        return f"neither {_t(inner.left, theme)} nor {_t(inner.right, theme)}"
+
+    # !(p -> q)
+    if isinstance(inner, ltlnode.ImpliesNode):
+        left_text = _t(inner.left, theme)
+        if isinstance(inner.right, ltlnode.LiteralNode):
+            right_text = theme.negative(inner.right.value)
+        else:
+            right_text = f"not {_t(inner.right, theme)}"
+        return f"{left_text}, but {right_text}"
+
+    return f"it is not the case that {_t(inner, theme)}"
+
+
+# --- AND ------------------------------------------------------------------
+
+def _t_and(node: ltlnode.AndNode, theme: Theme) -> str:
+    # !p & !q -> neither/nor
+    if isinstance(node.left, ltlnode.NotNode) and isinstance(node.right, ltlnode.NotNode):
+        ll = node.left.operand
+        rr = node.right.operand
+        if isinstance(ll, ltlnode.LiteralNode) and isinstance(rr, ltlnode.LiteralNode):
+            return f"neither {_t(ll, theme)} nor {_t(rr, theme)}"
+    return f"both {_t(node.left, theme)} and {_t(node.right, theme)}"
+
+
+# --- OR -------------------------------------------------------------------
+
+def _t_or(node: ltlnode.OrNode, theme: Theme) -> str:
+    # !p | !q -> not both
+    if isinstance(node.left, ltlnode.NotNode) and isinstance(node.right, ltlnode.NotNode):
+        ll = node.left.operand
+        rr = node.right.operand
+        if isinstance(ll, ltlnode.LiteralNode) and isinstance(rr, ltlnode.LiteralNode):
+            return f"it cannot be the case that both {_t(ll, theme)} and {_t(rr, theme)}"
+    return f"either {_t(node.left, theme)} or {_t(node.right, theme)}"
+
+
+# --- IMPLIES --------------------------------------------------------------
+
+def _t_implies(node: ltlnode.ImpliesNode, theme: Theme) -> str:
+    # (p & q) -> r
+    if isinstance(node.left, ltlnode.AndNode):
+        r = _t(node.right, theme)
+        return f"if both {_t(node.left.left, theme)} and {_t(node.left.right, theme)}, then {r}"
+
+    # (p | q) -> r
+    if isinstance(node.left, ltlnode.OrNode):
+        r = _t(node.right, theme)
+        return f"if either {_t(node.left.left, theme)} or {_t(node.left.right, theme)}, then {r}"
+
+    return f"if {_t(node.left, theme)}, then {_t(node.right, theme)}"
+
+
+# --- EQUIVALENCE ----------------------------------------------------------
+
+def _t_equiv(node: ltlnode.EquivalenceNode, theme: Theme) -> str:
+    return f"{_t(node.left, theme)} exactly when {_t(node.right, theme)}"
+
+
+# --- GLOBALLY -------------------------------------------------------------
+
+def _t_globally(node: ltlnode.GloballyNode, theme: Theme) -> str:
+    inner = node.operand
+
+    # G(!p) -> never
+    if isinstance(inner, ltlnode.NotNode):
+        negated = inner.operand
+        if isinstance(negated, ltlnode.LiteralNode):
+            return f"it is never the case that {theme.positive(negated.value)}"
+        return f"at no point may it be the case that {_t(negated, theme)}"
+
+    # G(p -> ...) patterns
+    if isinstance(inner, ltlnode.ImpliesNode):
+        left = inner.left
+        right = inner.right
+
+        # G(p -> X p) or G(p -> G p) — persistence
+        if isinstance(right, (ltlnode.NextNode, ltlnode.GloballyNode)):
+            if _same_literal(left, right.operand):
+                lit = left.value
+                return f"once {theme.event_on(lit)}, it stays that way forever"
+
+        # G(p -> F q) — response
+        if isinstance(right, ltlnode.FinallyNode):
+            if isinstance(left, ltlnode.UntilNode):
+                p = _t(left.left, theme)
+                q = _t(left.right, theme)
+                r = _t(right.operand, theme)
+                return _join(
+                    f"suppose {p} continues until {q}",
+                    f"then eventually, {r}",
+                    "this rule applies every time",
+                )
+            trigger = theme.event_on(left.value) if isinstance(left, ltlnode.LiteralNode) else _t(left, theme)
+            response = theme.positive(right.operand.value) if isinstance(right.operand, ltlnode.LiteralNode) else _t(right.operand, theme)
+            return f"whenever {trigger}, then eventually {response}"
+
+        # G(p -> X(F q)) — bounded response
+        if isinstance(right, ltlnode.NextNode) and isinstance(right.operand, ltlnode.FinallyNode):
+            trigger = theme.event_on(left.value) if isinstance(left, ltlnode.LiteralNode) else _t(left, theme)
+            response = theme.positive(right.operand.operand.value) if isinstance(right.operand.operand, ltlnode.LiteralNode) else _t(right.operand.operand, theme)
+            return f"whenever {trigger}, starting from the very next step, eventually {response}"
+
+        # G(p -> X q) — immediate response
+        if isinstance(right, ltlnode.NextNode):
+            trigger = theme.event_on(left.value) if isinstance(left, ltlnode.LiteralNode) else _t(left, theme)
+            response = _t(right.operand, theme)
+            return f"whenever {trigger}, then {response} in the very next step"
+
+        # G(p -> (q U r)) — chain precedence
+        if isinstance(right, ltlnode.UntilNode):
+            trigger = theme.event_on(left.value) if isinstance(left, ltlnode.LiteralNode) else _t(left, theme)
+            held = _t(right.left, theme)
+            goal = _t(right.right, theme)
+            return f"whenever {trigger}, it must remain the case that {held} until {goal}"
+
+        # G(p -> (F q & F r)) — chain response
+        if (isinstance(right, ltlnode.AndNode)
+                and isinstance(right.left, ltlnode.FinallyNode)
+                and isinstance(right.right, ltlnode.FinallyNode)):
+            trigger = theme.event_on(left.value) if isinstance(left, ltlnode.LiteralNode) else _t(left, theme)
+            ra = theme.event_on(right.left.operand.value) if isinstance(right.left.operand, ltlnode.LiteralNode) else _t(right.left.operand, theme)
+            rb = theme.event_on(right.right.operand.value) if isinstance(right.right.operand, ltlnode.LiteralNode) else _t(right.right.operand, theme)
+            return f"whenever {trigger}, two things must eventually happen: {ra}, and {rb}"
+
+        # G(p -> q) — generic
+        trigger = theme.event_on(left.value) if isinstance(left, ltlnode.LiteralNode) else _t(left, theme)
+        consequence = _t(right, theme)
+        return f"whenever {trigger}, it must be the case that {consequence}"
+
+    # G(F p) — recurrence
+    if isinstance(inner, ltlnode.FinallyNode):
+        fi = inner.operand
+        if isinstance(fi, ltlnode.AndNode):
+            return f"it must keep being the case, over and over forever, that {_t(fi.left, theme)} and {_t(fi.right, theme)}"
+        if isinstance(fi, ltlnode.LiteralNode):
+            return f"{theme.event_on(fi.value)} must keep happening over and over, forever"
+        target = _t(fi, theme)
+        return f"it must keep being the case, over and over forever, that {target}"
+
+    # G(G(...)) — idempotent
+    if isinstance(inner, ltlnode.GloballyNode):
+        return _t_globally(inner, theme)
+
+    # G(p & q) / G(p | q)
+    if isinstance(inner, ltlnode.AndNode):
+        return f"at every moment, {_t(inner.left, theme)} and {_t(inner.right, theme)}"
+    if isinstance(inner, ltlnode.OrNode):
+        return f"at every moment, either {_t(inner.left, theme)} or {_t(inner.right, theme)}"
+
+    # G(literal)
+    if isinstance(inner, ltlnode.LiteralNode):
+        return f"{theme.positive(inner.value)} at all times"
+    return f"at all times, {_t(inner, theme)}"
+
+
+# --- FINALLY --------------------------------------------------------------
+
+def _t_finally(node: ltlnode.FinallyNode, theme: Theme) -> str:
+    inner = node.operand
+
+    # F(F(...)) — idempotent
+    if isinstance(inner, ltlnode.FinallyNode):
+        return _t_finally(inner, theme)
+
+    # F(G(...)) patterns
+    if isinstance(inner, ltlnode.GloballyNode):
+        gi = inner.operand
+
+        # F(G(!p))
+        if isinstance(gi, ltlnode.NotNode) and isinstance(gi.operand, ltlnode.LiteralNode):
+            return _join(
+                f"eventually, {theme.event_off(gi.operand.value)}",
+                f"and from that point on, {theme.event_on(gi.operand.value)} never happens again",
+            )
+
+        # F(G(p -> F q))
+        if isinstance(gi, ltlnode.ImpliesNode) and isinstance(gi.right, ltlnode.FinallyNode):
+            trigger = theme.event_on(gi.left.value) if isinstance(gi.left, ltlnode.LiteralNode) else _t(gi.left, theme)
+            response = theme.positive(gi.right.operand.value) if isinstance(gi.right.operand, ltlnode.LiteralNode) else _t(gi.right.operand, theme)
+            return _join(
+                "eventually, the system stabilizes",
+                f"from that point on, whenever {trigger}, then eventually {response}",
+            )
+
+        # F(G(p & q))
+        if isinstance(gi, ltlnode.AndNode):
+            return f"eventually, {_t(gi.left, theme)} and {_t(gi.right, theme)}, and they stay that way forever"
+
+        # F(G p) — generic persistence
+        target = _t(gi, theme)
+        return f"eventually, {target}, and it stays that way forever"
+
+    # F(!p)
+    if isinstance(inner, ltlnode.NotNode) and isinstance(inner.operand, ltlnode.LiteralNode):
+        return f"eventually, {theme.event_off(inner.operand.value)}"
+
+    # F(p & G q) / F(G q & p) — persistence after trigger
+    if isinstance(inner, ltlnode.AndNode):
+        l, r = inner.left, inner.right
+        if isinstance(r, ltlnode.GloballyNode):
+            trigger = _t(l, theme)
+            persist = _t(r.operand, theme)
+            return _join(f"eventually, {trigger}", f"from that point on, {persist} forever")
+        if isinstance(l, ltlnode.GloballyNode):
+            trigger = _t(r, theme)
+            persist = _t(l.operand, theme)
+            return _join(f"eventually, {trigger}", f"from that point on, {persist} forever")
+        return f"eventually, {_t(l, theme)} and {_t(r, theme)} at the same time"
+
+    # F(p -> G q) — trigger to permanence
+    if isinstance(inner, ltlnode.ImpliesNode) and isinstance(inner.right, ltlnode.GloballyNode):
+        trigger = theme.event_on(inner.left.value) if isinstance(inner.left, ltlnode.LiteralNode) else _t(inner.left, theme)
+        result = _t(inner.right.operand, theme)
+        return f"eventually, once {trigger}, then {result} forever after"
+
+    # F(literal)
+    if isinstance(inner, ltlnode.LiteralNode):
+        return f"eventually, {theme.event_on(inner.value)}"
+
+    return f"eventually, {_t(inner, theme)}"
+
+
+# --- NEXT -----------------------------------------------------------------
+
+def _t_next(node: ltlnode.NextNode, theme: Theme) -> str:
+    steps, core = _count_next(node)
+
+    if steps == 1 and isinstance(core, ltlnode.UntilNode):
+        l = _t(core.left, theme)
+        r = _t(core.right, theme)
+        return f"starting from the next step, {l} until {r}"
+
+    if steps == 1 and isinstance(core, ltlnode.FinallyNode):
+        target = _t(core.operand, theme)
+        return f"starting from the next step, {target} must eventually happen"
+
+    target = _t(core, theme)
+    return f"in {_steps(steps)}, {target}"
+
+
+# --- UNTIL ----------------------------------------------------------------
+
+def _t_until(node: ltlnode.UntilNode, theme: Theme) -> str:
+    l_node, r_node = node.left, node.right
+
+    # (G p) U (F q)
+    if isinstance(l_node, ltlnode.GloballyNode) and isinstance(r_node, ltlnode.FinallyNode):
+        l = _t(l_node.operand, theme)
+        r_event = theme.event_on(r_node.operand.value) if isinstance(r_node.operand, ltlnode.LiteralNode) else _t(r_node.operand, theme)
+        return _join(
+            f"it must stay the case that {l}",
+            f"this continues until eventually {r_event}",
+        )
+
+    # (p U q) U r
+    if isinstance(l_node, ltlnode.UntilNode):
+        p = _t(l_node.left, theme)
+        q = _t(l_node.right, theme)
+        r = _t(r_node, theme)
+        return _join(
+            f"first, {p} continues until {q}",
+            f"that whole phase lasts until {r}",
+        )
+
+    l = _t(l_node, theme)
+    r = _t(r_node, theme)
+    return f"{l} must continue until {r}"
+
+
+# ---------------------------------------------------------------------------
+# Public API
+# ---------------------------------------------------------------------------
+
+def translate(node: ltlnode.LTLNode, theme: Optional[Theme] = None) -> str:
+    """Translate an LTL AST node into contextualized English.
+
+    Args:
+        node:  LTL formula AST node.
+        theme: A Theme mapping literals to concrete descriptions.
+               Defaults to the "lights" theme (red/green/blue lights).
+
+    Returns:
+        A capitalized, period-terminated English paragraph.
+    """
+    if theme is None:
+        theme = THEMES["lights"]
+
+    raw = _t(node, theme)
+    raw = raw.strip()
+    result = _capitalize(raw)
+    if result and result[-1] not in ".!?":
+        result += "."
+    return result
diff --git a/src/ltltoeng_prose.py b/src/ltltoeng_prose.py
new file mode 100644
index 0000000..cbd5fd6
--- /dev/null
+++ b/src/ltltoeng_prose.py
@@ -0,0 +1,578 @@
+"""
+Clause-chaining prose translator for LTL formulas.
+
+Produces flowing, natural prose that reads like a paragraph from a
+requirements document.  A single LTL formula may become multiple short
+sentences connected by discourse connectives ("After that point, ...",
+"Suppose that ...", "This applies every time ...").
+
+Public API
+----------
+    translate(node) -> str
+
+``node`` is any ``ltlnode.LTLNode`` produced by ``parse_ltl_string``.
+"""
+
+from __future__ import annotations
+
+import ltlnode
+
+
+# ---------------------------------------------------------------------------
+# Helpers
+# ---------------------------------------------------------------------------
+
+def _lit(node: ltlnode.LTLNode) -> str:
+    """Return the quoted literal value, e.g. ``'p'``."""
+    if isinstance(node, ltlnode.LiteralNode):
+        return f"'{node.value}'"
+    # Fallback: translate the subtree inline.
+    return _inner(node, _Ctx())
+
+
+def _is_lit(node: ltlnode.LTLNode) -> bool:
+    return isinstance(node, ltlnode.LiteralNode)
+
+
+def _same_literal(a: ltlnode.LTLNode, b: ltlnode.LTLNode) -> bool:
+    """True when *a* and *b* are LiteralNodes with identical value."""
+    return (_is_lit(a) and _is_lit(b) and a.value == b.value)
+
+
+def _capitalize(text: str) -> str:
+    """Capitalize the first letter, but leave quoted literals alone."""
+    if not text:
+        return text
+    text = " ".join(text.split())  # collapse whitespace
+    if text[0] == "'":
+        return text
+    return text[0].upper() + text[1:]
+
+
+def _ensure_period(text: str) -> str:
+    """Ensure *text* ends with exactly one period."""
+    text = text.rstrip()
+    if text and text[-1] not in ".!?":
+        text += "."
+    return text
+
+
+def _join_sentences(*parts: str) -> str:
+    """Join sentence fragments, capitalizing and adding periods."""
+    out: list[str] = []
+    for p in parts:
+        p = p.strip()
+        if not p:
+            continue
+        p = _capitalize(p)
+        p = _ensure_period(p)
+        out.append(p)
+    return " ".join(out)
+
+
+# ---------------------------------------------------------------------------
+# Translation context
+# ---------------------------------------------------------------------------
+
+class _Ctx:
+    """Tracks the temporal frame the translator is currently inside.
+
+    *frame* is one of:
+        ``"top"``      -- outermost level, no enclosing temporal operator
+        ``"globally"`` -- inside a G(...)
+        ``"finally"``  -- inside an F(...)
+        ``"next"``     -- inside an X(...)
+        ``"until"``    -- inside a U(...)
+    """
+
+    __slots__ = ("frame", "inline")
+
+    def __init__(self, frame: str = "top", inline: bool = False):
+        self.frame = frame
+        # When *inline* is True the caller wants a short fragment that can be
+        # embedded inside another sentence (no leading capital, no trailing
+        # period, no discourse connectives).
+        self.inline = inline
+
+    def child(self, frame: str | None = None, *, inline: bool | None = None) -> "_Ctx":
+        return _Ctx(
+            frame=frame if frame is not None else self.frame,
+            inline=inline if inline is not None else self.inline,
+        )
+
+
+# ---------------------------------------------------------------------------
+# Complexity heuristic
+# ---------------------------------------------------------------------------
+
+def _depth(node: ltlnode.LTLNode) -> int:
+    """Return the AST depth (leaves = 0)."""
+    if _is_lit(node):
+        return 0
+    if isinstance(node, ltlnode.UnaryOperatorNode):
+        return 1 + _depth(node.operand)
+    if isinstance(node, ltlnode.BinaryOperatorNode):
+        return 1 + max(_depth(node.left), _depth(node.right))
+    return 0
+
+
+def _is_simple(node: ltlnode.LTLNode) -> bool:
+    """True for nodes simple enough to translate as one inline clause."""
+    return _depth(node) <= 1
+
+
+# ---------------------------------------------------------------------------
+# Core recursive translator
+# ---------------------------------------------------------------------------
+
+def _inner(node: ltlnode.LTLNode, ctx: _Ctx) -> str:
+    """Recursively translate *node* in the given context.
+
+    Returns a **sentence fragment** (lowercase start, no trailing period)
+    unless the node is complex enough to warrant its own sentence(s), in
+    which case it returns already-joined prose.
+    """
+
+    # --- Literal -----------------------------------------------------------
+    if isinstance(node, ltlnode.LiteralNode):
+        return f"'{node.value}'"
+
+    # --- Not ---------------------------------------------------------------
+    if isinstance(node, ltlnode.NotNode):
+        return _translate_not(node, ctx)
+
+    # --- And / Or ----------------------------------------------------------
+    if isinstance(node, ltlnode.AndNode):
+        return _translate_and(node, ctx)
+    if isinstance(node, ltlnode.OrNode):
+        return _translate_or(node, ctx)
+
+    # --- Implies -----------------------------------------------------------
+    if isinstance(node, ltlnode.ImpliesNode):
+        return _translate_implies(node, ctx)
+
+    # --- Equivalence -------------------------------------------------------
+    if isinstance(node, ltlnode.EquivalenceNode):
+        return _translate_equivalence(node, ctx)
+
+    # --- Globally ----------------------------------------------------------
+    if isinstance(node, ltlnode.GloballyNode):
+        return _translate_globally(node, ctx)
+
+    # --- Finally -----------------------------------------------------------
+    if isinstance(node, ltlnode.FinallyNode):
+        return _translate_finally(node, ctx)
+
+    # --- Next --------------------------------------------------------------
+    if isinstance(node, ltlnode.NextNode):
+        return _translate_next(node, ctx)
+
+    # --- Until -------------------------------------------------------------
+    if isinstance(node, ltlnode.UntilNode):
+        return _translate_until(node, ctx)
+
+    # Fallback: use the node's own __str__
+    return str(node)
+
+
+# ---------------------------------------------------------------------------
+# Operator translators
+# ---------------------------------------------------------------------------
+
+# --- NOT ------------------------------------------------------------------
+
+def _translate_not(node: ltlnode.NotNode, ctx: _Ctx) -> str:
+    inner = node.operand
+
+    # !(F p) => "'p' never occurs."
+    if isinstance(inner, ltlnode.FinallyNode):
+        target = _inner(inner.operand, ctx.child(inline=True))
+        return f"{target} never occurs"
+
+    # !(G p) => "it is not always the case that 'p' holds"
+    if isinstance(inner, ltlnode.GloballyNode):
+        target = _inner(inner.operand, ctx.child(inline=True))
+        return f"it is not always the case that {target} holds"
+
+    # !!p => p  (double negation)
+    if isinstance(inner, ltlnode.NotNode):
+        return _inner(inner.operand, ctx)
+
+    # !(p & q) => De Morgan
+    if isinstance(inner, ltlnode.AndNode):
+        l = _inner(inner.left, ctx.child(inline=True))
+        r = _inner(inner.right, ctx.child(inline=True))
+        return f"not both {l} and {r}"
+
+    # !(p | q) => De Morgan
+    if isinstance(inner, ltlnode.OrNode):
+        l = _inner(inner.left, ctx.child(inline=True))
+        r = _inner(inner.right, ctx.child(inline=True))
+        return f"neither {l} nor {r}"
+
+    # !(p -> q)
+    if isinstance(inner, ltlnode.ImpliesNode):
+        l = _inner(inner.left, ctx.child(inline=True))
+        r = _inner(inner.right, ctx.child(inline=True))
+        return f"{l} holds, but {r} does not"
+
+    # Generic negation
+    if _is_lit(inner):
+        return f"'{inner.value}' does not hold"
+    target = _inner(inner, ctx.child(inline=True))
+    return f"it is not the case that {target}"
+
+
+# --- AND ------------------------------------------------------------------
+
+def _translate_and(node: ltlnode.AndNode, ctx: _Ctx) -> str:
+    # !p & !q  => neither ... nor
+    if isinstance(node.left, ltlnode.NotNode) and isinstance(node.right, ltlnode.NotNode):
+        ll = _inner(node.left.operand, ctx.child(inline=True))
+        rr = _inner(node.right.operand, ctx.child(inline=True))
+        return f"neither {ll} nor {rr}"
+
+    l = _inner(node.left, ctx.child(inline=True))
+    r = _inner(node.right, ctx.child(inline=True))
+    return f"both {l} and {r}"
+
+
+# --- OR -------------------------------------------------------------------
+
+def _translate_or(node: ltlnode.OrNode, ctx: _Ctx) -> str:
+    # !p | !q  => not both ... and
+    if isinstance(node.left, ltlnode.NotNode) and isinstance(node.right, ltlnode.NotNode):
+        ll = _inner(node.left.operand, ctx.child(inline=True))
+        rr = _inner(node.right.operand, ctx.child(inline=True))
+        return f"not both {ll} and {rr}"
+
+    l = _inner(node.left, ctx.child(inline=True))
+    r = _inner(node.right, ctx.child(inline=True))
+    return f"either {l} or {r}"
+
+
+# --- IMPLIES --------------------------------------------------------------
+
+def _translate_implies(node: ltlnode.ImpliesNode, ctx: _Ctx) -> str:
+    l = _inner(node.left, ctx.child(inline=True))
+    r = _inner(node.right, ctx.child(inline=True))
+
+    # p -> !q  (exclusion)
+    if isinstance(node.right, ltlnode.NotNode):
+        rr = _inner(node.right.operand, ctx.child(inline=True))
+        if _is_lit(node.left) and _is_lit(node.right.operand):
+            return f"{l} excludes {rr}"
+        return f"if {l} holds, then {rr} does not"
+
+    # !p -> q  (unless)
+    if isinstance(node.left, ltlnode.NotNode):
+        ll = _inner(node.left.operand, ctx.child(inline=True))
+        return f"{r} unless {ll}"
+
+    # (p & q) -> r
+    if isinstance(node.left, ltlnode.AndNode):
+        pl = _inner(node.left.left, ctx.child(inline=True))
+        pr = _inner(node.left.right, ctx.child(inline=True))
+        return f"if both {pl} and {pr}, then {r}"
+
+    # (p | q) -> r
+    if isinstance(node.left, ltlnode.OrNode):
+        pl = _inner(node.left.left, ctx.child(inline=True))
+        pr = _inner(node.left.right, ctx.child(inline=True))
+        return f"if either {pl} or {pr}, then {r}"
+
+    # p -> (q & r)
+    if isinstance(node.right, ltlnode.AndNode):
+        rl = _inner(node.right.left, ctx.child(inline=True))
+        rr = _inner(node.right.right, ctx.child(inline=True))
+        return f"if {l} holds, then both {rl} and {rr} follow"
+
+    # p -> (q | r)
+    if isinstance(node.right, ltlnode.OrNode):
+        rl = _inner(node.right.left, ctx.child(inline=True))
+        rr = _inner(node.right.right, ctx.child(inline=True))
+        return f"if {l} holds, then either {rl} or {rr}"
+
+    return f"if {l} holds, then {r}"
+
+
+# --- EQUIVALENCE ----------------------------------------------------------
+
+def _translate_equivalence(node: ltlnode.EquivalenceNode, ctx: _Ctx) -> str:
+    l = _inner(node.left, ctx.child(inline=True))
+    r = _inner(node.right, ctx.child(inline=True))
+    return f"{l} holds exactly when {r} holds"
+
+
+# --- GLOBALLY -------------------------------------------------------------
+
+def _translate_globally(node: ltlnode.GloballyNode, ctx: _Ctx) -> str:
+    inner = node.operand
+
+    # G(!p)  => "'p' never holds."
+    if isinstance(inner, ltlnode.NotNode):
+        target = _inner(inner.operand, ctx.child("globally", inline=True))
+        return f"{target} never holds"
+
+    # G(p -> ...) patterns
+    if isinstance(inner, ltlnode.ImpliesNode):
+        left = inner.left
+        right = inner.right
+
+        # -- G(p -> X p) or G(p -> G p):  persistence
+        if isinstance(right, (ltlnode.NextNode, ltlnode.GloballyNode)):
+            rhs_inner = right.operand
+            if _same_literal(left, rhs_inner):
+                lit = _lit(left)
+                return f"once {lit} becomes true, it remains true forever"
+
+        # -- G(p -> F q):  response pattern
+        if isinstance(right, ltlnode.FinallyNode):
+            # G((p U q) -> F r)
+            if isinstance(left, ltlnode.UntilNode):
+                p = _inner(left.left, ctx.child("globally", inline=True))
+                q = _inner(left.right, ctx.child("globally", inline=True))
+                r = _inner(right.operand, ctx.child("globally", inline=True))
+                return _join_sentences(
+                    f"suppose {p} holds continuously until {q} occurs",
+                    f"then {r} must eventually follow",
+                    "this applies every time such a situation arises",
+                )
+
+            lhs = _inner(left, ctx.child("globally", inline=True))
+            rhs = _inner(right.operand, ctx.child("globally", inline=True))
+            return f"whenever {lhs} holds, {rhs} must eventually follow"
+
+        # -- G(p -> X(F q)):  bounded response
+        if isinstance(right, ltlnode.NextNode) and isinstance(right.operand, ltlnode.FinallyNode):
+            lhs = _inner(left, ctx.child("globally", inline=True))
+            rhs = _inner(right.operand.operand, ctx.child("globally", inline=True))
+            return f"whenever {lhs} holds, starting from the very next step, {rhs} is guaranteed to eventually occur"
+
+        # -- G(p -> X q):  immediate response (not same literal)
+        if isinstance(right, ltlnode.NextNode):
+            lhs = _inner(left, ctx.child("globally", inline=True))
+            rhs = _inner(right.operand, ctx.child("globally", inline=True))
+            return f"whenever {lhs} holds, {rhs} must hold in the very next step"
+
+        # -- G(p -> (q U r)):  chain precedence
+        if isinstance(right, ltlnode.UntilNode):
+            lhs = _inner(left, ctx.child("globally", inline=True))
+            ul = _inner(right.left, ctx.child("globally", inline=True))
+            ur = _inner(right.right, ctx.child("globally", inline=True))
+            return f"whenever {lhs} holds, {ul} must hold until {ur} occurs"
+
+        # -- G(p -> (F q & F r)):  chain response
+        if isinstance(right, ltlnode.AndNode):
+            if isinstance(right.left, ltlnode.FinallyNode) and isinstance(right.right, ltlnode.FinallyNode):
+                lhs = _inner(left, ctx.child("globally", inline=True))
+                rl = _inner(right.left.operand, ctx.child("globally", inline=True))
+                rr = _inner(right.right.operand, ctx.child("globally", inline=True))
+                return f"whenever {lhs} holds, both {rl} and {rr} are guaranteed to eventually occur (though not necessarily at the same time)"
+
+        # -- G(p -> q):  generic rule
+        lhs = _inner(left, ctx.child("globally", inline=True))
+        rhs = _inner(right, ctx.child("globally", inline=True))
+        return f"whenever {lhs} holds, {rhs} must also hold"
+
+    # G(F p)  => recurrence / infinitely often
+    if isinstance(inner, ltlnode.FinallyNode):
+        fi = inner.operand
+        # G(F(p & q))
+        if isinstance(fi, ltlnode.AndNode):
+            l = _inner(fi.left, ctx.child("globally", inline=True))
+            r = _inner(fi.right, ctx.child("globally", inline=True))
+            return f"both {l} and {r} must occur together infinitely often"
+        target = _inner(fi, ctx.child("globally", inline=True))
+        return f"{target} must occur infinitely often"
+
+    # G(G(...)) => idempotent
+    if isinstance(inner, ltlnode.GloballyNode):
+        return _translate_globally(inner, ctx)
+
+    # G(p & q) / G(p | q) - simple
+    if isinstance(inner, ltlnode.AndNode):
+        l = _inner(inner.left, ctx.child("globally", inline=True))
+        r = _inner(inner.right, ctx.child("globally", inline=True))
+        return f"at all times, both {l} and {r} must hold"
+
+    if isinstance(inner, ltlnode.OrNode):
+        l = _inner(inner.left, ctx.child("globally", inline=True))
+        r = _inner(inner.right, ctx.child("globally", inline=True))
+        return f"at all times, either {l} or {r} must hold"
+
+    # G(literal) or G(complex)
+    target = _inner(inner, ctx.child("globally", inline=True))
+    if _is_lit(inner):
+        return f"{target} must hold at all times"
+    return f"at all times, {target}"
+
+
+# --- FINALLY --------------------------------------------------------------
+
+def _translate_finally(node: ltlnode.FinallyNode, ctx: _Ctx) -> str:
+    inner = node.operand
+
+    # F(F(...)) => idempotent
+    if isinstance(inner, ltlnode.FinallyNode):
+        return _translate_finally(inner, ctx)
+
+    # F(G(...)) patterns
+    if isinstance(inner, ltlnode.GloballyNode):
+        gi = inner.operand
+
+        # F(G(!p))
+        if isinstance(gi, ltlnode.NotNode):
+            target = _inner(gi.operand, ctx.child("finally", inline=True))
+            return f"eventually, a point is reached after which {target} never holds again"
+
+        # F(G(p -> F q))
+        if isinstance(gi, ltlnode.ImpliesNode) and isinstance(gi.right, ltlnode.FinallyNode):
+            lhs = _inner(gi.left, ctx.child("finally", inline=True))
+            rhs = _inner(gi.right.operand, ctx.child("finally", inline=True))
+            return _join_sentences(
+                "eventually, a stable regime is reached",
+                f"after that point, whenever {lhs} holds, {rhs} must eventually follow",
+            )
+
+        # F(G(p -> q))  generic stable rule
+        if isinstance(gi, ltlnode.ImpliesNode):
+            lhs = _inner(gi.left, ctx.child("finally", inline=True))
+            rhs = _inner(gi.right, ctx.child("finally", inline=True))
+            return _join_sentences(
+                "eventually, a stable regime is reached",
+                f"after that point, whenever {lhs} holds, {rhs} must also hold",
+            )
+
+        # F(G(p & q))
+        if isinstance(gi, ltlnode.AndNode):
+            l = _inner(gi.left, ctx.child("finally", inline=True))
+            r = _inner(gi.right, ctx.child("finally", inline=True))
+            return f"eventually, both {l} and {r} become true and remain true forever"
+
+        # F(G p) generic persistence / stability
+        target = _inner(gi, ctx.child("finally", inline=True))
+        return f"eventually, {target} becomes true and remains true forever"
+
+    # F(!p)
+    if isinstance(inner, ltlnode.NotNode):
+        target = _inner(inner.operand, ctx.child("finally", inline=True))
+        return f"eventually, {target} will cease to hold"
+
+    # F(p & G q)  or  F(G q & p)  -  persistence after trigger
+    if isinstance(inner, ltlnode.AndNode):
+        l, r = inner.left, inner.right
+        if isinstance(r, ltlnode.GloballyNode):
+            trigger = _inner(l, ctx.child("finally", inline=True))
+            persist = _inner(r.operand, ctx.child("finally", inline=True))
+            return _join_sentences(
+                f"eventually, {trigger} occurs",
+                f"from that point on, {persist} holds forever",
+            )
+        if isinstance(l, ltlnode.GloballyNode):
+            trigger = _inner(r, ctx.child("finally", inline=True))
+            persist = _inner(l.operand, ctx.child("finally", inline=True))
+            return _join_sentences(
+                f"eventually, {trigger} occurs",
+                f"from that point on, {persist} holds forever",
+            )
+        # F(p & q) simple simultaneity
+        ll = _inner(l, ctx.child("finally", inline=True))
+        rr = _inner(r, ctx.child("finally", inline=True))
+        return f"eventually, both {ll} and {rr} will be true at the same time"
+
+    # F(p -> G q)  trigger-to-permanence
+    if isinstance(inner, ltlnode.ImpliesNode) and isinstance(inner.right, ltlnode.GloballyNode):
+        trigger = _inner(inner.left, ctx.child("finally", inline=True))
+        result = _inner(inner.right.operand, ctx.child("finally", inline=True))
+        return f"eventually, once {trigger} holds, {result} will hold forever after"
+
+    # F(literal)
+    if _is_lit(inner):
+        return f"{_lit(inner)} must eventually occur"
+
+    # Generic F(...)
+    target = _inner(inner, ctx.child("finally", inline=True))
+    return f"eventually, {target}"
+
+
+# --- NEXT -----------------------------------------------------------------
+
+def _count_next_chain(node: ltlnode.LTLNode) -> tuple[int, ltlnode.LTLNode]:
+    """Count consecutive X nodes; return (count, innermost operand)."""
+    n = 0
+    while isinstance(node, ltlnode.NextNode):
+        n += 1
+        node = node.operand
+    return n, node
+
+
+def _translate_next(node: ltlnode.NextNode, ctx: _Ctx) -> str:
+    steps, core = _count_next_chain(node)
+
+    # X(p U q) => "starting from the next step, ..."
+    if steps == 1 and isinstance(core, ltlnode.UntilNode):
+        l = _inner(core.left, ctx.child("next", inline=True))
+        r = _inner(core.right, ctx.child("next", inline=True))
+        return f"starting from the next step, {l} holds until {r} occurs"
+
+    # X(F q) => "starting from the next step, q must eventually occur"
+    if steps == 1 and isinstance(core, ltlnode.FinallyNode):
+        target = _inner(core.operand, ctx.child("next", inline=True))
+        return f"starting from the next step, {target} must eventually occur"
+
+    target = _inner(core, ctx.child("next", inline=True))
+
+    if steps == 1:
+        return f"in the very next step, {target}"
+    return f"in {steps} steps, {target}"
+
+
+# --- UNTIL ----------------------------------------------------------------
+
+def _translate_until(node: ltlnode.UntilNode, ctx: _Ctx) -> str:
+    l_node, r_node = node.left, node.right
+
+    # (G p) U (F q) => obligation until release
+    if isinstance(l_node, ltlnode.GloballyNode) and isinstance(r_node, ltlnode.FinallyNode):
+        l = _inner(l_node.operand, ctx.child("until", inline=True))
+        r = _inner(r_node.operand, ctx.child("until", inline=True))
+        return _join_sentences(
+            f"{l} must hold continuously at all times",
+            f"this obligation persists until {r} eventually occurs",
+        )
+
+    # (p U q) U r => nested until
+    if isinstance(l_node, ltlnode.UntilNode):
+        p = _inner(l_node.left, ctx.child("until", inline=True))
+        q = _inner(l_node.right, ctx.child("until", inline=True))
+        r = _inner(r_node, ctx.child("until", inline=True))
+        return _join_sentences(
+            f"first, {p} holds until {q} occurs",
+            f"that whole phase lasts until {r} occurs",
+        )
+
+    l = _inner(l_node, ctx.child("until", inline=True))
+    r = _inner(r_node, ctx.child("until", inline=True))
+    return f"{l} must hold until {r} occurs"
+
+
+# ---------------------------------------------------------------------------
+# Public API
+# ---------------------------------------------------------------------------
+
+def translate(node: ltlnode.LTLNode) -> str:
+    """Translate an LTL AST node into requirements-style English prose.
+
+    The returned string is a complete, capitalized, period-terminated
+    paragraph (possibly multiple sentences for complex formulas).
+    """
+    raw = _inner(node, _Ctx())
+    # If _inner already produced joined sentences (with periods inside),
+    # just ensure it's clean.
+    raw = raw.strip()
+    # Capitalize and terminate.
+    result = _capitalize(raw)
+    if result and result[-1] not in ".!?":
+        result += "."
+    return result
diff --git a/src/static/js/checkanswers.js b/src/static/js/checkanswers.js
index 4d21ba4..28c3439 100644
--- a/src/static/js/checkanswers.js
+++ b/src/static/js/checkanswers.js
@@ -292,6 +292,10 @@ async function englishtoltl_getfeedback(button) {
     let correct = show_feedback(parent_node, QUESTION_TYPE);
     lockQuestionInteractions(parent_node);
 
+    // Read A/B test condition (abstract vs. contextualized)
+    let question_text_el = parent_node.querySelector('.actualQuestion');
+    let translation_mode = question_text_el ? (question_text_el.dataset.translationMode || '') : '';
+
     let data = {
         selected_option: selected_radio.value,
         correct_option: correct_option,
@@ -300,7 +304,8 @@ async function englishtoltl_getfeedback(button) {
         question_text: question_text,
         question_options: question_options,
         formula_for_mp_class: get_formula_for_MP_Classification(parent_node, QUESTION_TYPE),
-        exercise: getExerciseName()
+        exercise: getExerciseName(),
+        translation_mode: translation_mode
     }
 
     let response = await postFeedback(data, QUESTION_TYPE);
diff --git a/src/stepper.py b/src/stepper.py
index bb17e2a..295876b 100644
--- a/src/stepper.py
+++ b/src/stepper.py
@@ -1,5 +1,5 @@
 from ltlnode import UnaryOperatorNode, BinaryOperatorNode, LiteralNode, parse_ltl_string
-import ltltoeng
+import ltltoeng_prose
 from spotutils import is_trace_satisfied
 import re
 import random
@@ -28,7 +28,7 @@ def getLTLFormulaAsString(node, syntax):
     elif syntax == "English":
         ## We should hopefully never get here. However, 
         ## I'm adding it here to suggest a way forward.
-        return ltltoeng.finalize_sentence(node.__to_english__())
+        return ltltoeng_prose.translate(node)
 
     ## Default to classic syntax
     return str(node)
diff --git a/src/templates/exercise.html b/src/templates/exercise.html
index 6200357..b80ca27 100644
--- a/src/templates/exercise.html
+++ b/src/templates/exercise.html
@@ -93,7 +93,8 @@ <h5 id="{{ qindex }}question_text" class="card-title mb-2">
                     </h5>
                     {% else %}
                     <h5 id="{{ qindex }}question_text" class="card-title mb-2 actualQuestion"
-                        style="white-space: pre-wrap;">{{ q.question}}
+                        style="white-space: pre-wrap;"
+                        data-translation-mode="{{ q.translation_mode | default('') }}">{{ q.question}}
                     </h5>
                     <div class="row mb-2 ml-2">
                         {% if q.type == "englishtoltl" %}
diff --git a/test/test_contextualized.py b/test/test_contextualized.py
new file mode 100644
index 0000000..757a3a3
--- /dev/null
+++ b/test/test_contextualized.py
@@ -0,0 +1,181 @@
+"""Test the contextualized (Wason-style) LTL translator.
+
+Run with:
+    python -m pytest test/test_contextualized.py -v -s
+"""
+
+import unittest
+import sys
+import os
+import random
+
+sys.path.insert(0, os.path.abspath(os.path.join(os.path.dirname(__file__), "../src")))
+from unittest.mock import MagicMock
+sys.modules['spot'] = MagicMock()
+
+from ltlnode import parse_ltl_string
+import ltltoeng
+import ltltoeng_prose as prose
+import ltltoeng_contextualized as ctx
+
+
+FORMULAS = [
+    # (formula, description)
+    ("G r",                   "Invariant"),
+    ("F r",                   "Liveness"),
+    ("G !r",                  "Safety / never"),
+    ("G (r -> F g)",          "Response"),
+    ("G (r -> X g)",          "Immediate response"),
+    ("G(r -> (F g & F b))",   "Chain response"),
+    ("G(r -> (g U b))",       "Chain precedence"),
+    ("F (G r)",               "Persistence"),
+    ("G (F r)",               "Recurrence"),
+    ("(G r) U (F g)",         "Obligation until release"),
+    ("G(r -> X r)",           "Once true, stays true"),
+    ("!(F r)",                "Impossibility"),
+    ("r -> g",                "Simple implication"),
+    ("G(r -> X(F g))",        "Bounded response"),
+    ("F(G(r -> F g))",        "Eventual stable response"),
+    ("G((r U g) -> F b)",     "Until-triggered response"),
+    ("!(r & g)",              "Mutual exclusion"),
+]
+
+
+class TestContextualizedPrintComparison(unittest.TestCase):
+    """Print abstract vs. contextualized (lights) translations."""
+
+    def setUp(self):
+        random.seed(42)
+
+    def test_print_all_themes(self):
+        print("\n" + "=" * 110)
+        print("ABSTRACT vs. CONTEXTUALIZED TRANSLATIONS  (Wason-style)")
+        print("=" * 110)
+
+        for formula_str, desc in FORMULAS:
+            random.seed(42)
+            abstract = prose.translate(parse_ltl_string(formula_str))
+            lights   = ctx.translate(parse_ltl_string(formula_str), ctx.THEMES["lights"])
+
+            print(f"\n{'─' * 110}")
+            print(f"  {formula_str:30s}  ({desc})")
+            print(f"{'─' * 110}")
+            print(f"  Abstract:  {abstract}")
+            print(f"  Lights:    {lights}")
+
+        print("\n" + "=" * 110)
+
+
+class TestLightsTheme(unittest.TestCase):
+    """Verify the lights theme produces concrete, accurate translations."""
+
+    def setUp(self):
+        random.seed(42)
+        self.theme = ctx.THEMES["lights"]
+
+    def _tr(self, formula):
+        return ctx.translate(parse_ltl_string(formula), self.theme)
+
+    def test_globally_literal(self):
+        result = self._tr("G r")
+        self.assertIn("red light", result.lower())
+        self.assertIn("all times", result.lower())
+
+    def test_finally_literal(self):
+        result = self._tr("F r")
+        self.assertIn("red light", result.lower())
+        self.assertIn("eventually", result.lower())
+
+    def test_never(self):
+        result = self._tr("G !r")
+        self.assertIn("red light", result.lower())
+        self.assertIn("never", result.lower())
+
+    def test_response_uses_event_form(self):
+        """G(r -> F g) should use 'turns on' not just 'is on'."""
+        result = self._tr("G(r -> F g)")
+        self.assertIn("red light turns on", result.lower())
+        self.assertIn("green light", result.lower())
+        self.assertIn("eventually", result.lower())
+
+    def test_immediate_response(self):
+        result = self._tr("G(r -> X g)")
+        self.assertIn("red light turns on", result.lower())
+        self.assertIn("green light", result.lower())
+        self.assertIn("next step", result.lower())
+
+    def test_chain_response_mentions_both(self):
+        result = self._tr("G(r -> (F g & F b))")
+        self.assertIn("red light", result.lower())
+        self.assertIn("green light", result.lower())
+        self.assertIn("blue light", result.lower())
+
+    def test_persistence(self):
+        result = self._tr("G(r -> X r)")
+        self.assertIn("red light", result.lower())
+        self.assertIn("forever", result.lower())
+
+    def test_recurrence(self):
+        result = self._tr("G(F r)")
+        self.assertIn("red light", result.lower())
+        self.assertIn("over and over", result.lower())
+
+    def test_mutual_exclusion(self):
+        result = self._tr("!(r & g)")
+        self.assertIn("red light", result.lower())
+        self.assertIn("green light", result.lower())
+
+    def test_all_end_with_period(self):
+        for formula_str, _ in FORMULAS:
+            result = self._tr(formula_str)
+            self.assertTrue(result.endswith("."),
+                            f"{formula_str} => '{result}' missing period")
+
+    def test_all_start_capitalized(self):
+        for formula_str, _ in FORMULAS:
+            result = self._tr(formula_str)
+            self.assertTrue(result[0].isupper(),
+                            f"{formula_str} => '{result}' not capitalized")
+
+    def test_no_abstract_quotes(self):
+        """Contextualized output should never contain raw quoted literals."""
+        for formula_str, _ in FORMULAS:
+            result = self._tr(formula_str)
+            for lit in ["'r'", "'g'", "'b'"]:
+                self.assertNotIn(lit, result,
+                                 f"{formula_str} => still has abstract literal {lit}: {result}")
+
+
+class TestCustomTheme(unittest.TestCase):
+    """Verify that custom themes work correctly."""
+
+    def test_custom_theme(self):
+        elevator = ctx.Theme(
+            name="Elevator",
+            description="An elevator system",
+            literals={
+                "d": ("the door is open",       "the door is closed"),
+                "m": ("the elevator is moving",  "the elevator is stopped"),
+            },
+            event_form={
+                "d": ("the door opens",           "the door closes"),
+                "m": ("the elevator starts moving", "the elevator stops"),
+            },
+        )
+
+        # Safety: door must never be open while moving
+        node = parse_ltl_string("G(m -> !d)")
+        result = ctx.translate(node, elevator)
+        self.assertIn("elevator", result.lower())
+        self.assertIn("door", result.lower())
+
+        # Response: if door opens, elevator must eventually move
+        node = parse_ltl_string("G(d -> F m)")
+        result = ctx.translate(node, elevator)
+        self.assertIn("door opens", result.lower())
+        self.assertIn("elevator", result.lower())
+        self.assertIn("eventually", result.lower())
+
+
+if __name__ == "__main__":
+    unittest.main()