import jcsp.lang.*;
import jcsp.util.*;
import java.util.*;

public class LiftSystem {

	//Barriers for synchronization of entering and exiting
	protected static Barrier barrier_internalrequest = new Barrier ();
	protected static Barrier barrier_externalrequest = new Barrier ();
	protected static Barrier barrier_arrive = new Barrier ();
	protected static Barrier barrier_arrive_sub1 = new Barrier ();
	protected static Barrier barrier_servenextrequest = new Barrier ();
	protected static Barrier barrier_servenextrequest_sub1 = new Barrier ();
	protected static Barrier barrier_servenextrequest_sub2 = new Barrier ();
	protected static Barrier barrier_openclosedoor = new Barrier ();
	protected static Barrier barrier_reopendoorfrominside = new Barrier ();
	protected static Barrier barrier_reopendoorfromoutside = new Barrier ();
	protected static Barrier barrier_serveinitintrequest = new Barrier ();
	protected static Barrier barrier_serveinitintrequest_sub1 = new Barrier ();
	protected static Barrier barrier_serveinitextrequest = new Barrier ();
	protected static Barrier barrier_serveinitextrequest_sub1 = new Barrier ();
	protected static Barrier barrier_nomorerequest = new Barrier ();

	//Barriers for cold condition violation in the charts or sub-charts
	protected static Barrier servenextrequest_sub2_convio = new Barrier ();
	protected static Barrier reopendoorfrominside_convio = new Barrier ();
	protected static Barrier reopendoorfromoutside_convio = new Barrier ();
	protected static Barrier serveinitintrequest_convio = new Barrier ();
	protected static Barrier serveinitextrequest_convio = new Barrier ();
	protected static Barrier nomorerequest_convio = new Barrier ();

	//Main Method
	public static void main (String [] args) {

		//Channels connecting objects
		One2OneChannel usercontroller_intReq = new One2OneChannel ();
		One2OneChannel usercontroller_extReq = new One2OneChannel ();
		One2OneChannel shaftcontroller_arriving = new One2OneChannel ();
		One2OneChannel shaftcontroller_stop = new One2OneChannel ();
		One2OneChannel shaftcontroller_stopped = new One2OneChannel ();
		One2OneChannel doorcontroller_open = new One2OneChannel ();
		One2OneChannel doorcontroller_opened = new One2OneChannel ();
		One2OneChannel shaftcontroller_keepmoving = new One2OneChannel ();
		One2OneChannel shaftcontroller_turnaroundmoving = new One2OneChannel ();
		One2OneChannel doorcontroller_close = new One2OneChannel ();
		One2OneChannel doorcontroller_closed = new One2OneChannel ();
		One2OneChannel shaftcontroller_movingup = new One2OneChannel ();
		One2OneChannel shaftcontroller_movingdown = new One2OneChannel ();

		//Components in the system
		User user = new User (usercontroller_intReq, usercontroller_extReq);
		Controller controller = new Controller (usercontroller_intReq, usercontroller_extReq, shaftcontroller_arriving, shaftcontroller_stop, shaftcontroller_stopped, shaftcontroller_keepmoving, shaftcontroller_turnaroundmoving, doorcontroller_open, doorcontroller_opened, doorcontroller_close, doorcontroller_closed, 5);
		Shaft shaft = new Shaft (shaftcontroller_arriving, shaftcontroller_stop, shaftcontroller_stopped, shaftcontroller_keepmoving, shaftcontroller_turnaroundmoving, shaftcontroller_movingup, shaftcontroller_movingdown);
		Door door = new Door (doorcontroller_open, doorcontroller_opened, doorcontroller_close, doorcontroller_closed);

		//System initialization
		CSProcess[] parArray = new CSProcess[] {controller, user, shaft, door};
		Parallel sys = new Parallel (parArray);
		sys.run();
	}
}

//Object Users in the Specification
class User implements CSProcess {

	//All instances
	private User_InternalRequest internalrequest;
	private User_ExternalRequest externalrequest;
	private User_ReopenDoorFromInside reopendoorfrominside;
	private User_ReopenDoorFromOutside reopendoorfromoutside;
	private User_ServeInitIntRequest serveinitintrequest;
	private User_ServeInitExtRequest serveinitextrequest;

	//All channels

	private One2OneChannel usercontroller_intReq;
	private One2OneChannel usercontroller_extReq;

	//Data

	private User_Data user_data;

	public User (One2OneChannel usercontroller_intReq, One2OneChannel usercontroller_extReq) {
		user_data = new User_Data();

		this.usercontroller_intReq = usercontroller_intReq;
		this.usercontroller_extReq = usercontroller_extReq;

		internalrequest = new User_InternalRequest (user_data, usercontroller_intReq);
		externalrequest = new User_ExternalRequest (user_data, usercontroller_extReq);
		reopendoorfrominside = new User_ReopenDoorFromInside (user_data, usercontroller_intReq);
		reopendoorfromoutside = new User_ReopenDoorFromOutside (user_data, usercontroller_extReq);
		serveinitintrequest = new User_ServeInitIntRequest (user_data, usercontroller_intReq);
		serveinitextrequest = new User_ServeInitExtRequest (user_data, usercontroller_extReq);
	}

	public void run () {
			new Parallel (new CSProcess[]{internalrequest,externalrequest,reopendoorfrominside,reopendoorfromoutside,serveinitintrequest,serveinitextrequest}).run();
	}
}

//Data Class of Users

class User_Data {}

//Behavior of Users in Chart InternalRequest

class User_InternalRequest implements CSProcess {
	private ProcessManager manager;
	private User_InternalRequest_Child child;
	private User_Data user_data;
	private One2OneChannel usercontroller_intReq;

	public User_InternalRequest (User_Data user_data, One2OneChannel usercontroller_intReq) {
		this.user_data = user_data;
		this.usercontroller_intReq = usercontroller_intReq;
	}

	public void run () {
		while (true) {
			child = new User_InternalRequest_Child (user_data, usercontroller_intReq);
			manager = new ProcessManager (child);
			manager.start();
		}
	}
}

class User_InternalRequest_Child implements CSProcess {
	private One2OneChannel usercontroller_intReq;
	private Barrier barrier;
	private User_Data user_data;

	public User_InternalRequest_Child (User_Data user_data, One2OneChannel usercontroller_intReq) {
		this.user_data = user_data;
		this.usercontroller_intReq = usercontroller_intReq;
		barrier = LiftSystem.barrier_internalrequest;
		barrier.enroll();
	}

	public void run () {
		while (true) {
			Vector para = new Vector ();
			para.addElement(new Integer(2));
			Package pack = new Package ("level", para);
			usercontroller_intReq.write(pack);
			System.out.println ("User -> Controller: intReq(2)");
			barrier.sync();
			System.out.println ("User: Entering Chart InternalRequest");
			barrier.sync();
			System.out.println ("User: Exiting Chart InternalRequest");
		}
	}

	public void ResignBarrier () {
		barrier.resign();
	}
}

//Behavior of Users in Chart ExternalRequest

class User_ExternalRequest implements CSProcess {
	private One2OneChannel usercontroller_extReq;
	private User_Data user_data;
	private User_ExternalRequest_Child child;
	private ProcessManager manager;

	public User_ExternalRequest (User_Data user_data, One2OneChannel usercontroller_extReq) {
		this.user_data = user_data;
		this.usercontroller_extReq = usercontroller_extReq;
	}

	public void run () {
		while (true) {
			child = new User_ExternalRequest_Child (user_data, usercontroller_extReq);
			manager = new ProcessManager (child);
			manager.start();
		}
	}
}

class User_ExternalRequest_Child implements CSProcess {
	private One2OneChannel usercontroller_extReq;
	private Barrier barrier;
	private User_Data user_data;

	public User_ExternalRequest_Child (User_Data user_data, One2OneChannel usercontroller_extReq) {
		this.user_data = user_data;
		this.usercontroller_extReq = usercontroller_extReq;
		barrier = LiftSystem.barrier_externalrequest;
		barrier.enroll();
	}

	public void run () {
		while (true) {
			Vector para = new Vector ();
			para.addElement(new Integer(4));
			para.addElement(new Integer(1));
			Package pack = new Package ("level,dir", para);
			System.out.println ("User -> Controller: extReq(4, 1)");
			usercontroller_extReq.write(pack);
			barrier.sync();
			System.out.println ("User: Entering Chart ExternalRequest");
			barrier.sync();
			System.out.println ("User: Exiting Chart ExternalRequest");
		}
	}

	public void ResignBarrier () {
		barrier.resign();
	}
}

//Behavior of Users in Chart ReopenDoorFromInside

class User_ReopenDoorFromInside implements CSProcess {
	private One2OneChannel usercontroller_intReq;
	private User_Data user_data;
	private User_ReopenDoorFromInside_Child child;
	private Barrier reopendoorfrominside_convio;
	private ProcessManager manager;

	public User_ReopenDoorFromInside (User_Data user_data, One2OneChannel usercontroller_intReq) {
		this.user_data = user_data;
		this.usercontroller_intReq = usercontroller_intReq;

		reopendoorfrominside_convio = LiftSystem.reopendoorfrominside_convio;
		reopendoorfrominside_convio.enroll();
	}

