[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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,

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!




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/bacf24c8-8d2d-4f36-a9ac-195748e68af3n%40googlegroups.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/7D4630C9-6443-446E-9639-F33095F06B84%40gmail.com.