Introducing initializers

[konnov]

1. Context

We have introduced action-definitions to isolate side effects that are written as: delayed assignments x <- e, non-deterministic disjunctions { A | B }, and guesses S.guess { x => e }. These features work nicely:

https://github.com/informalsystems/tnt/blob/7e7e1853afadf2d19211dfafc3a0d188a8988184/examples/ewd840/ewd840.tnt#L85-L92
https://github.com/informalsystems/tnt/blob/7e7e1853afadf2d19211dfafc3a0d188a8988184/examples/ewd840/ewd840.tnt#L105-L106

2. Problem

We kept spec initialization as in TLA. That is the system is initialized with a predicate. Here is how it was written in ewd840:

https://github.com/informalsystems/tnt/blob/7e7e1853afadf2d19211dfafc3a0d188a8988184/examples/ewd840/ewd840.tnt#L34-L39

Technically, this should pose no problem, if we translate Quint to TLA+ and later use TLC or Apalache. They both treat some equalities as assignments.

There are two issues however:

• Technical: We do not want to do this analysis of assignments again in Quint. For instance, when writing the simulator, we have to figure out which equalities in Init should be used as assignments and which are not.
• Usability: Since we have assignments in actions, the users would expect to use the same set of primitives in the system initialization.

3. Solution

Similar to how we have introduced actions, I propose to introduce initializers. They will be like actions that are not allowed to read state variables (as there are no state variables before initialization). So our example of Init (see above) would look like follows:

initializer Init = {
  & setOfMaps(Node, Bool).guess { a =>
        active <- a
    }
  & setOfMaps(Node, Color).guess { c =>
        color <- c
    }
  & Node.guess { n =>
        tpos <- n
    }
  & tcolor <- "black"
}

We can use the effects checker to make sure that the definitions tagged with initializer do not read state variables, and they do write to state variables.

4. Complications

If we introduce the special initializers, we have to understand how to deal with the following issues.

4.1. Restricting the initial states

Quite often we want to further restrict the initial states with a predicate. For instance, if we wanted to state that all active tokens have the "black" color in the above example, it would be very easy to do in TLA+:

Init ==
  /\ active \in [Node -> BOOLEAN]
  /\ color \in [Node -> Color]
  /\ tpos \in Node
  /\ tcolor = "black"
  \* additional requirement
  /\ \A n \in Node: active[n] => color[n] = "black"

Since we are not allowed to refer to the next-state variables in Quint, we have refer to the guessed values. So the equivalent Quint code would look much more complex:

initializer Init = {
  & setOfMaps(Node, Bool).guess { a =>
        setOfMaps(Node, Color).guess { c => {
            & active <- a
            & color <- c
            & Node.forall(n => a[n] implies c[n] = "black")
          }
        }
    }
  & Node.guess { n =>
        tpos <- n
    }
  & tcolor <- "black"
}

This modification is probably bearable. But it becomes even more complex, if we want to use the common TLA+ idiom of restricting the initial states with TypeOK /\ Inv. Let's have a look at TypeOK and Inv, as defined in Quint:

https://github.com/informalsystems/tnt/blob/7e7e1853afadf2d19211dfafc3a0d188a8988184/examples/ewd840/ewd840.tnt#L23-L28
https://github.com/informalsystems/tnt/blob/7e7e1853afadf2d19211dfafc3a0d188a8988184/examples/ewd840/ewd840.tnt#L172-L176

We do not want to embed Inv into TypeOK, as it would be too much work, this would prevent us from reusing Inv, and this process is in general error-prone.

In principle, we would like to use TypeOK as an initializer and Inv as an additional predicate:

initializer TypeInit = {
  & setOfMaps(Node, Bool).guess { a => active <- a }
  & setOfMaps(Node, Color).guess { c => color <- c }
  & Node.guess { n => tpos <- n }
  & Color.guess { c => tcolor <- c }
}