	public void run () {
		while (true) {
			child = new User_ReopenDoorFromInside_Child (user_data, usercontroller_intReq);
			manager = new ProcessManager (child);
			manager.start();
			reopendoorfrominside_convio.sync();
			child.ResignBarrier();
			System.out.println ("User: Condition Violated in Chart ReopenDoorFromInside");
			manager.stop();
		}
	}

}

class User_ReopenDoorFromInside_Child implements CSProcess {
	private One2OneChannel usercontroller_intReq;
	private Barrier barrier;
	private User_Data user_data;

	public User_ReopenDoorFromInside_Child (User_Data user_data, One2OneChannel usercontroller_intReq) {
		this.user_data = user_data;
		this.usercontroller_intReq = usercontroller_intReq;
		barrier = LiftSystem.barrier_reopendoorfrominside;
		barrier.enroll();
	}

	public void run () {
		while (true) {
			Vector para = new Vector ();
			para.addElement(new Integer(2));
			Package pack = new Package ("level", para);
			usercontroller_intReq.write(pack);
			System.out.println ("User -> Controller: intReq(2)");
			barrier.sync();
			System.out.println ("User: Entering Chart ReopenDoorFromInside");
			barrier.sync();
			System.out.println ("User: Exiting Chart ReopenDoorFromInside");
		}
	}

	public void ResignBarrier () {
		barrier.resign();
	}
}

//Behavior of Users in Chart ReopenDoorFromOutside

class User_ReopenDoorFromOutside implements CSProcess {
	private One2OneChannel usercontroller_extReq;
	private User_Data user_data;
	private User_ReopenDoorFromOutside_Child child;
	private Barrier reopendoorfromoutside_convio;
	private ProcessManager manager;

	public User_ReopenDoorFromOutside (User_Data user_data, One2OneChannel usercontroller_extReq) {
		this.user_data = user_data;
		this.usercontroller_extReq = usercontroller_extReq;

		reopendoorfromoutside_convio = LiftSystem.reopendoorfromoutside_convio;
		reopendoorfromoutside_convio.enroll();
	}

	public void run () {
		while (true) {
			child = new User_ReopenDoorFromOutside_Child (user_data, usercontroller_extReq);
			manager = new ProcessManager (child);
			manager.start();
			reopendoorfromoutside_convio.sync();
			child.ResignBarrier();
			System.out.println ("User: Condition Violated in Chart ReopenDoorFromOutside");
			manager.stop();
		}
	}
}

class User_ReopenDoorFromOutside_Child implements CSProcess {
	private One2OneChannel usercontroller_extReq;
	private Barrier barrier;
	private User_Data user_data;

	public User_ReopenDoorFromOutside_Child (User_Data user_data, One2OneChannel usercontroller_extReq) {
		this.user_data = user_data;
		this.usercontroller_extReq = usercontroller_extReq;
		barrier = LiftSystem.barrier_reopendoorfromoutside;
		barrier.enroll();
	}

	public void run () {
		while (true) {
			Vector para = new Vector ();
			para.addElement(new Integer(2));
			para.addElement(new Integer(1));
			Package pack = new Package ("level", para);
			usercontroller_extReq.write(pack);
			System.out.println ("User -> Controller: extReq(2, 1)");
			barrier.sync();
			System.out.println ("User: Entering Chart ReopenDoorFromOutside");
			barrier.sync();
			System.out.println ("User: Exiting Chart ReopenDoorFromOutside");
		}
	}

	public void ResignBarrier () {
		barrier.resign();
	}
}

//Behavior of Users in Chart ServeInitIntRequest

class User_ServeInitIntRequest implements CSProcess {
	private One2OneChannel usercontroller_intReq;
	private User_Data user_data;
	private User_ServeInitIntRequest_Child child;
	private Barrier serveinitintrequest_convio;
	private ProcessManager manager;

	public User_ServeInitIntRequest (User_Data user_data, One2OneChannel usercontroller_intReq) {
		this.user_data = user_data;
		this.usercontroller_intReq = usercontroller_intReq;

		serveinitintrequest_convio = LiftSystem.serveinitintrequest_convio;
		serveinitintrequest_convio.enroll();
	}

	public void run () {
		while (true) {
			child = new User_ServeInitIntRequest_Child (user_data, usercontroller_intReq);
			manager = new ProcessManager (child);
			manager.start();
			serveinitintrequest_convio.sync();
			child.ResignBarrier();
			System.out.println ("User: Condition Violated in Chart ServeInitIntRequest");
			manager.stop();
		}
	}
}

class User_ServeInitIntRequest_Child implements CSProcess {
	private One2OneChannel usercontroller_intReq;
	private Barrier barrier;
	private Barrier barrier_sub1;
	private User_Data user_data;

	public User_ServeInitIntRequest_Child (User_Data user_data, One2OneChannel usercontroller_intReq) {
		this.user_data = user_data;
		this.usercontroller_intReq = usercontroller_intReq;
		barrier = LiftSystem.barrier_serveinitintrequest;
		barrier.enroll();
		barrier_sub1 = LiftSystem.barrier_serveinitintrequest_sub1;
		barrier_sub1.enroll();
	}

	public void run () {
		while (true) {
			Vector para = new Vector ();
			para.addElement(new Integer(2));
			Package pack = new Package ("level", para);
			usercontroller_intReq.write(pack);
			System.out.println ("User -> Controller: intReq(2)");
			barrier.sync();
			System.out.println ("User: Entering Chart ServeInitIntRequest");
			barrier.sync();
			System.out.println ("User: Exiting Chart ServeInitIntRequest");
		}
	}

	public void ResignBarrier () {
		barrier.resign();
		barrier_sub1.resign();
	}
}

//Behavior of Users in Chart ServeInitExtRequest

class User_ServeInitExtRequest implements CSProcess {
	private One2OneChannel usercontroller_extReq;
	private User_Data user_data;
	private User_ServeInitExtRequest_Child child;
	private Barrier serveinitextrequest_convio;
	private ProcessManager manager;

	public User_ServeInitExtRequest (User_Data user_data, One2OneChannel usercontroller_extReq) {
		this.user_data = user_data;
		this.usercontroller_extReq = usercontroller_extReq;

		serveinitextrequest_convio = LiftSystem.serveinitextrequest_convio;
		serveinitextrequest_convio.enroll();
	}

	public void run () {
		while (true) {
			child = new User_ServeInitExtRequest_Child (user_data, usercontroller_extReq);
			manager = new ProcessManager (child);
			manager.start();
			serveinitextrequest_convio.sync();
			child.ResignBarrier();
			System.out.println ("User: Condition Violated in Chart ServeInitExtRequest");
			manager.stop();
		}
	}
}

class User_ServeInitExtRequest_Child implements CSProcess {
	private One2OneChannel usercontroller_extReq;
	private Barrier barrier;
	private Barrier barrier_sub1;
	private User_Data user_data;

	public User_ServeInitExtRequest_Child (User_Data user_data, One2OneChannel usercontroller_extReq) {
		this.user_data = user_data;
		this.usercontroller_extReq = usercontroller_extReq;
		barrier = LiftSystem.barrier_serveinitextrequest;
		barrier.enroll();
		barrier_sub1 = LiftSystem.barrier_serveinitintrequest_sub1;
		barrier_sub1.enroll();
	}

	public void run () {
		while (true) {
			Vector para = new Vector ();
			para.addElement(new Integer(2));
			para.addElement(new Integer(1));
			Package pack = new Package ("level", para);
			usercontroller_extReq.write(pack);
			System.out.println ("User -> Controller: extReq(2,1)");
			barrier.sync();
			System.out.println ("User: Entering Chart ServeInitExtRequest");
			barrier.sync();
			System.out.println ("User: Exiting Chart ServeInitExtRequest");
		}
	}

	public void ResignBarrier () {
		barrier.resign();
		barrier_sub1.resign();
	}
}

//Data Class of The Door

class Door_Data {

	public Door_Data () {
	}
}

//Behaviors of The Door

class Door implements CSProcess {
	private Door_Arrive arrive;
	private Door_ServeNextRequest servenextrequest;
	private Door_OpenCloseDoor openclosedoor;
	private Door_ReopenDoorFromInside reopendoorfrominside;
	private Door_ReopenDoorFromOutside reopendoorfromoutside;
	private Door_NoMoreRequest nomorerequest;
	private Door_Data door_data;

	private One2OneChannel doorcontroller_open;
	private One2OneChannel doorcontroller_opened;
	private One2OneChannel doorcontroller_closed;
	private One2OneChannel doorcontroller_close;

	public Door (One2OneChannel doorcontroller_open, One2OneChannel doorcontroller_opened, One2OneChannel doorcontroller_closed, One2OneChannel doorcontroller_close) {
		this.doorcontroller_open = doorcontroller_open;
		this.doorcontroller_opened = doorcontroller_opened;
		this.doorcontroller_closed = doorcontroller_closed;
		this.doorcontroller_close = doorcontroller_close;

		door_data = new Door_Data ();

		arrive = new Door_Arrive (door_data, doorcontroller_open, doorcontroller_opened);
		servenextrequest = new Door_ServeNextRequest (door_data, doorcontroller_open, doorcontroller_closed);
		openclosedoor = new Door_OpenCloseDoor (door_data, doorcontroller_open, doorcontroller_opened, doorcontroller_closed, doorcontroller_close);
		reopendoorfrominside = new Door_ReopenDoorFromInside(door_data, doorcontroller_open, doorcontroller_opened);
		reopendoorfromoutside = new Door_ReopenDoorFromOutside(door_data, doorcontroller_open, doorcontroller_opened);
		nomorerequest = new Door_NoMoreRequest (door_data, doorcontroller_closed);
	}

