I loaded your spec with the Toolbox, had it instantiate the constant
`vertices' with a set {n1, n2, n3} of model values, and ran TLC on the
spec. It reported the error
TLC encountered a non-enumerable quantifier bound
Seq({n1, n2, n3}).
line 18, col 38 to line 18, col 38 of module Test
where the location was the first S in the definition of
existsUniqueIn(S, P(_))
If you read the section in Specifying Systems on how TLC checks a
spec, you should realize that evaluating isTree requires TLC to
enumerate the infinite set Seq(vertices).
The simplest way to fix this is to modify the definition of isTree so it
applies existsUniqueIn to a finite set of sequences--for example
sequences of length at most equal to the cardinality of `vertices'.
Your approach of defining a spec with a stuttering next-state action
works. However, you can accomplish the same thing by not having
any variables or behavior spec, and simply having the Toolbox
tell TLC to evaluate the constant formula
\A root \in vertices, edges \in SUBSET SUBSET vertices
/\ (\A e \in edges : Cardinality(e) = 2)
/\ isTree(edges, root)
/\ PrintT("tree:") /\ PrintT(<< edges, root >>)
However, my guess is that you'll run TLC out of memory with a set
`vertices' containing more than 3 nodes.
Personally, I have found it most convenient to define a tree to
be a set of vertices together with a function mapping each non-root
node to its parent. However, what works best depends on what you're
going to use the definition for.