Re: [tlaplus] How do you do functions of structures?

[Igor Konnov <igor.konnov@xxxxxxxxx>]

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

> On 08.06.2021, at 08:28, Stephan Merz <stephan.merz@xxxxxxxxx> wrote:
> 
>> On 8 Jun 2021, at 00:43, Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:
>> 
>> […]
>> VARIABLE me
>> 
>> Person == [name : STRING, age : Nat]
>> 
>> HaveBirthday ==
>>     /\ me' \in Person
>>     /\ me'.name = me.name
>>     /\ me'.age = me.age + 1
>> 
>> I think that would uniquely define the value of me' right? Kind of strange to think about how that could be implemented in the tools though.
> 
> that definition indeed uniquely defines the value of me'. TLAPS has no problem with it (assuming that me \in Person). TLC can handle it provided you override the definition of Person by a finite set that TLC can enumerate, but is slow due to the explicit enumeration that TLC implements. I believe that Apalache and ProB would handle it just fine because they rely on constraint solving.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/15192F22-4D07-4248-9427-07931F93D89B%40gmail.com.