	public void run () {
		new Parallel (new CSProcess[]{arrive, servenextrequest, openclosedoor, reopendoorfrominside, reopendoorfromoutside, nomorerequest}).run();
	}
}

//Behavior of the Door in Chart Arrive

class Door_Arrive implements CSProcess {
	private ProcessManager manager;
	private Door_Arrive_Child child;
	private Door_Data door_data;
	private One2OneChannel doorcontroller_open;
	private One2OneChannel doorcontroller_opened;

	public Door_Arrive (Door_Data door_data, One2OneChannel doorcontroller_open, One2OneChannel doorcontroller_opened) {
		this.door_data = door_data;
		this.doorcontroller_open = doorcontroller_open;
		this.doorcontroller_opened = doorcontroller_opened;
	}

	public void run () {
		while (true) {
			child = new Door_Arrive_Child (door_data, doorcontroller_open, doorcontroller_opened);
			manager = new ProcessManager (child);
			manager.start();
		}
	}
}

class Door_Arrive_Child implements CSProcess {
	private One2OneChannel doorcontroller_open;
	private One2OneChannel doorcontroller_opened;
	private Barrier barrier;
	private Barrier barrier_sub1;
	private Door_Data door_data;

	public Door_Arrive_Child (Door_Data door_data, One2OneChannel doorcontroller_open, One2OneChannel doorcontroller_opened) {
		this.door_data = door_data;
		this.doorcontroller_open = doorcontroller_open;
		this.doorcontroller_opened = doorcontroller_opened;

		barrier = LiftSystem.barrier_arrive;
		barrier.enroll();
		barrier_sub1 = LiftSystem.barrier_arrive_sub1;
		barrier_sub1.enroll();
	}

	public void run () {
		Package pack;

		while (true) {
			barrier.sync();
			System.out.println ("Door: Entering Chart Arrive");
			barrier_sub1.sync();
			System.out.println ("Door: Entering Chart Arrive_Sub1");

			ProcessManager local = new ProcessManager (
					new CSProcess () {public void run () {
							Package pack = (Package) doorcontroller_open.read();
							System.out.println ("Controller -> Door: open");
							pack = new Package("opened");
							doorcontroller_opened.write (pack);
							System.out.println ("Door -> Controller: opened");
					}});
			local.start();

			barrier_sub1.sync();
			System.out.println ("Door: Exiting Chart Arrive_Sub1");
			local.stop();
			barrier.sync();
			System.out.println ("Door: Exiting Chart Arrive");
		}
	}

	public void ResignBarrier () {
		barrier.resign();
		barrier_sub1.resign();
	}
}

//Behavior of the Door in Chart ServeNextRequest

class Door_ServeNextRequest implements CSProcess {
	private Barrier servenextrequest_sub2_convio;
	private ProcessManager manager;
	private Door_ServeNextRequest_Child child;
	private Door_Data door_data;
	private One2OneChannel doorcontroller_closed;
	private One2OneChannel doorcontroller_open;

	public Door_ServeNextRequest (Door_Data door_data, One2OneChannel doorcontroller_open, One2OneChannel doorcontroller_closed) {
		this.door_data = door_data;
		this.doorcontroller_open = doorcontroller_open;
		this.doorcontroller_closed = doorcontroller_closed;

		servenextrequest_sub2_convio = LiftSystem.servenextrequest_sub2_convio;
		servenextrequest_sub2_convio.enroll();
	}

	public void run () {
		while (true) {
			child = new Door_ServeNextRequest_Child (door_data, doorcontroller_open, doorcontroller_closed);
			manager = new ProcessManager (child);
			manager.start();
			servenextrequest_sub2_convio.sync();
			child.ResignBarrier();
			System.out.println ("Door: Condition Violated Somewhere in ServeNextRequest_Sub2");
			manager.stop();
		}
	}
}

class Door_ServeNextRequest_Child implements CSProcess {
	private One2OneChannel doorcontroller_closed;
	private One2OneChannel doorcontroller_open;
	private Barrier barrier;
	private Barrier barrier_sub1;
	private Barrier barrier_sub2;
	private Door_Data door_data;

	public Door_ServeNextRequest_Child (Door_Data door_data, One2OneChannel doorcontroller_open, One2OneChannel doorcontroller_closed) {
		this.door_data = door_data;
		this.doorcontroller_open = doorcontroller_open;
		this.doorcontroller_closed = doorcontroller_closed;

		barrier = LiftSystem.barrier_servenextrequest;
		barrier.enroll();
		barrier_sub1 = LiftSystem.barrier_servenextrequest_sub1;
		barrier_sub1.enroll();
		barrier_sub2 = LiftSystem.barrier_servenextrequest_sub2;
		barrier_sub2.enroll();
	}

	public void run () {
		Package pack;
		Alternative alt;

		while (true) {
			alt = new Alternative (new Guard[] {doorcontroller_closed, doorcontroller_open});
			final int index = alt.fairSelect();
			if (index == 0) {
				doorcontroller_closed.write(new Package("closed"));
				System.out.println ("Door -> Controller: closed");
				barrier.sync();
				System.out.println ("Door: Entering Chart ServeNextRequest");
				barrier_sub1.sync();
				System.out.println ("Door: Entering Chart ServeNextRequest_Sub1");

				ProcessManager local = new ProcessManager (
						new CSProcess () {public void run () {
							barrier_sub2.sync();

					ProcessManager local2 = new ProcessManager (
							new CSProcess () {public void run () {
								Package temp = (Package) doorcontroller_open.read();
							}});
					local2.start();

						barrier_sub2.sync();
						local2.stop();
					}});
				local.start();

				barrier_sub1.sync();
				local.stop();
				System.out.println ("Door: Exiting Chart ServeNextRequest_Sub1");
				barrier.sync();
				System.out.println ("Door: Exiting Chart ServeNextRequest");
			}
			else {
				Package temp = (Package) doorcontroller_open.read();
			}
		}
	}

	public void ResignBarrier () {
		barrier.resign();
		barrier_sub1.resign();
		barrier_sub2.resign();
	}
}

//Behavior of the Door in Chart OpenCloseDoor

class Door_OpenCloseDoor implements CSProcess {
	private ProcessManager manager;
	private Door_OpenCloseDoor_Child child;
	private Door_Data door_data;
	private One2OneChannel doorcontroller_open;
	private One2OneChannel doorcontroller_opened;
	private One2OneChannel doorcontroller_close;
	private One2OneChannel doorcontroller_closed;

	public Door_OpenCloseDoor (Door_Data door_data, One2OneChannel doorcontroller_open, One2OneChannel doorcontroller_opened, One2OneChannel doorcontroller_close, One2OneChannel doorcontroller_closed) {
		this.door_data = door_data;
		this.doorcontroller_open = doorcontroller_open;
		this.doorcontroller_opened = doorcontroller_opened;
		this.doorcontroller_close = doorcontroller_close;
		this.doorcontroller_closed = doorcontroller_closed;
	}

	public void run () {
		while (true) {
			child = new Door_OpenCloseDoor_Child (door_data, doorcontroller_open, doorcontroller_opened, doorcontroller_close, doorcontroller_closed);
			manager = new ProcessManager (child);
			manager.start();
		}
	}
}

class Door_OpenCloseDoor_Child implements CSProcess {
	private One2OneChannel doorcontroller_open;
	private One2OneChannel doorcontroller_opened;
	private One2OneChannel doorcontroller_close;
	private One2OneChannel doorcontroller_closed;
	private Barrier barrier;
	private Door_Data door_data;

	public Door_OpenCloseDoor_Child (Door_Data door_data, One2OneChannel doorcontroller_open, One2OneChannel doorcontroller_opened, One2OneChannel doorcontroller_close, One2OneChannel doorcontroller_closed) {
		this.door_data = door_data;
		this.doorcontroller_open = doorcontroller_open;
		this.doorcontroller_opened = doorcontroller_opened;
		this.doorcontroller_close = doorcontroller_close;
		this.doorcontroller_closed = doorcontroller_closed;

		barrier = LiftSystem.barrier_openclosedoor;
		barrier.enroll();
	}

	public void run () {
		Package pack;

		while (true) {
			Alternative alt = new Alternative (new Guard[] {doorcontroller_open, doorcontroller_opened, doorcontroller_close, doorcontroller_closed});
			final int index = alt.fairSelect();

			switch (index) {
				case 0:
					pack = (Package) doorcontroller_open.read();
					System.out.println ("Controller -> Door: open");

					Alternative alt2 = new Alternative (new Guard[] {doorcontroller_opened, doorcontroller_close, doorcontroller_closed});
					final int index2 = alt2.fairSelect();
					switch (index2) {
						case 0:
							doorcontroller_opened.write(new Package("opened"));
							System.out.println ("Door -> Controller: opened");
							barrier.sync();
							System.out.println ("Door: Entering Chart OpenCloseDoor");
							pack = (Package) doorcontroller_close.read();
							System.out.println ("Controller -> Door: close");
							doorcontroller_closed.write(new Package("closed"));
							System.out.println ("Door -> Controller: closed");
							barrier.sync();
							System.out.println ("Door: Exiting Chart OpenCloseDoor");
							break;
						case 1:
							doorcontroller_close.read();
							break;
						case 2:
							doorcontroller_closed.write(new Package("closed"));
							break;
						default:
							break;
					}
					break;
				case 1:
					doorcontroller_opened.write(new Package("opened"));
					break;
				case 2:
					doorcontroller_close.read();
					break;
				case 3:
					doorcontroller_closed.write(new Package("closed"));
				default:
					break;
			}
		}
	}

