Simplify randltl exercise formulas within the tutor grammar

CHANGELOG.md

@@ -3,6 +3,8 @@
 This document summarizes notable updates since February 2025, with commit dates from the repository history for context.【728428†L1-L48】
 
 ## 2026-07
+- **Bugfix (2.1.6):** Randomly generated exercise formulas are now simplified before becoming questions. SPOT's `randltl` freely emits redundant nestings such as `F G F G d` (≡ `F G d`), which rendered as absurd English ("Eventually, eventually, the document is open, and it stays that way forever, and it stays that way forever"). `gen_rand_ltl` now generates with `simplify=3`. Because the simplifier normalizes into operators outside the tutor grammar (`W`/`M`/`R`/`xor` — e.g. `!(a U b)` → `!a R !b`), those are rewritten back into the tutor's operator set via exact identities (`a R b ≡ !(!a U !b)`, `a W b ≡ (a U b) | G a`, `a M b ≡ b U (a & b)`, `a xor b ≡ !(a <-> b)`) rather than SPOT's `unabbreviate()`, whose chained R→W→U expansion can triple subterms; the R identity is the exact inverse of the normalization, so negated-until shapes survive simplification unchanged instead of being lost. Formulas that simplify to constants are skipped and redrawn until the requested batch is filled. Each identity is verified semantically equivalent under SPOT containment, and a 320-formula sweep parses cleanly against the tutor grammar with negated-until shapes present and no size blowups.
+- **Bugfix (2.1.6):** `gen_rand_ltl` now passes a random seed to `spot.randltl`. The default seed is 0 and a fresh generator was constructed per call, so every call with the same atoms/tree-size returned the *identical* formula sequence — the same exercise pool per complexity band, and constant "random" subformulas in misconception templates. Also documented (in `to_priority_string`) that SPOT's priority parser tokenizes the passed string buffer in place, corrupting the caller's Python string object — the string must be rebuilt fresh on every call, never hoisted into a shared constant.
 - **UX (2.1.5):** The "unclear sentence" report control on english-to-LTL questions no longer reads as a heading for the answer options. It was a bold rust question ("Is this English sentence confusing or unclear?") sitting an equal distance from the stem above and the radio list below, so it grouped with neither; its `.row.ml-2` wrapper also pulled it left of the stem's text edge, since Bootstrap's `.row` sets `margin-left: -15px` and `ml-2` only partly cancels it. It is now a quiet caption-style link reading "Report unclear wording" (imperative, so it cannot be mistaken for the question to answer), tucked under the sentence with asymmetric spacing (about 4px above, 18px below) that groups it with the stem. Being quiet means losing the color signal, so it carries a permanent underline rather than color alone (WCAG 1.4.1), and uses `--ink-2` at 8:1 rather than the muted `--ink-3`, which is 4.17:1 on the card and under AA for small text; color returns on hover and focus. The control stays a sibling of `.actualQuestion`, so its label never leaks into the logged `question_text`. The modal, its route, and its payload are unchanged.
 - **A11y (2.1.5):** The keyboard focus ring now actually appears on that control. The theme's global ring is a zero-specificity `:where(...):focus-visible` rule, which Bootstrap's `.btn:focus { outline: 0 }` outranks on any button, so the only focus signal would have been a color shift; `.btn.unclear-flag:focus-visible` restates it at (0,3,0). The letter key also uses `--ink-2` (8:1) rather than `text-muted` (`--ink-3`, 4.17:1 on the card, under AA at that size), since the key is the only place the letters in the options are defined. The rest of the page still pairs `text-muted` with `small` at that sub-AA ratio (card-header meta, question description); that is pre-existing and wants its own pass.
 - **Bugfix (2.1.4):** Themed english-to-LTL questions now state what their letters mean. The sentence was in words ("the document is open") while every answer option was in letters (`d`, `c`), and nothing connected the two, so a student also had to guess that `d` names the document being *open*, not the document, which has more than one state. Each themed question now carries a key listing only the literals its formula uses (`d`: the document is open), rendered above the sentence. Themed responses logged before this fix measured LTL reading confounded with guessing the naming, and both themed arms are affected; per-arm analyses spanning the change should be segmented. The abstract control arm is untouched, since it quotes its literals in the prose already and there is nothing to look up.

src/spotutils.py

