Action Properties

CHANGELOG.md

@@ -10,12 +10,19 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Added
 ### Changed
 
+- `orKeep` and `mustChange` now accept expressions using `next`, so action properties like `always((next(x) > x).orKeep(x))` can be written and checked with `--backend tlc`
+- Actions can be used as arguments of operators that are not specific to actions (e.g. `not`, `==`, `exists`, `forall`) in temporal definitions, making the result temporal, e.g. `always(not(A).orKeep(vars))`. Doing this in actions reports an error explaining it (and suggesting `nondet` instead of `exists`)
+- `if`-`else` can be used with temporal formulas, e.g. `always((if (x < 3) next(x) == x + 1 else next(x) == 0).orKeep(x))`. As before, both branches of an `if` in an action must update the same variables
+- Actions can take temporal arguments in temporal definitions, e.g. `Accept(owner.get(c), next(owner).get(c), c)`, so actions can be used as relations between the current and next state
 - Upgraded the default Apalache version to 0.62.1, which requires Java 21 or newer.
 
 ### Deprecated
 ### Removed
 ### Fixed
 
+- Fixed `and`, `or`, `implies` and `iff` being accepted to combine assignments in actions (e.g. `x > 0 and x' = 1`), a regression in v0.32.0. Use `all { ... }` and `any { ... }` in actions, as documented. In temporal definitions, they can combine actions and temporal formulas, e.g. `init and always(step.orKeep(vars))`
+- Fixed flattening of qualified imports (`import A as C`) when an imported name starts with the qualifier, e.g. `Credits` with `C`, which failed with "Name 'C::Credits' not found"
+- `mustChange` (`<<A>>_v` in TLA+) is now correctly printed in the TLA+ output, so it can be checked with `--backend tlc`. Quint now post-processes the TLA+ produced by Apalache to fix issues in its pretty printer
 - Fixed `--step`/`--init` resolving to a state variable instead of an action when the variable is named `step` or `init` (#1969)
 - `quint compile --target=json` no longer requires `init` and `step` to exist in the module (#1971)
 - Prevent stack overflow in `getTraceStatistics` (#1992)

docs/content/docs/lang.md

@@ -1801,12 +1801,42 @@ A.orKeep(x)
 
 The arguments to `orKeep` are as follows:
 
- - `A` is an expression in the Action mode,
+ - `A` is an expression in the Action mode, or a Temporal-mode expression
+   that relates the current and next states via `next`,
  - `x` is a variable or a tuple of variables.
 
 *Mode:* Temporal, Run. This operator converts an action (in the Action mode) to a
 temporal property or a run.
 
+Together with `always`, this operator lets us write action properties, that is,
+properties of every transition. For example, `always((next(x) > x).orKeep(x))`
+is like `[][x' > x]_x` of TLA+.
+
+Inside a temporal definition, actions may also be used as arguments of the
+operators that are not specific to actions, such as `not`, `==`, `exists`,
+`forall`, `if`-`else` or set operators. The result is temporal: the updates of the action are
+treated as references to the next state. Actions may also take arguments that
+refer to the next state, like `nextCo` below. For example:
+
+```quint
+// if the owner of a credit changes, it's because the new owner accepted an offer
+temporal ValidChange(c) = {
+  val co = owner.get(c)
+  temporal nextCo = next(owner).get(c)
+  co != nextCo implies Accept(co, nextCo, c)
+}
+temporal validChange = always(Credits.forall(c => ValidChange(c)).orKeep(owner))
+
+// "eventually, no node ever sends a message"
+temporal noMoreMessages = eventually(always(Nodes.forall(i => not(SendMsg(i))).orKeep(vars)))
+
+// the transition depends on the current state
+temporal byCase = always((if (x < 3) next(x) == x + 1 else next(x) == 0).orKeep(x))
+```
+
+This is not allowed in actions, where the action operators should be used
+instead, e.g., `nondet` instead of `exists` to pick a value.
+
 #### MustChange
 
 The following operator is similar to `<A>_x` of TLA+:
@@ -1818,7 +1848,8 @@ A.mustChange(x)
 
 The arguments to `mustChange` are as follows:
 
- - `A` is an expression in the Action mode,
+ - `A` is an expression in the Action mode, or a Temporal-mode expression
+   that relates the current and next states via `next`,
  - `x` is a variable or a tuple of variables.
 
 *Mode:* Temporal. This operator converts an action (in the Action mode) to a

examples/.scripts/run-example.sh

@@ -45,13 +45,16 @@ result () {
     # Run the command and record success / failure
     local quint_cmd="quint $cmd $args $file"
     local succeeded=false
-    if (eval "$quint_cmd &> /dev/null")
+    local output
+    if output=$(eval "$quint_cmd" 2>&1)
     then
         printf ":white_check_mark:"
         succeeded=true
     else
         printf ":x:"
         succeeded=false
+        # Show why the command failed in the job log, as the dashboard only records the result
+        printf '>>> %s failed:\n%s\n' "$quint_cmd" "$(echo "$output" | tail -n 30)" >&2
     fi
 
     # We only want to print additional info to annotate failing results

examples/classic/distributed/ewd840/ewd840.qnt

@@ -156,12 +156,17 @@ module ewd840 {
   // WF_vars(step) is used instead of only WF_vars(System) that requires fairness
   // of the actions controlled by termination detection.
 
-  // Not expressible in quint (for now), as it negates an action
-  // temporal AllNodesTerminateIfNoMessages =
-  //   step.orKeep(vars) and step.weakFair(vars) implies
-  //     eventually(always(
-  //         Node.forall(i => not(SendMsg(i))).orKeep(vars)
-  //     )) implies eventually(Node.forall(i => not(active.get(i))))
+  temporal AllNodesTerminateIfNoMessages =
+    eventually(always(Nodes.forall(i => not(SendMsg(i))).orKeep(vars)))
+      implies eventually(Nodes.forall(i => not(active.get(i))))
+
+  /// `AllNodesTerminateIfNoMessages` under fairness of `System` only. It does not hold.
+  temporal AllNodesTerminateIfNoMessagesFairSystem =
+    System.weakFair(vars) implies AllNodesTerminateIfNoMessages
+
+  /// `AllNodesTerminateIfNoMessages` under fairness of `step`. It holds.
+  temporal AllNodesTerminateIfNoMessagesFairStep =
+    step.weakFair(vars) implies AllNodesTerminateIfNoMessages
 
   /// Dijkstra's inductive invariant
   /// Check that it is indeed inductive (together with TypeOK) with: