# Re: [tlaplus] A recreative spec, as a learn-by-doing thing.

Hi Stephan,

Thank you very much for the feedback and comments :)
As a short reply  let me explain how things worked for me since then:

1.  I agree, defining "Z == <<0,0,1>>" is simpler and works fine. Thanks for pointing that out! Now I believe the best option is to drop Z and only deal with X,Y coordinates, the simpler the better.

2. I agree, this time, the design (wheels, shaft) let us identify the system with a finite set of integer vectors.
I find this topic really interesting: When the system description gets more complex, e.g. data structures as trees of arbitrary depths, identifying the system with a finite set of finite-size values may be nontrivial.

3. Thanks for the compact version of THEOREM ThType ! It helped me to understand better what the BY DEF actually means (prover search space).
THEOREM ThType == Spec => []Typing(x) /\ []Typing(y)
<1> SUFFICES ASSUME Spec
PROVE
/\ Spec => []Inv
/\ Inv => Typing(x) /\ Typing(y)
BY PTL DEF Inv, InvX, InvY, Typing
<1> Inv => Typing(x) /\ Typing(y)
BY DEF Inv, InvX, InvY, Typing
<1> QED BY ThInv, PTL

More generally, I have rewritten several variants of the spec and I am now reaching something more satisfying.
The module extends Integers and offers three possible versions of Vect (renamed "Circle").
Noteworthy, the most complicated and inefficient definition of Circle is
Circle == {
w \in Int \X Int \X {0}:
(* Manhattan norm:*)
/\ abs[w[1]] + abs[w[2]] = 1
(* Euclidian norm:*)
/\ abs[w[1]]*abs[w[1]] + abs[w[2]]*abs[w[2]] = 1
}

where abs[t \in Int] == IF t > 0 THEN t ELSE -t is the usual magnitude.
As a finite subset of Z x Z x {0}, it works (IF you strengthen InvX, InvY!) but really slowly.
Of course, it makes TLC  raise the regular exception.

Now I can go back to "real specs", with a better comprehension of TLAPS.

Thanks again for the feedback and the tips.

Best .

Gabriel

On Wed, 2 Aug 2023 at 17:42, Stephan Merz <stephan.merz@xxxxxxxxx> wrote:
Thanks for the nice example. I have not looked at the background material and can therefore not comment on the extent to which your spec represents Brunelleschi's hoist.

Just a few observations about the TLA+:

1. If Z has to be <<0,0,1>> it would be more appropriate to define it like this

Z == <<0,0,1>>

instead of declaring it as a constant. Also, it is a little strange to include the predicate InvZ in the invariant, since its value cannot change over a behavior: it only mentions constant Z. The above definition eliminates the need for having InvZ as part of the invariant; alternatively, you could include an assumption

ASSUME InvZ == Z = <<0,0,1>>

which would be useful if the constant Z could take more than one value but still had to satisfy some predicate. In fact, the relevance of including Z in the specification is not clear to me as it does not play a role in the dynamics of the system (it only occurs in the formula InvZ). I presume you mentally simplified your definitions (such as of Det) taking into account the fixed value of Z.

2. The tools supporting TLA+ do not really support real numbers. In your case, you only have integer vectors (moreover, with a single component equal to 1 or -1 and the others equal to 0), so everything works out fine, but a generalization to actual real numbers would quickly result in failures of model checking or proof.

3. TLC is a model checker. I am assuming you used it before you started writing proofs (for example by instantiating the constant parameter Z and telling TLC to check the invariant Inv). It will tell you that the invariant holds, and that your spec generates 4 reachable states. For such a small finite state space, this is an exhaustive verification technique. TLC actually ignores any THEOREM statements and proofs a module contains: it computes the graph of reachable states and checks properties on that graph.

The proofs that you wrote were checked by TLAPS, the TLA+ proof system (an interactive proof assistant). Your style of USEing all relevant defined operators and then writing OBVIOUS works for small formulas. For larger formulas, you want to selectively expand the operators that are really necessary for a given step in order to control the search space of the provers.

As you observe, theorem ThType is an immediate corollary of theorem ThInv. You can simplify its proof as follows:

THEOREM ThType == Spec => []Typing(x) /\ []Typing(y)
<1>. Inv => Typing(x) /\ Typing(y)
BY DEF Inv, InvX, InvY, Typing
<1>. QED
BY ThInv, PTL

Thanks again,
Stephan

On 2 Aug 2023, at 16:23, G.Cordier <jg.cordier@xxxxxxxxx> wrote:

A recreative spec, as a learn-by-doing thing.

The spec is about a reversible hoist, developed by the Renaissance Filippo Brunelleschi during the period 1420-1425.

At this time, Brunelleschi had won a competition for the cupola design and construction of the Florence Dome. In such context, he also designed an efficient way to lift and lower payloads: "The oxen no longer had to be un-harnessed and re-harnessed to change the direction of the hoist and lower the lifting tackle back to the ground".

The great idea of Brunlleschi is to reverse the motion by shifting a wheel; which is is much more efficient than re-harnessing the oxen.

In other words, Brunelleschi's hoist is reversible as the driving force remains unchanged; see http://bdml.stanford.edu/Main/BrunelleschiNotes for complete information, pictures, and relevant links.

IMHO this system is a remarkable feat of engineering.
I could write the hoist spec (the part about the motion reversing) and mathematically prove that it is effective.
To do so, I wrote structured proof, as explained at https://tla.msr-inria.inria.fr/tlaps/content/Home.html .

At a geometrical level of abstraction, the system and its environment are identified with a list (x, y, Z) of three normalized 3D vectors , so that a shift is a relevant action Next and that $det:= \det(x, y, Z) \in {-1, 1}$.
This way, proving that the hoist is reversible is only about proving that
det(x, y, Z) /\ Next \implies \det'= - det .

The spec help to capture greater generality: The design requests only one contact point at at time. Therefore, the design does not request entire wheels, one single material point would be enough… Anotther approach is to remark that the whole design is invariant under diffeomorphic reshaping f (where det f' > 0). In practice, such deformed gears would barely lift something, but that is not covered by the spec…

It's not a big thing, only a recreative exercise that I wrote as a "tutorial for myself". By the way, the TLC proof checker validated the proofs- yes, putting "OBVIOUS" is sometimes sufficient ;)

I'm enclosing figures and TLA+ source code.

Feel free to run the spec; comments/suggestions/feedbacks are welcome!

Best

Gabriel

sources:
http://bdml.stanford.edu/Main/BrunelleschiNotes
https://github.com/gitcordier/tlaplus/tree/main/brunelleschi

--
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.
<brunelleschi_gear.pdf><gear.tla>

--
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/7D4630C9-6443-446E-9639-F33095F06B84%40gmail.com.

--
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/CACWDo9x9r85pXw0CETkMqmLJehsC4AxYdznc-jYvCDjo2vC9pA%40mail.gmail.com.

Attachment: gear.tla
Description: Binary data

Attachment: gear.pdf