Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Rename second column of states table from "Diameter" to "Depth" #305

Open
heidihoward opened this issue Sep 27, 2023 · 1 comment
Open
Labels
enhancement New feature or request

Comments

@heidihoward
Copy link

Would it make sense to rename the second column of the states table, currently called Diameter, to something like Depth or Length? This would make it more sense to me and would be more consistent with tlc's cli output

@lemmy
Copy link
Member

lemmy commented Sep 28, 2023

The term 'diameter,' defined as "the longest shortest path between any two vertices in a graph", aligns with the statistical measurement. AFAIK 'Length' typically refers to the number of edges in a path, while 'depth' appears to correspond to a graph's thickness. The appearance of 'depth' in TLC's final result reporting likely serves to track the progress of the breadth-first search. Thus, it would perhaps be best to modify TLC, although such a change might potentially break TLC wrappers parsing its output.

Fortunately, both the VSCode extension and the TLA+ Toolbox are at least consistent and use "diameter."

@lemmy lemmy added the enhancement New feature or request label Sep 28, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Development

No branches or pull requests

2 participants