	public void ResignBarrier () {
		barrier.resign();
	}
}

//Behavior of the Door in Chart ReopenDoorFromInside

class Door_ReopenDoorFromInside implements CSProcess {
	private ProcessManager manager;
	private Door_ReopenDoorFromInside_Child child;
	private Door_Data door_data;
	private Barrier reopendoorfrominside_convio;
	private One2OneChannel doorcontroller_open;
	private One2OneChannel doorcontroller_opened;

	public Door_ReopenDoorFromInside (Door_Data door_data, One2OneChannel doorcontroller_open, One2OneChannel doorcontroller_opened) {
		this.door_data = door_data;
		this.doorcontroller_open = doorcontroller_open;
		this.doorcontroller_opened = doorcontroller_opened;
		reopendoorfrominside_convio = LiftSystem.reopendoorfrominside_convio;
		reopendoorfrominside_convio.enroll();
	}

	public void run () {
		while (true) {
			child = new Door_ReopenDoorFromInside_Child (door_data, doorcontroller_open, doorcontroller_opened);
			manager = new ProcessManager (child);
			manager.start();
			reopendoorfrominside_convio.sync();
			System.out.println ("Some Condition Violated in ReopenDoorFromInside");
			child.ResignBarrier();
			manager.stop();
		}
	}
}

class Door_ReopenDoorFromInside_Child implements CSProcess {
	private One2OneChannel doorcontroller_open;
	private One2OneChannel doorcontroller_opened;
	private Barrier barrier;
	private Door_Data door_data;

	public Door_ReopenDoorFromInside_Child (Door_Data door_data, One2OneChannel doorcontroller_open, One2OneChannel doorcontroller_opened) {
		this.door_data = door_data;
		this.doorcontroller_open = doorcontroller_open;
		this.doorcontroller_opened = doorcontroller_opened;

		barrier = LiftSystem.barrier_reopendoorfrominside;
		barrier.enroll();
	}

	public void run () {
		Package pack;

		while (true) {
			ProcessManager local = new ProcessManager (
					new CSProcess () {public void run () {
						while (true) {
							Alternative alt = new Alternative (new Guard[] {doorcontroller_open, doorcontroller_opened});
							final int index = alt.fairSelect();

							if (index == 0) {
								doorcontroller_open.read();
							}
							else {
								doorcontroller_opened.write(new Package("opened"));
							}
						}
				}});
			local.start();
			barrier.sync();
			local.stop();
			System.out.println ("Door: Entering Chart ReopenDoorFromInside");
			pack = (Package) doorcontroller_open.read();
			System.out.println ("Controller -> Door: open");
			doorcontroller_opened.write(new Package("opened"));
			System.out.println ("Door -> Controller: opened");
			barrier.sync();
			System.out.println ("Door: Exiting Chart ReopenDoorFromInside");
		}
	}

	public void ResignBarrier () {
		barrier.resign();
	}
}

//Behavior of the Door in Chart ReopenDoorFromOutside

class Door_ReopenDoorFromOutside implements CSProcess {
	private ProcessManager manager;
	private Door_ReopenDoorFromOutside_Child child;
	private Door_Data door_data;
	private Barrier reopendoorfromoutside_convio;
	private One2OneChannel doorcontroller_open;
	private One2OneChannel doorcontroller_opened;

	public Door_ReopenDoorFromOutside (Door_Data door_data, One2OneChannel doorcontroller_open, One2OneChannel doorcontroller_opened) {
		this.door_data = door_data;
		this.doorcontroller_open = doorcontroller_open;
		this.doorcontroller_opened = doorcontroller_opened;
		reopendoorfromoutside_convio = LiftSystem.reopendoorfromoutside_convio;
		reopendoorfromoutside_convio.enroll();
	}

	public void run () {
		while (true) {
			child = new Door_ReopenDoorFromOutside_Child (door_data, doorcontroller_open, doorcontroller_opened);
			manager = new ProcessManager (child);
			manager.start();
			reopendoorfromoutside_convio.sync();
			System.out.println ("Some Condition Violated in ReopenDoorFromOutside");
			child.ResignBarrier();
			manager.stop();
		}
	}
}

class Door_ReopenDoorFromOutside_Child implements CSProcess {
	private One2OneChannel doorcontroller_open;
	private One2OneChannel doorcontroller_opened;
	private Barrier barrier;
	private Door_Data door_data;

	public Door_ReopenDoorFromOutside_Child (Door_Data door_data, One2OneChannel doorcontroller_open, One2OneChannel doorcontroller_opened) {
		this.door_data = door_data;
		this.doorcontroller_open = doorcontroller_open;
		this.doorcontroller_opened = doorcontroller_opened;

		barrier = LiftSystem.barrier_reopendoorfromoutside;
		barrier.enroll();
	}

	public void run () {
		Package pack;

		while (true) {
			ProcessManager local = new ProcessManager (
					new CSProcess () {public void run () {
						while (true) {
							Alternative alt = new Alternative (new Guard[] {doorcontroller_open, doorcontroller_opened});
							final int index = alt.fairSelect();

							if (index == 0) {
								doorcontroller_open.read();
							}
							else {
								doorcontroller_opened.write(new Package("opened"));
							}
						}
				}});
			local.start();
			barrier.sync();
			local.stop();
			System.out.println ("Door: Entering Chart ReopenDoorFromInside");
			pack = (Package) doorcontroller_open.read();
			System.out.println ("Controller -> Door: open");
			doorcontroller_opened.write(new Package("opened"));
			System.out.println ("Door -> Controller: opened");
			barrier.sync();
			System.out.println ("Door: Exiting Chart ReopenDoorFromInside");
		}
	}

	public void ResignBarrier () {
		barrier.resign();
	}
}

//Behavior of the Door in Chart NoMoreRequest

class Door_NoMoreRequest implements CSProcess {
	private ProcessManager manager;
	private Door_NoMoreRequest_Child child;
	private Door_Data door_data;
	private Barrier nomorerequest_convio;
	private One2OneChannel doorcontroller_closed;

	public Door_NoMoreRequest (Door_Data door_data, One2OneChannel doorcontroller_closed) {
		this.door_data = door_data;
		this.doorcontroller_closed = doorcontroller_closed;
		nomorerequest_convio = LiftSystem.nomorerequest_convio;
		nomorerequest_convio.enroll();
	}

	public void run () {
		while (true) {
			child = new Door_NoMoreRequest_Child (door_data, doorcontroller_closed);
			manager = new ProcessManager (child);
			manager.start();
			nomorerequest_convio.sync();
			System.out.println ("Some Condition Violated in NoMoreRequest");
			child.ResignBarrier();
			manager.stop();
		}
	}
}

class Door_NoMoreRequest_Child implements CSProcess {
	private One2OneChannel doorcontroller_closed;
	private Barrier barrier;
	private Door_Data door_data;

	public Door_NoMoreRequest_Child (Door_Data door_data, One2OneChannel doorcontroller_closed) {
		this.door_data = door_data;
		this.doorcontroller_closed = doorcontroller_closed;

		barrier = LiftSystem.barrier_nomorerequest;
		barrier.enroll();
	}

	public void run () {
		Package pack;

		while (true) {
			doorcontroller_closed.write(new Package("closed"));
			barrier.sync();
			System.out.println ("Door: Entering Chart NoMoreRequest");
			barrier.sync();
			System.out.println ("Door: Exiting Chart NoMoreRequest");
		}
	}

	public void ResignBarrier () {
		barrier.resign();
	}
}

//Object Shaft

class Shaft_Data {
}

class Shaft implements CSProcess {
	private Shaft_Arrive shaft_arrive;
	private Shaft_ServeNextRequest shaft_servenextrequest;
	private Shaft_ServeInitIntRequest shaft_serveinitintrequest;
	private Shaft_ServeInitExtRequest shaft_serveinitextrequest;
	private Shaft_Data shaft_data;

	private One2OneChannel shaftcontroller_arriving;
	private One2OneChannel shaftcontroller_stop;
	private One2OneChannel shaftcontroller_stopped;
	private One2OneChannel shaftcontroller_keepmoving;
	private One2OneChannel shaftcontroller_turnaroundmoving;
	private One2OneChannel shaftcontroller_movingup;
	private One2OneChannel shaftcontroller_movingdown;

