- #1

- 818

- 8

Consider the following set of sentences that represent the requirements of a multi-threaded system for two threads t1 and t2:

□¬[(t1 active) ∧ (t2 active)].

□[(t1 active) ⊕ (t2 active)].

□[(t1 active) → O(t2 active)].

□[(t2 active) → O(t1 active)].

(Pretend the O letters are the circles denoting the unary "next" operator.)

Could someone please let me know whether that set of sentences is consistent or not (and why)?

Any input would be GREATLY appreciated!

P.S.

Basically, if I'm correct, for a set to be consistent, there needs to be at least one case where all the statements are simultaneously true, and I think my diagram (

Am I correct? If not, how is this problem supposed to be solved?

In the diagram, I use p to denote "(t1 active)" and q to denote "(t2 active)".

□¬[(t1 active) ∧ (t2 active)].

□[(t1 active) ⊕ (t2 active)].

□[(t1 active) → O(t2 active)].

□[(t2 active) → O(t1 active)].

(Pretend the O letters are the circles denoting the unary "next" operator.)

Could someone please let me know whether that set of sentences is consistent or not (and why)?

Any input would be GREATLY appreciated!

P.S.

Basically, if I'm correct, for a set to be consistent, there needs to be at least one case where all the statements are simultaneously true, and I think my diagram (

**[link removed by Mentors]**- also included as an attachment) shows such a case (but I'm not sure if I'm correct or if my diagram is even done properly). Basically, if p is true at t=i and q is true at t=i+1, then the four statements seem to hold true for me (where the bottommost one seems to be vacuously true). (If I'm correct, another case where the statements would be consistent would be if p is false and q is true, where each statement would similarly hold true, except that it would be the third statement that's vacuously true instead of the bottommost / fourth one.)Am I correct? If not, how is this problem supposed to be solved?

In the diagram, I use p to denote "(t1 active)" and q to denote "(t2 active)".

#### Attachments

Last edited by a moderator: