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

[Guo Hua <fchdir@xxxxxxxxx>]

Thank you.

This is what I want.

Guo

On Tuesday, February 22, 2022 at 1:04:18 PM UTC+8 Markus Alexander Kuppe wrote:

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 <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.

-- 
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/715a5560-e757-4684-8253-449266a5c5ben%40googlegroups.com.