	public Shaft (One2OneChannel shaftcontroller_arriving, One2OneChannel shaftcontroller_stop, One2OneChannel shaftcontroller_stopped, One2OneChannel shaftcontroller_keepmoving, One2OneChannel shaftcontroller_turnaroundmoving, One2OneChannel shaftcontroller_movingup, One2OneChannel shaftcontroller_movingdown) {
		this.shaftcontroller_arriving = shaftcontroller_arriving;
		this.shaftcontroller_stop = shaftcontroller_stop;
		this.shaftcontroller_stopped = shaftcontroller_stopped;
		this.shaftcontroller_keepmoving = shaftcontroller_keepmoving;
		this.shaftcontroller_turnaroundmoving = shaftcontroller_turnaroundmoving;
		this.shaftcontroller_movingup = shaftcontroller_movingup;
		this.shaftcontroller_movingdown = shaftcontroller_movingdown;

		shaft_data = new Shaft_Data ();

		shaft_arrive = new Shaft_Arrive (shaft_data, shaftcontroller_arriving, shaftcontroller_stop, shaftcontroller_stopped, shaftcontroller_keepmoving);
		shaft_servenextrequest = new Shaft_ServeNextRequest (shaft_data, shaftcontroller_keepmoving, shaftcontroller_turnaroundmoving);
		shaft_serveinitintrequest = new Shaft_ServeInitIntRequest (shaft_data, shaftcontroller_movingup, shaftcontroller_movingdown);
		shaft_serveinitextrequest = new Shaft_ServeInitExtRequest (shaft_data, shaftcontroller_movingup, shaftcontroller_movingdown);
	}

	public void run () {
			new Parallel (new CSProcess[]{shaft_arrive, shaft_servenextrequest, shaft_serveinitintrequest, shaft_serveinitextrequest}).run();
	}
}

class Shaft_Arrive implements CSProcess {
	private ProcessManager manager;
	private Shaft_Arrive_Child child;
	private Shaft_Data shaft_data;
	private One2OneChannel shaftcontroller_arriving;
	private One2OneChannel shaftcontroller_stop;
	private One2OneChannel shaftcontroller_stopped;
	private One2OneChannel shaftcontroller_keepmoving;

	public Shaft_Arrive (Shaft_Data shaft_data, One2OneChannel shaftcontroller_arriving, One2OneChannel shaftcontroller_stop, One2OneChannel shaftcontroller_stopped, One2OneChannel shaftcontroller_keepmoving) {
		this.shaft_data = shaft_data;
		this.shaftcontroller_arriving = shaftcontroller_arriving;
		this.shaftcontroller_stop = shaftcontroller_stop;
		this.shaftcontroller_stopped = shaftcontroller_stopped;
		this.shaftcontroller_keepmoving = shaftcontroller_keepmoving;
	}

	public void run () {
		while (true) {
			child = new Shaft_Arrive_Child (shaft_data, shaftcontroller_arriving, shaftcontroller_stop, shaftcontroller_stopped, shaftcontroller_keepmoving);
			manager = new ProcessManager (child);
			manager.start();
		}
	}
}

class Shaft_Arrive_Child implements CSProcess {
	private One2OneChannel shaftcontroller_arriving;
	private One2OneChannel shaftcontroller_stop;
	private One2OneChannel shaftcontroller_stopped;
	private One2OneChannel shaftcontroller_keepmoving;
	private Barrier barrier;
	private Barrier barrier_sub1;
	private Shaft_Data shaft_data;

	public Shaft_Arrive_Child (Shaft_Data shaft_data, One2OneChannel shaftcontroller_arriving, One2OneChannel shaftcontroller_stop, One2OneChannel shaftcontroller_stopped, One2OneChannel shaftcontroller_keepmoving) {
		this.shaft_data = shaft_data;
		this.shaftcontroller_arriving = shaftcontroller_arriving;
		this.shaftcontroller_stop = shaftcontroller_stop;
		this.shaftcontroller_stopped = shaftcontroller_stopped;
		this.shaftcontroller_keepmoving = shaftcontroller_keepmoving;

		barrier = LiftSystem.barrier_arrive;
		barrier.enroll();
		barrier_sub1 = LiftSystem.barrier_arrive_sub1;
		barrier_sub1.enroll();
	}

	public void run () {
		while (true) {
			Package pack = new Package ("arrving");
			shaftcontroller_arriving.write(pack);
			System.out.println ("Shaft: Entering Chart Arrive");
			barrier.sync();
			barrier_sub1.sync();

			Alternative alt = new Alternative (new Guard [] {shaftcontroller_stop, shaftcontroller_keepmoving});
			int index = alt.select();

			if (index == 0) {
				pack = (Package) shaftcontroller_stop.read();
				pack = new Package ("stopped");
				shaftcontroller_stopped.write(pack);
			}
			else {
				pack = (Package) shaftcontroller_keepmoving.read();
			}
			barrier_sub1.sync();
			barrier.sync();
			System.out.println ("Shaft: Exiting Chart Arrive");
		}
	}

	public void ResignBarrier () {
		barrier.resign();
		barrier_sub1.resign();
	}
}

class Shaft_ServeNextRequest implements CSProcess {
	private Barrier servenextrequest_sub2_convio;
	private ProcessManager manager;
	private Shaft_ServeNextRequest_Child child;
	private Shaft_Data shaft_data;
	private One2OneChannel shaftcontroller_keepmoving;
	private One2OneChannel shaftcontroller_turnaroundmoving;

	public Shaft_ServeNextRequest (Shaft_Data shaft_data, One2OneChannel shaftcontroller_keepmoving, One2OneChannel shaftcontroller_turnaroundmoving) {
		this.shaft_data = shaft_data;
		this.shaftcontroller_keepmoving = shaftcontroller_keepmoving;
		this.shaftcontroller_turnaroundmoving = shaftcontroller_turnaroundmoving;

		servenextrequest_sub2_convio = LiftSystem.servenextrequest_sub2_convio;
		servenextrequest_sub2_convio.enroll();
	}

	public void run () {
		while (true) {
			child = new Shaft_ServeNextRequest_Child (shaft_data, shaftcontroller_keepmoving, shaftcontroller_turnaroundmoving);
			manager = new ProcessManager (child);
			manager.start();
			System.out.println ("Shaft: Expecting Condition Violated Somewhere");
			servenextrequest_sub2_convio.sync();
			child.ResignBarrier();
			System.out.println ("Shaft: Condition Violated Somewhere");
			manager.stop();
			System.out.println ("Shaft Manager: Shaft Process Terminated");
		}
	}
}

class Shaft_ServeNextRequest_Child implements CSProcess {
	private One2OneChannel shaftcontroller_keepmoving;
	private One2OneChannel shaftcontroller_turnaroundmoving;
	private Barrier barrier;
	private Barrier barrier_sub1;
	private Shaft_Data shaft_data;

	public Shaft_ServeNextRequest_Child (Shaft_Data shaft_data, One2OneChannel shaftcontroller_keepmoving, One2OneChannel shaftcontroller_turnaroundmoving) {
		this.shaft_data = shaft_data;
		this.shaftcontroller_keepmoving = shaftcontroller_keepmoving;
		this.shaftcontroller_turnaroundmoving = shaftcontroller_turnaroundmoving;

		barrier = LiftSystem.barrier_servenextrequest;
		barrier.enroll();
		barrier_sub1 = LiftSystem.barrier_servenextrequest_sub1;
		barrier_sub1.enroll();
	}


	public void run () {
		Package pack;

		while (true) {
			ProcessManager local = new ProcessManager (
					new CSProcess () {public void run () {
						while (true) {
							Alternative alt = new Alternative (new Guard[] {shaftcontroller_keepmoving, shaftcontroller_turnaroundmoving});
							final int index = alt.fairSelect();

							if (index == 0) {
								shaftcontroller_keepmoving.read();
							}
							else {
								shaftcontroller_turnaroundmoving.read();
							}
						}
				}});
			local.start();

			barrier.sync();
			local.stop();
			barrier_sub1.sync();

			Alternative alt = new Alternative (new Guard[] {shaftcontroller_keepmoving, shaftcontroller_turnaroundmoving});
			int index = alt.select();

			if (index == 0) {
				pack = (Package) shaftcontroller_keepmoving.read();
			}
			else {
				pack = new Package ("turnaroundmoving");
				shaftcontroller_turnaroundmoving.write (pack);
			}

			barrier_sub1.sync();
			barrier.sync();
		}
	}

	public void ResignBarrier () {
		barrier.resign();
		barrier_sub1.resign();
	}
}

//Behavior of Shaft in ServeInitIntRequest

class Shaft_ServeInitIntRequest implements CSProcess {
	private Barrier serveinitintrequest_convio;
	private ProcessManager manager;
	private Shaft_ServeInitIntRequest_Child child;
	private Shaft_Data shaft_data;
	private One2OneChannel shaftcontroller_movingup;
	private One2OneChannel shaftcontroller_movingdown;

	public Shaft_ServeInitIntRequest (Shaft_Data shaft_data, One2OneChannel shaftcontroller_movingup, One2OneChannel shaftcontroller_movingdown) {
		this.shaft_data = shaft_data;
		this.shaftcontroller_movingup = shaftcontroller_movingup;
		this.shaftcontroller_movingdown = shaftcontroller_movingdown;

		serveinitintrequest_convio = LiftSystem.serveinitintrequest_convio;
		serveinitintrequest_convio.enroll();
	}

	public void run () {
		while (true) {
			child = new Shaft_ServeInitIntRequest_Child (shaft_data, shaftcontroller_movingup, shaftcontroller_movingdown);
			manager = new ProcessManager (child);
			manager.start();
			serveinitintrequest_convio.sync();
			child.ResignBarrier();
			System.out.println ("Shaft: Condition Violated Somewhere");
			manager.stop();
		}
	}
}

