TLA+, Event B comparison

[Adriano Carvalho]

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

[Stephan Merz]

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

> --
> 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+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/46345329-ae57-41b5-8e55-f0dd23d71a0b%40googlegroups.com.

[Michael Leuschel]

Hello,

I can concur with Stephan’s response.

You may also want to look at our article translating B to TLA+ for applying the TLC model checker to B/Event-B models, which contains some comparisons:
https://www.sciencedirect.com/science/article/pii/S0167642316300235

A full fledged comparison of B and TLA+ would be an article on its own, made more complicated by the fact that in the B world you have
- classical B for software development, supported by the commercial AtelierB prover and its code generators,
- and Event-B for systems modelling supported by the open-source Rodin toolset built on top of Eclipse (and also supported by Atelier-B).

Event-B’s events are more rigid than TLA+ actions, while classical B’s operations are quite flexible and allow constructs which do not exist in TLA+.

If code generation is really critical for your application, then you should definitely have a look at “classical B”.
There are code generators available for Event-B, but as far as I know they have not been used for industrial applications yet.

Best regards,
Michael Leuschel

-------------------
For your convenience here is an excerpt from the paper comparing B and TLA+:

B and TLA+ are both state-based formal methods rooted in predicate logic, combined with arithmetic, set theory and support for mathematical functions.
However, as already pointed out in [3], there are considerable differences:

B is strongly typed, while TLA+ is untyped.
For the translation, it is obviously easier to translate from a typed to an untyped language than vice versa.

The concepts of modularization are quite different.

Functions in TLA+ are total, while B supports relations, partial functions, injections, bijections, etc.

B is limited to invariance properties, while TLA+ also allows the specification of liveness properties.

The structure of a B machine or development is prescribed by the B-method, while in TLA+ a specification, any formula can be considered as a system specification.

As far as tool support is concerned, is supported by
the explicit state model checker and more recently by the TLAPS prover.
has been used to validate a variety of distributed algorithms (e.g.) and protocols.
B has extensive proof support, e.g., in the form of the commercial product AtelierB and
the animator, constraint solver and model checker ProB.
Both AtelierB and ProB are being used by companies, mainly in the railway sector for safety critical control software.

[Leslie Lamport]

A minor correction to Michael's post.--in particular, to this statement

   Functions in TLA+ are total, while B supports relations, partial functions, injections, bijections, etc.

 

I believe a partial function is usually said to be a function that is not necessarily defined on all
elements of its domain.  In math, the domain of a function is by definition the set of elements on 

which it's defined, so "partial function" is meaningless.  In typed languages, a function is defined

to have a domain type, and a partial function is one that is not necessarily defined on all elements

of that type.  Since TLA+ is untyped, it adopts the mathematical definition of a function and has

no need for anything like a partial functions.  

Mathematically, a relation on a pair S, T of sets is a subset of S X T.  By "supporting" relations,
injections, etc., Michael means that B provides a large collection of arrow symbols that express certain

sets (more precisely, types) of relations on pairs of sets.   For example S -some-kind-of-arrow-> T

might define the set of all relations R on S, T such that (s1,t) and (s2,t) in R implies s1=s2.  

Abrial liked those operators and apparently used them frequently when writing specs.

Operators corresponding to all those arrow symbols are easily defined in TLA+.   I occasionally

wrote specs that needed to define a set of relations on some pair of sets, and writing that set of

relations as  S -some-kind-of-arrow-> T would have been nice.  However, they were not always

the sets of relations defined by the B arrows.  I thought about providing a few user-defined
arrow symbols for the purpose in TLA+, but I decided they weren't useful enough.  Apparently Abrial

and I wrote different kind of specs.  Most of my specs were for concurrent systems; he designed

B for specifying sequential programs.   Or perhaps we just had different tastes.  I think he 

found the use of all those arrows elegant, while I found it confusing.

Leslie

[Jorge Adriano Branco Aires]

Just a small observation regarding partial functions. 

 

