TLA+《SpecifyingSystems》翻译初稿——Chapter11AdvancedExamples（P173~P174）

IsDirectedGraph $(G)$
当且仅当G为任意有向图时上述表达式成立， 即G是一个node 字段为N，edge 字段为E的记录，且E为集合$N \times N$的子集。对于一些需要在规约中识别有向图的场景，该操作十分有用。（想要了解如何断定G是一个由 node 字段和edge 字段组成的记录，请参阅第140页第10.3节中 IsChannel 的定义）。

DirectedSubgraph $(G)$
代表有向图G的所有子图的集合。或者，我们也可定义满足当且仅当H为G的子图时为真的表达式IsDirectedSubgraph$(H, G)$。用 DirectedSubgraph来表达IsDirectedSubgraph很容易，如下所示：

IsDirectedSubgraph $(H, G) \equiv H \in$ DirectedSubgraph$(G)$

另一方面，用IsDirectedSubgraph来表达DirectedSubgraph却相对复杂：

DirectedSubgraph $(G) = $CHOOSE $S: \forall H:(H \in S) \equiv$ IsDirectedSubgraph $(H, G)$

6.1节已经解释了为何我们无法定义一个包含所有有向图的集合，所以我们不得不定义操作符IsDirectedGraph。

IsUndirectedGraph$(G)$
UndirectedSubgraph $(G)$
上述两个表达式类似于有向图的操作符。正如前面所提到的，一张无向图也可视为一张满足如下准则的有向图G：针对集合$G.edge$中的每条边$\langle m, n\rangle$，它的逆边$\langle n, m\rangle$也隶属于集合$G.edge$。注意，排除特定的例外情况，诸如边数退化为零的图，DirectedSubgraph $(G)$仅包含有向图而不是无向图。

Path$(G)$
G中所有路径的集合，路径是图中沿着边的方向可获取的任意顶点的序列。由于图的许多属性可以用它的路径集合来表示，所以该定义很有用。对于图中任何顶点n，也可方便地将其表达为一元组路径$\langle n\rangle$。

AreConnectedIn$(m, n, G)$
当且仅当图G中存在一条从顶点m到顶点n的路径时，该表达式为真。该操作对于定义图的各种公共属性，例如连通性时作用很显著。

我们还可以定义很多图的其他属性类别，例如下面两种：