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
In math, the domain of a function is by definition the set of elements onwhich it's defined, so "partial function" is meaningless. In typed languages, a function is definedto have a domain type, and a partial function is one that is not necessarily defined on all elementsof that type. Since TLA+ is untyped, it adopts the mathematical definition of a function and hasno 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.
I believe the lift operator you want can be defined by choosing somevalue, 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'vemanaged to get along for well over 50 years without it.)
(* 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, ...} *)
TLA+ could include syntax for disjoint unions and anything else you candefine mathematically. As someone has said, a work of art is finishednot when there is nothing else to add, but when there is nothing elseto remove.
And by the way, I didn't know that TLA+ includes syntaxfor projections. Has something been added to the language when Iwasn't looking?
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 onwhich it's defined, so "partial function" is meaningless. In typed languages, a function is definedto have a domain type, and a partial function is one that is not necessarily defined on all elementsof that type. Since TLA+ is untyped, it adopts the mathematical definition of a function and hasno 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.
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.
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
--
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.