class Shaft_ServeInitIntRequest_Child implements CSProcess {
	private One2OneChannel shaftcontroller_movingup;
	private One2OneChannel shaftcontroller_movingdown;
	private Barrier barrier;
	private Barrier barrier_sub1;
	private Shaft_Data shaft_data;

	public Shaft_ServeInitIntRequest_Child (Shaft_Data shaft_data, One2OneChannel shaftcontroller_movingup, One2OneChannel shaftcontroller_movingdown) {
		this.shaft_data = shaft_data;
		this.shaftcontroller_movingup = shaftcontroller_movingup;
		this.shaftcontroller_movingdown = shaftcontroller_movingdown;

		barrier = LiftSystem.barrier_serveinitintrequest;
		barrier.enroll();
		barrier_sub1 = LiftSystem.barrier_serveinitintrequest_sub1;
		barrier_sub1.enroll();
	}


	public void run () {
		Package pack;

		while (true) {
			ProcessManager local = new ProcessManager (
					new CSProcess () {public void run () {
						while (true) {
							Alternative alt = new Alternative (new Guard[] {shaftcontroller_movingup, shaftcontroller_movingdown});
							final int index = alt.fairSelect();

							if (index == 0) {
								shaftcontroller_movingup.read();
							}
							else {
								shaftcontroller_movingdown.read();
							}
						}
				}});
			local.start();

			barrier.sync();
			local.stop();
			barrier_sub1.sync();

			Alternative alt = new Alternative (new Guard[] {shaftcontroller_movingup, shaftcontroller_movingdown});
			int index = alt.select();

			if (index == 0) {
				shaftcontroller_movingup.read();
			}
			else {
				shaftcontroller_movingdown.read();
			}

			barrier_sub1.sync();
			barrier.sync();
		}
	}

	public void ResignBarrier () {
		barrier.resign();
		barrier_sub1.resign();
	}
}

//Behavior of Shaft in ServeInitExtRequest

class Shaft_ServeInitExtRequest implements CSProcess {
	private Barrier serveinitextrequest_convio;
	private ProcessManager manager;
	private Shaft_ServeInitExtRequest_Child child;
	private Shaft_Data shaft_data;
	private One2OneChannel shaftcontroller_movingup;
	private One2OneChannel shaftcontroller_movingdown;

	public Shaft_ServeInitExtRequest (Shaft_Data shaft_data, One2OneChannel shaftcontroller_movingup, One2OneChannel shaftcontroller_movingdown) {
		this.shaft_data = shaft_data;
		this.shaftcontroller_movingup = shaftcontroller_movingup;
		this.shaftcontroller_movingdown = shaftcontroller_movingdown;

		serveinitextrequest_convio = LiftSystem.serveinitextrequest_convio;
		serveinitextrequest_convio.enroll();
	}

	public void run () {
		while (true) {
			child = new Shaft_ServeInitExtRequest_Child (shaft_data, shaftcontroller_movingup, shaftcontroller_movingdown);
			manager = new ProcessManager (child);
			manager.start();
			serveinitextrequest_convio.sync();
			child.ResignBarrier();
			System.out.println ("Shaft: Condition Violated Somewhere");
			manager.stop();
		}
	}
}

class Shaft_ServeInitExtRequest_Child implements CSProcess {
	private One2OneChannel shaftcontroller_movingup;
	private One2OneChannel shaftcontroller_movingdown;
	private Barrier barrier;
	private Barrier barrier_sub1;
	private Shaft_Data shaft_data;

	public Shaft_ServeInitExtRequest_Child (Shaft_Data shaft_data, One2OneChannel shaftcontroller_movingup, One2OneChannel shaftcontroller_movingdown) {
		this.shaft_data = shaft_data;
		this.shaftcontroller_movingup = shaftcontroller_movingup;
		this.shaftcontroller_movingdown = shaftcontroller_movingdown;

		barrier = LiftSystem.barrier_serveinitextrequest;
		barrier.enroll();
		barrier_sub1 = LiftSystem.barrier_serveinitextrequest_sub1;
		barrier_sub1.enroll();
	}


	public void run () {
		Package pack;

		while (true) {
			ProcessManager local = new ProcessManager (
					new CSProcess () {public void run () {
						while (true) {
							Alternative alt = new Alternative (new Guard[] {shaftcontroller_movingup, shaftcontroller_movingdown});
							final int index = alt.fairSelect();

							if (index == 0) {
								shaftcontroller_movingup.read();
							}
							else {
								shaftcontroller_movingdown.read();
							}
						}
				}});
			local.start();

			barrier.sync();
			local.stop();
			barrier_sub1.sync();

			Alternative alt = new Alternative (new Guard[] {shaftcontroller_movingup, shaftcontroller_movingdown});
			int index = alt.select();

			if (index == 0) {
				shaftcontroller_movingup.read();
			}
			else {
				shaftcontroller_movingdown.read();
			}

			barrier_sub1.sync();
			barrier.sync();
		}
	}

	public void ResignBarrier () {
		barrier.resign();
		barrier_sub1.resign();
	}
}

//Controller

class Controller_Data {
	private int N;
	private int [] int_req;;
	private int [] ext_req;;
	private int dir;
	private int pos;
	private int status;

	public Controller_Data (int n) {
		N = n;
		int_req = new int [N];
		ext_req = new int [N];
		dir = 0;
		pos = 0;
		status = 0;
	}

	public boolean Arrive_Condition_1 () {
		return pos >= 0 && pos < N;
	}

	public boolean toStop () {
		return pos == N-1 || pos == 0 || int_req[pos] == dir || ext_req[pos] == dir || (ext_req[pos] != 0 && existReqAtSameDirection());
	}

	public boolean existReqAtSameDirection () {
		int sum = 0;

		for (int i = pos+dir; i >= 0 && i < N; i = i + dir) {
			sum += int_req[i] + ext_req[i]*ext_req[i];
		}

		return sum > 0;
	}

	public boolean existReqAtPos () {
		return int_req[pos]==1 || ext_req[pos] != 0;
	}

	public boolean ReopenDoorFromInside_Condition_1 (int level) {
		return level == pos && status == 0;
	}

	public boolean ReopenDoorFromOutside_Condition_1 (int level, int dir) {
		return level == pos && ((status == 0 && dir == 0) || (status == 0 && dir == this.dir));
	}

	public boolean ServeInitIntRequest_Condition_1 (int level, int dir) {
		return level == pos && dir == 0;
	}

	public boolean ServeInitIntRequest_Condition_2 (int level) {
		return level > pos;
	}

	public boolean ServeInitIntRequest_Condition_3 (int level) {
		return level < pos;
	}

	public boolean ServeInitExtRequest_Condition_1 (int level, int dir) {
		return level == pos && dir == 0;
	}

	public boolean ServeInitExtRequest_Condition_2 (int level) {
		return level > pos;
	}

	public boolean ServeInitExtRequest_Condition_3 (int level) {
		return level < pos;
	}

	public boolean reqEmpty () {
		int sum = 0;

		for (int i = 0; i < N; i++) {
			sum += int_req[i] + ext_req[i]*ext_req[i];
		}

		return sum > 0;
	}

	public void UpdateIntReq (int level) {
		int_req[level] = 1;
	}

	public void UpdateExtReq (int level, int dir) {
		ext_req[level] = dir;
	}

	public void UpdatePos () {
		pos += dir;
	}

	public void SetStatusHolding () {
		status = 0;
	}

	public void SetStatusMoving () {
		status = 1;
	}

	public void TurnAround () {
		dir = dir*(-1);
	}

	public void ClearReq () {
		int_req[pos] = 0;
		if (ext_req[pos] == dir)
			ext_req[pos] = 0;
	}

	public void SetDirUp () {
		dir = 1;
	}

	public void SetDirDown () {
		dir = -1;
	}

	public void SetDirZero () {
		dir = 0;
	}

	public boolean existReqAtOppoDirection () {
		int sum = 0;

		for (int i = pos-dir; i >= 0 && i < N; i = i + dir) {
			sum += int_req[i] + ext_req[i]*ext_req[i];
		}

		return sum > 0;
	}

	public void Print () {
		System.out.println ("Data State of Controller: Int_req");
		System.out.print ("\t" + int_req[0]);
		System.out.print ("\t" + int_req[1]);
		System.out.print ("\t" + int_req[2]);
		System.out.print ("\t" + int_req[3]);
		System.out.println ("\t" + int_req[4]);
		System.out.println ("Data State of Controller: Ext_req");
		System.out.print ("\t" + int_req[0]);
		System.out.print ("\t" + int_req[1]);
		System.out.print ("\t" + int_req[2]);
		System.out.print ("\t" + int_req[3]);
		System.out.println ("\t" + int_req[4] + "\n");
	}
}

class Controller implements CSProcess {
	private Controller_InternalRequest internalrequest;
	private Controller_ExternalRequest externalrequest;
	private Controller_Arrive arrive;
	private Controller_ServeNextRequest servenextrequest;
	private Controller_OpenCloseDoor openclosedoor;

	private Controller_Data controller_data;
	private One2OneChannel controlleruser_intReq;
	private One2OneChannel controlleruser_extReq;
	private One2OneChannel controllershaft_arriving;
	private One2OneChannel controllershaft_stop;
	private One2OneChannel controllershaft_stopped;
	private One2OneChannel controllershaft_keepmoving;
	private One2OneChannel controllershaft_turnaroundmoving;
	private One2OneChannel controllerdoor_open;
	private One2OneChannel controllerdoor_opened;
	private One2OneChannel controllerdoor_close;
	private One2OneChannel controllerdoor_closed;

