[tlaplus] TLA+, Event B comparison

[Adriano Carvalho <adrian.dmc@xxxxxxxxx>]

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.