(*****************************************************************************
 ****		     This RSL file is an example of what 		  ****
 ****		        Milestone 4 should look like.	 		  ****
 ****		It is a refinement of the Milestone 3 Example		  ****
 ****		in which the following objects and operations		  ****
 ****			have been formally specified:			  ****
 ****				FoodMenu				  ****
 ****				AddMenuSection				  ****
 ****				DelMenuSection				  ****
 ****				UpdateMenuSection			  ****
 ****				EmptyFoodMenu				  ****
 ****				FindMenuItem				  ****
 ****				SetItemAvailability			  ****
 ****				AddMenuItem				  ****
 ****				DelMenuItem				  ****
 ****				UpdateMenutem				  ****
 ****				AddItem					  ****
 ****				DelItem				 	  ****
 ****				UpdateItem				  ****
 ****				FindItem				  ****
 ****				OrderItem				  ****
 ****				CancelAll				  ****
 ****				CancelOne				  ****
 *****************************************************************************)


(****
 **** OBJECTS
 ****)
object RestaurantDB
    components: FoodMenu and FoodStuffsInventory and FoodItemBreakdowns;
    operations: MaintainDB;
    description: (*
	The RestaurantDB is the repository of all electronic restaurant
	information.  The three main components are the menus seen by the
	customer, the food stuffs inventory that records all current stock on
	hand, and the food item breakdowns that describes the food stuffs that
	each menu item is composed of.
    *);
end RestaurantDB;

(*
 * The next several objects define the food menu seen by customers.
 *)
