@Giuliano @Hillel Wayne
Thanks for the TLA+ examples and instructions.
They are quite useful for me to start with.
@Leslie Lamport @Hillel Wayne
Apologies for the confusion.
The digraph represents a state space.
Each edge is labeled with the operation that causes the corresponding state transition.
For some reason, the operations are from a totally ordered set.
Correspondingly, the edges from the same node/state are also totally ordered according to their associated operations.
Given a node, a basic procedure of this protocol is to do something with the path from this node
following the *first* (according to the total order) edge each time it goes out of a node.
Hope this is a bit more clear.
On Friday, August 31, 2018 at 8:49:06 PM UTC+8, 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