/****************************************************************************
* Roller Coaster Simulation
*
* Title: roller_coaster.java, Kevin C. Rea, 1999
*
****************************************************************************
*
* Invariant:: 0 <= seats_available <= N

Ride() is the operation of getting in line and taking a ride on the coaster
Load() is the operation of loading the passengers and giving the ride
Unload() is the operation to unload the passengers when the ride is over
N is how many seats the coaster has

Coarse-Grained Solution:
Ride(): <await 0 < seats_available && <= N ==> --seats_available>
{coaster_loading_passengers == TRUE}

Load(): <await seats_available == 0 ==> seats_available += N>
{passengers_riding > 0}

Unload(): <--passengers_riding>

Ensuring the Invariant:
(passengers_waiting > 0 ==> seats_available == 0 || coaster_loading_passengers || passengers_riding > 0) &&
Exclusion::
(passengers_riding > 0 ==> !coaster_loading_passengers) &&
(coaster_loading_passengers ==> passengers_riding == 0) && (0 <= seats_available <= N)

*/

import Utilities.*;
import Synchronization.*;

/* Main Driver */
class roller_coaster extends MyObject {

public static int M = 25; // Number of people in park
public static int P = 1; // Number of passenger cars
public static int N = 4; // Number of passengers a car holds
public static void main(String[] args) {
Monitor rcMon = new Monitor();

/* Create the Objects */
car theCar;
passenger aPassenger;

/* Create arrays of threads for initialization */
Thread t1[] = new Thread[M];
Thread t2[] = new Thread[P];

/* Fill the thread arrays */
for (int i = 0; i < M; i++) {
aPassenger = new passenger(i, rcMon);
t1[i] = new Thread(aPassenger);
}

for (int i = 0; i < P; i++) {
theCar = new car(i, rcMon);
t2[i] = new Thread(theCar);
}

/* Start Threads */
for(int i = 0; i < M; i++) {
t1[i].start();
}

/* Start Threads */
for(int i = 0; i < P; i++) {
t2[0].start();
}

try {
for (int i = 0; i < M; i++) {
t1[i].join();
}
} catch (InterruptedException e) {
System.err.println("Interrupted out of passenger thread join");
}

try {
for (int i = 0; i < P; i++) {
t2[i].join();
}
} catch (InterruptedException e) {
System.err.println("Interrupted out of coaster thread join");
}

System.out.println("Program has terminated Normally");

} /* End Main */
} /* End coaster class */

////////////////////////////// PASSENGER CLASS //////////////////////////////
class passenger extends MyObject implements Runnable {
private int id;
private Monitor passengerMon;

public passenger(int i, Monitor monitorIn) {
id = i;
this.passengerMon = monitorIn;
}

public void run() {
while(true) {
nap((int) random(80));
passengerMon.Ride(id);
}
}
} // end passenger class

/////////////////////////////////// CAR CLASS //////////////////////////////
class car extends MyObject implements Runnable {
private int id;
private Monitor carMon;

public car(int i, Monitor monitorIn) {
id = i;
this.carMon = monitorIn;
}

public void run() {
while(true) {
carMon.Load(id);
nap((int) random(80));
carMon.Unload(id);

}
}
} // end car class

class Monitor {
private int i, line_length; // Number of passengers waiting to board the car.
private int seats_available = 0;
boolean coaster_loading_passengers = false;
boolean passengers_riding = true;

/* For each <awaitB¡ -> S¡>, declare one private notification instance
of class Object */
private Object notifyPassenger = new Object(); // enter/exit protocol provides mutual exclusion.
private Object notifyCar = new Object(); // the car waits on this.

// For each <awaitBi -> Si> define one private synchronized method (checkBSi)
public void Ride(int i) {
synchronized (notifyPassenger) {
while (!checkSeats()) {
try {
notifyPassenger.wait();
} catch (InterruptedException e){}
}
}
System.out.println("Passenger "+ i + " gets in car at: " + System.currentTimeMillis());
synchronized (notifyCar) {notifyCar.notify();}
}

// checkBSi
private synchronized boolean checkSeats() {
if ((seats_available > 0) && (seats_available <= roller_coaster.N) && (!passengers_riding)) {
seats_available--;
return true;
} else return false;
}

/* For each <awaitB¡ -> S¡>, define one public (non-synchronized) method¡ */
public void Load(int i) {
synchronized (notifyCar) {
while (!checkRiding()) {
try {
notifyCar.wait();
} catch (InterruptedException e){}
}
}
System.out.println("The Car is full and gives RIDE at >> "+ System.currentTimeMillis());
synchronized(notifyPassenger) {notifyPassenger.notifyAll();}
}

private synchronized boolean checkRiding() {
if (seats_available == 0) {
seats_available = roller_coaster.N;
coaster_loading_passengers = true;
passengers_riding = true;
return true;
} else return false;
}

/* <Sj> */
public void Unload(int i) {
synchronized (this) {
passengers_riding = false;
coaster_loading_passengers = false;
}
System.out.println("The Car RETURNS and unloads passengers at >> "+ System.currentTimeMillis());
synchronized(notifyPassenger) {notifyPassenger.notifyAll();}
}
} // end roller_coaster monitor class

/*

Java version=1.2.1, Java vendor=Sun Microsystems Inc.
OS name=Windows NT, OS arch=x86, OS version=4.0
Sat Aug 28 15:34:19 EDT 1999
The Car is full and gives RIDE at >> 935868859630
The Car RETURNS and unloads passengers at >> 935868859740
Passenger 23 gets in car at: 935868859740
Passenger 15 gets in car at: 935868859740
Passenger 8 gets in car at: 935868859740
Passenger 1 gets in car at: 935868859740
The Car is full and gives RIDE at >> 935868859750
The Car RETURNS and unloads passengers at >> 935868859780
Passenger 12 gets in car at: 935868859780
Passenger 21 gets in car at: 935868859790
Passenger 7 gets in car at: 935868859790
Passenger 4 gets in car at: 935868859800
The Car is full and gives RIDE at >> 935868859800
The Car RETURNS and unloads passengers at >> 935868859830
Passenger 6 gets in car at: 935868859830
Passenger 17 gets in car at: 935868859830
Passenger 20 gets in car at: 935868859830
Passenger 3 gets in car at: 935868859840
The Car is full and gives RIDE at >> 935868859840
The Car RETURNS and unloads passengers at >> 935868859910
Passenger 2 gets in car at: 935868859910
Passenger 0 gets in car at: 935868859910
Passenger 10 gets in car at: 935868859910
Passenger 16 gets in car at: 935868859910
The Car is full and gives RIDE at >> 935868859910
The Car RETURNS and unloads passengers at >> 935868859980
Passenger 1 gets in car at: 935868859990
Passenger 4 gets in car at: 935868859990
Passenger 6 gets in car at: 935868859990
The Car is full and gives RIDE at >> 935868859990
Passenger 5 gets in car at: 935868859990
The Car RETURNS and unloads passengers at >> 935868860061
Passenger 17 gets in car at: 935868860061
Passenger 3 gets in car at: 935868860071
Passenger 7 gets in car at: 935868860071
Passenger 12 gets in car at: 935868860071
The Car is full and gives RIDE at >> 935868860071
.....

*/
// end ouput run (compiled with Java 1.2.1 Native Threads)