diff --git a/modules/tlc2/overrides/Graphs.java b/modules/tlc2/overrides/Graphs.java new file mode 100644 index 0000000..015d6ee --- /dev/null +++ b/modules/tlc2/overrides/Graphs.java @@ -0,0 +1,256 @@ +/******************************************************************************* + * Copyright (c) 2026 NVIDIA Corporation. All rights reserved. + * + * The MIT License (MIT) + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is furnished to do + * so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN + * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION + * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * Contributors: + * Markus Alexander Kuppe - initial API and implementation + ******************************************************************************/ +package tlc2.overrides; + +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Collections; +import java.util.Deque; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import tlc2.output.EC; +import tlc2.tool.EvalException; +import tlc2.value.Values; +import tlc2.value.impl.BoolValue; +import tlc2.value.impl.RecordValue; +import tlc2.value.impl.SetEnumValue; +import tlc2.value.impl.StringValue; +import tlc2.value.impl.TupleValue; +import tlc2.value.impl.Value; +import tlc2.value.impl.ValueEnumeration; + +public final class Graphs { + + private Graphs() { + // no-instantiation! + } + + private static final StringValue NODE = new StringValue("node"); + private static final StringValue EDGE = new StringValue("edge"); + + /* + * Validate that v is a graph record, i.e. a record with a "node" and an "edge" + * field, both of which are sets. Reporting the argument's position (e.g. "third" + * for AreConnectedIn) and rejecting malformed records here yields a proper + * user-facing TLC module argument error instead of a NullPointerException or + * ClassCastException later in nodes/adjacency. + */ + private static RecordValue toGraph(final String op, final String argPos, final Value v) { + final Value rcd = v.toRcd(); + if (!(rcd instanceof RecordValue)) { + throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, + new String[] { argPos, op, "graph record with a node and an edge field", Values.ppr(v.toString()) }); + } + final RecordValue g = (RecordValue) rcd; + final Value node = g.select(NODE); + if (node == null || node.toSetEnum() == null) { + throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, + new String[] { argPos, op, "graph record whose node field is a set", Values.ppr(v.toString()) }); + } + final Value edge = g.select(EDGE); + if (edge == null || edge.toSetEnum() == null) { + throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, + new String[] { argPos, op, "graph record whose edge field is a set", Values.ppr(v.toString()) }); + } + return g; + } + + private static SetEnumValue nodes(final RecordValue g) { + final SetEnumValue nodes = (SetEnumValue) g.select(NODE).toSetEnum(); + nodes.normalize(); + return nodes; + } + + /* + * Adjacency list of the graph, restricted to edges whose endpoints are both + * elements of the node set. This mirrors the TLA+ definitions, in which any + * node on a path is drawn from G.node. + * + * The definitions test <> \in G.edge, i.e. membership of an exact + * 2-tuple. Any element of G.edge that is not a 2-tuple (e.g. <> or + * <>) can therefore never match and contributes no edge, so it is + * skipped rather than mis-parsed (as u -> v) or causing an out-of-bounds error. + */ + private static Map> adjacency(final RecordValue g, final SetEnumValue nodes, + final boolean transpose) { + final SetEnumValue edges = (SetEnumValue) g.select(EDGE).toSetEnum(); + final Map> adj = new HashMap<>(); + final ValueEnumeration ve = edges.elements(); + Value v; + while ((v = ve.nextElement()) != null) { + final Value tuple = v.toTuple(); + if (!(tuple instanceof TupleValue) || ((TupleValue) tuple).size() != 2) { + continue; + } + final TupleValue e = (TupleValue) tuple; + Value from = e.elems[0]; + Value to = e.elems[1]; + if (transpose) { + final Value tmp = from; + from = to; + to = tmp; + } + if (nodes.member(from) && nodes.member(to)) { + adj.computeIfAbsent(from, k -> new ArrayList<>()).add(to); + } + } + return adj; + } + + /* + * SimplePath(G) == + * {p \in SeqOf(G.node, Cardinality(G.node)) : + * /\ p # << >> + * /\ Cardinality({ p[i] : i \in DOMAIN p }) = Len(p) + * /\ \A i \in 1..(Len(p)-1) : <> \in G.edge} + * + * Enumerates the set of all (non-empty) simple paths of G via depth-first + * search. This avoids materializing the (exponentially large) set + * SeqOf(G.node, Cardinality(G.node)) that the pure TLA+ definition ranges over. + */ + @TLAPlusOperator(identifier = "SimplePath", module = "Graphs", warn = false) + public static Value simplePath(final Value graph) { + final RecordValue g = toGraph("SimplePath", "first", graph); + final SetEnumValue nodes = nodes(g); + final Map> adj = adjacency(g, nodes, false); + + final List paths = new ArrayList<>(); + final List path = new ArrayList<>(); + final Set visited = new HashSet<>(); + final ValueEnumeration ve = nodes.elements(); + Value start; + while ((start = ve.nextElement()) != null) { + path.add(start); + visited.add(start); + extendSimplePath(start, adj, path, visited, paths); + visited.remove(start); + path.remove(path.size() - 1); + } + + return new SetEnumValue(paths.toArray(new Value[paths.size()]), false); + } + + // Backtracking depth-first search: emit the current path, then recurse into + // each unvisited successor. + private static void extendSimplePath(final Value current, final Map> adj, + final List path, final Set visited, final List paths) { + // Every non-empty prefix of a simple path is itself a simple path. + paths.add(new TupleValue(path.toArray(new Value[path.size()]))); + for (final Value succ : adj.getOrDefault(current, Collections.emptyList())) { + if (visited.add(succ)) { + path.add(succ); + extendSimplePath(succ, adj, path, visited, paths); + path.remove(path.size() - 1); + visited.remove(succ); + } + } + } + + /* + * AreConnectedIn(m, n, G) == + * \E p \in SimplePath(G) : (p[1] = m) /\ (p[Len(p)] = n) + * + * There is a simple (hence any) directed path from m to n. Note that <> is a + * simple path, so a node is connected to itself iff it is a node of G. + */ + @TLAPlusOperator(identifier = "AreConnectedIn", module = "Graphs", warn = false) + public static Value areConnectedIn(final Value m, final Value n, final Value graph) { + final RecordValue g = toGraph("AreConnectedIn", "third", graph); + final SetEnumValue nodes = nodes(g); + + // Every node on a simple path is drawn from G.node, so m and n must both be + // nodes. Checking membership first also matches the pure definition on an + // empty node set: the existential domain SimplePath(G) is empty, hence the + // result is FALSE and no comparison of m and n happens. Comparing m and n + // up front (via the self-connection fast path below) would instead raise a + // type error for incompatible arguments, e.g. AreConnectedIn(1, "x", G). + if (!nodes.member(m) || !nodes.member(n)) { + return BoolValue.ValFalse; + } + if (m.equals(n)) { + return BoolValue.ValTrue; + } + + final Map> adj = adjacency(g, nodes, false); + return reachable(m, adj).contains(n) ? BoolValue.ValTrue : BoolValue.ValFalse; + } + + // Breadth-first search returning all nodes reachable from source (inclusive). + private static Set reachable(final Value source, final Map> adj) { + final Set visited = new HashSet<>(); + final Deque frontier = new ArrayDeque<>(); + visited.add(source); + frontier.add(source); + while (!frontier.isEmpty()) { + final Value current = frontier.remove(); + for (final Value succ : adj.getOrDefault(current, Collections.emptyList())) { + if (visited.add(succ)) { + frontier.add(succ); + } + } + } + return visited; + } + + /* + * IsStronglyConnected(G) == + * \A m, n \in G.node : AreConnectedIn(m, n, G) + * + * G is strongly connected iff, from an arbitrary node r, every node is reachable + * (forward) and r is reachable from every node (i.e., every node is reachable in + * the transposed graph). This is the two-pass reachability test underlying + * Kosaraju's algorithm and runs in linear time instead of enumerating all pairs + * of nodes. + */ + @TLAPlusOperator(identifier = "IsStronglyConnected", module = "Graphs", warn = false) + public static Value isStronglyConnected(final Value graph) { + final RecordValue g = toGraph("IsStronglyConnected", "first", graph); + final SetEnumValue nodes = nodes(g); + + final int order = nodes.size(); + if (order == 0) { + return BoolValue.ValTrue; + } + + final Value root = nodes.elements().nextElement(); + + final Map> adj = adjacency(g, nodes, false); + if (reachable(root, adj).size() != order) { + return BoolValue.ValFalse; + } + + final Map> radj = adjacency(g, nodes, true); + if (reachable(root, radj).size() != order) { + return BoolValue.ValFalse; + } + + return BoolValue.ValTrue; + } +} diff --git a/modules/tlc2/overrides/TLCOverrides.java b/modules/tlc2/overrides/TLCOverrides.java index 52ac71b..aff1ca5 100644 --- a/modules/tlc2/overrides/TLCOverrides.java +++ b/modules/tlc2/overrides/TLCOverrides.java @@ -45,7 +45,7 @@ public Class[] get() { Json.resolves(); return new Class[] { IOUtils.class, SVG.class, SequencesExt.class, Json.class, Bitwise.class, FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class, - DyadicRationals.class, Statistics.class, VectorClocks.class, GraphViz.class }; + DyadicRationals.class, Statistics.class, VectorClocks.class, GraphViz.class, Graphs.class }; } catch (NoClassDefFoundError e) { // Remove this catch when this Class is moved to `TLC`. System.out.println("gson dependencies of Json overrides not found, Json module won't work unless " @@ -53,6 +53,6 @@ public Class[] get() { } return new Class[] { IOUtils.class, SVG.class, SequencesExt.class, Bitwise.class, FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class, DyadicRationals.class, - Statistics.class, VectorClocks.class, GraphViz.class }; + Statistics.class, VectorClocks.class, GraphViz.class, Graphs.class }; } } diff --git a/tests/GraphsTests.tla b/tests/GraphsTests.tla index 46c3aa6..f7b225f 100644 --- a/tests/GraphsTests.tla +++ b/tests/GraphsTests.tla @@ -1,22 +1,205 @@ ------------------------- MODULE GraphsTests ------------------------- -EXTENDS Graphs, TLCExt +EXTENDS Graphs, SequencesExt, TLCExt ASSUME LET T == INSTANCE TLC IN T!PrintT("GraphsTests") +(******************************************************************************) +(* Pure TLA+ reference definitions, kept verbatim in sync with the operators *) +(* in modules/Graphs.tla. They serve as the oracle against which the Java *) +(* module overrides (SimplePath, AreConnectedIn, IsStronglyConnected) are *) +(* checked exhaustively below. ConnectionsIn (Warshall's algorithm) provides *) +(* a second, independent oracle for reachability. *) +(******************************************************************************) +LOCAL SimplePathPure(G) == + {p \in SeqOf(G.node, Cardinality(G.node)) : + /\ p # << >> + /\ Cardinality({ p[i] : i \in DOMAIN p }) = Len(p) + /\ \A i \in 1..(Len(p)-1) : <> \in G.edge} + +LOCAL AreConnectedInPure(m, n, G) == + \E p \in SimplePathPure(G) : (p[1] = m) /\ (p[Len(p)] = n) + +LOCAL IsStronglyConnectedPure(G) == + \A m, n \in G.node : AreConnectedInPure(m, n, G) + +\* One representative graph set of each node-set cardinality 0 through 3 +\* (including the empty graph and self-loops). The operators treat nodes as +\* opaque values and are invariant under renaming, so a graph on nodes {1, 3} +\* or {2, 3} is just a relabeling of one on {1, 2} and adds no coverage. It +\* therefore suffices to use the prefixes {}, {1}, {1, 2}, {1, 2, 3} rather +\* than all same-cardinality node sets (e.g. Graphs({1, 3}), Graphs({2, 3})). +LOCAL SmallGraphs == + Graphs({}) \cup Graphs({1}) \cup Graphs({1, 2}) \cup Graphs({1, 2, 3}) + +(******************************************************************************) +(* A graph whose edge set is built via a set image that yields the same edge *) +(* multiple times, i.e. a potentially non-normalized SetEnumValue. The *) +(* overrides enumerate sets via SetEnumValue#elements(), which normalizes *) +(* (deduplicates), so the result is unaffected by the input representation. *) +(******************************************************************************) +LOCAL DupEdgeGraph == + [node |-> {1, 2, 3}, + edge |-> {<<2, 3>>} \cup { <<1, 2>> : i \in {"a", "b", "c"} }] + +ASSUME AssertEq(Cardinality(SimplePath(DupEdgeGraph)), 6) +ASSUME AssertEq(SimplePath(DupEdgeGraph), + {<<1>>, <<2>>, <<3>>, <<1, 2>>, <<2, 3>>, <<1, 2, 3>>}) + +(******************************************************************************) +(* The TLA+ definitions test membership of an exact 2-tuple <> *) +(* in G.edge, so an edge element that is not a 2-tuple (e.g. <> or *) +(* <>) matches nothing and contributes no edge. The overrides must *) +(* neither crash on 1-tuples nor read <> as the edge u -> v. *) +(******************************************************************************) +LOCAL OneTupleEdgeGraph == [node |-> {1, 2}, edge |-> {<<1>>, <<2>>}] +LOCAL ThreeTupleEdgeGraph == [node |-> {1, 2, 3}, edge |-> {<<1, 2, 3>>}] +LOCAL MixedArityEdgeGraph == + [node |-> {1, 2, 3}, edge |-> {<<1>>, <<1, 2>>, <<2, 3, 4>>}] + +\* 1-tuple edges are ignored: only the trivial single-node paths remain. +ASSUME AssertEq(SimplePath(OneTupleEdgeGraph), {<<1>>, <<2>>}) +ASSUME AssertEq(AreConnectedIn(1, 2, OneTupleEdgeGraph), FALSE) +ASSUME AssertEq(IsStronglyConnected(OneTupleEdgeGraph), FALSE) + +\* A 3-tuple <<1, 2, 3>> is not the edge 1 -> 2 and is ignored. +ASSUME AssertEq(SimplePath(ThreeTupleEdgeGraph), {<<1>>, <<2>>, <<3>>}) +ASSUME AssertEq(AreConnectedIn(1, 2, ThreeTupleEdgeGraph), FALSE) + +\* Only the genuine 2-tuple <<1, 2>> is treated as an edge. +ASSUME AssertEq(SimplePath(MixedArityEdgeGraph), {<<1>>, <<2>>, <<3>>, <<1, 2>>}) +ASSUME AssertEq(AreConnectedIn(1, 2, MixedArityEdgeGraph), TRUE) +ASSUME AssertEq(AreConnectedIn(2, 3, MixedArityEdgeGraph), FALSE) + +\* The overrides agree with the pure TLA+ definitions on these graphs. +ASSUME \A G \in {OneTupleEdgeGraph, ThreeTupleEdgeGraph, MixedArityEdgeGraph} : + /\ SimplePath(G) = SimplePathPure(G) + /\ \A m, n \in G.node : AreConnectedIn(m, n, G) = AreConnectedInPure(m, n, G) + /\ IsStronglyConnected(G) = IsStronglyConnectedPure(G) + +(******************************************************************************) +(* SimplePath Tests *) +(******************************************************************************) ASSUME AssertEq(SimplePath([edge|-> {}, node |-> {}]), {}) ASSUME AssertEq(SimplePath([edge|-> {}, node |-> {1,2,3}]), {<<1>>, <<2>>, <<3>>}) ASSUME AssertEq(SimplePath([edge|-> {<<1,2>>, <<2,3>>}, node |-> {1,2,3}]), { <<1>>, <<2>>, <<3>>, <<1,2>>, <<2,3>>, <<1,2,3>> } ) +\* A self-loop never yields a path with a repeated node, so it does not add any +\* simple path beyond the single-node one. +ASSUME AssertEq(SimplePath([node |-> {1}, edge |-> {<<1, 1>>}]), {<<1>>}) +ASSUME AssertEq(SimplePath([node |-> {1, 2}, edge |-> {<<1, 1>>, <<1, 2>>}]), + {<<1>>, <<2>>, <<1, 2>>}) + +\* A 2-cycle contributes both directed edges as simple paths. +ASSUME AssertEq(SimplePath([node |-> {1, 2}, edge |-> {<<1, 2>>, <<2, 1>>}]), + {<<1>>, <<2>>, <<1, 2>>, <<2, 1>>}) + +\* A 3-cycle contributes every rotation as a simple path. +ASSUME AssertEq(SimplePath([node |-> {1, 2, 3}, edge |-> {<<1, 2>>, <<2, 3>>, <<3, 1>>}]), + {<<1>>, <<2>>, <<3>>, <<1, 2>>, <<2, 3>>, <<3, 1>>, + <<1, 2, 3>>, <<2, 3, 1>>, <<3, 1, 2>>}) + +\* Exhaustively: the Java override agrees with the original TLA+ definition for +\* every directed graph in SmallGraphs. +ASSUME \A g \in SmallGraphs : AssertEq(SimplePath(g), SimplePathPure(g)) + +(******************************************************************************) +(* AreConnectedIn Tests *) +(******************************************************************************) ASSUME \A g \in Graphs({"A", "B", "C"}): \A u,v \in g.node : AreConnectedIn(u, v, g) \in BOOLEAN +\* A node is connected to itself iff it is a node of the graph (via <>). +ASSUME AssertEq(AreConnectedIn(1, 1, [node |-> {1}, edge |-> {}]), TRUE) +ASSUME AssertEq(AreConnectedIn(1, 1, EmptyGraph), FALSE) + +\* Connectivity is directed and requires both endpoints to be nodes of the graph. +ASSUME AssertEq(AreConnectedIn(1, 2, [node |-> {1, 2}, edge |-> {<<1, 2>>}]), TRUE) +ASSUME AssertEq(AreConnectedIn(2, 1, [node |-> {1, 2}, edge |-> {<<1, 2>>}]), FALSE) +ASSUME AssertEq(AreConnectedIn(1, 9, [node |-> {1, 2}, edge |-> {<<1, 2>>}]), FALSE) + +\* Type-incompatible arguments must not be compared when no node matches: on the +\* empty graph the existential domain SimplePath(G) is empty, so the result is +\* FALSE (matching AreConnectedInPure) rather than a type error from m = n. +ASSUME AssertEq(AreConnectedIn(1, "x", EmptyGraph), FALSE) +ASSUME AssertEq(AreConnectedIn(1, "x", EmptyGraph), AreConnectedInPure(1, "x", EmptyGraph)) +ASSUME AssertEq(AreConnectedIn("x", "x", EmptyGraph), FALSE) + ASSUME LET G == [node |-> {1,2,3,4,5,6}, edge |-> {<<1,2>>, <<2,3>>, <<2,4>>, <<3,2>>, <<3,4>>, <<3,5>>, <<4,2>>, <<5,6>>, <<6,5>>}] IN \A m,n \in G.node : AreConnectedIn(m,n,G) <=> ConnectionsIn(G)[m,n] +\* Exhaustively: the override agrees with the original TLA+ definition and with +\* the independent ConnectionsIn oracle for every graph in SmallGraphs. +ASSUME \A g \in SmallGraphs : + \A m, n \in g.node : + /\ AreConnectedIn(m, n, g) = AreConnectedInPure(m, n, g) + /\ AreConnectedIn(m, n, g) <=> ConnectionsIn(g)[m, n] + +(******************************************************************************) +(* IsStronglyConnected Tests *) +(******************************************************************************) +ASSUME \A g \in Graphs({1, 2, 3}): IsStronglyConnected(g) \in BOOLEAN + +\* The empty graph is (vacuously) strongly connected. +ASSUME AssertEq(IsStronglyConnected(EmptyGraph), TRUE) + +\* A single node is strongly connected (a node is connected to itself via the +\* trivial path <>), with or without a self-loop. +ASSUME AssertEq(IsStronglyConnected([node |-> {1}, edge |-> {}]), TRUE) +ASSUME AssertEq(IsStronglyConnected([node |-> {1}, edge |-> {<<1, 1>>}]), TRUE) + +\* A simple directed cycle is strongly connected. +ASSUME AssertEq(IsStronglyConnected([node |-> {1, 2, 3}, + edge |-> {<<1, 2>>, <<2, 3>>, <<3, 1>>}]), TRUE) + +\* Two mutually connected nodes are strongly connected, ... +ASSUME AssertEq(IsStronglyConnected([node |-> {1, 2}, + edge |-> {<<1, 2>>, <<2, 1>>}]), TRUE) + +\* ... whereas a single directed edge between them is not. +ASSUME AssertEq(IsStronglyConnected([node |-> {1, 2}, + edge |-> {<<1, 2>>}]), FALSE) + +\* A directed line (path graph) is not strongly connected. +ASSUME AssertEq(IsStronglyConnected([node |-> {1, 2, 3}, + edge |-> {<<1, 2>>, <<2, 3>>}]), FALSE) + +\* A graph with two separate strongly connected components is not strongly +\* connected as a whole. +ASSUME AssertEq(IsStronglyConnected([node |-> {1, 2, 3, 4}, + edge |-> {<<1, 2>>, <<2, 1>>, + <<3, 4>>, <<4, 3>>}]), FALSE) + +\* Exhaustively: the override agrees with the original TLA+ definition and with +\* the independent ConnectionsIn oracle for every graph in SmallGraphs. +ASSUME \A g \in SmallGraphs : + /\ IsStronglyConnected(g) = IsStronglyConnectedPure(g) + /\ IsStronglyConnected(g) <=> (\A m, n \in g.node : ConnectionsIn(g)[m, n]) + +(******************************************************************************) +(* Value identity Tests *) +(* *) +(* These tests use composite node values (sets) that are written with *) +(* different internal orderings but denote the same TLA+ value, so that nodes *) +(* and edge endpoints are matched by value equality rather than by their *) +(* concrete representation. *) +(******************************************************************************) +ASSUME LET G == [node |-> {{1, 2}, {3}}, edge |-> {<<{1, 2}, {3}>>}] + IN /\ AssertEq(SimplePath(G), {<<{1, 2}>>, <<{3}>>, <<{1, 2}, {3}>>}) + /\ AssertEq(AreConnectedIn({1, 2}, {3}, G), TRUE) + /\ AssertEq(AreConnectedIn({3}, {1, 2}, G), FALSE) + /\ AssertEq(IsStronglyConnected(G), FALSE) + +\* The edge endpoint {2, 1} and the node/argument {1, 2} denote the same set, so +\* the override must treat them as identical despite the differing literal order. +ASSUME LET G == [node |-> {{1, 2}, {3}}, edge |-> {<<{2, 1}, {3}>>, <<{3}, {1, 2}>>}] + IN /\ AssertEq(AreConnectedIn({1, 2}, {3}, G), TRUE) + /\ AssertEq(AreConnectedIn({3}, {2, 1}, G), TRUE) + /\ AssertEq(IsStronglyConnected(G), TRUE) + (******************************************************************************) (* GraphUnion Tests *) (******************************************************************************)