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

["G.Cordier" <jg.cordier@xxxxxxxxx>]

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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/bacf24c8-8d2d-4f36-a9ac-195748e68af3n%40googlegroups.com.

Attachment: brunelleschi_gear.pdf
Description: Adobe PDF document

Attachment: gear.tla
Description: Binary data