TLA+ Reuse?

Scott Lewis

unread,

Jan 25, 2021, 6:27:34 PM1/25/21

to tlaplus

Greetings,

I'm brand new to TLA+ so please forgive the newbie question:

Other than examples, is it possible to structure specifications/models/modules/functions so that they can be easily reused by others? Are there any best practices and/or tooling for sharing such efforts?

Thanksinadvance,

Scott

Leandro Ostera

unread,

Jan 25, 2021, 6:53:39 PM1/25/21

to tla...@googlegroups.com

I don’t write TLA+ for a living, and I may be wrong here, but I’ll poorly quote Ron Pressler telling me that I need to stop thinking like a programmer and start thinking like a mathematician.

You don’t need reuse when you have abstraction.

You don’t need to compose your specifications into a larger whole.

That seems to be what I picked up from the few specs I’ve written, and all the reading I’ve done on this mailing list.

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c3f77a84-1a2f-48c4-8f6c-41ab79e94d9bn%40googlegroups.com.

--

/ Leandro

Leslie Lamport

unread,

Jan 25, 2021, 7:02:03 PM1/25/21

to tlaplus

See this posting from June 2019.

Scott Lewis

unread,

Jan 25, 2021, 7:38:16 PM1/25/21

to tlaplus

Thanks. I read your Reusing Specs posting and responses.

I'm curious as to how teams (Intel?, Amazon, tlaplus team, etc) that build specifications do it...i.e. is it simply copy, paste, modify for each person?

I haven't read them yet, so I'm hoping the experiences papers talk some about teamwork and process.