fix(tla): action constraints go through the full evaluator (LanguageFeatureMatrix) - #184
Merged
Merged
Conversation
…eatureMatrix) `eval_action_constraint` dispatched to a bespoke `eval_transition_expr` that, by its own admission, "only support[ed] simple comparisons" — it returned an error for anything that wasn't `x' <op> y`. An action constraint like `step' \in step..(step+1)` (membership over a range, mixing unprimed `step` from the pre-state and primed `step'` from the post-state) fell into the error path, which pruned every successor: LanguageFeatureMatrix explored 1 state where TLC finds 21. Route action-constraint evaluation through the same interpreter that generates successors: build an `EvalContext` from the pre-state and stage the post-state's variables as primes (`var'`) into its locals, then call `eval_expr`. This is exactly the staged-primes pattern the action-body evaluator already uses for guards, so `\in`, set/record expressions, and definition calls in constraints are all handled uniformly. The obsolete `eval_transition_expr` / `parse_simple_comparison` / `apply_comparison` helpers are deleted; `is_identifier` (used elsewhere) is retained. LanguageFeatureMatrix now explores 21 distinct states, matching TLC v2.19.
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.
Problem
eval_action_constraintdispatched to a bespokeeval_transition_exprthat — by its own source comment — "only support[ed] simple comparisons" (x' <op> y) and returned an error for any other shape. AnACTION_CONSTRAINTlike LanguageFeatureMatrix'sstep' \in step..(step+1)(membership over a range, mixing unprimedstepfrom the pre-state with primedstep'from the post-state) hit the error path, which pruned every successor: ours explored 1 state where TLC v2.19 finds 21.Fix
Route action-constraint evaluation through the same interpreter that generates successors:
EvalContextfrom the pre-state (current),next) variables into its locals as primes (var'),eval_expr.This is exactly the staged-primes pattern the action-body evaluator already uses for guards, so
\in, set/record expressions, and definition calls in constraints are now all handled uniformly instead of via an ad-hoc comparison parser. The obsoleteeval_transition_expr/parse_simple_comparison/apply_comparisonhelpers are deleted;is_identifier(imported elsewhere) is retained.Validation (on spot)
violation=false.action_constraint_membership_over_range(step' \in step..(step+1)satisfied in-range, pruned out-of-range).scripts/diff_tlc.sh: 14/14 pass.cargo test --release: 0 failures.