Request for comment: adding EXPECT statements to model files

[Andrew Helwer]

Hi all,

I've implemented a feature in TLC to accept an EXPECT statement in model files. This lets you assert that a given model file is expected to produce a violation. You can see the PR here; please leave feedback if you have any! https://github.com/tlaplus/tlaplus/pull/1269

Currently all this does is make TLC exit with code 0 if the expected violation is generated. It exits with a nonzero code if a different violation was generated, or if no violation was generated. You can assert one of the following in your model file:

• EXPECT NO_VIOLATION
• EXPECT ASSUMPTION_VIOLATION
• EXPECT DEADLOCK_VIOLATION
• EXPECT SAFETY_VIOLATION
• EXPECT LIVENESS_VIOLATION
• EXPECT ASSERT_VIOLATION

If feedback all seems positive I will write some tests for the feature.

Andrew Helwer

[Andrew Helwer]

Thank you to all who responded with your feedback. I somewhat arduously added unit tests for the various cases (would have been much easier if TLC could be run multiple times from within the same process but alas) so the changes implementing this feature are now ready for review and hopefully merge! https://github.com/tlaplus/tlaplus/pull/1269

Andrew Helwer

[Neil Talap]

Hey, Andrew. We need a really serious implementation in Zed for support of TLA+. Perhaps a CLI tool and an extension for Zed. 

Any thoughts on that?

[Andrew Helwer]

Don’t use zed myself. Generally these extensions are written by the people who want them.

--
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 visit https://groups.google.com/d/msgid/tlaplus/10fcb11e-a787-4774-80f5-078450ea3ca0n%40googlegroups.com.

[Miguel Raz-Guzmán Macedo]

Neil,

There's a simple extension for Zed that works at the moment:

https://github.com/Akanoa/Zed-editor-TLA-syntax

It's useful for syntax highlight and not much else (yet):

I found that new lines not doing smart logical indentation to be painful (but that happens in VSCode too).

Glad to see more people using Zed and TLA+!

[Neil Talap]

Super nice! 
I bet it's going to be a meme in the future, Zed is just like OCaml will too. They have a stupid concentration of very smart people using them.

The extension on the link is the one I am using right now, I think. I was thinking of taking it a level up, but just like Andrew said, it's implemented by the people who need it. So, I suppose I might start something a little later in Golang as a TLA+ reimplementation. 

Doing a next-generation distributed system right now, will do the whole system as a state machine first, in intensive use, some drawbacks and flaws will reveal themselves, I believe.

It's just that when I was doing finite state machines as part of computer engineering a couple of years back, we had these beautiful bubbly states and arrows that looked really nice, perhaps we can have that too in the new implementation.