object FoodMenu
    components: MenuSection*;

    operations:
	AddMenuSection (FoodMenu, MenuSection)->(FoodMenu),
	DelMenuSection (FoodMenu, MenuSectionName)->(FoodMenu),
	UpdateMenuSection (FoodMenu, MenuSection)->(FoodMenu),
	EmtpyFoodMenu ()->(FoodMenu),
	FindMenuItem (FoodMenu, MenuItemName)->(MenuItem),
	SetItemAvailability; (* Specified predicatively; see below. *)

    equations:
        var fm: FoodMenu;
        var ms: MenuSection;
        var sname: MenuSectionName;
	var iname: MenuItemName;

        DelMenuSection(EmptyFoodMenu(), sname) == EmptyFoodMenu();
        DelMenuSection(AddMenuSection(fm, ms), sname) ==
            if ms.name = sname
            then DelMenuSection(fm, sname')
            else AddMenuSection(DelMenuSection(fm, sname'), ms);

	FindMenuItem(EmptyFoodMenu) == EmptyMenuItem;
	FindMenuItem(AddMenuSection(fm, ms), name) ==
	    if FindItem(ms, name) != EmptyMenuItem() (* FindItem def'd below *)
	    then FindItem(ms, name)
	    else FindMenuItem(ms, name);

	UpdateMenuSection(fm, ms) ==
	    AddMenuSection(DelMenuSection(fm, ms.msn), ms);

    description: (*
	The FoodMenu is the top-level structure of menu seen by the customer
	from which order selections are made.  It is composed of a number of
	MenuSections.  The standard menu sections are Hamburgers, 
    *);
end FoodMenu;

operation FindMenuItem
    inputs: fm:FoodMenu, name:MenuItemName;
    outputs: mi':MenuItem;
    description: (*
	Find the item of the given name in the given menu.
    *);
end FindMenuItem;

operation SetItemAvailability
    inputs: fm:FoodMenu, name:MenuItemName, av:Availability;
    outputs: fm':FoodMenu;
    post:     FindMenuItem(fm, name).av = av;
end SetItemAvailability;

object MenuSection
    components: msn: MenuSectionName, mil:MenuItemList;

    operations:
	AddMenuItem (MenuSection, MenuItem)->(MenuSection),
	DelMenuItem (MenuSection, MenuItemName)->(MenuSection),
	UpdateMenuItem (MenuSection, MenuItem)->(MenuSection),
	UpdateMenuSectionName (MenuSection, MenuSectionName)->(MenuSection),
	EmptyMenuSection (MenuSectionName)->(MenuSection);

    description: (*
	Each MenuSection of the menu consists of a list of indivdual menu
	items.  For example, the hamburgers section contains a menu item for
	each of the different kinds of hamburgers
    *);
end MenuSection;

object MenuItemList
    components: MenuItem*;
    operations:
	AddItem (MenuItemList, MenuItem)->(MenuItemList),
	DelItem (MenuItemList, MenuItemName)->(MenuItemList),
	UpdateItem (MenuItemList, MenuItem)->(MenuItemList),
	FindItem (MenuItemList, MenuItemName)->(MenuItem),
	EmptyMenuItemList ()->(MenuItemList);

    equations:
	var mil: MenuItemList;
        var mi: MenuItem;
        var vname: MenuItemName;

        DelItem(EmptyMenuItemList(), name) == EmptyDB;
        DelItem(AddItem(mil, mi), name) ==
            if mi.name = name
            then DelMenuItem(mil, name)
            else Insert(DelMenuItem(mil, name), mi);

	UpdateItem(mil, mi) ==
	    AddItem(DelItem(mil, mi.name), mi);

	FindItem(EmptyMenuItemList(), name) == EmtpyMenuItem;
	FindItem(AddItem(mil, mi), name) ==
	    if mi.name = name
	    then mi
	    else FindItem(mil, name);

    description: (*
	MenuItemList is the body of a MenuSection, containing the individual
	menu items.
    *);
end MenuItemList;

operation EmptyMenuSection
    inputs: ;
    outputs: MenuSection;
    description: (* Standard constructor. *);
end EmptyMenuSection;

operation AddMenuItem
    inputs: MenuSection, MenuItem;
    outputs: MenuSection;
    description: (*
	Add a new menu item to a menu section.
    *);
end AddMenuItem;

operation DelMenuItem
    inputs: ms: MenuSection, name: MenuItemName;
    outputs: ms': MenuSection;
    precondition: exists (mi: MenuItem) ((mi.name = name) and (mi in ms.mil));
    postcondition:
        not (exists (mi: MenuItem) ((mi.name = name) and (mi in ms'.mil)));
    description: (*
        Delete an existing menu item
    *);
end DelMenuItem;


(*
 * The next several defintions define individual menu items.
 *)
object MenuItem
    components: name:MenuItemName and d:Description and price:Price and
	a:Accessories and av: Availability;
    operations: EmtpyMenuItem()->(MenuItem);
    description: (*
	Each MenuItem in a MenuSection has these components.  Four example, 
	a MenuItem for a plain hamburger is the following:
		Name: "Plain Hamburger"
		Description: "1/4 LB patty"
		Price: "$1.89"
		Accessories: "Mayonaise", "Mustard", "Catsup", "Lettuce",
			"Tomato", "Pickles", "Onion", "Cheese", "Mushrooms"
		IsAvailble: true;
	Note that the list of accessories includes an indication of whether a
	particular extra is or is not normally included, which detail is not
	shown here; see the definition of the Extras object below for details.
    *);
end MenuItem;

object Availability =  boolean;

object Accessiies
    components: Accessory*;
    description: (*
	This is the list of accessory items that can appear with a MenuItem.
	Accessories is also a component of the FoodItemBreakdown object defined
	farther below.
    *);
end Accessories;

object Accessory
    components: Name and IsStandard and Requested and ExtraRequested and Price;
    description: (*
	Each Accessory has a name, an indication as to whether it is standard,
	an indication as to whether it has been requested by the customer, an
	indication as to whether extra has been requested, and a price.  For
	example, here is the structure of a mayonaise accessory for a standard
	hamburger:
		Name: "Mayonaise"
		IsStandard: true
		Requested: true
		Extra:	false
		Price: "no charge"
	This example indicates that Mayonaise is standard, it has been
	requested by the customer, no extra is requested, and there is no
	charge for it.  If an Accessory is standard, then it is normally
	included on a food item unless the customer explicitly requests that it
	be removed.  The converse is true for non-standard a Accessory.  The
	ExtraRequested flag allows the customer to select extra of an
	Accessory, i.e., double it.  If ExtraRequested is true, then the Price
	is doubled.
    *);
end Accessory;


(*
 * Atomic objects appearing menu-related objects:
 *)
object MenuSectionName =  Name;
object MenuItemName =  Name;
object Description =  string;
object Price =  number;
object Requested =  boolean;
object ExtraRequested =  boolean;
object IsStandard =  boolean;


(*
 * The next two objects define the restaurant inventory structure.
 *)
object FoodStuffsInventory
    components: FoodStuffsItem*;
    description: (*
	FoodStuffsInventory is the inventory of raw food items, such as burger
	patties, buns etc.  This inventory contains a description of all stock
	on hand.
    *);
end FoodStuffsInventory;

object FoodStuffsItem
    components: FoodStuffsItemName and Quantity and Units;
    ops: ;
    description: (*
	A foods stuffs inventory item consisting of a name, quantity, and unit
	of measurement.  For example, if there are 500 hamburger patties on
	hand, then the inventory entry is:
		Name: "Patty"
		Quantity: 500
		Unit: "1/4 LB"
    *);
end FoodStuffsItem;

(*
 * The next defs are for atomic objects refereneced in FoodStuffsItem, and
 * elsewhere.
 *)
object FoodStuffsItemName =  string;
object Name =  string;
object Quantity =  number;
object Units =  string;


(*
 * The next several objects define the food item breakdown list.
 *)
object FoodItemBreakdowns
    components: FoodItemBreakdown*;
    description: (*
	The FoodItemsBreakdownList contains the complete breakdown for each
	food item on the menu.  Each breakdown describes exactly what raw food
	stuffs are need to prepare the menu item.
    *);
end FoodItemBreakdowns;

object FoodItemBreakdown
    components: Name and BasicParts and Extras;
    description: (*
	A FoodItemBreakdown Describes the food stuffs components of
	customer-level food items.  For example, the breakdown for a plain
	hambuger is:

		Name: "Plain Hamburger"
		BasicParts: "patty", "bun"
		Price: 1.89
		Extras: "Mayonaise", "Mustard", "Catsup", "Lettuce", "Tomato",
			"Pickles", "Onion", "Cheese", "Mushrooms"

	Note that there is similarity between a FoodItemBreakdown object and
	the MenuItem object defined above.  The difference is that a MenuItem
	is a description seen by the restaurant customer, whereas a
	FoodItemBreakdown is seen by the restaurant management and staff.
	The most important specific difference between the two types of object
	is that a MenuItem has a customer-oriented description, whereas a
	FoodItemBreakdown has a complete list of basic parts and extras.  In
	general, the customer-oriented description will not contain a full list
	of all parts.  For example, the customer-oriented description of a
	plain hamburger is "1/4 LB patty", whereas the basic parts list of a
	plain hamburger FoodItemBreakdown is the list consisting of "patty"
	and "bun".
    *);
end FoodItemBreakdown;

object BasicParts
    components: FoodStuffsItem*;
    description: (*
	The basic parts of a food item are those that are always included.  For
	example, the basic parts of a hamburger are the patty and bun.
    *);
end BasicParts;

object Extras
    components: Extra*;
    description: (*
	The list of extra items on a hamburger.
    *);
end Extras;

object Extra =  string;


(* Reports *)

object DBReports
    components: FoodItemList or InventoryList or IntervalInventoryReport;
    description: (*
	There are three types of reports that the system will generate.  A
	description of each is given below in the respective definitions.
    *);
end DBReports;

object FoodItemList
    components: FoodItemBreakdown*;
    description: (*
	A FoodItemList is a listing of all the food items currently
	available on the food menu.  This list can be sorted alpahbetically or
	by menu section.
    *);
end FoodItemList;

object InventoryList
    components: FoodStuffsItem*;
    description: (*
	An InventoryList is a listing of all the raw food stuffs currently in
	the food stuffs inventory.  The listing is sorted alphabetically.
    *);
end InventoryList;

object IntervalInventoryReport
    components: Interval and AnnotatedFoodItemList and AnnotatedInventoryList;
    operations: ProduceIntervalReport;
    description: (*
	An IntervalInventoryReport is a listing of how many items sold in a
	given interval and how the inventory fluctuated during that time.  The
	possible intervals are daily, weekly, monthly, and yearly.
    *);
end IntervalInventoryReport;

object AnnotatedFoodItemList
    components: AnnotatedFoodItem*;
    description: (*
	A list of food items, annotated with how many of each were sold in a
	given interval.  E.g., here is a short sample list:

		FOOD ITEM	UNITS SOLD	UNIT MEASURE
		==============================================
		Bun		486		single
		Patty		487		single
		Pickle		1792		single
    *);
end AnnotatedFoodItemList;

object AnnotatedFoodItem
    components: number and FoodStuffsItemName and SingleOrStandardUnit;
    description: (*
	The number indicates how many units of the named food stuffs item were
	sold in a given interval.  The unit of measure is that indicated by the
	SingleOrStandardUnit component, which indicates whether the numeric
	annotation is given in single units or the standard unit of measure
	associated with each food stuffs item.  E.g., an AnnotatedFoodItem of
	the form ["Bun", 486, SingleUnit] indicates that 486 single units of
	bun were sold.  The AnnotatedFoodItem ["Bun", 20, StandardUnit]
	indicates the 20 boxes of buns were sold, given that box is the
	standard unit of measure for a bun.
    *);
end AnnotatedFoodItem;

object SingleOrStandardUnit
    components: SingleUnit or StandardUnit;
    description: (*
	Selects the unit of measure in an inventory report.
    *);
end SingleOrStandardUnit;

object SingleUnit;
object StandardUnit;

object AnnotatedInventoryList
  components: ;
  operations: ;
  description: ;
end AnnotatedInventoryList;

object DailyInventoryReport extends IntervalInventoryReport
    where: Interval = Day;
    description: (*
	A DailyInventoryReport has inventory information for one day.
    *);
end DailyInventoryReport;

object WeeklyInventoryReport extends IntervalInventoryReport
    where: Interval = Week;
    description: (*
	Inventory information for one day.
    *);
end WeeklyInventoryReport;

object MonthlyIventoryReport
    where: Interval = Month;
    description: (*
	Inventory information for one month;
    *);
end MonthlyIventoryReport;

object YearlyInventoryReport
  where: Interval = Year;
  description:  (*
	Inventory information for one year.
    *);
end YearlyInventoryReport;

object Day
    components: DayName and DayDate and MonthName and YearNumber;
    description: (*
	A Day describes a single day in the calendar year, e.g., Wednesday 14
	October 1991.
    *);
end Day;

object DayName
    components: Mon or Tue or Wed or Thu or Fri or Sat or Sun;
end DayName;

value Mon = "Monday";
value Tue = "Tuesday";
value Wed = "Wednesday";
value Thu = "Thursday";
value Fri = "Friday";
value Sat = "Saturday";
value Sun = "Sunday";

object DayDate =  number;

object Week =  number;
  (* A week by itself is simply a numeric position in the year. *)

object Month
    components: MonthName and Day*;
    description: (*
        A Month describes a month in the calendar year.  It is organized as
        collection of days, as opposed to weeks.  Since each day carries its
        day name and date, the month can be composed into an appropriate month
        view.
    *);
end Month;

object Year
    components: YearNumber and Month*;
    operations: ;
    description: (*

    *);
end Year;

object MonthName
    components: Jan or Feb or Mar or Apr or May or Jun or
		Jul or Aug or Sep or Oct or Nov or Dec;
end MonthName;

value Jan = "January";
value Feb = "February";
value Mar = "March";
value Apr = "April";
value May = "May";
value Jun = "June";
value Jul = "July";
value Aug = "August";
value Sep = "September";
value Oct = "October";
value Nov = "November";
value Dec = "December";

object YearNumber =  number;
    axiom A1 = forall (yn: YearNumber) (yn > 0);

operation ProduceIntervalReport
    inputs: Interval, UnitMeasure;
    outputs: IntervalInventoryReport;
    description: (*

    *);
end ProduceIntervalReport;

object Interval
  components: Day or Week or Month or Year;
  description: ;
end Interval;

object UnitMeasure =  string;


(*
 * Food Orders
 *)
object OrderSoFar
    components:  ItemOrder*;
    description: (*
	The CustomerOrder is the collection of all individual item orders input
	by the customer.  As the ordering operation is performed, the customer
	order is built up from the ordered items.
    *);
end OrderSoFar;

object ItemOrder
    components: name:ItemName and amt:ItemAmount and acc:Accessories
		and price:ItemUnitPrice and ItemTotalPrice;
    description: (*
	An ItemOrder contains all of the information for a partcular item that
	the customer has ordered, including the item name, amount, extras, unit
	price, extras price, and total price.
    *);
end ItemOrder;

object ItemName =  string;
object ItemAmount =  number;
object ItemExtrasPrice =  number;
object ItemUnitPrice =  number;
object ItemTotalPrice =  number;


object CooksOrder
    components: OrderNumber, OrderedItems;
    description: (*
        A cooks order is a summarized version of the customer order.   
    *);
end CooksOrder;

object OrderedItems
    components: OrderedItem*;
    operations: ;
    description: (*
        The order of items in this list is specified by the CookOrderOrdering
        list, which specifies the order of items by major category.
    *);
end OrderedItems;

object OrderedItem
    components: ItemAmount, ItemName;
    operations: ;
    description: (*

    *);
end OrderedItem;

object CustomerReceipt =  (*. . .*) end CustomerReceipt;


(*
 * The next four definitions are concrete object values that define the current
 * contents of the food menu.  These constitute the default menu values, and
 * are changeable using the UpdateMenu operations defined below.
 *)

value StandardMenu:FoodMenu = [BurgerSection, DrinksSection, SidesSection];
    (*
	A StandardMenu represents the actual menu structure as presently in
	place at the restaurant.
    *)

value BurgerSection:MenuSection = [PlainBurgerItem, DoubleBurgerItem,
			ChiliBurgerItem, SkinnyBurgerItem, KiddieBurgerItem];
    (*
	These are the current items in the Burger section of the standard menu.
    *)

value DrinksSection:MenuSection = [CokeItem, OrangeItem, SevenUpItem,
					DietCokeItem];
    (*
	These are the current items in the Drinks section of the standard menu.
    *)

value SidesSection:MeunSection = [FriesItem, OnionRingsItem, ApplePieItem];
    (*
	These are the current items in the Side Orders section of the standard 
	menu.
    *)

(*
 * The next five objects are the definitions of the standard burgers.
 *)
value PlainBurgerItem = [
	(* Name: *) "Plain Hamburger",
	(* Description: *) "1/4 LB patty",
	(* Price: *) "1.89",
	(* AddOns: *) PlainBurgerAddOns
    ];

value DoubleBurgerItem = ["Double Hamburger", "Two 1/4 LB patties", "$2.69"];


(*
 * The next five objects will be the definitions of the standard burger
 * accessories.  They need to defined fully.
 *)
value PlainBurgerAccessories = [];



(*
 * OPERATIONS
 *)


(* Food Ordering *)

operation OrderFood
    components: OrderItem, AllDone, CancelAll, CancelOne;
    inputs: ms: MenuSelection, m: Menu, col: CookOrderList;
    outputs: cr: CustomerReceipt, col': CookOrderList;
    precondition:
	(*See component operations for preconditions.*) ;
    postcondition:
	(*See component operations for postconditions.*) ;
    description: (*
	Accumulate the individual customer entries and produce the food orders.
	The principal ordering constraint is that the customer-selected food
	item is on the input Menu.  The Menu will be updated as necessary
	during normal business to reflect immediate changes in inventory.
	E.g., if hamburger patties are consumed, then the Burger items will be
	deleted form the menu (deletion is specified by marking the item as
	``temporarily out of stock'' on the menu).  It should be noted that
	this ordering constraint requires human intervention to remove an item
	from the menu.  I.e., the manager must use the MaintainMenu function to
	perform the change.  Other alternatives for ordering constraints were
	considered, in particular, having the system automatically remove an
	item from the menu when the online inventory indicates that some
	comoponent of a FoodItem is out of stock.  This fully automatic
	operation was rejected on the grounds that the system may not have
	accurate information about the exact inventory on hand.  E.g., if the
	cook uses more of some FoodStuffs item then is required and fails to
	report the overuse to the system, the system will indicate that there
	is more of the FoodStuffs item than is actually available.  Instead of
	the fully automatic Menu update, the system will output a ``stock low''
	warning on the manager's console (see the MaintainMenu function).
    *);
end OrderFood;

operation OrderItem
    inputs: fm: FoodMenu, name:MenuItemName, osf: OrderSoFar;
    outputs: osf': OrderSoFar;
    precondition:  (*The selected item is available on the food menu.*)
	IsAvailable(fm, name);
    postcondition: (*An item of the given name is on the output order so far.
		    If there was no item of that name on the input order, then
		    then the item is put at the end of the order so far and the
		    amount of that item is 1, else the amount of the exisiting
		    item is one greater than on the input order.  Also, the
		    item price is equal to the item unit price times the
		    amount.*)

	exists (item:ItemOrder) (
	    (item.name = name) and		(* An item of the given name *)
	    (item in osf')			(*  is in the output order *)

		and

	    if (exists (item' in osf)		(* If there's an extant item *)
		    item.name = item'.name)	(*   of the given name, then *)
	    then ItemIsIncrement(item,osf,osf') (*  extant item incremented *)
	    else ItemIsLast(item, osf')		(*  else item put at ent *)


		and

	    (item.price =
		FindMenuItem(fm, name).price *	(* Item price is base menu *)
		    item.amt)			(*  price * amount ordered. *)
	);
    description: (*
	Order one item from the menu, including selecting an add-on or a size.
    *);
end OrderItem;

(*
 * Aux function that specifies an ordered item is the last on an order so far,
 * and the amount of that item is 1.
 *)
function ItemIsLast(item:ItemOrder, osf:OrderSoFar) -> (boolean) = 

    (item in osf) and	  (* Item is in the order so far *)
    (item.amt = 1) and	  (* Its amount is 1 *)
    (osf[#osf] = item);	  (* It's the last item.  Note use of list
			   * selection; see section 7.4 of RSL ref man *)

(*
 * Aux function that specifies an ordered item is an increment of an item of
 * the same name already in an order so far.
 *)
function ItemIsIncrement(item:ItemOrder, osf:OrderSoFar, osf':OrderSoFar) ->
	(boolean) = 
    forall (item' in osf)		(* For each current item,	    *)
	if (item.name = item'.name)	(*  if name is same as ordered item *)
	then				(*  then			    *)
	    exists (item'' in osf')	(*    there's item in new order w/  *)
		(item'.name = mi.name) and  (*  same name		    *)
		(item'.amt = item.amt + 1)  (*  and one more in amt field   *)
	else
	    exists (item'' in osf')	(*  else the new and old items	    *)
		(item' = item'');	(*   are the same		    *)


function IsAvailable(fm:FoodMenu, name:MenuItemName) -> (boolean) =
    FindMenuItem(fm, name).a = true;

operation OrderAccessoriedItem (* extends OrderItem *)
    inputs: acc:Accessories;
    outputs: acc':Accessories;
    description: (*
	This is a specific extends the OrderFood operation that orders a
	food item for which accessories are available.  In the standard menu,
	this operation applies to the Burgers section.
    *);
end OrderAccessoriedItem;

operation OrderSizedItem (* extends OrderItem *)
    description: (*
	This is a specific extends the OrderFood operation that orders a
	food item for which a size is required.  In the standard menu,
	this operation applies to the Drinks and Sides sections.
    *);
end OrderSizedItem;

operation AllDone
    inputs: OrderSoFar, RestaurantDB;
    outputs: CustomerReceipt, CooksOrder, RestaurantDB;
    description: (*
	This operation is invoked when the customer has completed ordering and
	is ready to eat.  It takes the completed OrderSoFar and produces a
	final CustomerReceipt and CookOrder.  The CustomerReceipt is presented
	to the customer at the table in paper form.  The CookOrder is sent to
	the kitchen, where it appears on an electronic monitor.  The CookOrders
	should be received in the kitchen in first-come, first-served order.*);
end AllDone;

operation CancelAll
    inputs: osf: OrderSoFar;
    outputs: osf': OrderSoFar;
    postcondition: osf' = empty;
    description: (*
	Cancel everything on the given order so far.
*);
end CancelAll;

operation CancelOne
    components: ;
    inputs: osf: OrderSoFar, iop: ItemOrderPosition;
    outputs: osf': OrderSoFar;
    post:    
	(#osf' = #osf - 1) and
	(forall (item: ItemOrder)
	    (item in osf') and
	    (item.name != osf[iop].name)
	);
    description: (*
	Cancel the item at the given postition in the given order so far.  An
	item position is used instead of an item name, since the item is
	selected by the user by poiting an an item postion in the order so far
	list, and such a pointed-to position is accurately represented as a
	numeric position in the list. *);
end CancelOne;

object ItemOrderPosition =  integer;


(* Database Management *)

operation MaintainDB
    components: ValidateUser, MaintainMenu, MaintainInventory,
			MaintainBreakdowns, GenerateReports;
    inputs: RestaurantDB, DBUpdates, UserPassword;
    outputs: RestaurantDB, DBReports;
    description: (*
	The MaintainDB operation manages all components of the restaurant
	database.  MaintainDB performs password validation on the user, to
	ensure that only legitimate restaurant personnel may gain access to the
	databases.  The three main suboperations of MaintaiDB are described
	below.
    *);
end MaintainDB;

operation MaintainMenu
    components: AddFoodItem, DelFoodItem, ChangeFoodItem, ListFoodItems;
    inputs: MenuUpdates, FoodMenu;
    outputs: FoodMenu, FoodItemList;
    description: (*
	MaintainMenu allows new menu items to be added to the FoodMenu.  It
	also allows existing menu items to deleted, changed, or listed.
    *);
end MaintainMenu;

(* The suboperations of MaintainMenu need to be defined. *)

operation MaintainInventory
    components: AddDelivery, DeleteSpoilage, AddFoodStuffsItem,
	DelFoodStuffsItem, ChangeFoodStuffsItem, ListInventory;
    inputs: InventoryUpdates, FoodStuffsInventory;
    outputs: FoodStuffsInventory, IntervalInventoryReport;
    description: (*
	MaintainInventory allows updates to the FoodStuffsInventory.  The
	AddDelivery suboperation is invoked when vendor deliveries arrive.
	DeleteSpoilage is typically invoked at the end of the business day to
	update the inventory based on how much food spoiled or was damaged
	during restaurant operations.  The Add, Del, and ChangeFoodStuffsItem
	operations provide the standard access to the inventory DB.  Finally,
	the ListInventory operation is used to produce an
	IntervalInventoryReport.
    *);
end MaintainInventory;

(* The suboperations of MaintainInventory need to be defined. *)

operation MaintainBreakdowns
    components: AddFoodItemBreakdown, DelFoodItemBreakdown,
	ChangeFoodItemBreakdown, ListFoodItemBreakdowns;
    inputs: BreakdownUpdates, FoodItemBreakdowns;
    outputs: FoodItemBreakdowns;
    description: (*
	This operation maintains the FoodItemBreakdowns.  It has the standard
	suboperations to add, delete, change, and list items.
    *);
end MaintainBreakdowns;

(* The suboperations of MaintainBreakdowns need to be defined. *)