search

tlaplus / CommunityModules

TLA+ snippets, operators, and modules contributed and curated by the TLA+ community
MIT License
273 stars 36 forks source link

Gconnect #70

Closed muenchnerkindl closed 2 years ago

muenchnerkindl commented 2 years ago

I am suggesting adding an operator to modules/Graph.tla that provides an alternative (and more efficient) definition of connectedness in graphs. In particular, TLC should be able to cache the result so that it does not have to be recomputed, for example when an invariant refers to nodes being connected.

I added a test for the operator in tests/GraphTests.tla but was not able to run the tests because they depend on TLCExt, which is no longer part of the Community modules.

lemmy commented 2 years ago

LGTM (https://github.com/tlaplus/CommunityModules/commit/a40c8c77c268769f80f8a3610c7b57c7c33d22e4)

By the way, the ant build should download the most up-to-date TLC nightly that contains TLCExt. What do you get if you run ant in the root folder?

muenchnerkindl commented 2 years ago

Yes, that works – thanks!