	public Controller (One2OneChannel controlleruser_intReq, One2OneChannel controlleruser_extReq, One2OneChannel controllershaft_arriving, One2OneChannel controllershaft_stop, One2OneChannel controllershaft_stopped, One2OneChannel controllershaft_keepmoving, One2OneChannel controllershaft_turnaroundmoving, One2OneChannel controllerdoor_open, One2OneChannel controllerdoor_opened, One2OneChannel controllerdoor_close, One2OneChannel controllerdoor_closed, int N) {
		controller_data = new Controller_Data(N);

		this.controlleruser_intReq = controlleruser_intReq;
		this.controlleruser_extReq = controlleruser_extReq;
		this.controllershaft_arriving = controllershaft_arriving;
		this.controllershaft_stop = controllershaft_stop;
		this.controllershaft_stopped = controllershaft_stopped;
		this.controllershaft_keepmoving = controllershaft_keepmoving;
		this.controllershaft_turnaroundmoving = controllershaft_turnaroundmoving;
		this.controllerdoor_open = controllerdoor_open;
		this.controllerdoor_opened = controllerdoor_opened;
		this.controllerdoor_close = controllerdoor_close;
		this.controllerdoor_closed = controllerdoor_closed;

		internalrequest = new Controller_InternalRequest (controller_data, controlleruser_intReq);
		externalrequest = new Controller_ExternalRequest (controller_data, controlleruser_extReq);
		arrive = new Controller_Arrive (controller_data, controllershaft_arriving, controllershaft_stop, controllershaft_stopped, controllershaft_keepmoving, controllerdoor_open, controllerdoor_opened);
		servenextrequest = new Controller_ServeNextRequest (controller_data, controllerdoor_close, controllershaft_keepmoving, controllershaft_turnaroundmoving,controllerdoor_open);
		openclosedoor = new Controller_OpenCloseDoor (controller_data, controllerdoor_open, controllerdoor_opened, controllerdoor_close, controllerdoor_closed);
	}

	public void run () {
		new Parallel (new CSProcess[]{internalrequest,externalrequest,arrive,servenextrequest,openclosedoor}).run();
	}

}

class Controller_InternalRequest implements CSProcess {
	private Controller_InternalRequest_Child child;
	private ProcessManager manager;
	private Controller_Data controller_data;
	private One2OneChannel controlleruser_intReq;

	public Controller_InternalRequest (Controller_Data controller_data, One2OneChannel controlleruser_intReq) {
		this.controlleruser_intReq = controlleruser_intReq;
		this.controller_data = controller_data;
	}

	public void run () {
		while (true) {
			child = new Controller_InternalRequest_Child (controller_data, controlleruser_intReq);
			manager = new ProcessManager (child);
			manager.start();
		}
	}
}

class Controller_InternalRequest_Child implements CSProcess {
	private One2OneChannel controlleruser_intReq;
	private Barrier barrier;
	private Controller_Data controller_data;

	public Controller_InternalRequest_Child (Controller_Data controller_data, One2OneChannel controlleruser_intReq) {
		this.controller_data = controller_data;
		this.controlleruser_intReq = controlleruser_intReq;

		barrier = LiftSystem.barrier_internalrequest;
		barrier.enroll();

	}

	public void run () {
		Package pack;

		while (true) {
			pack = (Package) controlleruser_intReq.read();
			barrier.sync();
			System.out.println ("Controller: Enterning Chart InternalRequest");
			controller_data.UpdateIntReq(((Integer)pack.getFirstParameter()).intValue());
			barrier.sync();
			System.out.println ("Controller: Exiting Chart InternalRequest");
		}
	}

	public void ResignBarrier () {
		barrier.resign();
	}
}

class Controller_ExternalRequest implements CSProcess {
	private Controller_ExternalRequest_Child child;
	private ProcessManager manager;
	private Controller_Data controller_data;
	private One2OneChannel controlleruser_extReq;

	public Controller_ExternalRequest (Controller_Data controller_data, One2OneChannel controlleruser_extReq) {
		this.controlleruser_extReq = controlleruser_extReq;
		this.controller_data = controller_data;
	}

	public void run () {
		while (true) {
			child = new Controller_ExternalRequest_Child (controller_data, controlleruser_extReq);
			manager = new ProcessManager (child);
			manager.start();
		}
	}
}

class Controller_ExternalRequest_Child implements CSProcess {
	private One2OneChannel controlleruser_extReq;
	private Barrier barrier;
	private Controller_Data controller_data;

	public Controller_ExternalRequest_Child (Controller_Data controller_data, One2OneChannel controlleruser_extReq) {
		this.controller_data = controller_data;
		this.controlleruser_extReq = controlleruser_extReq;
		barrier = LiftSystem.barrier_externalrequest;
		barrier.enroll();
	}

	public void run () {
		Package pack;

		while (true) {
			pack = (Package) controlleruser_extReq.read();
			System.out.println ("Controller: Enterning Chart ExternalRequest");
			barrier.sync();
			controller_data.UpdateExtReq(((Integer)pack.getFirstParameter()).intValue(),
					((Integer)pack.getSecondParameter()).intValue());
			System.out.println ("Controller: Exiting Chart ExternalRequest");
			barrier.sync();
		}
	}

	public void ResignBarrier () {
		barrier.resign();
	}
}

class Controller_Arrive implements CSProcess {
	private Controller_Arrive_Child child;
	private ProcessManager manager;
	private Controller_Data controller_data;
	private One2OneChannel controllershaft_arriving;
	private One2OneChannel controllershaft_stop;
	private One2OneChannel controllershaft_stopped;
	private One2OneChannel controllershaft_keepmoving;
	private One2OneChannel controllerdoor_open;
	private One2OneChannel controllerdoor_opened;

	public Controller_Arrive (Controller_Data controller_data, One2OneChannel controllershaft_arriving, One2OneChannel controllershaft_stop, One2OneChannel controllershaft_stopped, One2OneChannel controllershaft_keepmoving, One2OneChannel controllerdoor_open, One2OneChannel controllerdoor_opened) {
		this.controller_data = controller_data;
		this.controllershaft_arriving = controllershaft_arriving;
		this.controllershaft_stop = controllershaft_stop;
		this.controllershaft_stopped = controllershaft_stopped;
		this.controllershaft_keepmoving = controllershaft_keepmoving;
		this.controllerdoor_open = controllerdoor_open;
		this.controllerdoor_opened = controllerdoor_opened;
	}

	public void run () {
		while (true) {
			child = new Controller_Arrive_Child (controller_data, controllershaft_arriving, controllershaft_stop, controllershaft_stopped, controllershaft_keepmoving, controllerdoor_open, controllerdoor_opened);
			manager = new ProcessManager (child);
			manager.start();
		}
	}
}

class Controller_Arrive_Child implements CSProcess {
	private One2OneChannel controllershaft_arriving;
	private One2OneChannel controllershaft_stop;
	private One2OneChannel controllershaft_stopped;
	private One2OneChannel controllershaft_keepmoving;
	private One2OneChannel controllerdoor_open;
	private One2OneChannel controllerdoor_opened;
	private Barrier barrier;
	private Barrier barrier_sub1;
	private Controller_Data controller_data;

	public Controller_Arrive_Child (Controller_Data controller_data, One2OneChannel controllershaft_arriving, One2OneChannel controllershaft_stop, One2OneChannel controllershaft_stopped, One2OneChannel controllershaft_keepmoving, One2OneChannel controllerdoor_open, One2OneChannel controllerdoor_opened) {
		this.controller_data = controller_data;
		this.controllershaft_arriving = controllershaft_arriving;
		this.controllershaft_stop = controllershaft_stop;
		this.controllershaft_stopped = controllershaft_stopped;
		this.controllershaft_keepmoving = controllershaft_keepmoving;
		this.controllerdoor_open = controllerdoor_open;
		this.controllerdoor_opened = controllerdoor_opened;

		barrier = LiftSystem.barrier_arrive;
		barrier.enroll();
		barrier_sub1 = LiftSystem.barrier_arrive_sub1;
		barrier_sub1.enroll();
	}

	public void run () {
		Package pack;

		while (true) {
			Alternative alt = new Alternative (new Guard[] {controllershaft_arriving, controllershaft_stop, controllershaft_stopped, controllershaft_keepmoving, controllerdoor_open, controllerdoor_opened});
			final int index = alt.fairSelect();

			switch (index) {
				case 0:
					pack = (Package) controllershaft_arriving.read();
					System.out.println ("Controller: Enterning Chart Arrive");
					barrier.sync();
					controller_data.UpdatePos();
					if (!controller_data.Arrive_Condition_1()) {
						System.out.println ("Hot Condition Violated at Arrive Controller");
						System.exit(0);
					}
					barrier_sub1.sync();
					if (controller_data.toStop()) {
						pack = new Package ("stop");
						controllershaft_stop.write(pack);
						pack = (Package) controllershaft_stopped.read();
						controller_data.SetStatusHolding();
						controllerdoor_open.write (new Package("open"));
						pack = (Package) controllerdoor_opened.read();
						controller_data.ClearReq();
					}
					else {
						controllershaft_keepmoving.write(new Package("keepmoving"));
					}

					barrier_sub1.sync();
					System.out.println ("Controller: Exiting Chart Arrive");
					barrier.sync();
					break;
				case 1:
					controllershaft_stop.write(new Package("stop"));
					break;
				case 2:
					controllershaft_stopped.read();
					break;
				case 3:
					controllershaft_keepmoving.write(new Package("keepmoving"));
					break;
				case 4:
					controllerdoor_open.write(new Package("open"));
					break;
				case 5:
					controllerdoor_opened.read();
					break;
				default: break;
			}
		}
	}