pred Inv = (
  | Node.forall(i => tpos < i implies not(active[i]))
  | 0.to(tpos).exists(j => color[j] == "black")
  | tcolor == "black"
)

We want to write something like { TypeInit & Inv }. However, this should not be allowed, as Inv refers to previous-state variables, and TypeInit writes to next-state variables.

What we actually mean here is something like sequential composition: TypeInit; Inv. That is, TypeInit writes to the state variables, the operator ; rolls turns next-state variables in the previous-state variables, and the predicate Inv evaluates previous-state variables.

If we introduce the operator for sequential composition ; (which actually exists in TLA+ and is called \cdot), we can turn initializers into predicates like follows:

// the above definition
initializer TypeInit = { ... }

pred TypeOK = TypeInit; true

pred TypedInv = TypeInit; Inv

Having defined TypeInit and TypedInv, we can check inductive invariants with initializers and we reuse the same definitions of TypeInit and Inv, without the need for creative code duplication.

So if we introduce ;, then we probably should expect the user to give us the system initializer in the form Init; InitPred, where Init is an initializer, and InitPred is an additional predicate, which can be just true.

4.2. Using initializers in temporal formulas

This issue is similar to that in Section 4.1.

A TLA+ spec is usually summarized in the canonical form:

Init /\ [][Next]_vars /\ (* fairness *)

We can easily express [][Next]_vars in Quint as always(stutter(Next, vars)), but what about the initializer?

We have two options:

1. Introduce a special operator for translating an initializer to an initial-state predicate, e.g., init(Init).
2. Use the operator ; discussed in Section 4.1.

If we go with ;, then the spec in the canonical form would look like:

(Init; true) and always(stutter(Next, vars)) and /* fairness */

If this looks too ugly, we can always introduce an additional predicate:

pred InitP = Init; true

and use it in the temporal formula:

InitP and always(stutter(Next, vars)) and /* fairness */

[konnov]

@bugarela, @shonfeder, @Kukovec, @thpani, this is a long text. I would like to hear your opinion. This issue is kind of blocking me on the simulator. It looks like I have found a solution, but maybe it is not the optimal one.

[Kukovec]

Isn't " the definitions tagged with initializer do not read state variables" more restrictive than our current implementation? Concretely, a subsequent assignment may refer to a state variable previously assigned:

x <- ...
y <- f(x)

[konnov]

Isn't " the definitions tagged with initializer do not read state variables" more restrictive than our current implementation? Concretely, a subsequent assignment may refer to a state variable previously assigned:

x <- ...
y <- f(x)

This is not how delayed assignments work in Quint. In your example f(x) would refer to the value of x before the assignment.

[Kukovec]

Oh, sorry, this was supposed to be y <- f(next(x))

[konnov]

My idea was that we should only allow next(e) in temporal formulas, not in actions. In most of the specs I have seen, you can usually replace x' with its right-hand side in an action, so there is no real need for next in actions. Initialization seems to be trickier though, as we really want to have some non-trivial relations over multiple variables.

[bugarela]

You can just use let-in to write this, right?

val t = ...
{ 
  & x <- t
  & y <- f(t)
}

[bugarela]

As I said in the Quint meeting, I think we should try to abstract this complexity and give the user a clearer interface. And we don't have to define specs the same way TLA+ does in the surface syntax. We could instead have some syntax to define specs in the form:

Spec = Spec(initialAssignments: Init, initialConditions: TypeOK, next: Next)

and probably have some nice symbols/operator to this normal form. I can't think of a good syntax right now but will try later, so here's a bad example:

Spec = from(Init).satisfying(TypeOK).loop(Next)

[konnov]

I guess, my example above is configuration over convention :)

[konnov]

initializer Init1 = {
    , d == 10
    , a in 1.to(29)
    , b in set(1, 0).powerset()
    , c in a.to(100)
}

