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

Re: Request for a TLA+ Example Involving Graph Objects

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.