	public void ResignBarrier () {
		barrier.resign();
		barrier_sub1.resign();
	}
}

class Controller_ServeNextRequest implements CSProcess {
	private Barrier servenextrequest_sub2_convio;
	private Controller_ServeNextRequest_Child child;
	private ProcessManager manager;
	private Controller_Data controller_data;
	private One2OneChannel controllerdoor_closed;
	private One2OneChannel controllershaft_keepmoving;
	private One2OneChannel controllershaft_turnaroundmoving;
	private One2OneChannel controllershaft_open;

	public Controller_ServeNextRequest (Controller_Data controller_data, One2OneChannel controllerdoor_closed, One2OneChannel controllershaft_keepmoving, One2OneChannel controllershaft_turnaroundmoving, One2OneChannel controllershaft_open) {
		this.controller_data = controller_data;
		this.controllerdoor_closed = controllerdoor_closed;
		this.controllershaft_keepmoving = controllershaft_keepmoving;
		this.controllershaft_turnaroundmoving = controllershaft_turnaroundmoving;
		this.controllershaft_open = controllershaft_open;

		servenextrequest_sub2_convio = LiftSystem.servenextrequest_sub2_convio;
		servenextrequest_sub2_convio.enroll();
	}

	public void run () {
		while (true) {
			child = new Controller_ServeNextRequest_Child (controller_data, controllerdoor_closed, controllershaft_keepmoving, controllershaft_turnaroundmoving, controllershaft_open);
			manager = new ProcessManager (child);
			manager.start();
			System.out.println ("Contorller: Waiting for Synchronization on convio");
			servenextrequest_sub2_convio.sync();
			child.ResignBarrier();
			System.out.println ("Controller: Thanking for synchronization on convio");
			manager.stop();
		}
	}
}

class Controller_ServeNextRequest_Child implements CSProcess {
	private One2OneChannel controllerdoor_closed;
	private One2OneChannel controllershaft_keepmoving;
	private One2OneChannel controllershaft_turnaroundmoving;
	private One2OneChannel controllershaft_open;
	private Barrier barrier;
	private Barrier barrier_sub1;
	private Barrier barrier_sub2;
	private Controller_Data controller_data;
	private Barrier servenextrequest_sub2_convio;

	public Controller_ServeNextRequest_Child (Controller_Data controller_data, One2OneChannel controllerdoor_closed, One2OneChannel controllershaft_keepmoving, One2OneChannel controllershaft_turnaroundmoving, One2OneChannel controllershaft_open) {
		this.controller_data = controller_data;
		this.controllerdoor_closed = controllerdoor_closed;
		this.controllershaft_keepmoving = controllershaft_keepmoving;
		this.controllershaft_turnaroundmoving = controllershaft_turnaroundmoving;
		this.controllershaft_open = controllershaft_open;

		barrier = LiftSystem.barrier_servenextrequest;
		barrier.enroll();
		barrier_sub1 = LiftSystem.barrier_servenextrequest_sub1;
		barrier_sub1.enroll();
		barrier_sub2 = LiftSystem.barrier_servenextrequest_sub2;
		barrier_sub2.enroll();

		servenextrequest_sub2_convio = LiftSystem.servenextrequest_sub2_convio;
		servenextrequest_sub2_convio.enroll();
	}

	public void run () {
		Package pack;

		while (true) {
			Alternative alt = new Alternative (new Guard[] {controllerdoor_closed, controllershaft_keepmoving, controllershaft_turnaroundmoving, controllershaft_open});
			final int index = alt.fairSelect();

			switch (index) {
				case 0:
					pack = (Package) controllerdoor_closed.read();
					System.out.println ("Controller: Enterning Chart ServeNextRequest");
					barrier.sync();
					barrier_sub1.sync();
					if (controller_data.existReqAtSameDirection()) {
						controllershaft_keepmoving.write(new Package("keepmoving"));
						controller_data.SetStatusMoving();
					}
					else {
						barrier_sub2.sync();
						if (controller_data.existReqAtPos()) {
							controller_data.TurnAround();
							controllershaft_open.write(new Package("open"));
							controller_data.ClearReq();
						}
						else {
							if (controller_data.existReqAtSameDirection()) {
								controllershaft_turnaroundmoving.write("turningaroundmoving");
								controller_data.SetStatusMoving();
							}
							else {
								servenextrequest_sub2_convio.sync();
							}
						}
						barrier_sub2.sync();
					}

					barrier_sub1.sync();
					System.out.println ("Controller: Exiting Chart ServeNextRequest");
					barrier.sync();
					break;
				case 1:
					controllershaft_keepmoving.write(new Package("keepmoving"));
					break;
				case 2:
					controllershaft_turnaroundmoving.write(new Package("turnaroundmoving"));
					break;
				case 3:
					controllershaft_open.write(new Package("open"));
					break;
				default:
					break;
			}
		}
	}

	public void ResignBarrier () {
		barrier.resign();
		barrier_sub1.resign();
		barrier_sub2.resign();
		servenextrequest_sub2_convio.resign();
	}
}

class Controller_OpenCloseDoor implements CSProcess {
	private Controller_OpenCloseDoor_Child child;
	private ProcessManager manager;
	private Controller_Data controller_data;
	private One2OneChannel controllerdoor_open;
	private One2OneChannel controllerdoor_opened;
	private One2OneChannel controllerdoor_close;
	private One2OneChannel controllerdoor_closed;

	public Controller_OpenCloseDoor (Controller_Data controller_data, One2OneChannel controllerdoor_open, One2OneChannel controllerdoor_opened, One2OneChannel controllerdoor_close, One2OneChannel controllerdoor_closed) {
		this.controller_data = controller_data;
		this.controllerdoor_open = controllerdoor_open;
		this.controllerdoor_opened = controllerdoor_opened;
		this.controllerdoor_close = controllerdoor_close;
		this.controllerdoor_closed = controllerdoor_closed;
	}

	public void run () {
		while (true) {
			child = new Controller_OpenCloseDoor_Child (controller_data, controllerdoor_open, controllerdoor_opened, controllerdoor_close, controllerdoor_closed);
			manager = new ProcessManager (child);
			manager.start();
		}
	}
}

class Controller_OpenCloseDoor_Child implements CSProcess {
	private One2OneChannel controllerdoor_open;
	private One2OneChannel controllerdoor_opened;
	private One2OneChannel controllerdoor_close;
	private One2OneChannel controllerdoor_closed;
	private Barrier barrier;
	private Controller_Data controller_data;

	public Controller_OpenCloseDoor_Child (Controller_Data controller_data, One2OneChannel controllerdoor_open, One2OneChannel controllerdoor_opened, One2OneChannel controllerdoor_close, One2OneChannel controllerdoor_closed) {
		this.controller_data = controller_data;
		this.controllerdoor_open = controllerdoor_open;
		this.controllerdoor_opened = controllerdoor_opened;
		this.controllerdoor_close = controllerdoor_close;
		this.controllerdoor_closed = controllerdoor_closed;

		barrier = LiftSystem.barrier_openclosedoor;
		barrier.enroll();
	}

	public void run () {
		Package pack;

		while (true) {
			Alternative alt = new Alternative (new Guard[] {controllerdoor_open, controllerdoor_opened, controllerdoor_close, controllerdoor_closed});
			final int index = alt.fairSelect();

			switch (index) {
				case 0:
					controllerdoor_open.write(new Package("open"));
					Alternative alt2 = new Alternative (new Guard[] {controllerdoor_opened, controllerdoor_close, controllerdoor_closed});
					final int index2 = alt2.fairSelect();
					switch (index2) {
						case 0:
							pack = (Package) controllerdoor_opened.read();
							barrier.sync();
							final CSTimer timer = new CSTimer ();
							timer.sleep(5000);
							controllerdoor_close.write(new Package("close"));
							pack = (Package) controllerdoor_closed.read();
							barrier.sync();
						case 1:
							controllerdoor_close.write(new Package("close"));
							break;
						case 2:
							controllerdoor_closed.read();
							break;
						default:
							break;
					}
				case 1:
					controllerdoor_opened.read();
					break;
				case 2:
					controllerdoor_close.write(new Package("close"));
					break;
				case 3:
					controllerdoor_closed.read();
					break;
				default:
					break;
			}
		}
	}

	public void ResignBarrier () {
		barrier.resign();
	}
}


class Package {
	private String label = "Default Label";
	private boolean symbolic = false;
	private Vector parameters;

	public Package (String label) {
		this.label = label;
	}

	public Package (String label, Vector parameters) {
		this.parameters = parameters;
	}

	public Object getFirstParameter () {
		return parameters.get(0);
	}

	public Object getSecondParameter () {
		return parameters.get(1);
	}

	public Vector getParameters () {
		return parameters;
	}

	public String toString () {
		return label;
	}

	public int GetSize () {
		return parameters.size();
	}
}