Replies: 1 comment 7 replies
-
You can compute the reachability set in a graph with \* @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} >> |
Beta Was this translation helpful? Give feedback.
7 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
I'm trying to translate a TLA+ specification of a file system into typed TLA+ for Apalache. The file system is a directed graph:
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: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?
Beta Was this translation helpful? Give feedback.
All reactions