tlaplus / CommunityModules

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

TLC fails to evaluate `Graphs!Path` because of `Seq` #58

Closed lemmy closed 2 years ago

lemmy commented 2 years ago
(tla+) LET G == INSTANCE Graphs IN G!Path([node |-> {1,2,3}, edge |-> {<<1,2>>, <<2,3>>, <<3,1>>, <<1,3>>}])
{p \in Seq({1, 2, 3}) : <expression line 20, col 14 to line 21, col 68 of module Graphs> }

https://github.com/tlaplus/CommunityModules/blob/6f9596b80382704f47001943ed35a7e6dad8238b/modules/Graphs.tla#L19

For the definition AreConnected built on top of Path in Graphs, the new definition SimplePath based on SequencesExt!SeqOf(G.node, Cardinality(G.node)) should work.

Definition of SimplePath follows e.g. the "A directed path is simple if it has no repeated vertices." given in https://algs4.cs.princeton.edu/42digraph/.