Stan and Lacy were working on a real-time system and trying to debug the part of

Question

Stan and Lacy were working on a real-time system and trying to debug the part of the system dealing with the scheduling of real-time tasks. They noted that the following system requirements from the requirements team were relevant for their work.

Requirements:

(1) If the System is in Maintenance mode, than the Operational Tasking queue is empty (2) If the Operational Tasking queue is empty, then the MAIN task is in IDLE mode

They were considering a situation where the MAIN task was executing (not IDLE). Based on a simple argument, they were able to conclude that (given the system requirements), if an Operational Task is not IDLE (i.e., if it is executing), then the system can’t be in maintenance mode.

Use your knowledge of propositional logic to show that their argument is correct. Specifically, given

p = System is in Maintenance mode q = Operational Tasking queue is empty r = MAIN task is in IDLE mode

We would have the following formalization of the requirements

(1) p -> q (2) q -> r

And the situation being considered corresponds to ~r. The sequent that formalizes their argument is:

p q, q r, ¬r ¬p

Give a proposition logic proof for this sequent. Hint: this will use the ¬e and ¬i rules.

Extra Hint: Stan and Lucy’s argument about the requirements went something like this:

Lucy:

It’s a given that

If the System is in Maintenance mode, than the Operational Tasking queue is empty If the Operational Tasking queue is empty, then the MAIN task is in IDLE mode

…because we know that from the system requirements.

Stan:

Yeah, and we are also going to take as given that the MAIN task is NOT in IDLE mode.

So, for the sake of argument let’s assume that the system is in maintenance mode — is that going to cause any problems for us?

It would certainly mean that the Operational Tasking queue is empty due to Requirement (1)

Lucy:

And then it would follow that the MAIN task is in IDLE mode, based on Requirement (2).

Stan:

But hang on, I said that we going to work under the assumption that the MAIN task is NOT in idle. So what you just said is inconsistent with my assumption.

Lucy:

Well, OK, that must mean that what you assumed about the system maintenance mode can’t hold. That is, there is no way that given the requirements and our assumption about the MAIN task, that the system is in maintenance mode.

Explanation / Answer

We have the following predicates as:-

p = System is in Maintenance mode

q = Operational Tasking queue is empty

r = MAIN task is in IDLE mode

So we first take, p => q, which means that if System is in Maintainance Mode then Operational Tasking Queue in empty. Next, we take q => r, which means that if the Operational Tasking Queue is empty then the MAIN Task is in IDLE Mode. Combining both laws, we can say that p => r, which means if the System is in Maintainance Mode, the MAIN Task is in IDLE Mode by. Now we apply Converse Rule on this, which makes:-

p r as r p. Next we apply NOT on both sides of this logic, we get NOT(r) => NOT(p) also written as:-

~r   ~p. Lets us now try to prove this logic proof for this sequent.

If the System is in Mainatainace Mode, then the MAIN TASK is in IDLE MODE as the Operational Tasking Queue will be empty.

We can say this statement as, Since the MAIN TASK is in IDLE MODE, the definitely the System will be in Mainatainace Mode.

If we now negate the sentence, we can say, If the MAIN TASK is NOT IN IDLE MODE, then the System IS NOT in Mainatainace MODE as Opeartional Tasking Queue is NOT EMPTY.

This exatly corresponds to ~r   ~p [Proved!]

Please let me know in case of any clarifications required. Thanks!

Related Questions

Navigate

• Browse (All)
• Browse S
• Subjects

Integrity-first tutoring: explanations and feedback only — we do not complete graded work. Learn more.