Action Properties - #2025
Merged
Merged
Action Properties#2025
Conversation
bugarela
force-pushed
the
claude/funny-gates-hlc7d0
branch
from
September 27, 2026 23:16
8835436 to
334136a
Compare
bugarela
changed the title
bugarela
commented
Sep 27, 2026
bugarela
commented
Sep 27, 2026
bugarela
commented
Sep 27, 2026
bugarela
commented
Sep 27, 2026
Previously, the first argument of `orKeep`/`mustChange` had to be an action (Read & Update effects), so action properties relating the current and next state, like TLA+'s `[][x' > x]_x`, could not be written: `x'` is only allowed in assignments, and `next(x)` has a temporal effect. Writing `always(next(x) > x or next(x) == x)` instead typechecks, but TLC rejects it as "[] followed by action not of form [A]_v". Relax the effect signatures to also accept a temporal effect in the first argument, as was done for `weakFair`/`strongFair`, so that `always((next(x) > x).orKeep(x))` typechecks and is checked by `quint verify --backend tlc`.
Action properties often need to refer to an action under a quantifier, e.g. `[][\A c \in Credits: ... => \E u \in Users: Accept(owner[c], u, c)]_owner`. This was rejected, as the body of `exists`/`forall` could not update variables. Let the body of `exists`/`forall` be an action, and treat its updates as temporal effects in the result (the same effect `next(x)` has). Such expressions can be used in temporal definitions, while in actions the mode checker now reports that `exists` over an action is only allowed in temporal definitions, and suggests `nondet` instead (previously an effect unification error).
Negating an action, as in TLA+'s `<>[][\A i \in Node: ~SendMsg(i)]_vars`, was rejected, as `not` could only be applied to read/temporal expressions. Let `not` take an action and treat its updates as temporal effects in the result, as already done for the body of `exists`/`forall`. In actions, the mode checker reports that negating an action is only allowed in temporal definitions. This also fixes the mode checking of polymorphic operators such as `pure def myExists(S, p) = S.exists(i => p(i))` or `pure def myNot(b) = not(b)`, which were inferred as temporal: an update of a parameter that becomes temporal in the result is determined by the argument, so it doesn't make the operator itself temporal. Use this to write the `AllNodesTerminateIfNoMessages` property of ewd840, which was commented out as not expressible. As in EWD840.tla, TLC finds it violated under fairness of `System` only, and it holds under fairness of `step` (302 distinct states for N=3 in both the Quint and TLA+ versions).
Apalache's pretty printer prints `mustChange(A, v)` as `<A>_v` instead of TLA+'s `<<A>>_v`. SANY cannot parse this, so any module with a `mustChange` failed with `quint verify --backend tlc` (and produced invalid TLA+ with `quint compile --target tlaplus`). Add a post-processing step in `compileToTlaplus`, used by both, where fixes to Apalache's output can be added without waiting on an Apalache release. Each fix must be a no-op on correct output, so it keeps working once Apalache is fixed. The first fix rewrites `<A>_v` into `<<A>>_v`: outside comments and strings, `>_` only ends an angle action, so from each `>_` we go back over the action (a name, an application or a parenthesized expression, possibly spanning several lines) to its opening `<`. On the 40 examples that Apalache translates, the fix changes nothing.
Instead of dedicated signatures for `not`, `exists` and `forall`, let `standardPropagation` and the lambda propagation used by `exists`, `forall`, `filter`, `map`, `fold`, etc. accept updates in their arguments (and lambda bodies), turning them into temporal effects in the result. All operators that are not specific to actions or temporal formulas now work the same way with actions, e.g. `(next(x) == 1) == A` or `Set(A).size() == 1` in temporal definitions. The lambda parameters don't get updates, as they stand for the elements of the collection. Inferred effects of polymorphic operators now include an update variable, e.g. `def f(p) = p + x` has effect `(Read[v0] & Temporal[v1] & Update[v2]) => Read[v0, 'x'] & Temporal[v1, v2]`. The mode checker hint for using such operators on actions in actions is generalized accordingly: it applies to any application whose arguments update variables while the application itself doesn't, except for the temporal operators (e.g. `orKeep`), for which suggesting `temporal` is still the right fix. No example changes its typechecking result, and typechecking time on the largest examples is unchanged.
The effect signature of `ite` only allowed reads in the condition and reads/updates in the branches, so `if` could not be used in temporal formulas, e.g. `always((if (x < 3) next(x) == x + 1 else next(x) == 0).orKeep(x))` or `if (x == 0) eventually(p) else always(q)`. Let the condition and the branches have temporal effects, which are propagated. As in `standardPropagation`, an action in the condition makes the result temporal. Both branches must still update the same variables, so `if` keeps working as before in actions.
The mode checker detects any operator application that turns an action into a temporal expression, but still had dedicated wording for `not`, `exists` and `forall`, left over from when only those were supported. Use the generic message for all of them, keeping only the `nondet` suggestion for `exists`.
…fier The flattener checked whether a definition was already namespaced with `name.startsWith(namespace)`, without the `::` separator. So with `import credits as C`, the definition `Credits` was considered to be already namespaced, was not renamed to `C::Credits`, and flattening failed with "Name 'C::Credits' not found". Check for `namespace::`, as done in the namespacer and in the lookup table.
Parameters of actions could only be read, as the right-hand side of an assignment and the arguments of `all`/`any` could not have temporal effects. So `Accept(co, next(owner).get(c), c)` was rejected, and one had to write `Users.exists(u => next(owner).get(c) == u and Accept(co, u, c))` instead. Let `assign`, `actionAll` and `actionAny` propagate temporal effects. In actions, `x' = next(y)` is still rejected by the mode checker. This exposed an issue in the unification of a union of entities with a concrete entity, which bound each variable in the union to the whole concrete entity: `[u, 'x']` and `['x']` gave `u = ['x']` instead of `u = []`. With updates becoming temporal in `not`, this made actions like the one in #1091 (with `boolean and ...` / `not(boolean) and ...` branches) be inferred as temporal. Now the variables only need to cover the state variables that are not already in the union, which is also the only sensible choice for updates, as overlapping updates are multiple updates of the same variable.
Since #1932, `and`, `or`, `implies` and `iff` propagated updates, so that spec formulas like `init and always(step.orKeep(vars))` would typecheck. This also allowed them to combine assignments in actions, e.g. `x > 0 and x' = 1`, although the docs say that `and`/`or` are for non-action modes and `all`/`any` should be used in actions. Now that `standardPropagation` turns the updates of its arguments into temporal effects, use it for these operators too. Spec formulas still typecheck (the result is temporal), while using them to combine actions in actions is reported by the mode checker, with a hint to use `all { ... }` or `any { ... }` instead. No example or test fixture changes its typechecking result.
Add the examples of action properties from Hillel Wayne's "Action Properties" (https://www.hillelwayne.com/post/action-properties/) as a fixture, with one module per example of the post and the original TLA+ in comments, and test each of them with TLC: 32 tests, one per property that should hold or be violated (possibly with an alternative step). They cover what this branch enables: `next` in `orKeep`/`mustChange`, actions as arguments of `not`, `==`, `exists`/`forall`, `if` and other operators in temporal definitions, actions with temporal arguments, `mustChange` in the TLA+ output, `<>[][A]_v`, and qualified imports.
Combining assignments with `and`, `or`, `implies` and `iff` in actions was rejected in v0.31.0 and accepted in v0.32.0 (since #1932), so it is a regression fix rather than a change.
The dashboard only records whether each command succeeded, which makes a failing row impossible to diagnose from CI. Print the last lines of the output of failing commands to stderr, which goes to the job log and not to the dashboard.
Now that actions can take temporal arguments, `ValidChange` can call `Accept(co, nextCo, c)` directly instead of going through `exists`, as in the `credits` integration test fixture.
bugarela
force-pushed
the
claude/funny-gates-hlc7d0
branch
from
September 27, 2026 23:56
2c2f251 to
c5cd786
Compare
bugarela
marked this pull request as ready for review
September 27, 2026 23:56
4 of 5 tasks
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.
Hello
Quint currently doesn't support Action Properties mostly because the effect checker complains about way too much stuff in temporal mode. Here, we are adding support for them! My thinking is: temporal mode is already super advanced, so we can allow people to write mostly anything there. Only TLC can check temporal properties, so as long as we transpile them correctly to TLC, it should be fine.
I kept the original Quint design idea where we use
next(x)instead ofx'to distinguish this operator when used in temporal mode. I also deliberately kept the constraint thatnextcan only be used with variables, not with arbitrary expressions, as I think that will keep expressibility without introducing things that are unnecessarily harder to understand for non-experts.Changes
Core Features
Action properties in temporal definitions: Actions can now be used in the body of
existsandforallwithin temporal definitions, and actions can be negated withnot. This allows writing action properties like:always(S.exists(i => A(i)).orKeep(vars))always(not(SendMsg(i)).orKeep(vars))Extended
orKeepandmustChange: These operators now accept temporal-mode expressions that usenextto relate current and next states, enabling patterns likealways((next(x) > x).orKeep(x)).TLA+ postprocessing: Added
tlaplusPostprocessing.tsto fix Apalache's incorrect printing of angle actions (<A>_v→<<A>>_v), which SANY cannot parse.NOTE: I normally change Apalache's pretty printer whenever I hit errors like this but honestly that takes more time than I want to spend on this now, so I'm making a temporary ugly patch here to handle this for now.
Error Messages
Since this required several changes to the effect checker that is now more permissive in temporal mode, the error messages could have become more confusing than they already are. So now, when actions are misused in non-temporal contexts, users now get helpful guidance:
existsover an action in an action: suggests usingnondet x = S.oneOf()insteadnotof an action in an action: explains it's only allowed in temporal definitionsforallover an action in an action: similar temporal-only restriction messageTesting
Besides unit tests:
ewd840.qntexample to demonstrate the new capability with previously commented-out temporal propertiesChecklist
https://claude.ai/code/session_01XaNDc6rNPe4HWATuFY5QrL