I think we made a full circle, because that's exactly how Init looks like in most of the TLA+ specs. This is what engineers complained about in the first place :)

[shonfeder]

What part of this did engineers complain about? I don’t recall any discussion of complaints about this kind of clear declarative specification of unit. Could you refresh my memory or share a link?

[konnov]

I cannot give you a link to all conversations that have happened. I remember that explaining what Init does via set membership was always hard.

[shonfeder]

Really surprised to learn this! But discussion during our standup helped clarify. It's not clear to me that there is any better way of describing the set of initial states other than with constraints over the possible values of state variables.

So perhaps this is case where we should just expect users will need to learn the basic idea of constraints if they don't already?

[shonfeder]

I'd just like to note my, POV as a non-expert at specifying:

In this formula

initializer TypeInit = {
  & setOfMaps(Node, Bool).guess { a => active <- a }
  & setOfMaps(Node, Color).guess { c => color <- c }
  & Node.guess { n => tpos <- n }
  & Color.guess { c => tcolor <- c }
}

I find the fact that the reader has to descend into the innermost expression in each conjunct to figure out the state assignment really bad for readability. What we'd like, imo, is a way to always put the state variables being updated front and center. So if it were at all possible, I think this would be much nicer for users to read and write if it were something like:

initializer TypeInit = {
  & active <- setOfMaps(Node, Bool).guess()
  & color  <- setOfMaps(Node, Color).guess()
  & tpos   <- Node.guess()
  & tcolor <- Color.guess()
}

[konnov]

Yeah, that looks nice, except I don't know how to translate that to pure TLA+, if somebody wants to use TLC or TLAPS. It would work perfectly with Apalache though. This construct is very symbolic :)

[thpani]

Yeah, that looks nice, except I don't know how to translate that to pure TLA+, if somebody wants to use TLC or TLAPS.

I don't understand; how is it different from your initializer example under (3)?

[shonfeder]

Leslie Lamport apalache-mc/apalache#841 (comment) that our non-deterministic choose (which behaves exactly like guess in your extended syntax) is quite strange, as it looks like a function but it is not a function in mathematical sense.

I recall. But you are already using guess in the example, so I think I'm missing the significance of your remark.

[konnov]

The guess operator that we currently have in Quint is a Boolean operator, similar to exists. It contains a side effect inside. What you are proposing is a non-deterministic function, which is very much like non-deterministic choose implemented in Apalache.

[shonfeder]

Ah. Right. Thank you for explaining! I forget guess is only allowed to be boolean. I'm not entirely sure why boolean non-det functions are ok but non-det functions for other values are not, but I see the point now :)

Needing to bury every assignment inside a chain of operator calls is pretty problematic IMO. I would be really nice if, at least in the case of assignments, we can take x <- foo.guess() and give it the meaning of foo.guess(y => x <- y). It seems to me that this should be a pretty easy automatic translation? Could get harrier with nested stuff tho....

[konnov]

As previously discussed, I have tried to introduce a new qualifier initializer that would look like follows:

initializer init = all {
  x <- 0,
  y <- 1
}

After doing that, I have decided that we should not introduce the new keyword, for the following reasons:

• It is not immediately obvious that an initializer is a special kind of an action. Hence, the beginners would be confused about what kind of operators they could use in initializers.
• The word initializer is long, hard to type, and there is no good substitute for it.
• Initializers should be in the action mode, so it is not clear why they are simply not actions.

My conclusion is that we simply should use actions for initialization and use the effects checker to make sure that the initializing action only writes to but does not read state variables. Just to double check, would the effects checker able to this, @bugarela?

[bugarela]

Yes, it can. We just need to define a signature for whatever we decide to use to define a spec, which should accept only Update[vars] as the init parameter. This also checks that the given init action is setting a value for all state variables 😄

[konnov]

This was a nice discussion. It looks like we have solved the issue with the initialisers. Closing the discussion. We can always come back to other ideas mentioned here.