TLA+ | The way to specify

Does anyone have a definition of a transitive closure operator that is efficient for TLC to evaluate?

A paper [1] shows that transitive closure cannot be defined in first order logic, but it can be defined in Datalog, as datalog guarantees to use the least-fixed-point solution.
I would use this CHOOSE solution, which appears to work for small test cases. But per [2], TLA+ does not guarantee that CHOOSE finds the least fix-point solution, which means this definition is incorrect (I think). This definition is also very slow in TLC, for anything other than tiny inputs.

IsTransitive(r) == \A x, y, z \in Univ :
<<x, y>> \in r /\ <<y, z>> \in r => <<x, z>> \in r

TCChoose(r) == CHOOSE TCr \in SUBSET (Univ \X Univ) :
/\ r \subseteq TCr (* \subset doesn't parse, why? p273 *)
/\ IsTransitive(TCr)
/\ (* No smaller value meets the same conditions *)
~ \E tuple \in TCr :
LET one_smaller == TCr \ {tuple}
IN /\ r \subseteq one_smaller
/\ IsTransitive(one_smaller)

I wrote a constructive version that recurs until reaching least fixpoint (below).
But I’m planning to make heavy use of this operator, so I’d like to know if there’s a faster way.
Also, I recall reading that it’s possible to implement particular TLA+ modules in Java, for TLC. Has anyone found that to be worth the effort?

Thanks,

Chris

TCRecur(r) == LET RECURSIVE selfJoin(_)
selfJoin(r1) ==
LET MissingJoinTuples(left,right) == {<<x, z>> \in (Univ \X Univ) :
/\ <<x, z>> \notin left
/\ <<x, z>> \notin right
/\ \E y \in Univ : <<x, y>> \in left /\ <<y, z>> \in right}
mjt == MissingJoinTuples(r1, r1)
IN IF mjt = {} THEN r1 (* have reached least fixpoint, so this must be transitive closure *)
ELSE LET bigger == r1 \union mjt
IN bigger \union selfJoin(bigger)
IN selfJoin(r)

(* Test constant expressions, with Univ <- {a, b, c, d, e, f}

TCChoose({<<a, b>>, <<b, c>>, <<d, e>>, <<d, f>>}) = {<<a, b>>, <<a, c>>, <<b, c>>, <<d, e>>, <<d, f>>}
*)

[1] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.127.8266&rep=rep1&type=pdf

[2] From http://www.loria.fr/~merz/papers/tla+logic2008.pdf

Recursive functions can be defined in terms of choice, e.g.
factorial _=
choose f : f = [n ∈ Nat 7→ if n = 0 then 1 else n ∗ f [n − 1]]
which TLA+, using some syntactic sugar, offers to write more concisely as
factorial [n ∈ Nat ] _= if n = 0 then 1 else n ∗ factorial [n − 1]
Of course, as with any construction based on choice, such a definition should
be justified by proving the existence of a function that satisfies the recursive
equation. Unlike standard semantics of programming languages, TLA+ does
not commit to the least fixed point of a recursively defined function in cases
where there are several solutions.

Sorry, I forgot that this crappy web site doesn't allow you to type readable posts.
To get a readable version, copy this posting into a sensible text editor and replace
every @ with a space.
@@@@@@
@@@@@@

If R is a relation--that is a set of ordered pairs--let its support be
the set of all elements that appear in those pairs. Then R defines a
directed graph on its support, where there is an edge from s to t iff
<<s, t>> is in R. The closure of R is the set of all pairs
<<s, t>> such that s and t are in the support of R and there is a path
from s to t.
@@@
This leads to the following definition of the closure:
@@@
Support(R)@==@{r[1]@:@r@\in@R}@\cup@{r[2]@:@r@\in@R}
@@@
Closure(R)@==@
@@LET@S@==@Support(R)
@@IN@@{<<s,@t>>@\in@S@\X@S@:@\E@p@\in@Seq(S)@:@/\@Len(p)@>@1
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@/\@p[1]@=@s
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@/\@p[Len(p)]@=@t
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@/\@\A@i@\in@@1..(Len(p)-1)@:
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@<<p[i],@p[i+1]>>@\in@R}
@@@
This can't be evaluated by TLC because Seq(S) is an infinite set.
However, it's not hard to see that it suffices to consider paths
whose length is at most Cardinality(S). I'll let you modify the
definition to one that TLC will be able to evaluate.
@@@
However, the naive evaluation that TLC uses makes this definition
rather inefficient. (As an exercise, find an upper bound on its
complexity.) A definition that TLC can evaluate more efficiently is
obtained by recursively defining the function C with domain Nat such
that C[n] the set of all pairs <<s, t>> with s, t \in Support(R) such
that there exists a path of length at most n+1 from s to t in Support(R),
and then define Closure(R) to equal C[Cardinality(Support(R))-1].
@@@@
To check your definitions, define Closure1 and Closure2 with these two
definitions, and have TLC check
@@@@@
@@@ASSUME@\A@N@\in@0..3@:@\A@R@\in@SUBSET@((1..N)@\X@(1..N))@:@
@@@@@@@@@@@@@@@Closure1(R)@=@Closure2(R)