Alternative syntax for actions

[konnov]

As we have discussed recently, the syntax for action-level operators <-, guess, &, and | seems to be less intuitive than the syntax for other operators. For instance, here is one alternative for guess: #183 (comment)

At some point, we would like to conduct a user survey, to see which syntax is more intuitive to the engineers, who have never seen TLA+/Quint before. Let's collect all potential alternatives here. No judgement, all ideas are welcome. But no guarantee that any of these alternatives would be implemented.

Here are the four operators in question and their current syntax in Quint/TLA+:

1. Assignment: x <- e in Quint and x' = e in TLA+.
2. Non-deterministic choice: S.guess({ x => e }) in Quint and \E x \in S: e in TLA+.
3. Action-level conjunction: { A1 & ... & An } in Quint and A1 /\ ... /\ An in TLA+.
4. Action-level disjunction: { A1 | ... | An } in Quint and A1 \/ ... \/ An in TLA+.

[konnov]

One idea for conjunctions and disjunctions is to make them look a bit more like JS promises (but not exactly like them):

1. Action-level conjunction: all { A1, ..., An }.
2. Action-level disjunction: oneof { A1, ..., An }. JS has any, but I don't like it :)

[shonfeder]

How about choice { .... }?

[thpani]

choice is very close to CHOOSE, which could be confusing wrt (non)determinism.

[shonfeder]

Oh yeah, good point.

[konnov]

As a provisional solution I will replace & with all and | with any, as & and | seem to annoy people. Let's continue the discussion in the hope that we find even a better solution.

[shonfeder]

So to be clear for my view: & and | do not annoy me. i like them. What annoys me is not being able to use them uniformly.

[konnov]

More discussions about guess: #216 (comment)

[konnov]

I have been thinking about <- and guess, and Shon's suggestion. How about the following:

• We introduce the special syntax x <- oneOf(S) that is a syntax shorthand for S.guess(y => x <- e).
• We allow the users to write next(x) in actions.

As a result, in simple cases we will have a combination of oneOf and next, e.g.:

initializer Init = all {
  x <- oneOf(Int),
  next(x) % 2 == 0
}

In more complex cases, the users can still use guess, as it is the most general form. For instance, the above example could be written as:

initializer Init =
  Int.guess(i => all {
    i % 2 == 0,
    x <- i
  })

[shonfeder]

How should we represent the relation between states?

0. Context

A number of related questions have been circulating in our discussions:

• What syntax should we provide for specifying initial states?
  Introducing initializers #183 (comment)
• What syntax should we provide for specifying non-deterministic constraints on
  (state) variable "assignments"?
  Introducing initializers #183 (comment)
• What syntax will provide ergonomic and precise specification of variables that
  do not change between states?
  Unchanged syntax/behavior #70
• What syntax (if any) should we use to refer to the value of a variable in the
  next state? Alternative syntax for actions #207 (comment)
• This discussion, asking which sorts of syntax sugar we should use for actions
  generally.

More recently, in Quint meetings, we've pondered these questions:

• What syntax should we use for supplying values or constraints for parametric
  rigid variables (aka "CONSTANTS")?
• What do we do about the likely confusion resulting from our current
  "assignment" syntax?

The root issue in all these questions seems to be instability or inadequacy in
the ways we can currently represent the relation between states. In this thread,
I'll try to help spin up some discussion around this more holistic consideration.

My current hypothesis is that most of the problems we are seeing arise form lack of a clear and perspicuous method of representing the relations (qua relational) between states, which is the core concern of an actions. As per Lamport: "An action represents a relation between old states and new states". In the replies and discussion, I hope to tease out this hypothesis a bit.

[konnov]

Another idea for the guessing qualifier:

oracle val i = guess(Set(1, 2, 3))

I actually like the oracle qualifier the most. An oracle can be implemented in various ways: as non-deterministic choice, as random choice, as user input. The keyword should not suggest one mechanism.

[konnov]

I'm only reading this right now (sorry) and my first impression is that I love this alternative:

action Foo = all {
  now.x == 2,
  next.x <- 1,
  now.x == 1,
}

It's probably the less strict one we ever had for Quint, and it's still better then the prime operator, which can be applied to arbitrary expressions. I think it would help even the most experienced spec writers to read a specification and it makes actions actually look like transition specification, which was a think Zarko was missing when we talked about Quint at the retreat. I really really like this.

I agree that this approach looks much more self-explanatory, though now and next are kind of implicit global objects, that are not variables. Dafny has the operator old(x) to refer to the variable value upon function entry: https://dafny.org/latest/DafnyRef/DafnyRef#sec-old-expression. So instead of x and next(x), they have old(x) and x. I have always thought that it was weird, but it probably makes a lot of sense from the engineers perspective.

How about the following. We already have next(x), so we can write assignments like:

next(x) <- e

We could introduce now(x) which is simply an identity operator. We could say that this operator could be omitted, but using it improves readability.

So the above example would look like:

action Foo = all {
  now(x) == 2,
  next(x) <- 1,
  now(x) == 1,
}

I agree that it would improve the spec clarity a lot, for the price of nothing :)

[konnov]

Another option. We introduce old(x) instead of now(x) and recommend using old(x), once next(x) <- e was written. So the example would look like follows:

action Foo = all {
  x == 2,
  next(x) <- 1,
  old(x) == 1,
}

By doing so, we are saving on typing old(x), when it is not necessary, and also give the user means to disambiguate what x refers to.

[shonfeder]

At the moment, the syntax I like best for relating states is:

1. Adopt the proposal for lexical indication of state variables from Unambiguous lexical indicators for state variables #374
2. Use primes for "next state", but don't introduce them as a more general operator shifting the semantics of state functions.
3. Ditch <-, and expect to teach people how to think about relations between constraints on states.

Our running example would then look like this:

action Foo = all {
  @x  == 2,
  @x' == 1,
  @x  == 1,
}

[konnov]

Nice, I think we are converging to something nice here. I agree that we could introduce primes back, if we just treat a prime as a special assignment syntax, not an individual operator (as in TLA+). For instance:

action Foo = all {
  x == 2,
  x' = 1,
  x == 1,
}

Note that I would like to distinguish between assignments with = and equalities ==. Although an assignment is indeed an equality constraint (as in TLA+), assignments are more than that: they are unconditionally true, they modify x', and they can do only one modification in a transition.

[konnov]

Also closing this one, as we are not going to change the related syntax in the near future.