Proved deadlock cant occour in cupboard. QED.

Beverage.jr

@@ -6,7 +6,7 @@ public class Beverage {
   private final String name;
   private final int drinkingTime;
   private final BeverageWare bw;
-  private final Item[] ingredients;
+  private final ArrayList<Item> ingredients;
 
   @Override
   public String toString()
@@ -16,11 +16,11 @@ public class Beverage {
 
 
 
-  public Beverage(String name, int drinkingTime, BeverageWare bw, Item[] ingredients) {
+  public Beverage(String name, int drinkingTime, BeverageWare bw, List<Item> ingredients) {
     this.name = name;    
     this.drinkingTime = drinkingTime;
     this.bw = bw;
-    this.ingredients = ingredients;
+    this.ingredients = new ArrayList(ingredients);
   }
 
 
@@ -32,7 +32,7 @@ public class Beverage {
     return bw;
   }
 
-  public Item[] getIngredients() {
+  public List<Item> getIngredients() {
     return ingredients;
   }    
 

Cupboard.jr

@@ -19,8 +19,8 @@ public class Cupboard {
     this(Global.IngrediensList, Global.startGlassCount, Global.startCupsCount);    
   }  
 
-  public Cupboard(List<Item> items, int startNumGlasses, int startNumCups) {
-    this.items = new ArrayList(items);    
+  public Cupboard(List<Item> inItems, int startNumGlasses, int startNumCups) {
+    items = new ArrayList(inItems);    
     for(int i = 0; i < startNumGlasses; i++)
       {
         items.add(Global.glass);        
@@ -67,14 +67,14 @@ public class Cupboard {
   ***************************************************/
   public static void main(String[] args) {
     allCupboardTests();
-
   }
 
   public static void allCupboardTests()
   {
     testStartsWithItems();
     testAddItems();
     testAquireItems();
+    testTakeSeveralIngredients();
     System.out.println("Cupboard tests passed.");    
   }
 
@@ -103,7 +103,57 @@ public class Cupboard {
     cb.aquireItem(Global.beerTap);
     asserts(!cb.items.contains(Global.beerTap), "BeerTap still in cupboard. 3");           
   }  
+
+  public static void testTakeSeveralIngredients()
+  {
+    final List<Beverage> bl = Global.beverageList;
+    for(int tries = 0; tries < 10; tries++)
+      {        
+        for(int i = 0; i < bl.size(); i++)
+          for(int j = 0; j < bl.size(); j++)
+            {  
+              Cupboard cb = new Cupboard();
+              new ItemTaker(bl.get(i).getIngredients(), cb);
+              new ItemTaker(bl.get(j).getIngredients(), cb);                              
+            }
+      }
+
+    for(int i = 0; i < bl.size()*bl.size()*10*2; i++ )
+      {        
+        P(ItemTaker.s);   
+      }    
+  }  
 
+  // This class is ONLY used in testing
+  private static class ItemTaker
+  {
+    private List<Item> items;   
+    private Cupboard cb;    
+    static Random r = new Random();
+    public static sem s = 0;
+
+    public ItemTaker(List<Item> items, Cupboard cb)
+    {
+      this.items = items;      
+      this.cb = cb;
+
+    }    
+    public process p{
+      for (Iterator<Item> it = items.iterator(); it.hasNext();) {    
+        JR.nap(r.nextInt(100)); // testing randomness :)
+        Item item = it.next();        
+        call cb.aquireItem(item);    
+      }
+      for (Iterator<Item> it = items.iterator(); it.hasNext();) {
+        JR.nap(10);        
+        Item item = it.next();
+        call cb.putBackItem(item);
+      }
+      V(s);      
+    }    
+  }
+
+
   public static void asserts(boolean b, String s)
   {
     if(!b)

Global.jr

@@ -33,16 +33,15 @@ public class Global {
   public final static BeverageWare cup    = new BeverageWare("Cup",   2);  
 
   // Required Ingredients
-  private final static Item[] beerIngredients      = {beerTap};
-  private final static Item[] cappucinoIngredients = {milk, coffee};
-  private final static Item[] choclateIngredients  = {milk, choclatePowder};
-
-
+  private final static List<Item> beerIngredients      = Arrays.asList(beerTap);
+  private final static List<Item> cappucinoIngredients = Arrays.asList(milk, coffee);
+  private final static List<Item> choclateIngredients  = Arrays.asList(milk, choclatePowder);
 
   // Beverages
   public final static Beverage beer      = new Beverage("Beer",      BEER_DRINKING_TIME,      glass, beerIngredients);
   public final static Beverage cappucino = new Beverage("Cappucino", CAPPUCINO_DRINKING_TIME, cup,   cappucinoIngredients);
   public final static Beverage choclate  = new Beverage("Choclate",  CHOCLATE_DRINKING_TIME,  cup,   choclateIngredients);
 
-  public final static Beverage[] beverageList = {beer, cappucino, choclate};  
+  public final static List<Beverage> beverageList = 
+    Arrays.asList(beer, cappucino, choclate);  
 }

JRProcess.j_r

@@ -0,0 +1,14 @@
+import edu.ucdavis.jr.*;
+import java.util.*;
+
+
+public interface JRProcess {
+
+  public process p
+  {
+    run();    
+  }
+
+  public abstract void run();
+
+}

jrGen/Door.java

@@ -238,7 +238,7 @@ else if ((handler != null) && !(JRe instanceof java.rmi.RemoteException))
     @SuppressWarnings(value = "unchecked")
     private void startLoop() {
         InStatObj JRInstmt1 = new InStatObj(3, false);
-        JRLoop3: while (true) {
+        JRLoop9: while (true) {
             {
                 // Inni Statement without quantifier
                 JRInstmt1.armArray[0] = new QuantRec(new Cap_ext_(op_lock_Cap_voidTovoidTojavadotutildotArrayList, "java.util.ArrayList<Person>"), 0, 0);
@@ -500,7 +500,7 @@ else if ((JRrrecv1.handler != null) && !(JRe instanceof java.rmi.RemoteException
                                                 if (isLocked && entrants.size() == 0) {
                                                     { if (JRrrecv1.retOp != null)
                                                         JRrrecv1.retOp.send(jrvm.getTimestamp(), (java.lang.Object []) null);
-                                                    break JRLoop3;}
+                                                    break JRLoop9;}
                                                 }
                                             }
                                         } catch (Exception JRe) {

jrGen/Global.java

@@ -32,12 +32,13 @@ public Global() {
     public static final List IngrediensList = Arrays.asList(beerTap, coffee, milk, choclatePowder);
     public static final BeverageWare glass = new BeverageWare("Glass", 1);
     public static final BeverageWare cup = new BeverageWare("Cup", 2);
-    private static final Item[] beerIngredients = {beerTap};
-    private static final Item[] cappucinoIngredients = {milk, coffee};
-    private static final Item[] choclateIngredients = {milk, choclatePowder};
+    private static final List beerIngredients = Arrays.asList(beerTap);
+    private static final List cappucinoIngredients = Arrays.asList(milk, coffee);
+    private static final List choclateIngredients = Arrays.asList(milk, choclatePowder);
     public static final Beverage beer = new Beverage("Beer", BEER_DRINKING_TIME, glass, beerIngredients);
     public static final Beverage cappucino = new Beverage("Cappucino", CAPPUCINO_DRINKING_TIME, cup, cappucinoIngredients);
     public static final Beverage choclate = new Beverage("Choclate", CHOCLATE_DRINKING_TIME, cup, choclateIngredients);
+    public static final List beverageList = Arrays.asList(beer, cappucino, choclate);
     protected boolean JRcalled = false;
     protected JRGlobal jrresref;
     public Object JRgetjrresref()