Hi all,
To join the discussion, I would also vote for de-structuring state into worker_queue and worker_online. Here are my reasons from the tooling perspective:
1. The variable state is a function from Worker to WorkerState, the latter is essentially a Cartesian product of Seq(Msg) and BOOLEAN. For complex data structures, Apalache would sometimes give up and expand the product into plenty of symbolic constants. You have better chances, if it expands individual sets rather than products. I am not sure about TLAPS, but I would conjecture that quantification in SMT works better over simpler data structures than over complex data structures.
2. I think this applies both to TLAPS and Apalache: When you wrap something into a data structure, you introduce additional symbolic constraints, which makes solving harder. This is probably counterintuitive, as in programming it is often more convenient to wrap multiple variables into a single data structure. (As long as you don’t have concurrency, which may easily introduce inconsistency to your data structures.)
3. The definition of INSTANCE is built around individual state variables. So you can easily replace a state variable with an expression (e.g., another variable). If you carry all of your state in a single variable, it will be harder to use substitution in INSTANCE.
@Andrew, Stephan, Your example works almost out of the box in Apalache. However, you have to annotate the variable `me` with a type and replace `STRING` with a concrete finite set, e.g., `{“Alice”, “Bob”}`.
Apalache is not trying to invent new constants, in order to populate the set `STRING`; so we we do not translate `STRING`. Actually, it should be fairly easy to support quantification over strings, so I have added a feature request [1]. In practice, I don’t know how useful that feature would be, as the SMT solver will just produce some names like c!1, c!2, c!3. It will not do fuzzing for you.
Here is the complete example that works in Apalache:
----------------------- MODULE test_rec_assign -----------------------------
EXTENDS Integers
VARIABLE
\* @type: [ name: Str, age: Int ];
me
Person == [name : {"Alice", "Bob"}, age : Nat]
HaveBirthday ==
/\ me' \in Person
/\ me'.name =
me.name
/\ me'.age = me.age + 1
Init ==
/\ me \in Person
/\ me.age = 0
Next ==
HaveBirthday
============================================================================
After all preprocessing steps, Next looks like follows in Apalache (this can be seen in `x/**/OutAnalysis.tla`):
(*
@type: (() => Bool);
*)
Next_si_0 ==
Skolem((\E t_4$1 \in Nat:
Skolem((\E t_3$1 \in { "Alice", "Bob" }:
me' := [name |-> t_3$1, age |-> t_4$1]))))
/\ me'["name"] = me["name"]
/\ me'["age"] = me["age"] + 1
In normal words, Apalache rewrites the expression me' \in Person into a record constructor that is decorated with two existential quantifiers. Apalache tries to rewrite sets, especially the record sets and Cartesian products, as smaller sets are usually easier to reason about. Moreover, the analysis pass labels the existential quantifiers as Skolemizable, so they will be replaced with a constant in the SMT encoding.
Additionally, it labels the equality as an assignment with `:=`, so the variable me’ will be bound to the symbolic value of the expression in the right-hand side, when `Next_si_0` is fired. In general, Apalache would decompose `Next` into a disjunction of predicates Next_si_0, Next_si_1, …, Next_si_n, each of them having a distinct set of symbolic assignments.
[1]
https://github.com/informalsystems/apalache/issues/844
Hope this helps,
Igor
>> […]