1. Express the following statements in propositional logic and derive the relationships between the monitoring state, the test state, and the fact that the reactor is operating. (2 point) A. The reactor is either in the monitoring or test state. It cannot be in both states. The reactor is functioning normally only when it is in one of these states. B. If a reactor is functioning normally and is not in the test state then the reactor can be regarded as being operating. Two propositions must be defined one for each A and B. 2. Given the following inference rules, show that the following proposition is true (i.e., tautology). Denote which rule is applied in each step. (2 points) (ChannelOpen / ReceiverReady (LineClosed ChannelOpen -Receiver Ready))-LineClosed Inference Rules: pl p2 p1V p2 p1 Apt false p1 Vp1 p1 p1 p1 V p2 = impl = or 1 "(01/02) = contr(Contradiction) = or 5 p1 Vp2 p1 V true true pt A false false DeM A p1 Vp1 = or 2 true and 3 A p1 / (p2 v p3) (p1 ^ p2) V (p1 / p3) p1 = exmid (Tautology) p1 V false - or 3 =dist AV p1 v (p1 / p2) p1 - 04 3. Suppose the following requirements: A. If the operator types the ALARM command, then the subsidiary alarm will be activated and an alarm message will be written to the log file. B. Whenever the subsidiary alarm is activated, the main valve is closed and shut-down is started. C. If the main valve is closed, then the reactor can be regarded as being in a non-operational state. Express the requirements in propositional calculus. Using the inference rules in Question 2, show that if the alarm command is activated under the propositions, the reactor will be in a non-operational state. (2) points) 4. Supposed that a procedure update has two integer parameters-flag and valve. The procedure examines the first parameter flag and depending on the value of flag, the second parameter valve is set. If flag lies between zero and 10 then valve is set to zero. Otherwise, valve is unchanged. (2 point) A. Write the post-conditions in the predicate logic. B. Model the post-conditions as a predicate in Alloy. C. Run the model (e.g., "run predicate-name for 3 but exactly 2 Valve, 5 int"). D. Observe the first instance and check if the instance satisfies what you intended in your model. If not, fix it. E. Capture the screen of the first instance found. 5. Supposed that a procedure search has three parameters - vals, searchfor, and found. vals is an integer array with a range of 1..5. searchfor is an integer parameter. If searchfor is in vals, then found is set to one. Otherwise, it is set to two. (2 point) A. Write the post-conditions in the predication logic. B. Model the post-conditions as a predicate in Alloy. C. Run the model (c.g., "run predicate-name for 3 but exactly 5 Vals, 4 int") D. Observe the first instance and check if the instance satisfies what you intended in your model. If not, fix it. E. Capture the screen of the first instance found. 6. Complete the Academic Records model by specifying the following requirements (5 points): A. Eliminate any redundant prereqs (see the lecture notes for an example). B. Create a signature of grades with a constraint of which student has a grade in each course taken. C. Divide grades into exactly A, B, C, D, and F. D. Change graduation condition so student must pass (C or better) in each required course. E. Write assertion that if a student can graduate, they must have passed all required courses as well as transitive prerequisites of required courses. Fix the model if any counterexample is found. F. Allow departments multiple sets of required courses, and student can fulfill any one of those sets. G. Canonicalize required sets so that they do not have the same set of required courses (see the List example in the lecture notes). Note: Turn in the model and screen captures of the "canTake Course" and "canGraduate" predicates. Clearly comment the model with the above labels.