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

Re: [tlaplus] Request for a TLA+ Example Involving Graph Objects

There are a few definitions related to digraphs here: https://github.com/nano-o/TLA-Library/blob/master/DiGraph.tla
I'm not sure that the style is very good though.
Some definition are recursive; if I remember correctly the goal was to speed up TLC a bit compared to more declarative definitions.

On 8/31/18 5:49 AM, Hengfeng Wei wrote:
Dear all,

Recently I need to model a distributed protocol which uses a graph as its basic data structure.
Specifically, this is a directed graph with labeled edges and the edges from the same node are ordered by their labels.
It is a dynamic graph; you can add nodes and edges in the runtime.

Could you please share me with some TLA+ examples involving graph objects?

Best regards,
Hengfeng Wei
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.