* * Signatures * * Your model should contain the following (and potentially other) signatures. * If necessary, you have to make some of the signatures abstract and * make them extend other signatures. * / /* * Hints: You may need to define a Bool signature when crafting the following sig. * Consider to search online and find tutorials on this. * / sig Employee { ... } sig Intern { ... } sig Chef { ... } sig Courier { ... } sig Manager{ ... } sig Customer { ... } sig ManagementSystem { ... } sig Time { ... } sig Delivery { ... } sig Order { ... } sig Pizza { ... } /* * Predicates */ // True iff c is a premium customer. pred isPremiumCustomer[c : Customer] { ... } // True iff p is a gourmet pizza. pred isGourmetPizza[p : Pizza] { ... } // True iff c is carrying more than a single order. pred moreThanOneCourier[c: Courier] { ... } // True iff i is carrying more than a single order. pred moreThanOneInternCourier[i: Intern] { ... } // True iff c is cooking more than a single order pred moreThanOneChef[c: Chef] { ... } // True iff i is cooking more than a single order pred moreThanOneInternCook[i: Intern] { ... } // True iff i is a piazza delivering intern pred isDeliveringIntern[i : Intern] { ... } // True iff o1 is ordered before o2 pred orderIsBefore[o1, o2: Order] { ... } // True iff t1 is strictly before t2. pred isBefore[t1, t2: Time] { ... } /* * Functions */ // Returns all the orders which are being cooked by chef c fun getAllOrders[c: Chef] : set Order { ... } // Returns all the orders which are being delivered by courier c fun getAllOrdersFromCourier[c: Courier] : set Order { ... } // Returns all the orders which are being delivered by intern i fun getAllOrdersFromInternDelivery[i: Intern] : set Order { ... } // Returns all the orders which are being cooked by intern i fun getAllOrdersFromInternCooked[i: Intern] : set Order { ... } // Returns the start time of an order o fun getStart[o : Order] : Time { ... } // Returns the end time of an order o fun getEnd[o: Order] : Time { ... } // Returns the delivery address of an order o fun getDeliveryAddr[o: Order] : Address { ... } // Returns the payment information of the customer c fun getPayment[c: Customer] : Payment { ... } // Returns all the orders that are being cooked. fun getAllBeingCookedOrders[m: ManagementSystem] : set Order { ... } // Returns all the orders that are being delivered. fun getAllBeingDeliveredOrders[m: ManagementSystem] : set Order { ... }