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

Re: Request for a TLA+ Example Involving Graph Objects

@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