system BoundedBuffer
{
	/*********************************************************************
	*                                                                    *
	* Entry point                                                        *
	*                                                                    *
	*********************************************************************/

	// main dispatcher
	main thread MAIN ()
	{	
		loc loc0: live {}
			invoke {|BBDriver.main(java.lang.String[]|} ()
			return;
	}

	/*********************************************************************
	*                                                                    *
	* java.lang.Object                                                   *
	*                                                                    *
	*********************************************************************/

	// class instance data members
	top record (|java.lang.Object|)
	{
		lock l;
	}
		
	// constructor
	function {|java.lang.Object.()|} ((|java.lang.Object|) [|this|])
	{
		loc loc0: live {}
			when true do
			{
			}
			return;
	}
	
	/*********************************************************************
	*                                                                    *
	* java.lang.InterruptedException                                     *
	*                                                                    *
	*********************************************************************/

	// class instance data members
	throwable record (|java.lang.InterruptedException|)
		extends (|java.lang.Object|)
	{
	}

	// constructor
	function {|java.lang.InterruptedException.()|}
		((|java.lang.InterruptedException|) [|this|])
	{
		loc loc0: live {}
			when true do
			{
			}
			return;
	}
		
	/*********************************************************************
	*                                                                    *
	* BBDriver                                                           *
	*                                                                    *
	*********************************************************************/
	
	// class instance data members
	record (|BBDriver|) extends (|java.lang.Object|)
	{
	}
	
	// constructor
	function {|BBDriver.()|} ((|BBDriver|) [|this|])
	{
		// return;
		loc loc0: live {}
			when true do
			{
			}
			return;
	}
	
	// static method
	function {|BBDriver.main(java.lang.String[]|} ()
	{
		(|BoundedBuffer|) [|b1|];
		(|BoundedBuffer|) [|b2|];
		
		(|java.lang.Object|) temp$0;
		(|InOut|) temp$1;
		
		// BoundedBuffer b1 = new BoundedBuffer(3);
		loc loc0: live { [|b1|] }
			when true do invisible
			{
				[|b1|] := new (|BoundedBuffer|);
				[|b1|].l := new lock;
			}
			goto loc1;
		
		// BoundedBuffer b1 = new BoundedBuffer(3); (continued)
		loc loc1: live { [|b1|] }
			invoke {|BoundedBuffer.()|}([|b1|], 3)
			goto loc2;
		
		// BoundedBuffer b2 = new BoundedBuffer(3);
		loc loc2: live { [|b1|], [|b2|] }
			when true do invisible
			{
				[|b2|] := new (|BoundedBuffer|);
				[|b2|].l := new lock;
			}
			goto loc3;
		
		// BoundedBuffer b2 = new BoundedBuffer(3); (continued)
		loc loc3: live { [|b1|], [|b2|] }
			invoke {|BoundedBuffer.()|}([|b2|], 3)
			goto loc4;
			
		// b1.add(new Object());
		loc loc4: live { [|b1|], [|b2|], temp$0 }
			when true do invisible
			{
				temp$0 := new (|java.lang.Object|);
				temp$0.l := new lock;
			}
			goto loc5;
		
		// b1.add(new Object()); (continued)
		loc loc5: live { [|b1|], [|b2|], temp$0 }
			invoke {|java.lang.Object.()|}(temp$0)
			goto loc6;
			
		// b1.add(new Object()); (continued)
		loc loc6: live { [|b1|], [|b2|] }
			invoke {|BoundedBuffer.add()|}([|b1|], temp$0)
			goto loc7;
			//invoke {|BoundedBuffer.add()|}([|b2|], temp$0)
			//goto loc10;
			
		// b1.add(new Object());
		loc loc7: live { [|b1|], [|b2|], temp$0 }
			when true do invisible
			{
				temp$0 := new (|java.lang.Object|);
				temp$0.l := new lock;
			}
			goto loc8;
		
		// b1.add(new Object()); (continued)
		loc loc8: live { [|b1|], [|b2|], temp$0 }
			invoke {|java.lang.Object.()|}(temp$0)
			goto loc9;
			
		// b1.add(new Object()); (continued)
		loc loc9: live { [|b1|], [|b2|] }
			invoke {|BoundedBuffer.add()|}([|b1|], temp$0)
			goto loc10;
				
		// (new InOut(b1, b2)).start();
		loc loc10: live { [|b1|], [|b2|], temp$1 }
			when true do invisible
			{
				temp$1 := new (|InOut|);
				temp$1.l := new lock;
			}
			goto loc11;
			
		// (new InOut(b1, b2)).start(); (continued)
		loc loc11: live { [|b1|], [|b2|], temp$1 }
			invoke {|InOut.()|}(temp$1, [|b1|], [|b2|])
			goto loc12;
			
		// (new InOut(b1, b2)).start(); (continued)
		loc loc12: live { [|b1|], [|b2|] }
			when true do
			{
				start {|InOut|}(temp$1);
			}
			goto loc13;			
				
		// (new InOut(b2, b1)).start();
		loc loc13: live { [|b1|], [|b2|], temp$1 }
			when true do invisible
			{
				temp$1 := new (|InOut|);
				temp$1.l := new lock;
			}
			goto loc14;
			
		// (new InOut(b2, b1)).start(); (continued)
		loc loc14: live { [|b1|], [|b2|], temp$1 }
			invoke {|InOut.()|}(temp$1, [|b2|], [|b1|])
			goto loc15;
			
		// (new InOut(b2, b1)).start(); (continued)
		loc loc15: live { [|b1|], [|b2|] }
			when true do
			{
				start {|InOut|}(temp$1);
			}
			return;
	}
	
	/*********************************************************************
	*                                                                    *
	* BoundedBuffer                                                      *
	*                                                                    *
	*********************************************************************/
	
	// class instance data members
	record (|BoundedBuffer|) extends (|java.lang.Object|)
	{
		(|java.lang.Object|)[] /|BoundedBuffer.buffer|\;
		int /|BoundedBuffer.bound|\;
		int /|BoundedBuffer.head|\;
		int /|BoundedBuffer.tail|\;
	}

	// constructor
	function {|BoundedBuffer.()|} ((|BoundedBuffer|) [|this|],
	                                     int [|b|])
	{
		(|java.lang.Object|)[] temp$0;
		
		// bound = b;
		loc loc0: live {}
			when true do
			{
				[|this|]./|BoundedBuffer.bound|\ := [|b|];
			}
			goto loc1;
		
		// buffer = new Object[b];
		loc loc1: live { temp$0 }
			when true do
			{
				[|this|]./|BoundedBuffer.buffer|\ :=
					new (|java.lang.Object|)[[|b|]];
				[|this|]./|BoundedBuffer.buffer|\.l := new lock;
			}
			goto loc2;
			
     	// head = 0;
		loc loc2: live {}
			when true do
			{
				[|this|]./|BoundedBuffer.head|\ := 0;
			}
			goto loc3;
			
     	// tail = b - 1;
		loc loc3: live {}
			when true do
			{
				[|this|]./|BoundedBuffer.tail|\ := [|b|] - 1;
			}
			return;
	}
	
	// public synchronized void add(Object o)
	function {|BoundedBuffer.add()|} ((|BoundedBuffer|) [|this|],
	                                  (|java.lang.Object|) [|o|])
	{
		(|java.lang.InterruptedException|) [|ie|];
		
		int temp$0;
		int temp$1;
		(|java.lang.Object|)[] temp$2;
		
		// ... synchronized
		loc loc0: live {}
			when lockAvailable ([|this|].l) do
			{
				assert ([|o|] != null);
				lock ([|this|].l);
			}
			goto loc1;
		
		// while (tail == head)
		loc loc1: live { temp$0 }
			when true do
			{
				temp$0 := [|this|]./|BoundedBuffer.head|\;
			}
			goto loc2;
		
		// while (tail == head) (continued)	
		loc loc2: live { temp$0, temp$1 }
			when true do
			{
				temp$1 := [|this|]./|BoundedBuffer.tail|\;
			}
			goto loc3;
			
		// while (tail == head) (continued)	
		loc loc3: live {}
			when temp$0 == temp$1 do
			{
			}
			goto loc4;
			when temp$0 != temp$1 do
			{
			}
			goto loc6;
		
		// wait();
		loc loc4: live {}
			when lockAvailable ([|this|].l) do
			{
				wait ([|this|].l);
			}
			goto loc5;
			
		// wait(); (continued)
		loc loc5: live {}
			when lockAvailable ([|this|].l) && wasNotified ([|this|].l) do
			{
				unwait ([|this|].l);
			}
			goto loc1;
			
		// buffer[head] = o;
		loc loc6: live { temp$0 }
			when true do
			{
				temp$0 := [|this|]./|BoundedBuffer.head|\;
			}
			goto loc7;
			
		// buffer[head] = o; (continued)
		loc loc7: live { temp$0, temp$2 }
			when true do
			{
				temp$2 := [|this|]./|BoundedBuffer.buffer|\;
			}
			goto loc8;
			
		// buffer[head] = o; (continued)
		loc loc8: live {}
			when true do
			{
				temp$2[temp$0] := [|o|];
			}
			goto loc9;
			
		// head = (head + 1) % bound;
		loc loc9: live { temp$0 }
			when true do
			{
				temp$0 := [|this|]./|BoundedBuffer.head|\;
				temp$0 := temp$0 + 1;
			}
			goto loc10;
		
		// head = (head + 1) % bound; (continued)
		loc loc10: live { temp$0 }
			when true do
			{
				temp$1 := [|this|]./|BoundedBuffer.bound|\;
				temp$0 := temp$0 % temp$1;
			}
			goto loc11;
			
		// head = (head + 1) % bound; (continued)
		loc loc11: live {}
			when true do
			{
				[|this|]./|BoundedBuffer.head|\ := temp$0;
			}
			goto loc12;
			
		// notifyAll();
		loc loc12: live {}
			when hasLock ([|this|].l) do
			{
				notifyAll ([|this|].l);
			}
			goto loc13;
		
		// ... synchronized	
		loc loc13: live {}
			when hasLock ([|this|].l) do
			{
				unlock ([|this|].l);
			}
			return;
			
		catch (|java.lang.InterruptedException|) [|ie|]
			at loc4, loc5 goto loc1;
	}
	
	// public synchronized Object take()
	function {|BoundedBuffer.take()|}((|BoundedBuffer|) [|this|])
		returns (|java.lang.Object|)
	{
		(|java.lang.Object|) $ret;

		(|java.lang.InterruptedException|) [|ie|];
		
		int temp$0;
		int temp$1;
		int temp$2;
		(|java.lang.Object|)[] temp$3;
		
		// ... synchronized
		loc loc0: live {}
			when lockAvailable ([|this|].l) do
			{
				lock ([|this|].l);
			}
			goto loc1;
		
		// while (head == ((tail + 1) % bound))
		loc loc1: live { temp$0 }
			when true do
			{
				temp$0 := [|this|]./|BoundedBuffer.head|\;
			}
			goto loc2;
		
		// while (head == ((tail + 1) % bound)) (continued)
		loc loc2: live { temp$0, temp$1 }
			when true do
			{
				temp$1 := [|this|]./|BoundedBuffer.tail|\;
				temp$1 := temp$1 + 1;
			}
			goto loc3;
			
		// while (head == ((tail + 1) % bound)) (continued)
		loc loc3: live { temp$0, temp$1 }
			when true do
			{
				temp$2 := [|this|]./|BoundedBuffer.bound|\;
				temp$1 := temp$1 % temp$2;
			}
			goto loc4;
			
		// while (head == ((tail + 1) % bound)) (continued)
		loc loc4: live {}
			when temp$0 == temp$1 do
			{
			}
			goto loc5;
			when temp$0 != temp$1 do
			{
			}
			goto loc7;
		
		// wait();
		loc loc5: live {}
			when lockAvailable ([|this|].l) do
			{
				wait ([|this|].l);
			}
			goto loc6;
			
		// wait(); (continued)
		loc loc6: live {}
			when lockAvailable ([|this|].l) && wasNotified ([|this|].l) do
			{
				unwait ([|this|].l);
			}
			goto loc1;
			
		// tail = (tail + 1) % bound;
		loc loc7: live { temp$0 }
			when true do
			{
				temp$0 := [|this|]./|BoundedBuffer.tail|\;
				temp$0 := temp$0 + 1;
			}
			goto loc8;
		
		// tail = (tail + 1) % bound; (continued)
		loc loc8: live { temp$0 }
			when true do
			{
				temp$1 := [|this|]./|BoundedBuffer.bound|\;
				temp$0 := temp$0 % temp$1;
			}
			goto loc9;
			
		// tail = (tail + 1) % bound; (continued)
		loc loc9: live {}
			when true do
			{
				[|this|]./|BoundedBuffer.tail|\ := temp$0;
			}
			goto loc10;
			
		// notifyAll();
		loc loc10: live {}
			when hasLock ([|this|].l) do
			{
				notifyAll ([|this|].l);
			}
			goto loc11;
		
		// return buffer[tail];
		loc loc11: live { temp$0 }
			when true do
			{
				temp$0 := [|this|]./|BoundedBuffer.tail|\;
			}
			goto loc12;
		
		// return buffer[tail]; (continued)
		loc loc12: live { temp$3, $ret }
			when true do
			{
				temp$3 := [|this|]./|BoundedBuffer.buffer|\;
			}
			goto loc13;
			
		// return buffer[tail]; (continued)
		loc loc13: live { $ret }
			when true do
			{
				$ret := temp$3[temp$0];
				assert ($ret != null);
			}
			goto loc14;
		
		// ... synchronized	
		loc loc14: live { $ret }
			when hasLock ([|this|].l) do
			{
				unlock ([|this|].l);
			}
			return $ret;
			
		catch (|java.lang.InterruptedException|) [|ie|]
			at loc5, loc6 goto loc1;
	}
	
	// public synchronized boolean isEmpty()
	function {|BoundedBuffer.isEmpty()|}
		((|BoundedBuffer|) [|this|]) returns boolean
	{
		boolean $ret;
		
		int temp$0;
		int temp$1;
		int temp$2;
		
		// return head == ((tail + 1) % bound);
		loc loc0: live { temp$0 }
			when true do
			{
				temp$0 := [|this|]./|BoundedBuffer.head|\;
			}
			goto loc1;
			
		// return head == ((tail + 1) % bound); (continued)
		loc loc1: live { temp$0, temp$1 }
			when true do
			{
				temp$1 := [|this|]./|BoundedBuffer.tail|\;
				temp$1 := temp$1 + 1;
			}
			goto loc2;
			
		// return head == ((tail + 1) % bound); (continued)
		loc loc2: live { temp$0, temp$1 }
			when true do
			{
				temp$2 := [|this|]./|BoundedBuffer.bound|\;
				temp$1 := temp$1 + temp$2;
			}
			goto loc3;
			
		// return head == ((tail + 1) % bound); (continued)
		loc loc3: live { $ret }
			when true do
			{
				$ret := temp$0 == temp$1;
			}
			return $ret;
	}
	
	/*********************************************************************
	*                                                                    *
	* InOut                                                              *
	*                                                                    *
	*********************************************************************/
	
	// class instance data members
	record (|InOut|) extends (|java.lang.Object|)
	{
		(|BoundedBuffer|) /|InOut.in|\;
		(|BoundedBuffer|) /|InOut.out|\;
	}
	
	// thread
	thread {|InOut|} ((|InOut|) [|this|])
	{
		loc loc0: live {}
			invoke {|InOut.run()|} ([|this|])
			return;
	}
	
	// constructor
	function {|InOut.()|} ((|InOut|) [|this|],
	                             (|BoundedBuffer|) [|in|],
	                             (|BoundedBuffer|) [|out|])
	{	
		// this.lock1 = lock1;	
		loc loc0: live {}
			when true do
			{
				[|this|]./|InOut.in|\ := [|in|];
			}
			goto loc1;
			
		// this.lock2 = lock2;	
		loc loc1: live {}
			when true do
			{
				[|this|]./|InOut.out|\ := [|out|];
			}
			return;
	}
	
	// instance method
	function {|InOut.run()|} ((|InOut|) [|this|])
	{
		(|java.lang.Object|) [|tmp|];
		
		(|BoundedBuffer|) temp$0;

		// while(true)
		// tmp = in.take();
		loc loc0: live { [|tmp|], temp$0 }
			when true do
			{
				temp$0 := [|this|]./|InOut.in|\;
			}
			goto loc1;
		
		// tmp = in.take(); (continued)
		loc loc1: live { [|tmp|] }
			[|tmp|] := invoke {|BoundedBuffer.take()|}(temp$0)
			goto loc2;
			
		// out.take(tmp);
		loc loc2: live { [|tmp|], temp$0 }
			when true do
			{
				temp$0 := [|this|]./|InOut.out|\;
			}
			goto loc3;
			
		// out.take(tmp); (continued)
		loc loc3: live {}
			invoke {|BoundedBuffer.add()|}(temp$0, [|tmp|])
			goto loc0;		
	}
}