Re: [tlaplus] TLA+, Event B comparison

[Stephan Merz <stephan.merz@xxxxxxxxx>]

Hello,

there is currently no support for code generation from TLA+ specifications. Doing so for a well-defined fragment of TLA+ matching a suitable class of target systems would IMHO be a nice research project.

As you say, Event B specifications have a more rigid structure, which can be beneficial (in particular, fine-grained proof obligations can be generated schematically) but may also restrain you in expressing things: for example, you cannot have an event X sometimes refine a higher-level event A and sometimes another event B.

Finally, Event B doesn't have explicit temporal logic, and therefore there is no support for general liveness properties, although there are some pre-defined schemas, such as for showing that low-level events that correspond to high-level stuttering cannot happen forever.

I am obviously a bit partial to TLA+ but I think that you'll have to find out for yourself which formalism works better for you and for your intended application.

Regards,
Stephan


> On 19 Aug 2019, at 21:47, Adriano Carvalho <adrian.dmc@xxxxxxxxx> wrote:
> 
> 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.

-- 
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/1D262017-74FF-45BD-AD44-2550E5E0BDAB%40gmail.com.