@@ -169,17 +169,91 @@ def generate_traces(f_accepted, f_rejected, max_traces=5):
 ### Some are obvious : Implicit G means, add more G
 ### Some are less obvious: eg "BadStateIndex"
 
+# Operators outside the tutor's grammar (ltl.g4).  randltl never emits them
+# (their priorities are zeroed), but SPOT's simplifier can introduce them,
+# e.g. !(a U b) -> !a R !b.
+_NON_GRAMMAR_OPS = (spot.op_W, spot.op_M, spot.op_R, spot.op_Xor)
+
+
+def _in_tutor_grammar(f):
+    if f.kind() in _NON_GRAMMAR_OPS:
+        return False
+    return all(_in_tutor_grammar(child) for child in f)
+
+
+def _rewrite_to_tutor_grammar(f):
+    """Rewrite W/M/R/xor into the tutor's operator set via exact identities.
+
+    These direct identities duplicate at most one operand once; SPOT's own
+    unabbreviate() instead chains R -> W -> U and can triple subterms.
+    Since R only ever arises here from the simplifier normalizing a negated
+    until, !a R !b maps straight back to !(a U b) (the formula constructors
+    cancel the double negations).
+    """
+    f = f.map(_rewrite_to_tutor_grammar)
+    kind = f.kind()
+    if kind == spot.op_R:
+        # a R b == !(!a U !b)
+        return spot.formula.Not(spot.formula.U(
+            spot.formula.Not(f[0]), spot.formula.Not(f[1])))
+    if kind == spot.op_W:
+        # a W b == (a U b) | G a
+        return spot.formula.Or([spot.formula.U(f[0], f[1]),
+                                spot.formula.G(f[0])])
+    if kind == spot.op_M:
+        # a M b == b U (a & b)
+        return spot.formula.U(f[1], spot.formula.And([f[0], f[1]]))
+    if kind == spot.op_Xor:
+        # a xor b == !(a <-> b)
+        return spot.formula.Not(spot.formula.Equiv(f[0], f[1]))
+    return f
+
+
 def gen_rand_ltl(atoms, tree_size, ltl_priorities, num_formulae = 5):
-    
+
     def to_priority_string(d):
+        # SPOT's priority parser tokenizes the string buffer in place,
+        # corrupting the Python string it was handed; always build a fresh
+        # string here rather than reusing a shared constant.
         return ','.join(f'{k}={v}' for k, v in d.items())
 
-    # Need to do the correct kind of manipulation here
-    ltl_priorities_string = to_priority_string(ltl_priorities)
-
-    f = spot.randltl(atoms, tree_size=tree_size, ltl_priorities = ltl_priorities_string)
-
-    return [str(next(f)) for _ in range(num_formulae)]
+    def new_generator():
+        # simplify=3 (randltl's own default level) rewrites away redundant
+        # nestings like F G F G d that read absurdly when rendered as English.
+        # randltl's default seed is 0, and we build a fresh generator per
+        # call, so without an explicit seed every call would yield the same
+        # sequence.  The priority string is rebuilt each time (see above).
+        return spot.randltl(atoms, tree_size=tree_size,
+                            ltl_priorities=to_priority_string(ltl_priorities),
+                            simplify=3, seed=random.randrange(2**30))
+
+    # Simplification can collapse a formula to a constant (skip those and
+    # keep drawing) or rewrite it into W/M/R/xor, which the tutor cannot
+    # parse or display (rewrite those back into the tutor's operator set).
+    # Keep drawing until the requested batch is filled; a generator only
+    # yields distinct formulas, so when it exhausts the unique-formula space
+    # at this tree size, reseed a fresh one (duplicates across generators
+    # are acceptable — callers ask for a pool, not a set).  The draw budget
+    # is a safety net against pathologically tiny formula spaces.
+    f = new_generator()
+    formulae = []
+    for _ in range(max(num_formulae * 50, 500)):
+        if len(formulae) >= num_formulae:
+            break
+        try:
+            candidate = next(f)
+        except StopIteration:
+            candidate = None
+        if candidate is None:
+            f = new_generator()
+            continue
+        if candidate.is_tt() or candidate.is_ff():
+            continue
+        candidate = _rewrite_to_tutor_grammar(candidate)
+        if not _in_tutor_grammar(candidate):
+            continue
+        formulae.append(str(candidate))
+    return formulae
 
 
 def is_trivial(formula_str):

src/templates/version.html

@@ -1 +1 @@
-2.1.5
+2.1.6