This test is worth a total of 100 points This test is closed…
This test is worth a total of 100 points This test is closed book and closed notes (no supplementary materials are allowed) The test is timed — you may not take longer than one hour and twenty minutes. Therefore, before you begin, please take a moment to look over the entire test so that you can budget your time. Number your answers according to the question number below You are to construct a simple model of organizational charts that describe managerial and reporting relationships between employees in a multi-division company. There are two types of information captured in our organizational chart: (1) for each employee e, a set of employees that e manages (and the “manages” relation forms a hierarchy), and (2) the division to which a particular employee belongs. There are three categories of employees in the portion of the management hierarchy that we will model: (1) entry level, (2) management, and (3) vice-presidents (VP). Each employee belongs to exactly one of these categories. Consider the following incomplete specification of the signatures for an Alloy model of organizational charts. sig Division {}sig OrgChart { // maps each employee to the division to which they belong division : Employee -> Division, // maps each employee to the set of employees that they manage // (if employee A manages employee B, A is said to be B’s “boss”) manages : Employee -> Employee} { // OrgChart constraints defined here} 1. (6 points) Specify signatures for Employee and employee categories EntryLevel, Management, and VP such that each employee belongs to exactly one category (the categories partition the members of the Employee signature). 2. (4 points) Multiplicity declaration: Some constraints/invariants can be captured using Alloy multiplicity declarations. Respecify the division relation with Alloy multiplicities to capture the following constraints: (a) each division has at least one employee, and (b) each employee belongs to at most one division. In the following questions, you will add several signature constraints for the OrgChart signature. Specify each informal constraint requirement below but write them just as you would if they appeared directly in the constraint section of the OrgChart signature.Hints: recall that for a relation R, you could access its inverse using the transpose operator ~R and that ^R computes the transitive closure of R. Also note that a VP is allowed to manage employees. 3. (5 points) There is exactly one VP in each division 4. (5 points) A VP does not have a manager 5. (5 points) Each management and entry-level employee has exactly one manager 6. (5 points) Every VP and every management employee manage someone 7. (5 points) An entry level employee manages no one 8. (7 points) If an employee e has managers, the managers for e must work in the same division as e 9. (7 points) Each manager m only manages employees that work for m’s division 10. (7 points) There are no cycles in the management hierarchy (i.e., an employee cannot directly or indirectly manage herself) How would you use ACA to check whether the following scenario is allowed by your specification (give the definition of all Alloy predicates, assertions, and run/check constructs that you would use during this checking process): 11. (8 points) There is one division, at least two management employees, and more than two entry level employees (you need only show that such a scenario exists when considering only one OrgChart). 12. (8 points) There exist two different management Level employees that both manage the same employee. Define an Alloy predicate to specify: 13. (28 points) An operation moveEntryLevel that describes a transformation of the organizational chart in which an entry level employee e currently managed by oldBoss is transferred to a different manager newBoss who may work in the same or a different division. Your operation should capture all appropriate pre-, post-, and frame- conditions (these should be clearly identified and explained with comments in your code or annotations on your exam paper) – in particular, you should construct frame conditions in your operation to guarantee that the only changes that occur in the organizational chart are those directly associating with the moving of the employee. Remember that you should construct your operation so that the pre/post/frame conditions guarantee that if you start in a state that satisfies all your invariants stated above and the preconditions of your operations are satisfied, then you will produce a new state where all your invariants hold.For example, there is an invariant that constrains the number of employees that a manager can manage – make sure that you use a precondition that guarantees that invariant holds after the operation completes. sig Division {}//… Employee, etc.sig OrgChart { division : Employee -> Division, manages : Employee -> Employee} { }pred moveEntryLevel (o, o’: OrgChart, e: EntryLevel, oldBoss, newBoss : Management) { // constraints defined here}
Read Details