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