Simplify randltl exercise formulas within the tutor grammar#173
Open
sidprasad wants to merge 2 commits into
Open
Simplify randltl exercise formulas within the tutor grammar#173sidprasad wants to merge 2 commits into
sidprasad wants to merge 2 commits into
Conversation
randltl freely emits redundant nestings like 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 and rewrites the operators
the simplifier introduces but the tutor grammar lacks (W/M/R/xor) back
into the supported set via exact identities, chosen over SPOT's
unabbreviate() because its chained R->W->U expansion can triple
subterms. The R identity is the exact inverse of the simplifier's
negated-until normalization, so !(a U b) shapes survive unchanged.
Constants are skipped and redrawn.
Also pass a random seed to spot.randltl: the default seed is 0 and a
fresh generator was built per call, so every call with the same
atoms/tree-size returned the identical formula sequence (same exercise
pool per complexity band, constant template subformulas). And document
that SPOT's priority parser tokenizes the passed string buffer in
place, so the priority string must be rebuilt on every call.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Contributor
Author
|
@codex please review |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 7fed150d75
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Skipped constants and generator exhaustion could leave gen_rand_ltl returning fewer than num_formulae. Reseed a fresh generator when the unique-formula space at the given tree size runs out (duplicates across generators are fine — callers ask for a pool, not a set), bounded by a generous draw budget for pathologically tiny spaces. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Random exercise formulas from SPOT's
randltlare now simplified before becoming questions, without ever leaving the tutor's operator set (X F G U & | ! -> <->).Why
randltlfreely emits redundant nestings such asF G F G d(≡F G d), which rendered as absurd English in english-to-LTL questions:How
gen_rand_ltlgenerates withsimplify=3(randltl's own CLI default level), collapsing redundant nestings likeFGFG d → FG d.W/M/R/xor— e.g.!(a U b) → !a R !b). These are rewritten back via exact identities instead of SPOT'sunabbreviate(), whose chainedR→W→Uexpansion can triple subterms:a R b ≡ !(!a U !b)— the exact inverse of the negated-until normalization, so!(a U b)shapes survive simplification verbatim rather than being lost from the poola W b ≡ (a U b) | G a,a M b ≡ b U (a & b),a xor b ≡ !(a <-> b)1/0) are skipped and redrawn to fill the batch.gen_rand_ltlnow passes a random seed tospot.randltl. Previously the default seed (0) plus a fresh generator per call meant 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.Reviewer notes
'ap\x005\x00G\x00…'). The code is only safe becauseto_priority_stringbuilds a fresh string per call — that string must never be hoisted into a shared constant.W/M/R/xorin any output, negated-until shapes present (~9%), and no size blowups (avg 21 chars, max 123).Version bumped to 2.1.3 with changelog entries.