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]>
tlaplus · Jun 26, 2024 · 6eacad2 · 6eacad2
1 parent d0036f8
commit 6eacad2
Showing 1 changed file with 0 additions and 7 deletions.
diff --git a/specifications/SpanningTree/SpanTreeRandom.tla b/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)