system Deadlock
{
	/*********************************************************************
	*                                                                    *
	* Entry point                                                        *
	*                                                                    *
	*********************************************************************/

	// main dispatcher
	main thread MAIN ()
	{	
		loc loc0: live {}
			invoke {|Deadlock.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;
	}
	
	/*********************************************************************
	*                                                                    *
	* Deadlock                                                           *
	*                                                                    *
	*********************************************************************/

	// class static data members
	int /|Deadlock.state|\;
	
	// class instance data members
	record (|Deadlock|) extends (|java.lang.Object|)
	{
	}
	
	// constructor
	function {|Deadlock.()|} ((|Deadlock|) [|this|])
	{
		// return;
		loc loc0: live {}
			when true do
			{
			}
			return;
	}
	
	// static method
	function {|Deadlock.main(java.lang.String[]|} ()
	{
		// locals
		(|java.lang.Object|) [|lock1|];
		(|java.lang.Object|) [|lock2|];
		(|Process|) [|process1|];
		(|Process|) [|process2|];
		
		// lock1 = new java.lang.Object();
		loc loc0: live { [|lock1|] }
			when true do invisible
			{
				[|lock1|] := new (|java.lang.Object|);
				[|lock1|].l := new lock;
			}
			goto loc1;
			
		// lock1 = new java.lang.Object(); (continued)
		loc loc1: live { [|lock1|] }
			invoke {|java.lang.Object.()|} ([|lock1|])
			goto loc2;

		// lock2 = new java.lang.Object();
		loc loc2: live { [|lock1|], [|lock2|] }
			when true do invisible
			{
				[|lock2|] := new (|java.lang.Object|);
				[|lock2|].l := new lock;
			}
			goto loc3;

		// lock2 = new java.lang.Object(); (continued)
		loc loc3: live { [|lock1|], [|lock2|] }
			invoke {|java.lang.Object.()|} ([|lock2|])
			goto loc4;

		// process1 = new Process();
		loc loc4: live { [|lock1|], [|lock2|], [|process1|] }
			when true do invisible
			{
				[|process1|] := new (|Process|);
				[|process1|].l := new lock;
			}
			goto loc5;

		// process1 = new Process(); (continued)
		loc loc5: live { [|lock1|], [|lock2|], [|process1|] }
			invoke {|Process.()|} ([|process1|],
			                             [|lock1|], [|lock2|])
			goto loc6;

		// process2 = new Process();
		loc loc6: live { [|lock1|], [|lock2|], [|process1|],
			             [|process2|] }
			when true do invisible
			{
				[|process2|] := new (|Process|);
				[|process2|].l := new lock;
			}
			goto loc7;

		// process2 = new Process(); (continued)
		loc loc7: live { [|lock1|], [|lock2|], [|process1|],
			             [|process2|] }
			invoke {|Process.()|} ([|process2|], 
			                            [|lock2|], [|lock1|])
			goto loc8;

		// process1.start();
		loc loc8: live { [|lock1|], [|lock2|], [|process1|],
			             [|process2|] }
			when true do
			{
				start {|Process|} ([|process1|]);
			}
			goto loc9;

		// process2.start();
		loc loc9: live { [|lock1|], [|lock2|], [|process1|],
			             [|process2|] }
			when true do
			{
				start {|Process|} ([|process2|]);
			}
			goto loc10;

		// return;
		loc loc10: live {}
			when true do
			{
			}
			return;
	}

	/*********************************************************************
	*                                                                    *
	* Process                                                            *
	*                                                                    *
	*********************************************************************/
	
	// class instance data members
	record (|Process|) extends (|java.lang.Object|)
	{
		(|java.lang.Object|) /|Process.lock1|\;
		(|java.lang.Object|) /|Process.lock2|\;
	}
	
	// thread
	thread {|Process|} ((|Process|) [|this|])
	{
		loc loc0: live {}
			invoke virtual +|Process.run()|+ ([|this|])
			return;
	}
	
	// constructor
	function {|Process.()|} ((|Process|) [|this|],
	                               (|java.lang.Object|) [|lock1|],
	                               (|java.lang.Object|) [|lock2|])
	{	
		// this.lock1 = lock1;	
		loc loc0: live {}
			when true do
			{
				[|this|]./|Process.lock1|\ := [|lock1|];
			}
			goto loc1;
			
		// this.lock2 = lock2;	
		loc loc1: live {}
			when true do
			{
				[|this|]./|Process.lock2|\ := [|lock2|];
			}
			goto loc2;
		
		// return;
		loc loc2: live {}
			when true do
			{
			}
			return;
	}
	
	// instance method
	function {|Process.run()|} ((|Process|) [|this|])
	{
		// temps
		int temp0;
		(|java.lang.Object|) temp1;
		(|java.lang.Object|) temp2;
		
		// Deadlock.state++;
		loc loc0: live { temp0 }
			when true do
			{
				temp0 := /|Deadlock.state|\;
			}
			goto loc1;

		// Deadlock.state++; (continued)
		loc loc1: live { temp0 }
			when true do
			{
				temp0 := temp0 + 1;
			}
			goto loc2;

		// Deadlock.state++; (continued)
		loc loc2: live {}
			when true do
			{
				/|Deadlock.state|\ := temp0;
			}
			goto loc3;
			
		// synchronized (lock1) { ...
		loc loc3: live { temp1 }
			when true do
			{
				temp1 := [|this|]./|Process.lock1|\;
			}
			goto loc4;
		
		// synchronized (lock1) { ... (continued)
		loc loc4: live { temp1 }
			when lockAvailable (temp1.l) do
			{
				lock (temp1.l);
			}
			goto loc5;
			
		// synchronized (lock2) { ...
		loc loc5: live { temp1, temp2 }
			when true do
			{
				temp2 := [|this|]./|Process.lock2|\;
			}
			goto loc6;
			
		// synchronized (lock2) { ... (continued)
		loc loc6: live { temp1, temp2 }
			when lockAvailable (temp2.l) do
			{
				lock (temp2.l);
			}
			goto loc7;
			
		// Deadlock.state++;
		loc loc7: live { temp0, temp1, temp2 }
			when true do
			{
				temp0 := /|Deadlock.state|\;
			}
			goto loc8;
			
		// Deadlock.state++; (continued)
		loc loc8: live { temp0, temp1, temp2 }
			when true do
			{
				temp0 := temp0 + 1;
			}
			goto loc9;
			
		// Deadlock.state++; (continued)
		loc loc9: live { temp1, temp2 }
			when true do
			{
				/|Deadlock.state|\ := temp0;
			}
			goto loc10;
			
		// ... } synchronized (lock2) (continued)
		loc loc10: live { temp1 }
			when hasLock (temp2.l) do
			{
				unlock (temp2.l);
			}
			goto loc11;
			
		// ... } synchronized (lock1) (continued)
		loc loc11: live {}
			when hasLock (temp1.l) do
			{
				unlock (temp1.l);
			}
			goto loc12;
		
		// return;
		loc loc12: live {}
			when true do
			{
			}
			return;
	}
	
	// virtual table
	virtual +|Process.run()|+
	{
		(|Process|) -> {|Process.run()|}
	}
}