How to compute path or transitive closure in a graph without RECURSIVE?

[BGR360]

I'm trying to translate a TLA+ specification of a file system into typed TLA+ for Apalache. The file system is a directed graph:

CONSTANT
    \* @type: Set(FILE_ID);
    FileIdT

\* Each link is an edge in the directed graph.
\*
\* @typeAlias: LINK = {
\*  parent  : FILE_ID,
\*  child   : FILE_ID
\* };
LinkT == [
    parent  : FileIdT,
    child   : FileIdT
]

\* A file system represented as a directed graph.
\*
\* @typeAlias: FS = {
\*  files   : Set(FILE_ID),
\*  links   : Set(LINK)
\* };
FileSystemT == [
    files   : SUBSET FileIdT,
    links   : SUBSET LinkT
]

I need to be able to compute the ancestors and descendants of a given file.

In the previous TLA+ specification, I achieved this with a Reachable operator:

\* @type: (FS, FILE_ID, FILE_ID) => Bool;
Linked(fs, p, c) == [ parent |-> p, child |-> c ] \in fs.links

\* @type: (FS, FILE_ID, FILE_ID) => Bool;
RECURSIVE Reachable(_, _, _)
Reachable(fs, start, end) ==
    \/ Linked(fs, start, end)
    \/ \E middle \in fs.files \ {start} :
        /\ Linked(fs, middle, end)
        /\ Reachable(fs, start, middle)

This apparently doesn't work since Apalache doesn't support recursive operations. I'm really struggling to figure out how to compute this using ApaFold_ or some other method.

Any tips?

[Kukovec]

You can compute the reachability set in a graph with N nodes in at most N steps (worst case you have a line-graph). It is going to be incredibly inefficient using fold just as N-step iteration, but here's how (I'll write down how you compute the set of all reachable states, you can adapt it a bit if you just care about whether a can reach b):

\* @type: Set(FILE_ID);
EmptySet == {}

OneStepReachable(fs, a) == { b \in fs.files: [ parent |-> a, child |-> b ] \in fs.links }

Reachable(fs, a) ==
LET
 \* @type: <<Set(FILE_ID), Set(FILE_ID)>>;
 foldPair == ApaFoldSet( FoldFn, << OneStepReachable(fs,a) , EmptySet  >>, 1..N )
IN foldPair[2]

where

FoldFn( toVisitAndSeen, irrelevant ) == 
  LET 
    toVisit == toVisitAndSeen[1]  
    seen == toVisitAndSeen[2]
  IN
    IF toVisit = {} 
    THEN toVisitAndSeen
    ELSE
      LET x == CHOOSE y \in toVisit: TRUE
      IN << toVisit \union (OneStepReachable(fs, x) \ seen) \ {x}, seen \union {y} >> 

[Kukovec]

An alternate way to describe reachability, which you may want to explore, is by defining:

Reachable(fs, a, b) == \E k \in 1..N: kStepReachable(k, fs, a, b)

Where you can define k-step reachability without folding:

kStepReachable(k, fs, a, b) == 
  \E kSet \in SUBSET Nodes:
  \E orderFn \in [kSet -> 1..(k+1)]:
  /\ {a,b} \subseteq kSet
  /\ IsBijective(orderFn)
  /\ orderFn[a] = 1
  /\ orderFn[b] = k + 1
  /\ \A x,y \in kSet:
    orderFn[x] = orderFn[y] + 1 => OneStepReachable(fs, y, x)

[Kukovec]

I'll make no promise that this will actually be, in any way, shape, or form, efficient. Nor would it work in Apalache out of the box, because of the 1..(k+1) range, though you could tweak that.

[BGR360]

What is it about the 1..(k+1) range that doesn't work with apalache?

[Kukovec]

You can read about it here: https://apalache.informal.systems/docs/apalache/known-issues.html#integer-ranges-with-non-constant-bounds

Essentially, it boils down to how sets are represented in Apalache. Concretely, we need to be able to give a static overapproximation of a set, which means 1..k, where k is not a literal (or CONSTANT), such as in the cases of \E k \in S: ... or Op(k, ...) = ... won't work out of the box. A typical workaround would be defining

range(a,b) == { x \in Nmin..Nmax: a <= x /\ x <= b }

In the above case, you can take

oneToK(k) == { x \in 1..N: x <=k } 

[Kukovec]

Alternatively,

\E orderFn \in [kSet -> 1..(N+1)]:
  /\ \A v \in DOMAIN orderFn: orderFn <= k + 1
  /\ ...