[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] TLA+, Event B comparison

Hello everyone,

I am currently looking for a formal modeling tool and, with no experience on the domain, i am having trouble deciding which tool is right for my goals (e.g., code generation is important for me).

After having studied some of the introductory materials on TLA+ and Event B, I've reached the following conclusions.

At the moment, I am more inclined towards Event B. Tool support, including code generation, is available.

Compared to TLA+, the disadvantages of Event B is that Event B, in terms of syntax, looks more rigid than TLA+. Furthermore, this rigidity probably means that it is less capable than TLA+.

The major shortcoming (for my purposes at least) of TLA+ is, as far as I can tell, the lack of support for code generation -- can someone confirm this? Code generation, which, seems to be actually discouraged -- I could not find the reasons why...

Even if code generation support was available for TLA+, I think I still would prefer Event B because the added rigidity seems to make it easier to work with. Is this a reasonable thought?

(Z, it seems to me, is outdated and not as well supported as Event B or TLA+. Alloy also seems to lack code generation support.)

What would be your comments on this? Can you convince me that TLA+ is a better option?

Thank you in advance.

Best regards.
Adriano Carvalho

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/46345329-ae57-41b5-8e55-f0dd23d71a0b%40googlegroups.com.