Re: [tlaplus] TLA+ extensions for user-defined procedure writing by programming language

[tlaplus-google-group@xxxxxxxxxxx]

Hi Guo,

you can override any TLA+ constant-level operator with Java code (the IOUtils module that Hillel mentioned is implemented this way). This diff [1] should give you an example of how to override operators with Java code.

Markus

[1] https://github.com/tlaplus/CommunityModules/commit/8245307786478dfb6de01e2c07107f30ead0b202

On Feb 19, 2022, at 12:12 AM, Guo Hua <fchdir@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.

--
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/6C6CE559-EEC6-4D70-84E6-2784AD495582%40lemmster.de.