In math, the domain of a function is by definition the set of elements on 

which it's defined, so "partial function" is meaningless.  In typed languages, a function is defined

to have a domain type, and a partial function is one that is not necessarily defined on all elements

of that type.  Since TLA+ is untyped, it adopts the mathematical definition of a function and has

no need for anything like a partial functions.  

 

Indeed the classical definition of partial function doesn’t fit an untyped framework like TLA+. That however does not imply partial functions can’t be modelled in an untyped framework. They can. The classical construction for that purpose would be the lifting of partial functions f: A->>B to total functions lift(f): A -> 1 + B. Here "+" represents disjoint union, 1 represents some singleton, and lift(f)(a) = * (left injected) if f undefined in a, and lift(f)(a) = b (right injected) otherwise. 

TLA+ could include syntax for disjoint unions, injections, cotuples, much like it includes for products, projections and tuples. And TLA+ could define syntax and operators for partial functions modelled as the corresponding lifting. Whether these are worth including or not is then a matter of design choice and personally taste. 

J.A.

[Leslie Lamport]

I believe the lift operator you want can be defined by choosing some

value, lets call it Bottom, and writing:

  lift(f,a) == [x \in a \union DOMAIN f |-> 

                 IF x \in DOMAIN f THEN f[x] ELSE Bottom]

But I don't know why I would ever want to use such an operator.  (I've

managed to get along for well over 50 years without it.)

TLA+ could include syntax for disjoint unions and anything else you can

define mathematically.  As someone has said, a work of art is finished

not when there is nothing else to add, but when there is nothing else

to remove.  And by the way, I didn't know that TLA+ includes syntax

for projections.  Has something been added to the language when I

wasn't looking?

Leslie

[Jorge Adriano Branco Aires]

On Mon, 6 Jan 2020 at 02:28, Leslie Lamport <tlapl...@gmail.com> wrote:

I believe the lift operator you want can be defined by choosing some

value, lets call it Bottom, and writing:

  lift(f,a) == [x \in a \union DOMAIN f |-> 

                 IF x \in DOMAIN f THEN f[x] ELSE Bottom]

But I don't know why I would ever want to use such an operator.  (I've

managed to get along for well over 50 years without it.)

I wasn't clear in my previous comment. I was not suggesting the lifting construction as an operator in TLA+. My point was that partial functions can be modelled as a particular kind of total function (the lifting construction describes how). Should we adopt such a definition of partial function then the untyped nature of TLA+ becomes a non-issue. 

Disclaimer, my TLA+ writing skills are a bit rusty. But just to illustrate what I meant,  

(* disjoin union *)

SUM(A,B) == ({0} \X A) \cup ({1} \X B)  

INJ0(a) == <<0,a>>

INJ1(b) == <<1,b>>

 

(* introducing the possibility of failure *)  

BOTTOM == CHOOSE x: TRUE   

UNIT == {BOTTOM} 

PDOM(A) == SUM(UNIT, A)

FAIL == INJ0(BOTTOM)

SUCCESS(a) == INJ1(a)

(* partial functions are total functions with an added failure element *) 

PARTIAL(A,B) == [A -> PDOM(B)]

(* domain of definition of a partial function *)

