@@ -0,0 +1,2545 @@
+// Copyright (c) 2003 Compaq Corporation.  All rights reserved.%0A// Portions Copyright (c) 2003 Microsoft Corporation.  All rights reserved.%0A// Last modified on Mon 30 Apr 2007 at 15:29:55 PST by lamport%0A//      modified on Tue Nov  9 11:06:41 PST 1999 by yuanyu%0A%0Apackage tlc2.tool.impl;%0A%0Aimport tla2sany.semantic.SymbolNode;%0Aimport tlc2.output.EC;%0Aimport tlc2.tool.IContextEnumerator;%0Aimport tlc2.util.Context;%0Aimport tlc2.value.impl.TupleValue;%0Aimport tlc2.value.impl.Value;%0Aimport tlc2.value.impl.ValueEnumeration;%0Aimport util.Assert;%0A%0Apublic final class RandomizingContextEnumerator implements IContextEnumerator %7B%0A  private Context con;%0A  private Object%5B%5D vars;%0A  private ValueEnumeration%5B%5D enums;%0A  private Value%5B%5D currentElems;%0A  private boolean isDone;%0A%0A  public RandomizingContextEnumerator(Object%5B%5D vars, ValueEnumeration%5B%5D enums, Context con) %7B%0A    this.con = con;%0A    this.vars = vars;%0A    this.enums = enums;%0A    this.currentElems = new Value%5Benums.length%5D;%0A    this.isDone = false;%0A    for (int i = 0; i %3C enums.length; i++) %7B%0A      this.currentElems%5Bi%5D = this.enums%5Bi%5D.someElement();%0A      if (this.currentElems%5Bi%5D == null) %7B%0A%09this.isDone = true;%0A%09break;%0A      %7D%0A    %7D%0A  %7D%0A  %0A  @Override%0A  public final Context nextElement() %7B%0A      Context con1 = this.con;%0A      if (this.isDone) return null;%0A      for (int i = 0; i %3C enums.length; i++) %7B%0A          if (this.vars%5Bi%5D instanceof SymbolNode) %7B%0A              con1 = con1.cons((SymbolNode)this.vars%5Bi%5D, this.currentElems%5Bi%5D);%0A          %7D%0A          else %7B%0A              SymbolNode%5B%5D varList = (SymbolNode%5B%5D)this.vars%5Bi%5D;%0A              Value argVal = this.currentElems%5Bi%5D;%0A              if (!(argVal instanceof TupleValue)) %7B%0A                  Assert.fail(EC.TLC_ARGUMENT_MISMATCH, varList%5B0%5D.toString());%0A              %7D%0A              Value%5B%5D valList = ((TupleValue)argVal).elems;%0A              if (varList.length != valList.length) %7B%0A                  Assert.fail(EC.TLC_ARGUMENT_MISMATCH, varList%5B0%5D.toString());%0A              %7D%0A              for (int j = 0; j %3C varList.length; j++) %7B%0A                  con1 = con1.cons(varList%5Bj%5D, valList%5Bj%5D);%0A              %7D%0A          %7D%0A      %7D%0A      for (int i = 0; i %3C enums.length; i++) %7B%0A          this.currentElems%5Bi%5D = this.enums%5Bi%5D.someElement();%0A          if (this.currentElems%5Bi%5D != null) break;%0A          if (i == this.enums.length - 1) %7B%0A              this.isDone = true;%0A              break;%0A          %7D%0A          this.enums%5Bi%5D.reset();%0A          this.currentElems%5Bi%5D = this.enums%5Bi%5D.someElement();%0A      %7D%0A      return con1;%0A  %7D%0A%0A%7D%0A%0A

Break non-determinism in simulation mode by picking one successor state probabilistically (uniform).