They term you're looking for is model-based testing. Usually this is done by pre-generating a system trace then translating that trace to events in your system and running those events against your system. It seems simpler than the on-line method you've described. There have been a number of talks at the past couple TLA+ confs about model-based testing: http://conf.tlapl.us/home/AndrewOn Saturday, February 19, 2022 at 3:12:01 AM UTC-5 fch...@xxxxxxxxx wrote:Can TLA+ support such an extension that allows running user-defined procedures written by some programming language when an event happens?
Or is there any plan for this?
It may be helpful to provide this function, such as auto-generating test cases.
Best,
Guo