The purpose of this lab is to participate in activities related to the formal specification of requirements, assumptions, and domain properties. In particular, it will exercise your ability to formally specify requirements statements using propositional logic, predicate logic, and linear temporal logic (LTL). Consider the following requirements statements for the RealEstateManager system. (a) A clients information should be deleted when the clients status is inactive. (b) A clients information can be changed, or removed, only if the client has been added to the system. (c) A clients status shall be active if and only if an agent is assigned to the client and the client has not requested to cancel the service. (d) A clients status is set as inactive if the client has not answered calls for more than a month. (e) The system shall not match a property to an inactive client. (f) The system shall not match a property to a tenant if the number of bedrooms on the property is fewer than the number of bedrooms needed by the tenant. (g) An agent shall not have more than 10 clients at one time. (h) A clients information can only be changed by the secretary or the agent assigned to the client. (i) Every client that is listed as active, shall have one agent assigned to them. (j) The system shall ensure that the same client has not been assigned to two different agents. (k) A clients status shall be new until an agent is assigned to the client or the client has requested to cancel the service. (l) If a client has called the company to cancel the service, then it will be guaranteed that the clients information will be deleted from the system. (m) The system shall ensure that if a real estate staff member enters their valid username and password pair, then the next state will give them access to the clients information. (n) A newly added client will always eventually be assigned to an agent, unless the client calls to cancel the service. (o) If a deal is closed or a client calls to cancel the service, then the clients status will become inactive. *Important Note* If you feel it necessary to make assumptions regarding missing information, or to clarify the stated requirements, please ensure that your assumptions are clearly and properly documented, and that they are reasonable for the given system.

Problem 1 [10 points] Consider each of the requirements statements listed on Page 2. Specify the notation that you will use to specify each of the statements in Problems 2-4. Define appropriate propositions, sets, functions, and/or predicates to simplify the presentation of the specification. Provide a short description of each notation. Be sure to avoid having redundant or inconsistent notations. Problem 2 [8 points] Specify requirements statements (a)-(d) using propositional logic. Problem 3 [12 points] Specify requirements statements (e)-(j) using predicate logic. Problem 4 [10 points] Specify requirements statements (k)-(o) using linear temporal logic (LTL).