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