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

*From*: Hengfeng Wei <hengx...@xxxxxxxxx>*Date*: Fri, 31 Aug 2018 19:09:27 -0700 (PDT)*References*: <3569897a-9cfe-415d-8c1d-2f8a8101a70b@googlegroups.com>

@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

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

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