def(f) == {a \in DOMAIN f: f[a] # FAIL} 

(* partial composition `f after g` *) 

pc(f,g) == [x \in DOMAIN(f) |-> IF x \in def(f) THEN g[f[x][2]] ELSE FAIL]

(* example sqrt partial function on naturals *) 

sqrt[n \in Nat] == 

  LET candidates == {i \in 0 .. n : i * i = n} IN 

  IF candidates = {} THEN FAIL ELSE SUCCESS(CHOOSE i \in candidates: TRUE)   

(* def(pc(sqrt, sqrt)) = {0, 1, 16, ...} *) 

Nothing special here. Just the usual "monadic" approach to partiality. 

Also to be clear, in the above I didn't mean to claim partial functions should be provided. But only that the language being untyped isn't necessarily an issue if all we want is some abstraction for partial functions. 

TLA+ could include syntax for disjoint unions and anything else you can

define mathematically.  As someone has said, a work of art is finished

not when there is nothing else to add, but when there is nothing else

to remove.  

And by the way, I didn't know that TLA+ includes syntax

for projections.  Has something been added to the language when I

wasn't looking?

True, good point. 

 

Leslie

On Sunday, January 5, 2020 at 3:32:32 PM UTC-8, Jorge Adriano Branco Aires wrote:

Just a small observation regarding partial functions. 

 

In math, the domain of a function is by definition the set of elements on 

which it's defined, so "partial function" is meaningless.  In typed languages, a function is defined

to have a domain type, and a partial function is one that is not necessarily defined on all elements

of that type.  Since TLA+ is untyped, it adopts the mathematical definition of a function and has

no need for anything like a partial functions.  

 

Indeed the classical definition of partial function doesn’t fit an untyped framework like TLA+. That however does not imply partial functions can’t be modelled in an untyped framework. They can. The classical construction for that purpose would be the lifting of partial functions f: A->>B to total functions lift(f): A -> 1 + B. Here "+" represents disjoint union, 1 represents some singleton, and lift(f)(a) = * (left injected) if f undefined in a, and lift(f)(a) = b (right injected) otherwise. 

TLA+ could include syntax for disjoint unions, injections, cotuples, much like it includes for products, projections and tuples. And TLA+ could define syntax and operators for partial functions modelled as the corresponding lifting. Whether these are worth including or not is then a matter of design choice and personally taste. 

J.A.

--

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+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/09c58c33-2c74-4720-8343-8bae2dba3baa%40googlegroups.com.

[Leslie Lamport]

I believe your proposal is to represent a partial function in TLA+ as one having a special value
Bottom in its domain.  However, that means that to talk about partial functions on, say the real
numbers, one would have to add an assumption that Bottom is not a real number.  Perhaps some
people find partial functions useful enough to add such an assumption for every set on which
they want to define a partial function.  The alternative would be to modify the semantics of
TLA+ to add Bottom as something other than a value--analogous to adding a truth value "undefined"
to turn ordinary logic into three-valued logic.  This would require modifying the definition

of every primitive TLA+ operator to specify its value when one or more of its arguments is Bottom.
(I wonder if 2 = Bottom should equal FALSE or Bottom.)  I see no reason to do this to support a
concept I find to be useless.

Your remark about the untyped nature of TLA+ becoming a non-issue implies that it is now an
issue.  I trust that you were talking only about it being an issue for dealing with partial
functions.  The general question of whether being untyped is an "issue" is best discussed
off this forum.

Leslie

[Jorge Adriano Branco Aires]

On Tue, 7 Jan 2020 at 03:10, Leslie Lamport <tlapl...@gmail.com> wrote:

I believe your proposal is to represent a partial function in TLA+ as one having a special value
Bottom in its domain.  However, that means that to talk about partial functions on, say the real
numbers, one would have to add an assumption that Bottom is not a real number. 

Perhaps some
people find partial functions useful enough to add such an assumption for every set on which
they want to define a partial function. 

There is no such assumption required, because we don't return a value in {BOTTOM} \cup Real, but in the disjoint union SUM({BOTTOM, Real}). That is, the return value is either of the form <<0, BOTTOM>> for failure or of the form <<1, x>> for success. 

 

Your remark about the untyped nature of TLA+ becoming a non-issue implies that it is now an
issue.  I trust that you were talking only about it being an issue for dealing with partial
functions.  The general question of whether being untyped is an "issue" is best discussed
off this forum.

Indeed. Could have phrased that better. All I meant is that if we do want to model the concept of a partial function in TLA+ for some reason, it is doable via that encoding. 

 

Leslie

--
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+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/05d9dacb-4d7e-4223-b261-b9a908116bdd%40googlegroups.com.