TLC now properly supports RandomElement and operators from the

Randomization module in constants and constant definitions.

Related to Github issue #866
tlaplus/tlaplus#866

Signed-off-by: Markus Alexander Kuppe <[email protected]>

Author: lemmy

specifications/SpanningTree/SpanTreeRandom.tla

@@ -40,13 +40,6 @@ Edges ==
   (*    expression equals a set that depends on the value of n.            *)
   (*************************************************************************)
 
-(***************************************************************************)
-(* Refuse to run TLC with multiple workers because RandomElement is a hack *)
-(* and may cause bogus counterexamples to be reported.                     *)
-(* See: https://github.com/tlaplus/tlaplus/issues/866                      *)
-(***************************************************************************)
-ASSUME TLCGet("config").worker = 1
-
 ASSUME /\ Root \in Nodes
        /\ MaxCardinality \in Nat
        /\ MaxCardinality >= Cardinality(Nodes)