/*
 * Starter skeleton for Cafe using channels
 */

#define NCUSTS 3		/* number of customers */
#define NCASHIERS 1		/* number of cashiers */
#define NSERVERS 2		/* number of servers */

#define NOBODY 255		/* default assignment for nobody */

mtype = {CHILI, SANDWICH, PIZZA} ;	/* the types of foods */
mtype favorite_foods[3] ;			/* default assignment of customers' favorite foods */


/* Channel definitions (suggested) */


/*
 * Channel for customers to give an order to the cashier
 */
chan customer_order[NCUSTS] = [0] of { mtype } ;
mtype { WAITING, ORDER } ;

/*
 * Channel for cashier to tell a customer they can order
 */
chan cashier_order = [0] of { mtype, byte, mtype } ;
mtype { AVAILABLE, ORDER_TAKEN } ;

/*
 * Channel for cashier to give a server a new order
 */
chan cashier_to_server[NSERVERS] = [0] of { mtype, byte, mtype } ;
mtype { COOK } ;

/*
 * Channel for a server to give a customer their
 * finished order
 */
chan server_to_customer[NCUSTS] = [0] of { mtype, mtype } ;
mtype { SERVED }


/*
 * Process representing a customer.
 * Takes in their favorite food and an integer id
 * to represent them
 */
proctype Customer(mtype favorite; byte id)
{
	mtype order;

	do
	::

	printf("C%d enters.\n", id) ;


	/* customer tells the cashier they are waiting to order */
	cashier_order ! WAITING, id ;

	printf("C%d is waiting to order...\n", id) ;

	/* block until the cashier says they may order */
	customer_order[id] ? AVAILABLE ;

	/* tell the cashier their order */
	cashier_order ! ORDER, id, favorite ;

	printf("C%d orders %e.\n", id, favorite);

	/* block until the customer receives their food */
	server_to_customer[id] ? SERVED, order ;

	printf("C%d leaves with %e.\n", id, order);

	od ;

}


/*
 * Process representing a cashier
 */
proctype Cashier()
{

	/* the current customer ordering*/
	byte current ;

	/* the current customer's order */
	mtype order ;

	do
	::

	printf("Cashier is waiting for a new customer.\n");

	/* block until a customer wants to order */
	cashier_order ? WAITING, current, order;

	/* tell a customer they can order */
	customer_order[current] ! AVAILABLE ;

	printf("Cashier tells C%d that they can order\n", current);

	/* block until the cashier receives the customer's order */
	cashier_order ? ORDER, current, order;

	printf("Cashier puts in C%d's order\n", current);

	/* give the order to the server */
	cashier_order ! ORDER_TAKEN, current, order;

	od ;


}

/*
 * Process representing a server
 */
proctype Server(byte id)
{
	/* the customer the server is making food for */
	byte my_customer ;

	/* the order the server is making */
	mtype order ;

	do
	::
		printf("Server%d is free.\n", id) ;

		/* block until an order is given */
		cashier_order ? ORDER_TAKEN, my_customer, order;

		printf("Server%d makes %e for C%d.\n", id, order, my_customer) ;

		/* make and give the order to the customer */
		server_to_customer[my_customer] ! SERVED, order;
	od ;


}


/*
 * Sets up processes. This model creates three
 * customers with a specific favorite food, and
 * two servers.
 */
init{
	favorite_foods[0] = PIZZA ;
	favorite_foods[1] = SANDWICH ;
	favorite_foods[2] = CHILI ;
	atomic{
		run Customer(PIZZA, 0) ;
		run Customer(SANDWICH, 1);
		run Customer(CHILI, 2);
		run Cashier();
		run Server(0);
		run Server(1);

	}

}


/*
 * Safety:  The cashier always sends the correct order
 * for a customer to the servers.
 */
ltl S_CashierCorrectOrder {
	true;
}

/*
 * Safety: It is never the case that the two servers
 * are busy working on the same order.
 */
ltl S_NeverSameOrder {
 true;
}

/*
 * Liveness: If a customer wants to place
 * an order then a customer eventually does.
 */
ltl L_EventuallyOrder {
	true;
}

/*
 * Liveness: it is always the case that eventually
 * a server is busy making an order
 */
ltl L_EventuallyServerBusy {
	true;
}