| Example |
|
|
|
|
|
|
|
|
|
|
|
|
| • | Q
== T1 implies AF C1 |
||||||||||
| – | If
Process 1 is trying to acquire the mutex, then |
||||||||||
| it is
inevitably true it will get it sometime |
|||||||||||
| • | Q
== (not T) OR AF C1 |
||||||||||
| – | Rewriting
with DeMorgan’s Laws |
||||||||||
| • | First,
label all the states where T1, not T1, |
||||||||||
| and C1
are true |
|||||||||||
| – | These
are atomic properties |
||||||||||
