[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Hillel Wayne <hwa...@xxxxxxxxx>*Date*: Fri, 31 Aug 2018 15:38:52 -0700 (PDT)*References*: <3569897a-9cfe-415d-8c1d-2f8a8101a70b@googlegroups.com>

Section 11.1.2 of *Specifying Systems* has an example Graph module you can use as a starting point. To have multiple edges between the same two nodes but with different labels, you could modify the second clause of IsDirectedGraph(G) to G.edge \subseteq (G.node \X G.node \X Labels). You'd have to more precisely define what "ordered by their labels" means, though.

**References**:**Request for a TLA+ Example Involving Graph Objects***From:*Hengfeng Wei

- Prev by Date:
**Problem with instance substitutions** - Next by Date:
**Re: Request for a TLA+ Example Involving Graph Objects** - Previous by thread:
**Re: [tlaplus] Request for a TLA+ Example Involving Graph Objects** - Next by thread:
**Re: Request for a TLA+ Example Involving Graph Objects** - Index(es):